some lattice examples

lattice.ml

(* REPL: #use "lattice.ml";; *)
#require "batteries";;
#require "ppx_deriving.std";;
open BatteriesExceptionless

let nopath x = let open String in let i = (rindex x '.' |? -1) + 1 in sub x i (length x - i);;

module type PartialOrder = sig
  type d [@@deriving show, enum]
  val leq : d -> d -> bool
end

module F (PO : PartialOrder) = struct
  open PO
  let ds = Set.(map (Option.get%d_of_enum) (of_enum (min_d -- max_d)))
  let show x = "{"^(Set.to_list x |> List.map (nopath%show_d) |> String.concat ", ")^"}"
  let relations = Set.filter (uncurry leq) (Set.cartesian_product ds ds) |> Set.to_list |> List.map (Tuple2.mapn show_d)
  let filter p = Set.filter p ds
  let inter f xs = List.fold_right (Set.intersect%f) xs ds
  let min s = Set.filter (fun x -> Set.for_all (leq x) s) s
  let max s = Set.filter (fun x -> Set.for_all (flip leq x) s) s
  let ub' x = filter (leq x)
  let lb' x = filter (flip leq x)
  let ub = inter ub'
  let lb = inter lb'
  let lub = min % ub
  let glb = max % lb
  (* gives some counter example if PO is not a complete lattice *)
  let counter_example = Set.cartesian_product ds ds |> Set.to_list |> List.find_map (fun (a,b) -> if Set.is_empty (lub [a;b]) then Some (a,b) else None)
end

(*
 * C
 * |
 * B
 * |
 * A
 *)
module Ex1 = struct
  module PO = struct
    type d = A | B | C [@@deriving show, enum]
    let leq = (<=)
  end
  include PO include F (PO)
end

(*
 *   D
 *  / \
 * B   C
 *  \ /
 *   A
 *)
module Ex2 = struct
  module PO = struct
    type d = A | B | C | D [@@deriving show, enum]
    let leq x y = x=y || x=A || y=D
  end
  include PO include F (PO)
end

(*
 *   E
 *   |
 *   D
 *  / \
 * B   C
 *  \ /
 *   A
 *)
module Ex3 = struct
  module PO = struct
    type d = A | B | C | D | E [@@deriving show, enum]
    let leq x y = x=y || x=A || y=E || y=D && x<>E
  end
  include PO include F (PO)
end

(*
 *   F
 *  / \
 * D   E
 * | X |
 * B   C
 *  \ /
 *   A
 *
 *)
module Ex4 = struct
  module PO = struct
    type d = A | B | C | D | E | F [@@deriving show, enum]
    let leq = curry @@ function
      | A,_ | _,F | B,D | B,E | C,D | C,E -> true
      | x,y when x=y -> true
      | _ -> false
  end
  include PO include F (PO)
end

(* some examples *)
open Ex4;;
show @@ ub  [B;C];; (* = "{D, E, F}" *)
show @@ lub [B;C];; (* = "{}" *)
show @@ glb [B;C];; (* = "{A}" *)
counter_example;;   (* = Some (B, C) *)