keep track of bound names everywhere to be able to output names instead of de bruijn indices

1 files changed, 10 insertions, 10 deletions

diff --git a/lib/Eval.ml b/lib/Eval.ml
index 033ee8c..bd8326e 100644
--- a/lib/Eval.ml
+++ b/lib/Eval.ml
@@ -15,7 +15,7 @@ struct
     Eff.run ~env @@ fun () -> eval body
 
   and app v w = match v with
-    | D.Lam clo -> inst_clo clo w
+    | D.Lam (_, clo) -> inst_clo clo w
     | D.Neutral (hd, frms) -> D.Neutral (hd, frms <: D.App w)
     | _ -> invalid_arg "Eval.app"
 
@@ -29,18 +29,18 @@ struct
     | 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 })
+  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 })
     | _ -> invalid_arg "Eval.bool_elim"
 
   and eval = function
     | S.Var i -> Bwd.nth (Eff.read()) i
-    | S.Pi (base, fam) -> D.Pi (eval base, make_clo fam)
-    | S.Lam body -> D.Lam (make_clo body)
+    | 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)
-    | S.Sg (base, fam) -> D.Sg (eval base, make_clo fam)
+    | S.Sg (name, base, fam) -> D.Sg (name, eval base, make_clo fam)
     | S.Pair (a, b) -> D.Pair (eval a, eval b)
     | S.Fst a -> fst (eval a)
     | S.Snd a -> snd (eval a)
@@ -48,8 +48,8 @@ struct
     | S.Bool -> D.Bool
     | S.True -> D.True
     | S.False -> D.False
-    | S.BoolElim { motive; true_case; false_case; scrut } ->
-      bool_elim (make_clo motive) (eval true_case) (eval false_case) (eval scrut)
+    | S.BoolElim { motive_var; motive; true_case; false_case; scrut } ->
+      bool_elim motive_var (make_clo motive) (eval true_case) (eval false_case) (eval scrut)
 end
 
 let eval ~env tm = Internal.Eff.run ~env @@ fun () -> Internal.eval tm