core syntax, semantic domain, evaluation

10 files changed, 130 insertions, 24 deletions

diff --git a/dune-project b/dune-project
index ede6aa8..61494e3 100644
--- a/dune-project
+++ b/dune-project
@@ -15,7 +15,7 @@
  (name toytt)
  (synopsis "A short synopsis")
  (description "A longer description")
- (depends ocaml dune ppx_deriving asai)
+ (depends ocaml dune menhir ppx_deriving algaeff asai bwd)
  (tags
   (topics "to describe" your project)))
 
diff --git a/flake.nix b/flake.nix
index 6be9e8b..0b8acde 100644
--- a/flake.nix
+++ b/flake.nix
@@ -24,7 +24,7 @@
           (on.listRepo (on.makeOpamRepo ./.));
         devPackagesQuery = {
           ocaml-lsp-server = "*";
-          ocamlformat = "*";
+          ocp-indent = "*";
         };
         query = devPackagesQuery // {
           ocaml-base-compiler = "*";
diff --git a/lib/Ast.ml b/lib/Ast.ml
index f7c90dd..d26cc0f 100644
--- a/lib/Ast.ml
+++ b/lib/Ast.ml
@@ -6,6 +6,14 @@ and arg = raw_arg Asai.Range.located
 
 and raw_expr =
   | Var of raw_ident
+  | Pi of arg * expr
+  | Lam of ident * expr
+  | App of expr * expr
+  | Sg of arg * expr
+  | Pair of expr * expr
+  | Fst of expr
+  | Snd of expr
+  | Type
   | Bool
   | True
   | False
@@ -16,14 +24,6 @@ and raw_expr =
       false_case : expr;
       scrut : expr;
     }
-  | Pi of arg * expr
-  | Lam of ident * expr
-  | App of expr * expr
-  | Sg of arg * expr
-  | Pair of expr * expr
-  | Fst of expr
-  | Snd of expr
-  | Type
 
 and expr = raw_expr Asai.Range.located
 
diff --git a/lib/Domain.ml b/lib/Domain.ml
new file mode 100644
index 0000000..cf07a4b
--- /dev/null
+++ b/lib/Domain.ml
@@ -0,0 +1,27 @@
+open Bwd
+
+type value =
+  | Neutral of ne
+  | Pi of value * clos
+  | Lam of clos
+  | Sg of value * clos
+  | Pair of value * value
+  | Type
+  | Bool
+  | True
+  | False
+
+and ne = ne_head * frame bwd
+and ne_head = Var of int (* De Bruijn levels *)
+and frame = 
+  | BoolElim of {
+      cmot: clos;
+      vtrue: value;
+      vfalse: value;
+    }
+  | App of value
+  | Fst
+  | Snd
+
+and env = value bwd
+and clos = Clos of { body : Syntax.tm; env : env }
diff --git a/lib/Eval.ml b/lib/Eval.ml
new file mode 100644
index 0000000..29ede14
--- /dev/null
+++ b/lib/Eval.ml
@@ -0,0 +1,55 @@
+open Bwd
+open Bwd.Infix
+
+module S = Syntax
+module D = Domain
+
+module Internal =
+struct
+  module Eff = Algaeff.Reader.Make (struct type nonrec t = D.env end)
+
+  let make_clos body = D.Clos { body; env = Eff.read() }
+
+  let rec inst_clos (D.Clos { body; env }) arg =
+    let env = env <: arg in
+    Eff.run ~env @@ fun () -> eval body
+
+  and app v w = match v with
+    | D.Lam clos -> inst_clos clos w
+    | D.Neutral (hd, frms) -> D.Neutral (hd, frms <: D.App w)
+    | _ -> invalid_arg "Eval.app"
+
+  and fst = function
+    | D.Pair (v, _) -> v
+    | D.Neutral (hd, frms) -> D.Neutral (hd, frms <: D.Fst)
+    | _ -> invalid_arg "Eval.fst"
+
+  and snd = function
+    | D.Pair (_, v) -> v
+    | D.Neutral (hd, frms) -> D.Neutral (hd, frms <: D.Snd)
+    | _ -> invalid_arg "Eval.snd"
+
+  and bool_elim cmot vtrue vfalse = function
+    | D.True -> vtrue
+    | D.False -> vfalse
+    | D.Neutral (hd, frms) -> D.Neutral (hd, frms <: D.BoolElim { cmot; vtrue; vfalse })
+    | _ -> invalid_arg "Eval.bool_elim"
+
+  and eval = function
+    | S.Var i -> BwdLabels.nth (Eff.read()) i
+    | S.Pi (base, fam) -> D.Pi (eval base, make_clos fam)
+    | S.Lam body -> D.Lam (make_clos body)
+    | S.App (a, b) -> app (eval a) (eval b)
+    | S.Sg (base, fam) -> D.Sg (eval base, make_clos fam)
+    | S.Pair (a, b) -> D.Pair (eval a, eval b)
+    | S.Fst a -> fst (eval a)
+    | S.Snd a -> snd (eval a)
+    | S.Type -> D.Type
+    | S.Bool -> D.Bool
+    | S.True -> D.True
+    | S.False -> D.False
+    | S.BoolElim { motive; true_case; false_case; scrut } ->
+      bool_elim (make_clos motive) (eval true_case) (eval false_case) (eval scrut)
+end
+
+let eval ~env tm = Internal.Eff.run ~env (fun () -> Internal.eval tm)
diff --git a/lib/Eval.mli b/lib/Eval.mli
new file mode 100644
index 0000000..aaa8977
--- /dev/null
+++ b/lib/Eval.mli
@@ -0,0 +1 @@
+val eval : env:Domain.env -> Syntax.tm -> Domain.value
diff --git a/lib/Lexer.mll b/lib/Lexer.mll
index a8410d0..3f178f5 100644
--- a/lib/Lexer.mll
+++ b/lib/Lexer.mll
@@ -20,13 +20,13 @@ rule lex =
   | "," { COMMA }
   | "." { DOT }
   | "=>" { FATARROW }
