From 17206ca3d01fada34e34e60e1995b03609292b61 Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Tue, 29 Aug 2023 21:56:03 -0500
Subject: [PATCH] fix: adjust signatures to hide parameters (#13)

---
 src/Builder.ml  | 40 ++++++++++++++++++++-------------
 src/Builder.mli | 60 +++++++++++++++++++++++++++----------------------
 src/Theory.ml   | 19 +++++++++++-----
 src/Theory.mli  | 14 +++++++-----
 4 files changed, 78 insertions(+), 55 deletions(-)

diff --git a/src/Builder.ml b/src/Builder.ml
index 0f5438b..400a352 100644
--- a/src/Builder.ml
+++ b/src/Builder.ml
@@ -13,8 +13,13 @@ struct
 
   module type S =
   sig
-    type dim
-    type cof
+    module Param : sig
+      type dim
+      type cof
+    end
+    open Param
+
+    type t = cof
     val cof : (dim, cof) Syntax.endo -> cof
     val le : dim -> dim -> cof
     val bot : cof
@@ -28,9 +33,11 @@ struct
     val forall : dim * cof -> cof
   end
 
-  module Make (P : Param) : S with type dim = P.dim and type cof = P.cof =
+  module Make (Param : Param) : S with module Param := Param =
   struct
-    include P
+    include Param
+
+    type t = cof
 
     let (=) = equal_dim
 
@@ -105,27 +112,28 @@ struct
 
   module type S =
   sig
-    type dim
-    type var
-    type cof = (dim, var) Syntax.free
-
-    val var : var -> cof
-    include Endo.S with type dim := dim and type cof := cof
+    module Param : sig
+      type dim
+      type var
+    end
+    open Param
+    include Endo.S with type Param.cof := (dim, var) Syntax.free and module Param := Param
+    val var : var -> t
   end
 
-  module Make (P : Param) : S with type dim = P.dim and type var = P.var =
+  module Make (Param : Param) : S with module Param := Param =
   struct
     open Syntax.Free
 
-    let var = var
-    module P = struct
-      include P
+    module Param = struct
+      include Param
       type cof = (dim, var) Syntax.free
       let cof phi = Cof phi
       let uncof phi = match phi with Cof phi -> Some phi | _ -> None
     end
+    include Param
+    include Endo.Make(Param)
 
-    include P
-    include Endo.Make(P)
+    let var = var
   end
 end
diff --git a/src/Builder.mli b/src/Builder.mli
index 20c069a..80d8222 100644
--- a/src/Builder.mli
+++ b/src/Builder.mli
@@ -30,23 +30,29 @@ sig
   (** The signature of smart constructors. *)
   module type S =
   sig
-    (** The interval algebra. *)
-    type dim
+    module Param : sig
+      (** The interval algebra. *)
+      type dim
 
-    (** The type that embeds cofibrations. *)
-    type cof
+      (** The type that embeds cofibrations. *)
+      type cof
+    end
+    open Param
+
+    (** The type of built cofibrations. *)
+    type t = cof
 
     (** The embedding of cofibrations to [cof]. *)
-    val cof : (dim, cof) Syntax.endo -> cof
+    val cof : (dim, t) Syntax.endo -> t
 
     (** Smarter version of {!val:Syntax.Endo.le}. *)
-    val le : dim -> dim -> cof
+    val le : dim -> dim -> t
 
     (** The bottom cofibration. *)
-    val bot : cof
+    val bot : t
 
     (** The top cofibration. *)
-    val top : cof
+    val top : t
 
     (** Smarter version of {!val:Syntax.Endo.join} that simplifies cofibrations using syntactic criteria.
         For example, [join [meet []]] gives [cof (Meet [])].
@@ -55,34 +61,34 @@ sig
         and thus it will not perform all possible syntactic reduction. To obtain more reduced cofibrations,
         use only smart constructors (instead of raw constructors) to build cofibrations.
     *)
-    val join : cof list -> cof
+    val join : t list -> t
 
     (** Smarter version of {!val:Syntax.Endo.meet} that simplifies cofibrations using syntactic criteria.
         See {!val:join}. *)
-    val meet : cof list -> cof
+    val meet : t list -> t
 
     (** [eq] is equivalent to [meet [le x y; le y x]]. *)
-    val eq : dim -> dim -> cof
+    val eq : dim -> dim -> t
 
     (** [eq0 r] is equivalent to [eq r dim0]. *)
-    val eq0 : dim -> cof
+    val eq0 : dim -> t
 
     (** [eq1 r] is equivalent to [eq r dim1]. *)
-    val eq1 : dim -> cof
+    val eq1 : dim -> t
 
     (** [boundary r] is equivalent to [join [eq0 r; eq1 r]]. *)
-    val boundary : dim -> cof
+    val boundary : dim -> t
 
     (** [forall (r, cof)] computes [forall r. cof], using the syntactic quantifier elimination
         and potentially other simplification procedures used in {!val:le}, {!val:join}, and {!val:meet}.
 
         Note: [r] cannot be [dim0] or [dim1].
     *)
-    val forall : dim * cof -> cof
+    val forall : dim * t -> t
   end
 
   (** The implementation of smart constructors. *)
-  module Make (P : Param) : S with type dim = P.dim and type cof = P.cof
+  module Make (Param : Param) : S with module Param := Param
 end
 
 (** Smart constructors for {!type:Syntax.free}. *)
@@ -111,22 +117,22 @@ sig
   (** The signature of smart constructors. *)
   module type S =
   sig
-    (** The interval algebra. *)
-    type dim
+    module Param : sig
+      (** The interval algebra. *)
+      type dim
 
-    (** The type of cofibration variables. *)
-    type var
+      (** The type of cofibration variables. *)
+      type var
+    end
+    open Param
 
-    (** The type of freely generated cofibrations. *)
-    type cof = (dim, var) Syntax.free
+    (** @open *)
+    include Endo.S with type Param.cof := (dim, var) Syntax.free and module Param := Param
 
     (** Alias of {!val:Syntax.Free.var}. *)
-    val var : var -> cof
-
-    (** @open *)
-    include Endo.S with type dim := dim and type cof := cof
+    val var : var -> t
   end
 
   (** The implementation of smart constructors. *)
-  module Make (P : Param) : S with type dim = P.dim and type var = P.var
+  module Make (Param : Param) : S with module Param := Param
 end
diff --git a/src/Theory.ml b/src/Theory.ml
index 86d6a13..94d5077 100644
--- a/src/Theory.ml
+++ b/src/Theory.ml
@@ -13,8 +13,12 @@ end
 
 module type S =
 sig
-  type dim
-  type var
+  module Param : sig
+    type dim
+    type var
+  end
+  open Param
+
   type cof = (dim, var) Syntax.free
   type alg_thy
   type disj_thy
@@ -43,9 +47,9 @@ sig
   end
 end
 
-module Make (P : Param) : S with type dim = P.dim and type var = P.var =
+module Make (Param : Param) : S with module Param := Param =
 struct
-  include P
+  include Param
 
   open Syntax
 
@@ -58,7 +62,10 @@ struct
       let terminal = dim1
     end)
   module VarSet = Set.Make (struct type t = var let compare = compare_var end)
