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/Quote.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'src/nbe/Quote.ml') diff --git a/src/nbe/Quote.ml b/src/nbe/Quote.ml index cc5a81e..94c8395 100644 --- a/src/nbe/Quote.ml +++ b/src/nbe/Quote.ml @@ -12,9 +12,10 @@ struct let arg = D.var (Eff.read()) in Eff.scope (fun size -> size + 1) @@ fun () -> f arg - + let rec quote = function | D.Neutral ne -> quote_ne ne + | D.Unfold uf -> quote_unfold uf | D.Pi (name, base, fam) -> S.Pi (name, quote base, quote_clo fam) | D.Lam (name, clo) -> S.Lam (name, quote_clo clo) | D.Sg (name, base, fam) -> S.Sg (name, quote base, quote_clo fam) @@ -27,9 +28,11 @@ struct and quote_clo clo = bind @@ fun arg -> quote (Eval.inst_clo clo arg) and quote_ne (hd, frms) = Bwd.fold_left quote_frm (quote_ne_head hd) frms - and quote_ne_head (D.Var i) = S.Var (Eff.read() - i - 1) (* converting from levels to indices *) + and quote_unfold (hd, frms, _) = Bwd.fold_left quote_frm (quote_unfold_head hd) frms + and quote_unfold_head (D.Def (p, v)) = S.Def (p, v) + and quote_frm hd = function | D.App v -> S.App (hd, quote v) | D.Fst -> S.Fst hd @@ -45,3 +48,4 @@ struct end let quote ~size v = Internal.Eff.run ~env:size (fun () -> Internal.quote v) +let quote_toplevel v = quote ~size:0 v -- cgit 1.4.1