diff options
author | Malte Voos <git@mal.tc> | 2024-06-23 23:31:59 +0200 |
---|---|---|
committer | Malte Voos <git@mal.tc> | 2024-06-24 00:16:55 +0200 |
commit | 5d227bcd0055d02e1d49a3dcd27e80a756923d5b (patch) | |
tree | da468ad3a8f3caf709b731ca2678c86a5a015990 /lib/Quote.ml | |
parent | 8d40541003736d5319ec981278338e8c8c66daf6 (diff) | |
download | toytt-5d227bcd0055d02e1d49a3dcd27e80a756923d5b.tar.gz toytt-5d227bcd0055d02e1d49a3dcd27e80a756923d5b.zip |
split code into smaller libraries and make a better repl
Diffstat (limited to 'lib/Quote.ml')
-rw-r--r-- | lib/Quote.ml | 48 |
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) |