-  module B = Builder.Free.Make (struct include P let equal_dim x y = Int.equal (compare_dim x y) 0 end)
+  module B = Builder.Free.Make (struct
+      include Param
+      let equal_dim x y = Int.equal (compare_dim x y) 0
+    end)
 
   (** A presentation of an algebraic theory over the language of intervals and cofibrations. *)
   type alg_thy' =
@@ -132,7 +139,7 @@ struct
     let test_le (thy : t') (r, s) =
       Graph.test r s thy.le
 
-    let test_inconsistent (thy' : t') = test_le thy' (P.dim1, P.dim0)
+    let test_inconsistent (thy' : t') = test_le thy' (dim1, dim0)
 
     (** [unsafe_test_and_assume_eq] fuses [test_eq] and [assume_eq] (if there was one).
       * It is "unsafe" because we do not check consistency here. *)
diff --git a/src/Theory.mli b/src/Theory.mli
index 045555d..1d53607 100644
--- a/src/Theory.mli
+++ b/src/Theory.mli
@@ -23,12 +23,14 @@ end
 (** The signature of cofibration solvers. *)
 module type S =
 sig
+  module Param : sig
+    (** The type of dimensions. *)
+    type dim
 
-  (** The type of dimensions. *)
-  type dim
-
-  (** The type of cofibration variables. *)
-  type var
+    (** The type of cofibration variables. *)
+    type var
+  end
+  open Param
 
   (** The type of cofibrations. *)
   type cof = (dim, var) Syntax.free
@@ -108,4 +110,4 @@ sig
 end
 
 (** The cofibration solver. *)
-module Make (P : Param) : S with type dim = P.dim and type var = P.var
+module Make (Param : Param) : S with module Param := Param