1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
|
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)
|