Merge pull request #25 from ToposInstitute/docs/annotate-constructors…

…-with-syntax Annotates Constructors with Syntax
ToposInstitute · Jun 23, 2023 · 9f69ad8 · 9f69ad8
2 parents a2b2e0c + dd3867d
commit 9f69ad8
Show file tree

Hide file tree

Showing 2 changed files with 70 additions and 41 deletions.
diff --git a/lib/core/Data.ml b/lib/core/Data.ml
@@ -12,12 +12,12 @@ type syn =
   | Var of int
   | Borrow of int
   (** Negative variables are DeBruijn levels, even in the syntax! *)
-  | Pi of Ident.t * syn * syn (* Π (a : A) (B a) *)
-  | Lam of Ident.t * syn (* λ x. e *)
-  | Let of Ident.t * syn * syn (* let x = e in t *)
-  | Ap of syn * syn (* f a *)
-  | Sigma of Ident.t * syn * syn (* Σ[ a ∈ A] (B a) *)
-  | Pair of syn * syn (* A × B *)
+  | Pi of Ident.t * syn * syn 
+  | Lam of Ident.t * syn 
+  | Let of Ident.t * syn * syn 
+  | Ap of syn * syn 
+  | Sigma of Ident.t * syn * syn
+  | Pair of syn * syn
   | Fst of syn
   | Snd of syn
   | Eq of syn * syn * syn
@@ -30,13 +30,13 @@ type syn =
       -> P y p
   *)
   (* | AxiomJ of  *)
-  | Nat (* ℕ *)
-  | Zero (* zero *)
-  | Succ of syn (* succ n *)
+  | Nat 
+  | Zero 
+  | Succ of syn 
   | NatElim of { mot : syn; zero : syn; succ : syn; scrut : syn }
-  | FinSet of labelset (* #{ foo, bar } *)
-  | Label of labelset * label (* .foo *)
-  | Cases of syn * syn labeled * syn (* { foo = syn₁, bar = syn₂ } e *)
+  | FinSet of labelset 
+  | Label of labelset * label 
+  | Cases of syn * syn labeled * syn 
   | Univ
   | Poly
   | PolyIntro of Ident.t * syn * syn

diff --git a/lib/core/Syntax.ml b/lib/core/Syntax.ml
@@ -13,35 +13,64 @@ type 'a labeled = (string * 'a) list
 type ppenv = { pos : Ident.t bwd; neg_size : int; neg : Ident.t bwd }
 
 type t = Data.syn =
-  | Var of int
-  | Borrow of int
-  | Pi of Ident.t * t * t
-  | Lam of Ident.t * t
-  | Let of Ident.t * t * t
-  | Ap of t * t
-  | Sigma of Ident.t * t * t
-  | Pair of t * t
-  | Fst of t
-  | Snd of t
-  | Eq of t * t * t
-  | Refl of t
-  | Nat
-  | Zero
-  | Succ of t
-  | NatElim of { mot : t; zero : t; succ : t; scrut : t }
-  | FinSet of labelset
-  | Label of labelset * label
-  | Cases of t * t labeled * t
-  | Univ
-  | Poly
-  | PolyIntro of Ident.t * t * t
-  | Base of t
-  | Fib of t * t
-  | Hom of t * t
-  | HomLam of t
-  | HomElim of t * t
-  | Hole of t * int
-  | Skolem of t
+  | (* t *) 
+    Var of int
+  | (* borrow t *)
+    Borrow of int
+  | (* Π (a : A), (B a) *)
+    Pi of Ident.t * t * t
+  | (* λ x. e *) 
+    Lam of Ident.t * t 
+  | (* let x = e in t *)
+    Let of Ident.t * t * t 
+  | (* f a *)
+    Ap of t * t
+  | (* Σ (x : A), B x *)
+    Sigma of Ident.t * t * t 
+  | (* (a , b) *)
+    Pair of t * t 
+  | (* fst x *)
+    Fst of t 
+  | (* snd x *) 
+    Snd of t 
+  | (* a = b *)
+    Eq of t * t * t 
+  | (* refl *) 
+    Refl of t 
+  | (* ℕ *)
+    Nat
+  | (* zero *) 
+    Zero
+  | (* succ n *)
+    Succ of t
+  | (* elim mot z s scrut *)
+    NatElim of { mot : t; zero : t; succ : t; scrut : t }
+  | (* #{ foo, bar } *)
+    FinSet of labelset
+  | (* .foo *)
+    Label of labelset * label
+  | (* { foo = syn₁, bar = syn₂ } e *)
+    Cases of t * t labeled * t
+  | (* Type *) 
+    Univ 
+  | (* Poly *) 
+    Poly
+  | (* (p : P) × q *) 
+    PolyIntro of Ident.t * t * t
+  | (* base p *)
+    Base of t
+  | (* fib x y *)
+    Fib of t * t
+  | (* p ⇒ q *)
+    Hom of t * t
+  | (* λ a⁺ a⁻ ⇝ p *) 
+    HomLam of t
+  | (* x y *)
+    HomElim of t * t
+  | (* ? *) 
+    Hole of t * int 
+  | (* skolem *)
+    Skolem of t
 
 let pp_sep_list ?(sep = ", ") pp_elem fmt xs =
   Format.pp_print_list ~pp_sep:(fun fmt () -> Format.pp_print_string fmt sep) pp_elem fmt xs