docs: start working on the "tutorial"

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,19 @@
+{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}
+
+A universe level expression in this library is represented as a pair of a variable together with a {i displacement}. For example, [x + 10] means the variable level [x] shifted by 10 levels. The "shifting of 10 levels" is a displacement in our terminology. While it looks limited to consider only a variable and a displacement, we proved that it is in a sense a universal scheme if you allow all mathematically possible displacements beyond natural numbers. We also call the minimum algebra of disablements 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 level expressions.
+
+{1 Choose Your Displacements}
+
+The first step is to choose your favorite {i displacements}.
+
+{1 Define Your Syntax}
+
+{1 Build Level Expressions}
+
+{1 Compare Level Expressions}

example/Bidir.ml

@@ -8,19 +8,19 @@ 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 = Syntax.UnivLvlShift.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));
+    let l1 = check ctx l1 TpUnivLvl in
+    assert (UnivLvl.lt (UnivLvl.of_con (NbE.eval (to_env ctx) l1)) (UnivLvl.of_con l2));
     Univ l1
-  | CS.TpULvl, Univ (ULvl Top) -> TpULvl
-  | CS.Shift (l, s), TpULvl ->
-    let l = check ctx l TpULvl in
-    ULvl (Shifted (l, shift s))
+  | CS.TpUnivLvl, Univ (UnivLvl Top) -> TpUnivLvl
+  | CS.Shift (l, s), TpUnivLvl ->
+    let l = check ctx l TpUnivLvl in
+    UnivLvl (Shifted (l, shift s))
   | _ ->
     let tm, tp' = infer ctx tm in
     NbE.subtype (to_size ctx) tp' tp;

example/ConcreteSyntax.ml

@@ -2,5 +2,5 @@
 type t =
   | Var of int
   | Univ of t
-  | TpULvl
+  | TpUnivLvl
   | Shift of t * int

example/Domain.ml

@@ -2,20 +2,22 @@ open Bwd
 
 type env = t bwd
 
