feat: dimension inequalities (#9)

* feat(Graph)!: replace disjoint sets with graphs

* feat: implement inequalities

* docs(Theory): update the doc

* fix(Theory): handle dim0 and dim1 correctly

* test(Graph): add testing for Graph

* fix: really handle dim0 and dim1

* fix(Builder): fix another bug

Author: favonia

kado.opam

@@ -14,6 +14,7 @@ depends: [
   "dune" {>= "2.0"}
   "ocaml" {>= "4.10"}
   "bwd" {>= "1.0"}
+  "qcheck-core" {>= "0.18" & with-test}
   "odoc" {with-doc}
 ]
 build: [

src/Builder.ml

@@ -16,6 +16,7 @@ struct
     type dim
     type cof
     val cof : (dim, cof) Syntax.endo -> cof
+    val le : dim -> dim -> cof
     val eq : dim -> dim -> cof
     val eq0 : dim -> cof
     val eq1 : dim -> cof
@@ -31,32 +32,15 @@ struct
   struct
     include P
 
-    let eq x y = cof @@
-      let (=) = equal_dim in
-      if x = y then
-        Syntax.Endo.top
-      else if (x = dim0 && y = dim1) || (x = dim1 && y = dim0) then
-        Syntax.Endo.bot
-      else
-        Syntax.Endo.eq x y
-
-    let eq0 x = cof @@
-      let (=) = equal_dim in
-      if x = dim0 then
-        Syntax.Endo.top
-      else if x = dim1 then
-        Syntax.Endo.bot
-      else
-        Syntax.Endo.eq x dim0
+    let (=) = equal_dim
 
-    let eq1 x = cof @@
-      let (=) = equal_dim in
-      if x = dim1 then
+    let le x y = cof @@
+      if dim0 = x || x = y || y = dim1 then
         Syntax.Endo.top
-      else if x = dim0 then
+      else if x = dim1 && y = dim0 then
         Syntax.Endo.bot
       else
-        Syntax.Endo.eq x dim1
+        Syntax.Endo.le x y
 
     let bot = cof Syntax.Endo.bot
     let top = cof Syntax.Endo.top
@@ -81,17 +65,24 @@ struct
         | [phi] -> phi
         | l -> cof @@ Syntax.Endo.meet l
 
+    let eq x y = meet [le x y; le y x]
+
+    let eq0 x = eq x dim0
+
+    let eq1 x = eq x dim1
+
     let boundary r = join [eq0 r; eq1 r]
 
     let forall (sym, cof) =
       let rec go cof =
         match uncof cof with
         | None -> cof
-        | Some Eq (x, y) ->
+        | Some Le (x, y) ->
           begin
             match equal_dim x sym, equal_dim y sym with
             | true, true -> top
-            | true, false | false, true -> bot
+            | true, false -> if y = dim1 then top else bot
+            | false, true -> if x = dim0 then top else bot
             | _ -> eq x y
           end
         | Some Meet phis -> meet @@ List.map go phis

src/Builder.mli

@@ -39,7 +39,10 @@ sig
     (** The embedding of cofibrations to [cof]. *)
     val cof : (dim, cof) Syntax.endo -> cof
 
-    (** Smarter version of {!val:Syntax.Endo.eq} that checks equality. *)
+    (** Smarter version of {!val:Syntax.Endo.le} that checks equality. *)
+    val le : dim -> dim -> cof
+
+    (** Smarter version of [meet [le x y; le y x]]. *)
     val eq : dim -> dim -> cof
 
     (** [eq0 r] is [eq r dim0]. *)
@@ -71,7 +74,10 @@ sig
     val boundary : dim -> cof
 
     (** [forall (r, cof)] computes [forall r. cof], using the syntactic quantifier elimination
-        and potentially other simplification procedures used in {!val:eq}, {!val:join}, and {!val:meet}. *)
+        and potentially other simplification procedures used in {!val:eq}, {!val:join}, and {!val:meet}.
+
+        Note: [r] cannot be [dim0] or [dim1].
+    *)
     val forall : dim * cof -> cof
   end
 

src/DisjointSet.ml

@@ -0,0 +1,90 @@
+module type Vertex =
+sig
+  type t
+  val compare : t -> t -> int
+
+  val initial : t (* if you pretent the graph is a category *)
+  val terminal : t
+end
+
+module type S =
+sig
+  type key
+  type t
+
+  val empty : t
+  val test : key -> key -> t -> bool
+  val union : key -> key -> t -> t
+  val test_and_union : key -> key -> t -> bool * t
+
+  val merge : t -> t -> t
+end
+
+module Make (V : Vertex) : S with type key = V.t =
+struct
+  module M = Map.Make (V)
+  module S = Set.Make (V)
+
+  type vertex = V.t
+  type key = vertex
+
+  let (=) v1 v2 = V.compare v1 v2 = 0
+
+  type t =
+    { reachable : S.t M.t;
+      reduced : V.t list M.t }
+
+  let empty : t =
+    { reachable = M.of_seq @@ List.to_seq
+          [V.initial, S.of_list [V.initial; V.terminal];
+           V.terminal, S.singleton V.terminal];
+      reduced = M.of_seq @@ List.to_seq
+          [V.initial, [V.terminal];
+           V.terminal, []] }
+
+  let mem_vertex (v : vertex) (g : t) : bool = M.mem v g.reachable
+
+  let touch_vertex (v : vertex) (g : t) : t =
+    if mem_vertex v g then g else
+      { reachable =
+          M.add v (S.add v (M.find V.terminal g.reachable)) @@
+          M.map (fun s -> if S.mem V.initial s then S.add v s else s) @@
+          g.reachable;
+        reduced =
+          M.update V.initial (fun l -> Some (v :: Option.get l)) @@
+          M.update v (function None -> Some [V.terminal] | _ as l -> l) @@
+          g.reduced
+      }
+
+  let raw_test (u : vertex) (v : vertex) (g : t) =
+    S.mem v (M.find u g.reachable)
+
+  let test (u : vertex) (v : vertex) (g : t) =
+    match mem_vertex u g, mem_vertex v g with
+    | true, true -> raw_test u v g
+    | true, false -> raw_test u V.initial g
+    | false, true -> raw_test V.terminal v g
+    | false, false -> u = v || raw_test V.terminal V.initial g
+
+  let union (u : vertex) (v : vertex) (g : t) =
+    if test u v g then g else
+      let g = touch_vertex v @@ touch_vertex u g in
+      let rec meld i rx =
+        let f rx j = if S.mem j rx then rx else meld j (S.add j rx) in
+        List.fold_left f rx (M.find i g.reduced)
+      in
+      { reduced = M.update u (fun l -> Some (v :: Option.get l)) g.reduced;
+        reachable =
+          g.reachable
+          |> M.map @@ fun rx ->
+          if S.mem u rx && not (S.mem v rx) then
+            meld v @@ S.add v rx
+          else
+            rx }
+
+  let test_and_union (u : vertex) (v : vertex) (g : t) =
+    test u v g, union u v g
+
+  let merge (g1 : t) (g2 : t) =
+    M.fold (fun u -> List.fold_right (union u)) g1.reduced g2
+end

src/Graph.ml

@@ -1,3 +1,12 @@
+module type Vertex =
+sig
+  type t
+  val compare : t -> t -> int
+
+  val initial : t
+  val terminal : t
+end
+
 module type S =
 sig
   type key
@@ -9,10 +18,6 @@ sig
   val test_and_union : key -> key -> t -> bool * t
 
   val merge : t -> t -> t
-
-  type finger
-  val finger : key -> t -> finger
-  val test_finger : key -> finger -> bool
 end
 
-module Make (O : Map.OrderedType) : S with type key = O.t
+module Make (V : Vertex) : S with type key = V.t

src/DisjointSet.mli renamed to src/Graph.mli

@@ -3,3 +3,5 @@ module Syntax = Syntax
 module Builder = Builder
 
 module Theory = Theory
+
+module Graph = Graph

src/Kado.ml

@@ -12,3 +12,7 @@ module Builder : module type of Builder
 
 (** The {!module:Theory} module implements decision procedures for sequents relative to a theory over the interval, stated in the language of cofibrations. *)
 module Theory : module type of Theory
+
+(**/**)
+
+module Graph : module type of Graph

src/Kado.mli

@@ -1,5 +1,5 @@
 type ('r, 'a) endo =
-  | Eq of 'r * 'r
+  | Le of 'r * 'r
   | Join of 'a list
   | Meet of 'a list
 
@@ -10,7 +10,7 @@ type ('r, 'v) free =
 module Endo =
 struct
   type ('r, 'a) t = ('r, 'a) endo =
-    | Eq of 'r * 'r
+    | Le of 'r * 'r
     | Join of 'a list
     | Meet of 'a list
 
@@ -20,18 +20,18 @@ struct
   let bot = join []
   let top = meet []
 
-  let eq x y = Eq (x, y)
+  let le x y = Le (x, y)
 
   let map f =
     function
-    | Eq _ as phi -> phi
+    | Le _ as phi -> phi
     | Join l -> Join (List.map f l)
     | Meet l -> Meet (List.map f l)
 
   let dump dump_r dump_a fmt =
     function
-    | Eq (r1, r2) ->
-      Format.fprintf fmt "@[<hv 1>eq[@,@[%a@];@,@[%a@]]@]" dump_r r1 dump_r r2
+    | Le (r1, r2) ->
+      Format.fprintf fmt "@[<hv 1>le[@,@[%a@];@,@[%a@]]@]" dump_r r1 dump_r r2
     | Join l ->
       Format.fprintf fmt "@[<hv 1>join[@,%a]@]"
         (Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt ";@,") dump_a) l
@@ -43,7 +43,7 @@ end
 module Free =
 struct
   type nonrec ('r, 'a) endo = ('r, 'a) endo =
-    | Eq of 'r * 'r
+    | Le of 'r * 'r
     | Join of 'a list
     | Meet of 'a list
 
@@ -54,7 +54,7 @@ struct
   let var v = Var v
   let cof c = Cof c
 
-  let eq x y = cof @@ Endo.eq x y
+  let le x y = cof @@ Endo.le x y
   let join phis = cof @@ Endo.join phis
   let meet phis = cof @@ Endo.meet phis
   let bot = cof Endo.bot