start work on raw syntax

lib/Raw/RawSyntax.ml

@@ -1,5 +1,38 @@
+type var = Ix of int
 type name = string
 
-type bind
+type icit
   = Imp
   | Exp
+
+type ast
+  = Var of var
+
+  | Type
+
+  | T0
+  | Ind0 of ast * ast
+
+  | T1
+  | T1tr (* Unit eta rule instead of elimination principle *)
+
+  | TNat
+  | Zero
+  | Suc  of ast
+  | IndN of ast * ast * ast * ast
+
+  | TBool
+  | True
+  | False
+  | IndB of ast * ast * ast * ast (* ordered true, false *)
+
+  | Pi   of icit * ast * ast
+  | Lam  of icit * ast
+  | App  of icit * ast
+
+  | Sg   of ast * ast
+  | Pair of ast * ast
+  | Fst  of ast
+  | Snd  of ast
+
+  | Let  of ast * ast * ast (* tr : ty in sc *)

lib/Raw/implicitt.cf

@@ -0,0 +1,41 @@
+layout toplevel ;
+layout "let" ;
+layout stop "in" ;
+
+entrypoints [Def], Exp ;
+
+token Id ((letter|digit|["[]_"])+) ;
+
+comment "--" ;
+comment "{-" "-}" ;
+
+Assign. Assign ::= Id ":=" Exp ;
+separator nonempty Assign ";" ;
+
+BD. BE ::= Id
+BD. BI ::= "{" Id "}"
+separator nonempty BD "" ;
+
+ExpPiE.    Exp ::= "Π" "(" Id ":" Exp ")" Exp
+ExpPiI.    Exp ::= "Π" "{" Id ":" Exp "}" Exp
+ExpSig.    Exp ::= "Σ" "(" Id ":" Exp ")" Exp
+ExpLet.    Exp ::= "let" "{" [Assign] "}" "in" Exp
+ExpLam.    Exp ::= "λ" [BD] "." Exp
+ExpVar.    Exp ::= Id
+ExpT0.     Exp ::= "⊥"
+ExpT1.     Exp ::= "⊤"
+ExpT1tr.   Exp ::= "⋆"
+ExpTNat.   Exp ::= "ℕ"
+ExpTZero.  Exp ::= "0"
+ExpTSuc.   Exp ::= "S"
+ExpTBool.  Exp ::= "𝔹"
+ExpTTrue.  Exp ::= "T"
+ExpTFalse. Exp ::= "F"
+ExpTPair.  Exp ::= "⟨" Exp , Exp "⟩"
+ExpTFst.   Exp ::= "pr₁"
+ExpTSnd.   Exp ::= "pr₂"
+ExpApp.    Exp ::= Exp Exp
+
+VarDef. Def ::= "def" Id ":" Exp ":=" Exp
+
+seperator Def ";"