lattices.re

module type EQ = {
  type t;
  let (==): (t, t) => bool;
};

module type PARTIAL_ORDER = {
  type t;
  let (<=): (t, t) => bool;
};

module type JOIN_SEMILATTICE = {
  type t;
  let join: (t, t) => t;
};

module type MEET_SEMILATTICE = {
  type t;
  let meet: (t, t) => t;
};

module type BOUNDED_JOIN_SEMILATTICE = {
  include JOIN_SEMILATTICE;
  let bottom: t;
};

module type BOUNDED_MEET_SEMILATTICE = {
  include MEET_SEMILATTICE;
  let top: t;
};

module type LATTICE = {
  type t;
  include JOIN_SEMILATTICE with type t := t;
  include MEET_SEMILATTICE with type t := t;
};

module type BOUNDED_LATTICE = {
  type t;
  include BOUNDED_JOIN_SEMILATTICE with type t := t;
  include BOUNDED_MEET_SEMILATTICE with type t := t;
};

module type EQ_JOIN_SEMILATTICE = {
  type t;
  include EQ with type t := t;
  include JOIN_SEMILATTICE with type t := t;
};

module type EQ_BOUNDED_LATTICE = {
  type t;
  include EQ with type t := t;
  include BOUNDED_LATTICE with type t := t;
};

module NatDivisionLattice: EQ_BOUNDED_LATTICE = {
  type t = int;

  let top = 0;
  let bottom = 1;

  let rec gcd = (a, b) =>
    switch (a, b) {
    | (a, 0) => a
    | (a, b) => gcd(b, a % b)
    };
  let lcm = (a, b) => a * b / gcd(a, b);

  let meet = lcm;
  let join = gcd;

  let (==) = (==);
};

module PartialOrderFromJoinSemilattice =
       (L: EQ_JOIN_SEMILATTICE)
       : PARTIAL_ORDER => {
  type t = L.t;
  let (<=) = (x, y) => L.(join(x, y) == x);
};

module Divisibility: PARTIAL_ORDER =
  PartialOrderFromJoinSemilattice(NatDivisionLattice);

module LevitatedLattice =
       (L: LATTICE)
       : {
         type t;
         include BOUNDED_LATTICE with type t := t;
         let lift: L.t => t;
       } => {
  type t =
    | Top
    | Levitate(L.t)
    | Bottom;

  let top = Top;
  let lift = x => Levitate(x);
  let bottom = Bottom;

  let meet = (x, y) =>
    switch (x, y) {
    | (Top, _)
    | (_, Top) => Top
    | (x, Bottom)
    | (Bottom, x) => x
    | (Levitate(x), Levitate(y)) => Levitate(L.meet(x, y))
    };

  let join = (x, y) =>
    switch (x, y) {
    | (Bottom, _)
    | (_, Bottom) => Bottom
    | (x, Top)
    | (Top, x) => x
    | (Levitate(x), Levitate(y)) => Levitate(L.join(x, y))
    };
};

module L = LevitatedLattice(NatDivisionLattice);

quantity.re

open Base;

module Quantity: {
  type t;
  let of_int: int => Result.t(t, [> | `NegativeQuantityError]);
  let to_int: t => int;
  let (+): (t, t) => t;
} = {
  type t = int;
  let of_int =
    fun
    | x when x >= 0 => Ok(x)
    | _ => Error(`NegativeQuantityError);
  let to_int = Fn.id;
  let (+) = (+);
};