1 files changed, 55 insertions, 0 deletions
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)