initial post process

README.md

@@ -1,4 +1,4 @@
-# implicitt
+# implicitt (WIP)
 
 A "proof assistant" with holes and implicit arguments. Developed to learn about elaboration, meta variables and OCaml
 
@@ -14,9 +14,13 @@ A "proof assistant" with holes and implicit arguments. Developed to learn about
   * Parser (BNFC)
 
 * Metas
-* Unification
+	* Holes
+	* Unification
 * Implicit arguments
 
 * More types
   * Id
-  * Tarski Universes (in the core)
+  * W?
+  * Tarski Universes (in the core)?
+  
+* Pretty elimination syntax (cooltt esque)

lib/Raw/PostProcess.ml

@@ -1,4 +1,42 @@
-module A = AbsImplicitt
+module P = AbsImplicitt
 module R = RawSyntax
 
 open R
+
+exception UnboundVar
+
+let rec lookup (k : P.id) (env : P.id list) = 
+  match env with
+  | []      -> raise UnboundVar
+  | x :: xs -> if k == x then 0 else 1 + lookup k xs
+
+let rec proc (e : P.id list) (ex : P.exp) =
+  match ex with
+  | ExpPiE (name, dom, cod) -> Pi (Exp, proc e dom, proc (name :: e) cod)
+  | ExpPiI (name, dom, cod) -> Pi (Imp, proc e dom, proc (name :: e) cod)
+  | ExpSig (name, ty, fib) -> Sg (proc e ty, proc (name :: e) fib)
+  | ExpLet (name, tr, ty, sc) -> Let (proc e tr, proc e ty, proc (name :: e) sc)
+  | ExpLam ([], _) -> failwith "impossible empty lambda"
+  | ExpLam (bs, sc) -> unwrapLambda e bs sc
+  | ExpAppI (e1, e2) -> App (Imp, proc e e1, proc e e2)
+  | ExpAppE (e1, e2) -> App (Exp, proc e e1, proc e e2)
+  | ExpVar i -> Var (Ix (lookup i e)) (* todo: definitions, elimination *)
+  | ExpT0 -> T0
+  | ExpT1 -> T1
+  | ExpT1tr -> T1tr
+  | ExpTNat -> TNat
+  | ExpZero -> Zero
+  | ExpSuc e1 -> Suc (proc e e1)
+  | ExpTBool -> TBool
+  | ExpTrue -> True
+  | ExpFalse -> False
+  | ExpPair (e1, e2) -> Pair (proc e e1, proc e e2)
+  | ExpFst e1 -> Fst (proc e e1)
+  | ExpSnd e1 -> Snd (proc e e1)
+  | ExpHole -> failwith "hole not implemented"
+
+and unwrapLambda (e : P.id list) (bs : P.bD list) (sc : P.exp) =
+  match bs with
+  | [] -> proc e sc
+  | BE n :: bs -> Lam (Exp, unwrapLambda (n :: e) bs sc)
+  | BI n :: bs -> Lam (Imp, unwrapLambda (n :: e) bs sc)

lib/Raw/RawSyntax.ml

@@ -28,7 +28,7 @@ type ast
 
   | Pi   of icit * ast * ast
   | Lam  of icit * ast
-  | App  of icit * ast
+  | App  of icit * ast * ast
 
   | Sg   of ast * ast
   | Pair of ast * ast

lib/Raw/implicitt.cf

@@ -12,26 +12,27 @@ separator nonempty BD "" ;
 ExpPiE.    Exp  ::= "Π" "(" Id ":" Exp ")" Exp;
 ExpPiI.    Exp  ::= "Π" "{" Id ":" Exp "}" Exp;
 ExpSig.    Exp  ::= "Σ" "(" Id ":" Exp ")" Exp;
-ExpLet.    Exp  ::= "let" Id ":" Exp ":=" Exp "in" Exp;
+ExpLet.    Exp  ::= "let" Id ":" Exp "≔" Exp "in" Exp;
 ExpLam.    Exp  ::= "λ" [BD] "." Exp;
 ExpAppI.   Exp1 ::= Exp1 "{" Exp "}";
 ExpAppE.   Exp1 ::= Exp1 Exp2;
+ExpFst.    Exp1 ::= "pr₁" Exp2;
+ExpSnd.    Exp1 ::= "pr₂" Exp2;
+ExpSuc.    Exp1 ::= "S" Exp2;
 ExpVar.    Exp2 ::= Id;
 ExpT0.     Exp2 ::= "⊥";
 ExpT1.     Exp2 ::= "⊤";
 ExpT1tr.   Exp2 ::= "⋆";
 ExpTNat.   Exp2 ::= "ℕ";
-ExpTZero.  Exp2 ::= "0";
-ExpTSuc.   Exp2 ::= "S";
+ExpZero.   Exp2 ::= "0";
 ExpTBool.  Exp2 ::= "𝔹";
-ExpTTrue.  Exp2 ::= "T";
-ExpTFalse. Exp2 ::= "F";
-ExpTPair.  Exp2 ::= "⟨" Exp "," Exp "⟩";
-ExpTFst.   Exp2 ::= "pr₁";
-ExpTSnd.   Exp2 ::= "pr₂";
+ExpTrue.   Exp2 ::= "T";
+ExpFalse.  Exp2 ::= "F";
+ExpPair.   Exp2 ::= "⟨" Exp "," Exp "⟩";
+ExpHole.   Exp2 ::= "?";
 
 coercions Exp 2 ;
 
-VarDef. Def ::= "def" Id ":" Exp ":=" Exp;
+VarDef. Def ::= "def" Id ":" Exp "≔" Exp;
 
 separator Def "" ;