From 00667c11af32322a73d2e7a367db3ba92f405c1e Mon Sep 17 00:00:00 2001
From: depsterr <depsterr@protonmail.com>
Date: Wed, 25 Jan 2023 21:17:49 +0100
Subject: [PATCH] start work on raw syntax

---
 lib/Raw/RawSyntax.ml | 35 ++++++++++++++++++++++++++++++++++-
 lib/Raw/implicitt.cf | 41 +++++++++++++++++++++++++++++++++++++++++
 2 files changed, 75 insertions(+), 1 deletion(-)
 create mode 100644 lib/Raw/implicitt.cf

diff --git a/lib/Raw/RawSyntax.ml b/lib/Raw/RawSyntax.ml
index c485af7..92abd2c 100644
--- a/lib/Raw/RawSyntax.ml
+++ b/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 *)
diff --git a/lib/Raw/implicitt.cf b/lib/Raw/implicitt.cf
new file mode 100644
index 0000000..6669b12
--- /dev/null
+++ b/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 ";"
\ No newline at end of file