docs: first edition of tutorial (#21)

docs/dune

@@ -0,0 +1,2 @@
+(documentation
+  (package mugen))

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.

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.

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 ->

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)

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 ->

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

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)

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