From 97f84ccace4e634b4e02178a702818e69292dc9f Mon Sep 17 00:00:00 2001 From: Malte Voos Date: Mon, 8 Jul 2024 22:01:42 +0200 Subject: implement top-level definitions --- src/nbe/Eval.ml | 27 +++++++++++++++++++++++---- 1 file changed, 23 insertions(+), 4 deletions(-) (limited to 'src/nbe/Eval.ml') 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 -- cgit 1.4.1