From 5252fe93e5e7ef77888c06c97de4e350dce90448 Mon Sep 17 00:00:00 2001
From: Malte Voos <git@mal.tc>
Date: Tue, 20 Feb 2024 12:48:36 +0100
Subject: nbe: quotation

---
 lib/Domain.ml |  4 ++++
 lib/Eval.ml   |  3 ++-
 lib/Eval.mli  |  1 +
 lib/Quote.ml  | 47 +++++++++++++++++++++++++++++++++++++++++++++++
 lib/Quote.mli |  2 ++
 5 files changed, 56 insertions(+), 1 deletion(-)
 create mode 100644 lib/Quote.ml
 create mode 100644 lib/Quote.mli

(limited to 'lib')

diff --git a/lib/Domain.ml b/lib/Domain.ml
index cf07a4b..88560c2 100644
--- a/lib/Domain.ml
+++ b/lib/Domain.ml
@@ -25,3 +25,7 @@ and frame =
 
 and env = value bwd
 and clos = Clos of { body : Syntax.tm; env : env }
+
+type cell = { tm : value; tp : value }
+
+let var i = Neutral (Var i, Bwd.Emp)
diff --git a/lib/Eval.ml b/lib/Eval.ml
index 29ede14..8f6722b 100644
--- a/lib/Eval.ml
+++ b/lib/Eval.ml
@@ -36,7 +36,7 @@ struct
     | _ -> invalid_arg "Eval.bool_elim"
 
   and eval = function
-    | S.Var i -> BwdLabels.nth (Eff.read()) i
+    | S.Var i -> Bwd.nth (Eff.read()) i
     | S.Pi (base, fam) -> D.Pi (eval base, make_clos fam)
     | S.Lam body -> D.Lam (make_clos body)
     | S.App (a, b) -> app (eval a) (eval b)
@@ -53,3 +53,4 @@ struct
 end
 
 let eval ~env tm = Internal.Eff.run ~env (fun () -> Internal.eval tm)
+let inst_clos = Internal.inst_clos
diff --git a/lib/Eval.mli b/lib/Eval.mli
index aaa8977..24fa87d 100644
--- a/lib/Eval.mli
+++ b/lib/Eval.mli
@@ -1 +1,2 @@
 val eval : env:Domain.env -> Syntax.tm -> Domain.value
+val inst_clos : Domain.clos -> Domain.value -> Domain.value
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)
diff --git a/lib/Quote.mli b/lib/Quote.mli
new file mode 100644
index 0000000..c55aa8b
--- /dev/null
+++ b/lib/Quote.mli
@@ -0,0 +1,2 @@
+val quote : size:int -> Domain.value -> Syntax.tm
+val quote_ne : size:int -> Domain.ne -> Syntax.tm
-- 
cgit 1.4.1