split code into smaller libraries and make a better repl

1 files changed, 0 insertions, 48 deletions

diff --git a/lib/Quote.ml b/lib/Quote.ml
deleted file mode 100644
index 4b88e91..0000000
--- a/lib/Quote.ml
+++ /dev/null
@@ -1,48 +0,0 @@
-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 (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)
-    | 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_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_frm hd = function
-    | D.App v -> S.App (hd, quote v)
-    | D.Fst -> S.Fst hd
-    | D.Snd -> S.Snd hd
-    | D.BoolElim { motive_var; motive; true_case; false_case } ->
-      S.BoolElim {
-        motive_var;
-        motive = quote_clo motive;
-        true_case = quote true_case;
-        false_case = quote false_case;
-        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)