1 files changed, 47 insertions, 0 deletions
diff --git a/lib/Quote.ml b/lib/Quote.ml
new file mode 100644
index 0000000..5989870
--- /dev/null
+++ b/lib/Quote.ml
@@ -0,0 +1,47 @@
+open Bwd
+
+module S = Syntax
+module D = Domain
+
+module Internal =
+struct
+  (* keeping track of the context size *)
+  module Eff = Algaeff.Reader.Make (struct type t = int end)
+
+  let bind f =
+    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.Pi (base, fam) -> S.Pi (quote base, quote_clos fam)
+    | D.Lam clos -> S.Lam (quote_clos clos)
+    | D.Sg (base, fam) -> S.Sg (quote base, quote_clos fam)
+    | D.Pair (v, w) -> S.Pair (quote v, quote w)
+    | D.Type -> S.Type
+    | D.Bool -> S.Bool
+    | D.True -> S.True
+    | D.False -> S.False
+
+  and quote_clos clos = bind @@ fun arg -> quote (Eval.inst_clos clos arg)
+
+  and quote_ne (hd, frms) = Bwd.fold_left quote_frame (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_frame hd = function
+    | D.App v -> S.App (hd, quote v)
+    | D.Fst -> S.Fst hd
+    | D.Snd -> S.Snd hd
+    | D.BoolElim { cmot; vtrue; vfalse } ->
+      S.BoolElim {
+        motive = quote_clos cmot;
+        true_case = quote vtrue;
+        false_case = quote vfalse;
+        scrut = hd;
+      }
+end
+
+let quote ~size v = Internal.Eff.run ~env:size (fun () -> Internal.quote v)
+let quote_ne ~size ne = Internal.Eff.run ~env:size (fun () -> Internal.quote_ne ne)