+and univ_lvl = (Syntax.UnivLvlShift.t, 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
+  | TpUnivLvl
+  | UnivLvl of univ_lvl
   (** Use [endo] to embed universe levels into your datatype. *)
 
 (** Instantiate the theory module to handle universe levels your datatype. *)
-module ULvl =
+module UnivLvl =
   Mugen.Semantics.Endo.Make
     (struct
-      module Shift = Syntax.ULvlShift
+      module Shift = Syntax.UnivLvlShift
       type level = t
-      let level l = ULvl l
-      let unlevel = function ULvl l -> Some l | _ -> None
+      let level (l : univ_lvl) : t = UnivLvl l
+      let unlevel : t -> univ_lvl option = function UnivLvl l -> Some l | _ -> None
     end)

example/NbE.ml

@@ -3,15 +3,15 @@ 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.UnivLvl.top
+  | M.Shifted (b, s) -> Domain.UnivLvl.shifted (eval env b) s
 
 and eval env : Syntax.t -> Domain.t =
   function
   | Var i -> Bwd.nth env i
   | Univ l -> Univ (eval env l)
-  | TpULvl -> TpULvl
-  | ULvl l -> eval_ulvl env l
+  | TpUnivLvl -> TpUnivLvl
+  | UnivLvl l -> eval_ulvl env l
 
 let rec quote_ulvl ctx : _ Mugen.Syntax.endo -> _ Mugen.Syntax.endo =
   function
@@ -22,37 +22,37 @@ and quote ctx : Domain.t -> Syntax.t =
   function
   | Var i -> Var ((ctx-1) - i)
   | Univ l -> Univ (quote ctx l)
-  | TpULvl -> TpULvl
-  | ULvl l -> ULvl (quote_ulvl ctx l)
+  | TpUnivLvl -> TpUnivLvl
+  | UnivLvl l -> UnivLvl (quote_ulvl ctx l)
 
 let equate_ulvl l1 l2 =
-  assert (ULvl.equal (ULvl.of_endo l1) (ULvl.of_endo l2))
+  assert (UnivLvl.equal (UnivLvl.of_endo l1) (UnivLvl.of_endo l2))
 
 let rec equate ctx (v1 : Domain.t) (v2 : Domain.t) =
   match v1, v2 with
   | Var i1, Var i2 ->
     assert (Int.equal i1 i2)
   | Univ l1, Univ l2 ->
     equate ctx l1 l2
-  | TpULvl, TpULvl ->
+  | TpUnivLvl, TpUnivLvl ->
     ()
-  | ULvl l1, ULvl l2 ->
+  | UnivLvl l1, UnivLvl l2 ->
     equate_ulvl l1 l2
   | _ ->
     failwith "equate"
 
 let leq_ulvl l1 l2 =
-  assert (ULvl.leq (ULvl.of_con l1) (ULvl.of_con l2))
+  assert (UnivLvl.leq (UnivLvl.of_con l1) (UnivLvl.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
-  | TpULvl, TpULvl ->
+  | TpUnivLvl, TpUnivLvl ->
     ()
-  | ULvl l1, ULvl l2 ->
+  | UnivLvl l1, UnivLvl l2 ->
     equate_ulvl l1 l2
   | _ ->
     failwith "subtype"

example/Syntax.ml

@@ -1,7 +1,9 @@
-module ULvlShift = Mugen.Shift.Int
+module UnivLvlShift = Mugen.Shift.Int
 
-type t =
+type univ_lvl = (UnivLvlShift.t, t) Mugen.Syntax.endo
+
+and t =
   | Var of int
   | Univ of t
-  | TpULvl
-  | ULvl of (ULvlShift.t, t) Mugen.Syntax.endo
+  | TpUnivLvl
+  | UnivLvl of univ_lvl

example/ULvl.ml → example/UnivLvl.ml

@@ -1,21 +1,23 @@
 (** A convenience module for freely generated universe level expressions. *)
 
+type t = (Syntax.UnivLvlShift.t, int) Mugen.Syntax.free
+
 include
   Mugen.Semantics.Free.Make
     (struct
-      module Shift = Syntax.ULvlShift
+      module Shift = Syntax.UnivLvlShift
       type var = int
       let equal_var = Int.equal
     end)
 
 (** Conversion from the domain. *)
-let rec of_con =
+let rec of_con : Domain.t -> t =
   function
   | Domain.Var i -> Mugen.Syntax.Var i
-  | Domain.ULvl endo -> of_endo endo
+  | Domain.UnivLvl endo -> of_endo endo
   | _ -> invalid_arg "of_con"
 
-and of_endo =
+and of_endo : Domain.univ_lvl -> t =
   let module M = Mugen.Syntax in
   function
   | M.Shifted (l, s) -> shifted (of_con l) s

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

src/Semantics.mli → 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

src/SemanticsSigs.ml → src/BuilderSigs.ml

@@ -1,4 +1,4 @@
-(** Semantic operations for {!type:Syntax.endo}. *)
+(** Smart builders for {!type:Syntax.endo}. *)
 module Endo =
 struct
 
@@ -37,7 +37,7 @@ struct
   end
 end
 
-(** Semantic operations for {!type:Syntax.free}. *)
+(** Smart builders for {!type:Syntax.free}. *)
 module Free =
 struct
 
@@ -49,9 +49,6 @@ struct
 
     (** 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. *)
@@ -70,45 +67,5 @@ struct
     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

src/Mugen.mli

@@ -1,14 +1,29 @@
-(** Structured types used in this library *)
-module StructuredType : module type of StructuredType
+(**
+   A gallary of
+*)
+
+(** {1 Gallery of Displacement Algebras} *)
 
 (** Displacement algebras *)
 module Shift : module type of Shift
 
 (** 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