From 8d40541003736d5319ec981278338e8c8c66daf6 Mon Sep 17 00:00:00 2001 From: Malte Voos Date: Sun, 23 Jun 2024 01:36:48 +0200 Subject: keep track of bound names everywhere to be able to output names instead of de bruijn indices --- lib/Eval.ml | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'lib/Eval.ml') 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 -- cgit 1.4.1