From 60f620c00e208051a8c45c4b426825b07cbe86da Mon Sep 17 00:00:00 2001
From: depsterr <depsterr@protonmail.com>
Date: Sat, 3 Sep 2022 12:36:13 +0200
Subject: [PATCH] I hate grammers

---
 bin/dune                 |  2 +-
 lib/Parse/PostProcess.ml |  4 +++
 lib/Parse/dune           |  4 ++-
 lib/Parse/implicitt.cf   | 54 +++++++++++++++++++++-------------------
 lib/Raw/RawSyntax.ml     |  0
 lib/Raw/dune             |  2 ++
 6 files changed, 38 insertions(+), 28 deletions(-)
 create mode 100644 lib/Parse/PostProcess.ml
 create mode 100644 lib/Raw/RawSyntax.ml
 create mode 100644 lib/Raw/dune

diff --git a/bin/dune b/bin/dune
index 4f94a6e..b6a52d7 100644
--- a/bin/dune
+++ b/bin/dune
@@ -1,4 +1,4 @@
 (executable
  (public_name implicitt)
  (name main)
- (libraries implicitt))
+ (libraries Core Raw Parse))
diff --git a/lib/Parse/PostProcess.ml b/lib/Parse/PostProcess.ml
new file mode 100644
index 0000000..773ae6a
--- /dev/null
+++ b/lib/Parse/PostProcess.ml
@@ -0,0 +1,4 @@
+open Raw
+
+module A = AbsImplicitt
+module R = RawSyntax
diff --git a/lib/Parse/dune b/lib/Parse/dune
index c6755e3..746b65d 100644
--- a/lib/Parse/dune
+++ b/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)
diff --git a/lib/Parse/implicitt.cf b/lib/Parse/implicitt.cf
index e22f696..063bb30 100644
--- a/lib/Parse/implicitt.cf
+++ b/lib/Parse/implicitt.cf
@@ -13,48 +13,50 @@ NImp.   Name ::= "{" Id "}";
 NExp.   Name ::= Id;
 separator nonempty Name "" ;
 
--- Term 2
-TVar.   Term2 ::= Id;
+-- Term 3
+TType.  Term3 ::= "Type";
 
-TType.  Term2 ::= "Type";
+TT0.    Term3 ::= "𝟘";
+TInd0.  Term3 ::= "𝟘-elim";
 
-TT0.    Term2 ::= "𝟘";
+TT1.    Term3 ::= "𝟙";
+TT1tr.  Term3 ::= "★";
 
-TT1.    Term2 ::= "𝟙";
-TT1tr.  Term2 ::= "★";
+TBool.  Term3 ::= "𝟚";
+TTrue.  Term3 ::= "true";
+TFalse. Term3 ::= "false";
+TIndB.  Term3 ::= "𝟚-elim";
 
-TBool.  Term2 ::= "𝟚";
-TTrue.  Term2 ::= "true";
-TFalse. Term2 ::= "false";
+TNat.   Term3 ::= "ℕ";
+TZero.  Term3 ::= "0";
+TSuc.   Term3 ::= "suc";
+TIndN.  Term3 ::= "ℕ-elim";
 
-TNat.   Term2 ::= "ℕ";
-TZero.  Term2 ::= "0";
+TFst.   Term3 ::= "pr₁";
+TSnd.   Term3 ::= "pr₂";
 
-TLam.   Term2 ::= "λ" [Name] "." Term;
+TLam.   Term3 ::= "λ" [Name] "." Term;
+
+TVar.   Term3 ::= Id;
+
+-- Term2
+
+TAppEx. Term2 ::= Term2 Term3;
+TAppIm. Term2 ::= Term2 "{" Term "}";
 
 -- Term1
-TInd0.  Term1 ::= "𝟘-elim" Term2 Term2;
-
-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;
+TPiAr.  Term1 ::= Term2 "→" Term1;
+TSgCr.  Term1 ::= Term2 "×" Term1;
 
 -- 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;
diff --git a/lib/Raw/RawSyntax.ml b/lib/Raw/RawSyntax.ml
new file mode 100644
index 0000000..e69de29
diff --git a/lib/Raw/dune b/lib/Raw/dune
new file mode 100644
index 0000000..f044d4c
--- /dev/null
+++ b/lib/Raw/dune
@@ -0,0 +1,2 @@
+(library
+ (name Raw))