From 963015801e636358cdc458c1422a6700860635b0 Mon Sep 17 00:00:00 2001 From: depsterr Date: Sat, 3 Sep 2022 11:06:12 +0200 Subject: [PATCH] added basic parser --- lib/{ => Core}/Convert.ml | 0 lib/{ => Core}/Eval.ml | 1 + lib/{ => Core}/Term.ml | 2 ++ lib/{ => Core}/Value.ml | 0 lib/Core/dune | 2 ++ lib/Parse/dune | 10 +++++++ lib/Parse/implicitt.cf | 60 +++++++++++++++++++++++++++++++++++++++ lib/dune | 2 -- 8 files changed, 75 insertions(+), 2 deletions(-) rename lib/{ => Core}/Convert.ml (100%) rename lib/{ => Core}/Eval.ml (97%) rename lib/{ => Core}/Term.ml (90%) rename lib/{ => Core}/Value.ml (100%) create mode 100644 lib/Core/dune create mode 100644 lib/Parse/dune create mode 100644 lib/Parse/implicitt.cf delete mode 100644 lib/dune diff --git a/lib/Convert.ml b/lib/Core/Convert.ml similarity index 100% rename from lib/Convert.ml rename to lib/Core/Convert.ml diff --git a/lib/Eval.ml b/lib/Core/Eval.ml similarity index 97% rename from lib/Eval.ml rename to lib/Core/Eval.ml index 82df1ab..4977293 100644 --- a/lib/Eval.ml +++ b/lib/Core/Eval.ml @@ -39,6 +39,7 @@ let rec eval (env : V.env) (tr : T.term) = | Pair (x, y) -> V.Pair (eval env x, eval env y) | Fst tr -> fst (eval env tr) | Snd tr -> snd (eval env tr) + | Let (tr, _, B sc) -> eval (eval env tr :: env) sc (* B b, B B ts *) and indN (env : V.env) (b : T.term) (tz : V.value) (ts : T.term) (n : V.value) = diff --git a/lib/Term.ml b/lib/Core/Term.ml similarity index 90% rename from lib/Term.ml rename to lib/Core/Term.ml index b509b6c..1fa1886 100644 --- a/lib/Term.ml +++ b/lib/Core/Term.ml @@ -31,3 +31,5 @@ type term | Pair of term * term | Fst of term | Snd of term + + | Let of term * term * term binder (* tr : ty in sc *) diff --git a/lib/Value.ml b/lib/Core/Value.ml similarity index 100% rename from lib/Value.ml rename to lib/Core/Value.ml diff --git a/lib/Core/dune b/lib/Core/dune new file mode 100644 index 0000000..a27e659 --- /dev/null +++ b/lib/Core/dune @@ -0,0 +1,2 @@ +(library + (name Core)) diff --git a/lib/Parse/dune b/lib/Parse/dune new file mode 100644 index 0000000..405a68d --- /dev/null +++ b/lib/Parse/dune @@ -0,0 +1,10 @@ +(library + (name Parse) + (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 (system "bnfc --ocaml implicitt.cf"))) +(ocamllex LexImplicitt) +(ocamlyacc ParImplicitt) diff --git a/lib/Parse/implicitt.cf b/lib/Parse/implicitt.cf new file mode 100644 index 0000000..e22f696 --- /dev/null +++ b/lib/Parse/implicitt.cf @@ -0,0 +1,60 @@ +entrypoints [Def], Term; + +token Id ((letter|digit|["[]_"])+) ; + +comment "--" ; +comment "{-" "-}" ; + +Defn. Def ::= "def" Id ":" Term ":=" Term; +separator nonempty Def "" ; + +-- names bound by lambdas +NImp. Name ::= "{" Id "}"; +NExp. Name ::= Id; +separator nonempty Name "" ; + +-- Term 2 +TVar. Term2 ::= Id; + +TType. Term2 ::= "Type"; + +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; + +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 "⟩"; + + +coercions Term 2; diff --git a/lib/dune b/lib/dune deleted file mode 100644 index c76f468..0000000 --- a/lib/dune +++ /dev/null @@ -1,2 +0,0 @@ -(library - (name implicitt))