-  | "bool" { BOOL }
-  | "true" { TRUE }
-  | "false" { FALSE }
-  | "bool-elim" { BOOL_ELIM }
   | "at" { AT }
   | "fst" { FST }
   | "snd" { SND }
   | "type" { TYPE }
+  | "bool" { BOOL }
+  | "true" { TRUE }
+  | "false" { FALSE }
+  | "bool-elim" { BOOL_ELIM }
   | ident { IDENT (Lexing.lexeme lexbuf) }
   | eof { EOF }
diff --git a/lib/Parser.mly b/lib/Parser.mly
index 5c587b2..d0395ac 100644
--- a/lib/Parser.mly
+++ b/lib/Parser.mly
@@ -12,7 +12,7 @@ open Ast
 %token EOF
 
 %right ARROW ASTERISK
-%left IDENT LPR APP BACKSLASH FST SND BOOL TRUE FALSE BOOL_ELIM
+%left IDENT LPR APP BACKSLASH FST SND TYPE BOOL TRUE FALSE BOOL_ELIM
 
 %start <Ast.expr> parse
 
@@ -35,15 +35,6 @@ raw_expr:
 	{ Var name }
   | LPR; e = raw_expr; RPR
 	{ e }
-  | BOOL
-	{ Bool }
-  | TRUE
-	{ True }
-  | FALSE
-	{ False }
-  | BOOL_ELIM; scrut = expr; AT; motive_var = ident; ARROW; motive_body = expr;
-	LBR; TRUE; FATARROW; true_case = expr; COMMA; FALSE; FATARROW; false_case = expr; RBR
-	{ BoolElim { motive_var; motive_body; true_case; false_case; scrut } }
 
   | a = arg; ARROW; b = expr
 	{ Pi (a, b) }
@@ -64,6 +55,16 @@ raw_expr:
   | TYPE
 	{ Type }
 
+  | BOOL
+	{ Bool }
+  | TRUE
+	{ True }
+  | FALSE
+	{ False }
+  | BOOL_ELIM; scrut = expr; AT; motive_var = ident; ARROW; motive_body = expr;
+	LBR; TRUE; FATARROW; true_case = expr; COMMA; FALSE; FATARROW; false_case = expr; RBR
+	{ BoolElim { motive_var; motive_body; true_case; false_case; scrut } }
+
 %inline
 expr: e = locate(raw_expr) { e }
 
diff --git a/lib/Syntax.ml b/lib/Syntax.ml
new file mode 100644
index 0000000..6cd988a
--- /dev/null
+++ b/lib/Syntax.ml
@@ -0,0 +1,19 @@
+type tm =
+  | Var of int
+  | Pi of tm * (* BINDS *) tm
+  | Lam of (* BINDS *) tm
+  | App of tm * tm
+  | Sg of tm * (* BINDS *) tm
+  | Pair of tm * tm
+  | Fst of tm
+  | Snd of tm
+  | Type
+  | Bool
+  | True
+  | False
+  | BoolElim of {
+      motive : (* BINDS *) tm;
+      true_case : tm;
+      false_case : tm;
+      scrut : tm;
+    }
diff --git a/toytt.opam b/toytt.opam
index 1a4a45c..c2dd3f6 100644
--- a/toytt.opam
+++ b/toytt.opam
@@ -12,8 +12,11 @@ bug-reports: "https://github.com/username/reponame/issues"
 depends: [
   "ocaml"
   "dune" {>= "3.13"}
+  "menhir"
   "ppx_deriving"
+  "algaeff"
   "asai"
+  "bwd"
   "odoc" {with-doc}
 ]
 build: [