1 files changed, 23 insertions, 4 deletions
diff --git a/src/nbe/Eval.ml b/src/nbe/Eval.ml
index bd8326e..2730ac0 100644
--- a/src/nbe/Eval.ml
+++ b/src/nbe/Eval.ml
@@ -16,27 +16,41 @@ struct
 
   and app v w = match v with
     | D.Lam (_, clo) -> inst_clo clo w
-    | D.Neutral (hd, frms) -> D.Neutral (hd, frms <: D.App w)
+    | D.Neutral (hd, frms) ->
+      D.Neutral (hd, frms <: D.App w)
+    | D.Unfold (hd, frms, v) ->
+      D.Unfold (hd, frms <: D.App w, Lazy.map (fun v -> app v w) v)
     | _ -> invalid_arg "Eval.app"
 
   and fst = function
     | D.Pair (v, _) -> v
-    | D.Neutral (hd, frms) -> D.Neutral (hd, frms <: D.Fst)
+    | D.Neutral (hd, frms) ->
+      D.Neutral (hd, frms <: D.Fst)
+    | D.Unfold (hd, frms, v) ->
+      D.Unfold (hd, frms <: D.Fst, Lazy.map (fun v -> fst v) v)
     | _ -> invalid_arg "Eval.fst"
 
   and snd = function
     | D.Pair (_, v) -> v
-    | D.Neutral (hd, frms) -> D.Neutral (hd, frms <: D.Snd)
+    | D.Neutral (hd, frms) ->
+      D.Neutral (hd, frms <: D.Snd)
+    | D.Unfold (hd, frms, v) ->
+      D.Unfold (hd, frms <: D.Snd, Lazy.map (fun v -> snd v) v)
     | _ -> invalid_arg "Eval.snd"
 
   and bool_elim motive_var motive true_case false_case = function
     | D.True -> true_case
     | D.False -> false_case
-    | D.Neutral (hd, frms) -> D.Neutral (hd, frms <: D.BoolElim { motive_var; motive; true_case; false_case })
+    | D.Neutral (hd, frms) ->
+      D.Neutral (hd, frms <: D.BoolElim { motive_var; motive; true_case; false_case })
+    | D.Unfold (hd, frms, v) ->
+      D.Unfold (hd, frms <: D.BoolElim { motive_var; motive; true_case; false_case }, 
+                Lazy.map (fun v -> bool_elim motive_var motive true_case false_case v) v)
     | _ -> invalid_arg "Eval.bool_elim"
 
   and eval = function
     | S.Var i -> Bwd.nth (Eff.read()) i
+    | S.Def (p, v) -> D.def p v
     | S.Pi (name, base, fam) -> D.Pi (name, eval base, make_clo fam)
     | S.Lam (name, body) -> D.Lam (name, make_clo body)
     | S.App (a, b) -> app (eval a) (eval b)
@@ -53,4 +67,9 @@ struct
 end
 
 let eval ~env tm = Internal.Eff.run ~env @@ fun () -> Internal.eval tm
+let eval_toplevel tm = eval ~env:Emp tm
 let inst_clo = Internal.inst_clo
+
+let rec force_all = function
+  | D.Unfold (_, _, v) -> force_all (Lazy.force v)
+  | v -> v