I hate grammers

bin/dune

@@ -1,4 +1,4 @@
 (executable
  (public_name implicitt)
  (name main)
- (libraries implicitt))
+ (libraries Core Raw Parse))

lib/Parse/PostProcess.ml

@@ -0,0 +1,4 @@
+open Raw
+
+module A = AbsImplicitt
+module R = RawSyntax

lib/Parse/dune

@@ -1,10 +1,12 @@
 (library
  (name Parse)
+ (libraries Raw)
  (flags (:standard -w -27 -w -39 -w -33)))
+
 (rule
-  (alias bnfc)
   (deps "implicitt.cf")
   (targets AbsImplicitt.ml BNFC_Util.ml LexImplicitt.mll ParImplicitt.mly PrintImplicitt.ml ShowImplicitt.ml SkelImplicitt.ml TestImplicitt.ml)
   (action (run bnfc --ocaml %{deps})))
+
 (ocamllex LexImplicitt)
 (ocamlyacc ParImplicitt)

lib/Parse/implicitt.cf

@@ -13,48 +13,50 @@ NImp.   Name ::= "{" Id "}";
 NExp.   Name ::= Id;
 separator nonempty Name "" ;
 
+-- Term 3
+TType.  Term3 ::= "Type";
+
+TT0.    Term3 ::= "𝟘";
+TInd0.  Term3 ::= "𝟘-elim";
+
+TT1.    Term3 ::= "𝟙";
+TT1tr.  Term3 ::= "★";
+
+TBool.  Term3 ::= "𝟚";
+TTrue.  Term3 ::= "true";
+TFalse. Term3 ::= "false";
+TIndB.  Term3 ::= "𝟚-elim";
+
+TNat.   Term3 ::= "ℕ";
+TZero.  Term3 ::= "0";
+TSuc.   Term3 ::= "suc";
+TIndN.  Term3 ::= "ℕ-elim";
+
+TFst.   Term3 ::= "pr₁";
+TSnd.   Term3 ::= "pr₂";
+
+TLam.   Term3 ::= "λ" [Name] "." Term;
+
+TVar.   Term3 ::= Id;
+
 -- Term2
-TVar.   Term2 ::= Id;
 
-TType.  Term2 ::= "Type";
+TAppEx. Term2 ::= Term2 Term3;
-
+TAppIm. Term2 ::= Term2 "{" Term "}";
-TT0.    Term2 ::= "𝟘";
-
-TT1.    Term2 ::= "𝟙";
-TT1tr.  Term2 ::= "★";
-
-TBool.  Term2 ::= "𝟚";
-TTrue.  Term2 ::= "true";
-TFalse. Term2 ::= "false";
-
-TNat.   Term2 ::= "ℕ";
-TZero.  Term2 ::= "0";
-
-TLam.   Term2 ::= "λ" [Name] "." Term;
 
 -- Term1
-TInd0.  Term1 ::= "𝟘-elim" Term2 Term2;
+TPiAr.  Term1 ::= Term2 "→" Term1;
-
+TSgCr.  Term1 ::= Term2 "×" Term1;
-TIndB.  Term1 ::= "𝟚-elim" Term2 Term2 Term2 Term2;
-
-TSuc.   Term1 ::= "suc" Term2;
-TIndN.  Term1 ::= "ℕ-elim" Term2 Term2 Term2 Term2;
-
-TFst.   Term1 ::= "pr₁" Term2;
-TSnd.   Term1 ::= "pr₂" Term2;
-
-TApp.   Term1 ::= Term1 Term2;
 
 -- Term0
 TLet.   Term ::= "let" Id ":" Term ":=" Term "in" Term ;
 
-TPiAr.  Term ::= Term "→" Term;
 TPiEx.  Term ::= "(" Id ":" Term ")" "→" Term;
 TPiIm.  Term ::= "{" Id ":" Term "}" "→" Term;
 
-TSgCr.  Term ::= Term "×" Term;
 TSg.    Term ::= "(" Id ":" Term ")" "×" Term;
 TPair.  Term ::= "⟨" Term "," Term "⟩";
 
+THole.  Term ::= "?";
 
-coercions Term 2;
+coercions Term 3;

lib/Raw/dune

@@ -0,0 +1,2 @@
+(library
+ (name Raw))