From f0aab593a677befc15c5785e02a1da489970ccaf Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Thu, 30 May 2024 12:05:53 -0500
Subject: [PATCH] docs: first edition of tutorial (#21)

---
 docs/dune                          |   2 +
 docs/index.mld                     |  11 ++
 docs/quickstart.mld                | 158 +++++++++++++++++++++++++++++
 example/Bidir.ml                   |   4 +-
 example/Domain.ml                  |  38 +++++--
 example/NbE.ml                     |  11 +-
 example/Syntax.ml                  |   6 +-
 example/ULvl.ml                    |  40 ++++----
 src/Builder.ml                     |  42 ++++++++
 src/{Semantics.mli => Builder.mli} |   8 +-
 src/BuilderSigs.ml                 |  72 +++++++++++++
 src/Mugen.ml                       |   5 +-
 src/Mugen.mli                      |  23 +++--
 src/Semantics.ml                   |  87 ----------------
 src/SemanticsSigs.ml               | 114 ---------------------
 src/Shift.mli                      |   2 +-
 src/ShiftWithJoin.mli              |   2 +-
 src/Syntax.ml                      |   1 -
 src/Syntax.mli                     |  14 +--
 src/Theory.ml                      |  54 ++++++++++
 src/Theory.mli                     |   8 ++
 src/TheorySigs.ml                  |  65 ++++++++++++
 22 files changed, 506 insertions(+), 261 deletions(-)
 create mode 100644 docs/dune
 create mode 100644 docs/index.mld
 create mode 100644 docs/quickstart.mld
 create mode 100644 src/Builder.ml
 rename src/{Semantics.mli => Builder.mli} (77%)
 create mode 100644 src/BuilderSigs.ml
 delete mode 100644 src/Semantics.ml
 delete mode 100644 src/SemanticsSigs.ml
 create mode 100644 src/Theory.ml
 create mode 100644 src/Theory.mli
 create mode 100644 src/TheorySigs.ml

diff --git a/docs/dune b/docs/dune
new file mode 100644
index 0000000..946d98c
--- /dev/null
+++ b/docs/dune
@@ -0,0 +1,2 @@
+(documentation
+  (package mugen))
diff --git a/docs/index.mld b/docs/index.mld
new file mode 100644
index 0000000..d96dd28
--- /dev/null
+++ b/docs/index.mld
@@ -0,0 +1,11 @@
+{0 mugen: Universe Levels}
+
+{1 Links}
+
+{ul
+  {- {{!page:quickstart} 🔰 Quickstart tutorial}}
+  {- {{!module:Mugen} 📔 API reference}}}
+
+{1 What is "mugen"?}
+
+"mugen" is the transliteration of "無限" in Japanese, possibly a learned borrowing of "無限" from Chinese. It literally means "without limits", and is widely used in anime for the obvious reason. It is fitting in the context of universe polymorphism.
diff --git a/docs/quickstart.mld b/docs/quickstart.mld
new file mode 100644
index 0000000..c14aac7
--- /dev/null
+++ b/docs/quickstart.mld
@@ -0,0 +1,158 @@
+{0 Quickstart Tutorial}
+
+This tutorial is for an implementer (you!) to integrate this library into your type theory as quickly as possible. We will assume you are already familiar with OCaml and dependent type theory, and are using a typical OCaml package structure.
+
+{1 Introduction}
+
+Following {{: https://personal.cis.strath.ac.uk/conor.mcbride/Crude.pdf} Conor McBride’s crude but effective stratification} and {{: https://doi.org/10.1145/3571250} our algebraic reformulation}, a universe level in this library is represented as a pair of a variable together with some {i displacement}. For example, a universe level might be [x + 10], meaning the variable level [x] shifted (bumped) by 10 levels. The shifting of 10 levels is the displacement. For the same variable [x], the level [x + n] is larger than [x + m] if [n] is larger than [m], while levels [x + n] and [y + m] are in general incomparable for different variables [x] and [y]. Substituting [x + n1] for [y] in [y + n2] results in the level [x + (n1 + n2)].
+
+While this scheme (with only a variable and some displacement) looks limited, we proved that it is in a sense {e universal} if you allow all mathematically possible displacements beyond natural numbers. We also call the minimum algebra of displacements that would make the scheme work a {i displacement algebra}. See our {{: https://doi.org/10.1145/3571250} POPL paper} for more details.
+
+This library implements several displacement algebras you could choose from, along with a uniform interface to construct and compare universe levels.
+
+{1 Choose Your Displacements}
+
+The first step is to choose your favorite {i displacements}. We will use {!module:Mugen.Shift.Int} (integers) as the starting point, and it is easy to switch to another displacement algebra later. Other displacements are under {!module:Mugen.Shift} and {!module:Mugen.ShiftWithJoin}.
+
+{1 Free Level Expressions}
+
+{i Free} level expressions are expressions freely generated by only variables and shifting operators. In contrast, we will have a different kind of level expressions embedded in your datatype holding terms or types. The free level expressions are the only ones that can be compared against each other, while the embedded ones must be converted to free ones before comparing them. More on this later.
+
+Save the following file as [ULvl.ml] for free level expressions, assuming that you are using integers to represent variables.
+
+{[
+module Param =
+struct
+  (** Your chosen displacement algebra *)
+  module Shift = Mugen.Shift.Int
+
+  (** The representation of variables in free level expressions *)
+  type var = int
+
+  (** The equality checker for variables *)
+  let equal_var : var -> var -> bool = Int.equal
+end
+include Param
+
+(** An alias to the type of displacements *)
+type shift = Shift.t
+
+(** An alias to the type of free level expressions *)
+type t = (shift, int) Mugen.Syntax.free
+
+(** Smart constructors for free level expressions *)
+include Mugen.Builder.Free.Make (Param)
+
+(** Comparators for free level expressions *)
+include Mugen.Theory.Make (Param)
+]}
+
+Take a look at {!type:Mugen.Syntax.free} for the definition of free level expressions.
+
+{1 Extend Your Syntax}
+
+Now we have the free level expressions ready, you need to extend your datatype to embed levels and define the conversion functions to free ones. A typical datatype holding terms or types will have the following pattern:
+{[
+type t =
+  | Var of int (* maybe using De Bruijn indexes or levels *)
+  (* ... *)
+]}
+There are three steps to add level expressions to your datatype
+
+{2 Change the Datatype}
+
+The idea is to use {!Mugen.Syntax.endo}, instead of {!Mugen.Syntax.free}, so that displacements can syntactically apply to any term or type in your language (but most of them will be ill-formed terms or types). The first parameter of {!Mugen.Syntax.endo} is the type of displacements, and the second parameter is your datatype. It needs to be defined together with your datatype due to the mutual recursion; in the following example, we choose to add a new constructor, [ULvl], to embed level expressions:
+
+{[
+(** Use [endo] to embed levels into your datatype. *)
+type ulvl = (ULvl.shift, t) Mugen.Syntax.endo
+
+(** The datatype of terms. *)
+and t =
+  | Var of int
+  (* ... *)
+  | ULvl of ulvl
+]}
+
+You can take a look at {!type:Mugen.Syntax.endo} for the definition of embedded level expressions.
+
+{2 Add Converters}
+
+Remember that only free level expressions can be compared. Therefore, we should add conversion functions from embedded level expressions to free ones. Copy and paste the following code after the definition of your datatype:
+
+{[
+(** Conversion to free level expressions *)
+let rec to_ulvl : t -> ULvl.t =
+  function
+  | Var i -> Mugen.Syntax.Var i
+  | ULvl endo -> endo_to_ulvl endo
+  | _ -> invalid_arg "to_ulvl"
+
+and endo_to_ulvl : ulvl -> ULvl.t =
+  let module M = Mugen.Syntax in
+  function
+  | M.Shifted (l, s) -> ULvl.shifted (to_ulvl l) s
+  | M.Top -> ULvl.top
+]}
+
+You might have noticed that there is a "top" level---we added the top level for convenience.
+
+{2 Add Smart Constructors}
+
+This step is technically optional, but it may be desirable to add smart constructors that will attempt to consolidate displacements when building an embedded level expressions. The rest of the tutorial will assume you have done this. To do so, the smart constructors need to know how to check whether an expression in your datatype is a level expression. Here is the snippet to include smart constructors for embedded level expressions:
+
+{[
+include
+  Mugen.Builder.Endo.Make
+    (struct
+      (** Your chosen displacement algebra *)
+      module Shift = ULvl.Shift
+
+      (** The type of embedded level expressions *)
+      type level = t
+
+      (** A function to embed a level expression *)
+      let level (l : ulvl) : t = ULvl l
+
+      (** A function to check whether an expression is an embed a level expression *)
+      let unlevel : t -> ulvl option = function ULvl l -> Some l | _ -> None
+    end)
+]}
+
+{1 Comparing Levels}
+
+The most common tasks are to compare two embedded levels. The code is straightforward---the [ULvl] module you have created in the earlier step comes with comparators. It is enough to first convert embedded level expressions to free ones, and compare them accordingly:
+{[
+  let equal_ulvl l1 l2 = ULvl.equal (to_ulvl l1) (to_ulvl l2)
+  let leq_ulvl l1 l2 = ULvl.leq (to_ulvl l1) (to_ulvl l2)
+  let lt_ulvl l1 l2 = ULvl.lt (to_ulvl l1) (to_ulvl l2)
+]}
+
+{1 Building Levels}
+
+Another common task in a real system is to parse user inputs and construct corresponding (embedded) level expressions. Remember that you have included the smart constructors in previous steps. The essential one
+{[
+  let _ = shifted l s
+]}
+to obtain the level [l] shifted by the displacement [s]. Constructing the displacement [s] depends on your chosen displacement algebra. If you were using integers, aliasing the stock {!module:Mugen.Shift.Int} as [ULvl.Shift]), then the shifting by 10 levels can be implemented as:
+{[
+  let _ = shifted l (ULvl.Shift.of_int 10)
+]}
+
+For convenience, we also introduced the top level
+{[
+  let _ = top
+]}
+that will be greater than any other level. (Note that you cannot shift the distinguished top level!)
+
+{1 Concluding Notes}
+
+That's it! Now you have rich universe levels. Here are a few remarks:
+
+{2 Ugly Printers for Debugging}
+
+It is recommended to write your own pretty printer. However, if you wish to dump the universe levels, check out {!val:Mugen.Syntax.Free.dump} for free level expressions and {!val:Mugen.Syntax.Endo.dump} for embedded ones.
+
+{2 Changing the Displacement Algebra}
+
+It is trivial to switch to another displacement algebra by aliasing [ULvl.Shift] to another module implementing the interface {!module-type:Mugen.Shift.S}. Changing the displacement algebra only affects how displacements are constructed and printed.
diff --git a/example/Bidir.ml b/example/Bidir.ml
index 0a8aa1b..5126546 100644
--- a/example/Bidir.ml
+++ b/example/Bidir.ml
@@ -8,14 +8,14 @@ type ctx = cell bwd
 let to_env ctx = Bwd.map (fun {tm; _} -> tm) ctx
 let to_size ctx = Bwd.length ctx
 
-let shift s = Syntax.ULvlShift.of_int s
+let shift s = ULvl.Shift.of_int s
 
 (** Type checking. *)
 let rec check ctx (tm : CS.t) (tp : Domain.t) =
   match tm, tp with
   | CS.Univ l1, Univ l2 ->
     let l1 = check ctx l1 TpULvl in
-    assert (ULvl.lt (ULvl.of_con (NbE.eval (to_env ctx) l1)) (ULvl.of_con l2));
+    assert (ULvl.lt (Domain.to_ulvl (NbE.eval (to_env ctx) l1)) (Domain.to_ulvl l2));
     Univ l1
   | CS.TpULvl, Univ (ULvl Top) -> TpULvl
   | CS.Shift (l, s), TpULvl ->
diff --git a/example/Domain.ml b/example/Domain.ml
index d6df558..efc9174 100644
--- a/example/Domain.ml
+++ b/example/Domain.ml
@@ -2,20 +2,42 @@ open Bwd
 
 type env = t bwd
 
+(** Use [endo] to embed universe levels into your datatype. *)
+and ulvl = (ULvl.shift, t) Mugen.Syntax.endo
+
 (** The (NbE) domain. *)
 and t =
   | Var of int
   | Univ of t
   | TpULvl
-  | ULvl of (Syntax.ULvlShift.t, t) Mugen.Syntax.endo
-  (** Use [endo] to embed universe levels into your datatype. *)
+  | ULvl of ulvl
+
+(** Conversion from the domain to free universe level expressions *)
+let rec to_ulvl : t -> ULvl.t =
+  function
+  | Var i -> Mugen.Syntax.Var i
+  | ULvl endo -> endo_to_ulvl endo
+  | _ -> invalid_arg "to_ulvl"
+
+and endo_to_ulvl : ulvl -> ULvl.t =
+  let module M = Mugen.Syntax in
+  function
+  | M.Shifted (l, s) -> ULvl.shifted (to_ulvl l) s
+  | M.Top -> ULvl.top
 
-(** Instantiate the theory module to handle universe levels your datatype. *)
-module ULvl =
-  Mugen.Semantics.Endo.Make
+(** Smart builders for universe levels *)
+include
+  Mugen.Builder.Endo.Make
     (struct
-      module Shift = Syntax.ULvlShift
+      (** Your chosen displacement algebra *)
+      module Shift = ULvl.Shift
+
+      (** The type of embedded level expressions *)
       type level = t
-      let level l = ULvl l
-      let unlevel = function ULvl l -> Some l | _ -> None
+
+      (** A function to embed a level expression *)
+      let level (l : ulvl) : t = ULvl l
+
+      (** A function to check whether an expression is an embed a level expression *)
+      let unlevel : t -> ulvl option = function ULvl l -> Some l | _ -> None
     end)
diff --git a/example/NbE.ml b/example/NbE.ml
index 12d7888..62b0a8a 100644
--- a/example/NbE.ml
+++ b/example/NbE.ml
@@ -3,8 +3,8 @@ open Bwd
 let rec eval_ulvl env =
   let module M = Mugen.Syntax in
   function
-  | M.Top -> Domain.ULvl.top
-  | M.Shifted (b, s) -> Domain.ULvl.shifted (eval env b) s
+  | M.Top -> Domain.top
+  | M.Shifted (b, s) -> Domain.shifted (eval env b) s
 
 and eval env : Syntax.t -> Domain.t =
   function
@@ -26,7 +26,7 @@ and quote ctx : Domain.t -> Syntax.t =
   | ULvl l -> ULvl (quote_ulvl ctx l)
 
 let equate_ulvl l1 l2 =
-  assert (ULvl.equal (ULvl.of_endo l1) (ULvl.of_endo l2))
+  assert (ULvl.equal (Domain.endo_to_ulvl l1) (Domain.endo_to_ulvl l2))
 
 let rec equate ctx (v1 : Domain.t) (v2 : Domain.t) =
   match v1, v2 with
@@ -41,15 +41,12 @@ let rec equate ctx (v1 : Domain.t) (v2 : Domain.t) =
   | _ ->
     failwith "equate"
 
-let leq_ulvl l1 l2 =
-  assert (ULvl.leq (ULvl.of_con l1) (ULvl.of_con l2))
-
 let subtype _ctx (v1 : Domain.t) (v2 : Domain.t) =
   match v1, v2 with
   | Var i1, Var i2 ->
     assert (Int.equal i1 i2)
   | Univ l1, Univ l2 ->
-    leq_ulvl l1 l2
+    assert (ULvl.leq (Domain.to_ulvl l1) (Domain.to_ulvl l2))
   | TpULvl, TpULvl ->
     ()
   | ULvl l1, ULvl l2 ->
diff --git a/example/Syntax.ml b/example/Syntax.ml
index c94dedf..f1bd7c2 100644
--- a/example/Syntax.ml
+++ b/example/Syntax.ml
@@ -1,7 +1,7 @@
-module ULvlShift = Mugen.Shift.Int
+type ulvl = (ULvl.shift, t) Mugen.Syntax.endo
 
-type t =
+and t =
   | Var of int
   | Univ of t
   | TpULvl
-  | ULvl of (ULvlShift.t, t) Mugen.Syntax.endo
+  | ULvl of ulvl
diff --git a/example/ULvl.ml b/example/ULvl.ml
index 0ef268d..147b05b 100644
--- a/example/ULvl.ml
+++ b/example/ULvl.ml
@@ -1,22 +1,26 @@
 (** A convenience module for freely generated universe level expressions. *)
 
-include
-  Mugen.Semantics.Free.Make
-    (struct
-      module Shift = Syntax.ULvlShift
-      type var = int
-      let equal_var = Int.equal
-    end)
+module Param =
+struct
+  (** Your chosen displacement algebra *)
+  module Shift = Mugen.Shift.Int
 
-(** Conversion from the domain. *)
-let rec of_con =
-  function
-  | Domain.Var i -> Mugen.Syntax.Var i
-  | Domain.ULvl endo -> of_endo endo
-  | _ -> invalid_arg "of_con"
+  (** The representation of variables in free level expressions *)
+  type var = int
 
-and of_endo =
-  let module M = Mugen.Syntax in
-  function
-  | M.Shifted (l, s) -> shifted (of_con l) s
-  | M.Top -> top
+  (** The equality checker for variables *)
+  let equal_var : var -> var -> bool = Int.equal
+end
+include Param
+
+(** An alias to the type of displacements *)
+type shift = Shift.t
+
+(** An alias to the type of free level expressions *)
+type t = (shift, int) Mugen.Syntax.free
+
+(** Smart builders for free level expressions *)
+include Mugen.Builder.Free.Make (Param)
+
+(** Comparators for free level expressions *)
+include Mugen.Theory.Make (Param)
diff --git a/src/Builder.ml b/src/Builder.ml
new file mode 100644
index 0000000..5e6793b
--- /dev/null
+++ b/src/Builder.ml
@@ -0,0 +1,42 @@
+module Endo =
+struct
+  include BuilderSigs.Endo
+
+  module Make (P : Param) : S with type shift := P.Shift.t and type level := P.level =
+  struct
+    include P
+    open Syntax.Endo
+
+    let top = level Top
+
+    let shifted l s =
+      match unlevel l with
+      | Some Top -> invalid_arg "cannot shift the top level"
+      | Some (Shifted (l, s')) ->
+        let s = Shift.compose s' s in
+        level @@ Shifted (l, s)
+      | None ->
+        level @@ Shifted (l, s)
+  end
+end
+
+module Free =
+struct
+  include BuilderSigs.Free
+
+  module Make (P : Param) : S with type shift := P.Shift.t and type var := P.var =
+  struct
+    open Syntax.Free
+
+    let var = var
+    module P = struct
+      include P
+      type level = (Shift.t, var) Syntax.free
+      let level t = Level t
+      let unlevel t = match t with Level l -> Some l | _ -> None
+    end
+
+    include P
+    include Endo.Make(P)
+  end
+end
diff --git a/src/Semantics.mli b/src/Builder.mli
similarity index 77%
rename from src/Semantics.mli
rename to src/Builder.mli
index ff92f97..8a90f28 100644
--- a/src/Semantics.mli
+++ b/src/Builder.mli
@@ -3,10 +3,10 @@ module Endo :
 sig
 
   (** Parameters of smart constructors. *)
-  module type Param = SemanticsSigs.Endo.Param
+  module type Param = BuilderSigs.Endo.Param
 
   (** The signature of smart constructors. *)
-  module type S = SemanticsSigs.Endo.S
+  module type S = BuilderSigs.Endo.S
 
   (** The implementation of smart constructors. *)
   module Make (P : Param) : S with type shift := P.Shift.t and type level := P.level
@@ -17,10 +17,10 @@ module Free :
 sig
 
   (** Parameters of smart constructors. *)
-  module type Param = SemanticsSigs.Free.Param
+  module type Param = BuilderSigs.Free.Param
 
   (** The signature of smart constructors. *)
-  module type S = SemanticsSigs.Free.S
+  module type S = BuilderSigs.Free.S
 
   (** The implementation of smart constructors. *)
   module Make (P : Param) : S with type shift := P.Shift.t and type var := P.var
diff --git a/src/BuilderSigs.ml b/src/BuilderSigs.ml
new file mode 100644
index 0000000..b76efc4
--- /dev/null
+++ b/src/BuilderSigs.ml
@@ -0,0 +1,72 @@
+(** Smart constructors for {!type:Syntax.endo}. *)
+module Endo =
+struct
+
+  (** Parameters of smart constructors. *)
+  module type Param =
+  sig
+    (** The displacement algebra. *)
+    module Shift : Shift.S
+
+    (** The type that embeds level expressions. *)
+    type level
+
+    (** The embedding of level expressions into {!type:level}. *)
+    val level : (Shift.t, level) Syntax.endo -> level
+
+    (** Extract the embedded level, if any. *)
+    val unlevel : level -> (Shift.t, level) Syntax.endo option
+  end
+
+  (** The signature of smart constructors. *)
+  module type S =
+  sig
+    (** The displacement algebra. *)
+    type shift
+
+    (** The type that embeds levels. *)
+    type level
+
+    (** [shifted s l] is the smarter version of {!val:Syntax.Endo.shifted} that collapses multiple displacements,
+        representing the level [l] shifted by the displacement [s].
+
+        @raise Invalid_argument When it (directly or indirectly) attempts to shift the top level. *)
+    val shifted : level -> shift -> level
+
+    (** [top] is {!val:Syntax.Endo.top}, the additional top level for convenience. *)
+    val top : level
+  end
+end
+
+(** Smart constructors for {!type:Syntax.free}. *)
+module Free =
+struct
+
+  (** Parameters of smart constructors. *)
+  module type Param =
+  sig
+    (** The displacement algebra. *)
+    module Shift : Shift.S
+
+    (** The type of level variables. *)
+    type var
+  end
+
+  (** The signature of smart constructors. *)
+  module type S =
+  sig
+    (** The displacement algebra. *)
+    type shift
+
+    (** The type of level variables. *)
+    type var
+
+    (** The type of freely generated levels. *)
+    type level = (shift, var) Syntax.free
+
+    (** [var] is {!val:Syntax.Free.var}, representing the variable level [v]. *)
+    val var : var -> level
+
+    include Endo.S with type shift := shift and type level := level
+  end
+end
diff --git a/src/Mugen.ml b/src/Mugen.ml
index fcdb7c2..9cc2bfb 100644
--- a/src/Mugen.ml
+++ b/src/Mugen.ml
@@ -1,5 +1,6 @@
-module StructuredType = StructuredType
 module Shift = Shift
 module ShiftWithJoin = ShiftWithJoin
 module Syntax = Syntax
-module Semantics = Semantics
+module Builder = Builder
+module Theory = Theory
+module StructuredType = StructuredType
diff --git a/src/Mugen.mli b/src/Mugen.mli
index 48ec955..07f5d16 100644
--- a/src/Mugen.mli
+++ b/src/Mugen.mli
@@ -1,14 +1,25 @@
-(** Structured types used in this library *)
-module StructuredType : module type of StructuredType
+(** {1 Gallery of Displacement Algebras} *)
 
-(** Displacement algebras *)
+(** Stock displacement algebras *)
 module Shift : module type of Shift
 
-(** Displacement algebras with joins *)
+(** Stock displacement algebras with joins *)
 module ShiftWithJoin : module type of ShiftWithJoin
 
-(** Syntax of universe levels with displacements *)
+(** {1 Syntax of Level Expressions} *)
+
+(** Syntax of universe level expressions *)
 module Syntax : module type of Syntax
 
+(** Smart builders for universe level expressions *)
+module Builder : module type of Builder
+
+(** {1 Comparators of Level Expressions} *)
+
 (** Semantic operations for universe levels with displacements *)
-module Semantics : module type of Semantics
+module Theory : module type of Theory
+
+(**/**)
+
+(** Structured types used in this library *)
+module StructuredType : module type of StructuredType
diff --git a/src/Semantics.ml b/src/Semantics.ml
deleted file mode 100644
index 54b36ea..0000000
--- a/src/Semantics.ml
+++ /dev/null
@@ -1,87 +0,0 @@
-module Endo =
-struct
-  include SemanticsSigs.Endo
-
-  module Make (P : Param) : S with type shift := P.Shift.t and type level := P.level =
-  struct
-    include P
-    open Syntax.Endo
-
-    let top = level Top
-
-    let shifted l s =
-      match unlevel l with
-      | Some Top -> invalid_arg "cannot shift the top level"
-      | Some (Shifted (l, s')) ->
-        let s = Shift.compose s' s in
-        level @@ Shifted (l, s)
-      | None ->
-        level @@ Shifted (l, s)
-  end
-end
-
-module Free =
-struct
-  include SemanticsSigs.Free
-
-  module Make (P : Param) : S with type shift := P.Shift.t and type var := P.var =
-  struct
-    open Syntax.Free
-
-    let var = var
-    module P = struct
-      include P
-      type level = (Shift.t, var) Syntax.free
-      let level t = Level t
-      let unlevel t = match t with Level l -> Some l | _ -> None
-    end
-
-    include P
-    include Endo.Make(P)
-
-    let normalize l =
-      let rec go l acc =
-        match l with
-        | Level Top ->
-          if acc = []
-          then level Top
-          else invalid_arg "cannot shift the top level"
-        | Level (Shifted (l, s)) -> go l (s :: acc)
-        | Var v -> Level (Shifted (Var v, List.fold_left Shift.compose Shift.id acc))
-      in
-      go l []
-
-    let equal x y =
-      match normalize x, normalize y with
-      | Level Top, Level Top -> true
-      | Level (Shifted (Var vx, sx)), Level (Shifted (Var vy, sy)) ->
-        equal_var vx vy && Shift.equal sx sy
-      | _ -> false
-
-    let lt x y =
-      match normalize x, normalize y with
-      | Level (Shifted (Var _, _)), Level Top -> true
-      | Level (Shifted (Var vx, sx)), Level (Shifted (Var vy, sy)) ->
-        equal_var vx vy && Shift.lt sx sy
-      | _ -> false
-
-    let leq x y =
-      match normalize x, normalize y with
-      | _, Level Top -> true
-      | Level (Shifted (Var vx, sx)), Level (Shifted (Var vy, sy)) ->
-        equal_var vx vy && Shift.leq sx sy
-      | _ -> false
-
-    let gt x y = lt y x
-    let geq x y = leq y x
-
-    module Infix =
-    struct
-      let (=) = equal
-      let (<) = lt
-      let (<=) = leq
-      let (>) = gt
-      let (>=) = geq
-    end
-  end
-end
diff --git a/src/SemanticsSigs.ml b/src/SemanticsSigs.ml
deleted file mode 100644
index 591da29..0000000
--- a/src/SemanticsSigs.ml
+++ /dev/null
@@ -1,114 +0,0 @@
-(** Semantic operations for {!type:Syntax.endo}. *)
-module Endo =
-struct
-
-  (** Parameters of smart constructors. *)
-  module type Param =
-  sig
-    (** The displacement algebra. *)
-    module Shift : Shift.S
-
-    (** The type that embeds levels. *)
-    type level
-
-    (** The embedding of levels into [level]. *)
-    val level : (Shift.t, level) Syntax.endo -> level
-
-    (** Extract the embedded level, if any. *)
-    val unlevel : level -> (Shift.t, level) Syntax.endo option
-  end
-
-  (** The signature of smart constructors. *)
-  module type S =
-  sig
-    (** The displacement algebra. *)
-    type shift
-
-    (** The type that embeds levels. *)
-    type level
-
-    (** Smarter version of {!val:Syntax.Endo.shifted} that collapses multiple displacements
-
-        @raise Invalid_argument When it attempts to shift the top level. *)
-    val shifted : level -> shift -> level
-
-    (** [top] is {!val:Syntax.Endo.top} *)
-    val top : level
-  end
-end
-
-(** Semantic operations for {!type:Syntax.free}. *)
-module Free =
-struct
-
-  (** Parameters of smart constructors. *)
-  module type Param =
-  sig
-    (** The displacement algebra. *)
-    module Shift : Shift.S
-
-    (** The type of level variables. *)
-    type var
-
-    (** [equal_var x y] checks whether two level variables [x] and [y] are the same. *)
-    val equal_var : var -> var -> bool
-  end
-
-  (** The signature of smart constructors. *)
-  module type S =
-  sig
-    (** The displacement algebra. *)
-    type shift
-
-    (** The type of level variables. *)
-    type var
-
-    (** The type of freely generated levels. *)
-    type level = (shift, var) Syntax.free
-
-    (** [var] is {!val:Syntax.Free.var} *)
-    val var : var -> level
-
-    include Endo.S with type shift := shift and type level := level
-
-    (** [equal l1 l2] checks whether [l1] and [l2] are the same universe level.
-
-        @raise Invalid_argument When [l1] or [l2] is shifted top. *)
-    val equal : level -> level -> bool
-
-    (** [lt l1 l2] checks whether [l1] is strictly less than [l2]. Note that trichotomy fails for general universe levels.
-
-        @raise Invalid_argument When [l1] or [l2] is shifted top. *)
-    val lt : level -> level -> bool
-
-    (** [leq l1 l2] checks whether [l1] is less than or equal to [l2]. Note that trichotomy fails for general universe levels.
-
-        @raise Invalid_argument When [l1] or [l2] is shifted top. *)
-    val leq : level -> level -> bool
-
-    (** [gt l1 l2] is [lt l2 l1]. *)
-    val gt : level -> level -> bool
-
-    (** [geq l1 l2] is [leq l2 l1]. *)
-    val geq : level -> level -> bool
-
-    (** Infix notation. *)
-    module Infix :
-    sig
-      (** Alias of {!val:equal}. *)
-      val (=) : level -> level -> bool
-
-      (** Alias of {!val:lt}. *)
-      val (<) : level -> level -> bool
-
-      (** Alias of {!val:leq}. *)
-      val (<=) : level -> level -> bool
-
-      (** Alias of {!val:gt}. *)
-      val (>) : level -> level -> bool
-
-      (** Alias of {!val:geq}. *)
-      val (>=) : level -> level -> bool
-    end
-  end
-end
diff --git a/src/Shift.mli b/src/Shift.mli
index acc5083..448b60a 100644
--- a/src/Shift.mli
+++ b/src/Shift.mli
@@ -1,6 +1,6 @@
 open StructuredType
 
-(** A displacement algebra. *)
+(** The signature of a displacement algebra. *)
 module type S =
 sig
   (** To form a valid displacement algebra, {!val:compose} and {!val:id} should form a monoid, and {!val:lt} (the strict order) must be left-invariant respect to {!val:compose}. *)
diff --git a/src/ShiftWithJoin.mli b/src/ShiftWithJoin.mli
index f9bd69b..943368a 100644
--- a/src/ShiftWithJoin.mli
+++ b/src/ShiftWithJoin.mli
@@ -1,4 +1,4 @@
-(** A displacement algebra with joins. *)
+(** The signature of a displacement algebra with binary joins. (Note that this refers to joins of displacements, not joins of universe levels.) *)
 module type Semilattice =
 sig
   (** @closed *)
diff --git a/src/Syntax.ml b/src/Syntax.ml
index 1bbf82b..d2d7b95 100644
--- a/src/Syntax.ml
+++ b/src/Syntax.ml
@@ -1,4 +1,3 @@
-(** A family of polynomial endofunctors [('s, -) endo] indexed by the type of displacements ['s]. *)
 type ('s, 'a) endo =
   | Shifted of 'a * 's
   | Top
diff --git a/src/Syntax.mli b/src/Syntax.mli
index 689a450..35fb64c 100644
--- a/src/Syntax.mli
+++ b/src/Syntax.mli
@@ -16,13 +16,13 @@ sig
     | Shifted of 'a * 's
     | Top
 
-  (** [shifted l s] is [Shifted (l, s)]. *)
+  (** [shifted l s] is [Shifted (l, s)], representing the level [l] shifted by the displacement [s]. *)
   val shifted : 'a -> 's -> ('s, 'a) t
 
-  (** [top] is [Top]. *)
+  (** [top] is [Top], the additional top level for convenience. *)
   val top : ('s, 'a) t
 
-  (** Ugly printer. *)
+  (** [dump dump_s dump_a] is the ugly printer for levels, where [dump_s] is the printer for displacements and [dump_a] is the printer for inner sub-expressions. *)
   val dump :
     (Format.formatter -> 's -> unit) ->
     (Format.formatter -> 'a -> unit) ->
@@ -37,16 +37,16 @@ sig
     | Level of ('s, ('s, 'v) free) endo
     | Var of 'v
 
-  (** [shifted l s] is [Level (Shifted (l, s))]. *)
+  (** [shifted l s] is [Level (Shifted (l, s))], representing the level [l] shifted by the displacement [s]. *)
   val shifted : ('s, 'v) t -> 's -> ('s, 'v) t
 
-  (** [top] is [Level Top]. *)
+  (** [top] is [Top], the additional top level for convenience. *)
   val top : ('s, 'v) t
 
-  (** [var v] is [Var v]. *)
+  (** [var v] is [Var v], representing the variable level [v]. *)
   val var : 'v -> ('s, 'v) t
 
-  (** Ugly printer. *)
+  (** [dump dump_s dump_v] is the ugly printer for levels, where [dump_s] is the printer for displacements and [dump_v] is the printer for variables. *)
   val dump :
     (Format.formatter -> 's -> unit) ->
     (Format.formatter -> 'v -> unit) ->
diff --git a/src/Theory.ml b/src/Theory.ml
new file mode 100644
index 0000000..7f4899f
--- /dev/null
+++ b/src/Theory.ml
@@ -0,0 +1,54 @@
+include TheorySigs
+
+module Make (P : Param) : S with type shift := P.Shift.t and type var := P.var =
+struct
+  open Syntax.Free
+
+  include P
+  include Builder.Free.Make(P)
+
+  let normalize l =
+    let rec go l acc =
+      match l with
+      | Level Top ->
+        if acc = []
+        then Level Top
+        else invalid_arg "cannot shift the top level"
+      | Level (Shifted (l, s)) -> go l (s :: acc)
+      | Var v -> Level (Shifted (Var v, List.fold_left Shift.compose Shift.id acc))
+    in
+    go l []
+
+  let equal x y =
+    match normalize x, normalize y with
+    | Level Top, Level Top -> true
+    | Level (Shifted (Var vx, sx)), Level (Shifted (Var vy, sy)) ->
+      equal_var vx vy && Shift.equal sx sy
+    | _ -> false
+
+  let lt x y =
+    match normalize x, normalize y with
+    | Level (Shifted (Var _, _)), Level Top -> true
+    | Level (Shifted (Var vx, sx)), Level (Shifted (Var vy, sy)) ->
+      equal_var vx vy && Shift.lt sx sy
+    | _ -> false
+
+  let leq x y =
+    match normalize x, normalize y with
+    | _, Level Top -> true
+    | Level (Shifted (Var vx, sx)), Level (Shifted (Var vy, sy)) ->
+      equal_var vx vy && Shift.leq sx sy
+    | _ -> false
+
+  let gt x y = lt y x
+  let geq x y = leq y x
+
+  module Infix =
+  struct
+    let (=) = equal
+    let (<) = lt
+    let (<=) = leq
+    let (>) = gt
+    let (>=) = geq
+  end
+end
diff --git a/src/Theory.mli b/src/Theory.mli
new file mode 100644
index 0000000..526d77f
--- /dev/null
+++ b/src/Theory.mli
@@ -0,0 +1,8 @@
+(** Parameters of the theory. *)
+module type Param = TheorySigs.Param
+
+(** The signature of the theory. *)
+module type S = TheorySigs.S
+
+(** The implementation of the theory. *)
+module Make (P : Param) : S with type shift := P.Shift.t and type var := P.var
diff --git a/src/TheorySigs.ml b/src/TheorySigs.ml
new file mode 100644
index 0000000..6f6fd14
--- /dev/null
+++ b/src/TheorySigs.ml
@@ -0,0 +1,65 @@
+(** Parameters of smart constructors. *)
+module type Param =
+sig
+  (** The displacement algebra. *)
+  module Shift : Shift.S
+
+  (** The type of level variables. *)
+  type var
+
+  (** [equal_var x y] checks whether two level variables [x] and [y] are the same. *)
+  val equal_var : var -> var -> bool
+end
+
+(** The signature of smart constructors. *)
+module type S =
+sig
+  (** The displacement algebra. *)
+  type shift
+
+  (** The type of level variables. *)
+  type var
+
+  (** The type of freely generated levels. *)
+  type level = (shift, var) Syntax.free
+
+  (** [equal l1 l2] checks whether [l1] and [l2] are the same universe level.
+
+      @raise Invalid_argument When [l1] or [l2] is shifted top. *)
+  val equal : level -> level -> bool
+
+  (** [lt l1 l2] checks whether [l1] is strictly less than [l2]. Note that trichotomy fails for general universe levels.
+
+      @raise Invalid_argument When [l1] or [l2] is shifted top. *)
+  val lt : level -> level -> bool
+
+  (** [leq l1 l2] checks whether [l1] is less than or equal to [l2]. Note that trichotomy fails for general universe levels.
+
+      @raise Invalid_argument When [l1] or [l2] is shifted top. *)
+  val leq : level -> level -> bool
+
+  (** [gt l1 l2] is [lt l2 l1]. *)
+  val gt : level -> level -> bool
+
+  (** [geq l1 l2] is [leq l2 l1]. *)
+  val geq : level -> level -> bool
+
+  (** Infix notation. *)
+  module Infix :
+  sig
+    (** Alias of {!val:equal}. *)
+    val (=) : level -> level -> bool
+
+    (** Alias of {!val:lt}. *)
+    val (<) : level -> level -> bool
+
+    (** Alias of {!val:leq}. *)
+    val (<=) : level -> level -> bool
+
+    (** Alias of {!val:gt}. *)
+    val (>) : level -> level -> bool
+
+    (** Alias of {!val:geq}. *)
+    val (>=) : level -> level -> bool
+  end
+end