implement top-level definitions

1 files changed, 6 insertions, 2 deletions

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