diff --git a/lib/Raw/dune b/lib/Raw/dune index f044d4c..f6d34e6 100644 --- a/lib/Raw/dune +++ b/lib/Raw/dune @@ -1,2 +1,10 @@ +(ocamllex "LexImplicitt") +(ocamlyacc "ParImplicitt") + +(env + (dev + (flags (:standard -warn-error -A)))) + (library - (name Raw)) + (name Raw) + (modules "AbsImplicitt" "BNFC_Util" "LexImplicitt" "ParImplicitt")) diff --git a/lib/Raw/implicitt.cf b/lib/Raw/implicitt.cf index 6669b12..58f8f14 100644 --- a/lib/Raw/implicitt.cf +++ b/lib/Raw/implicitt.cf @@ -1,7 +1,3 @@ -layout toplevel ; -layout "let" ; -layout stop "in" ; - entrypoints [Def], Exp ; token Id ((letter|digit|["[]_"])+) ; @@ -9,33 +5,30 @@ token Id ((letter|digit|["[]_"])+) ; comment "--" ; comment "{-" "-}" ; -Assign. Assign ::= Id ":=" Exp ; -separator nonempty Assign ";" ; - -BD. BE ::= Id -BD. BI ::= "{" Id "}" +BE. BD ::= Id; +BI. BD ::= "{" 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 +ExpPiE. Exp ::= "Π" "(" Id ":" Exp ")" Exp; +ExpPiI. Exp ::= "Π" "{" Id ":" Exp "}" Exp; +ExpSig. Exp ::= "Σ" "(" Id ":" Exp ")" Exp; +ExpLet. Exp ::= "let" Id ":" Exp ":=" Exp "in" Exp; +ExpLam. Exp ::= "λ" [BD] "." Exp; +ExpApp. Exp1 ::= Exp1 Exp2; +ExpVar. Exp2 ::= Id; +ExpT0. Exp2 ::= "⊥"; +ExpT1. Exp2 ::= "⊤"; +ExpT1tr. Exp2 ::= "⋆"; +ExpTNat. Exp2 ::= "ℕ"; +ExpTZero. Exp2 ::= "0"; +ExpTSuc. Exp2 ::= "S"; +ExpTBool. Exp2 ::= "𝔹"; +ExpTTrue. Exp2 ::= "T"; +ExpTFalse. Exp2 ::= "F"; +ExpTPair. Exp2 ::= "⟨" Exp "," Exp "⟩"; +ExpTFst. Exp2 ::= "pr₁"; +ExpTSnd. Exp2 ::= "pr₂"; -VarDef. Def ::= "def" Id ":" Exp ":=" Exp +VarDef. Def ::= "def" Id ":" Exp ":=" Exp; -seperator Def ";" \ No newline at end of file +separator Def ";" ; \ No newline at end of file