diff options
| -rw-r--r-- | lib/Domain.ml | 4 | ||||
| -rw-r--r-- | lib/Eval.ml | 3 | ||||
| -rw-r--r-- | lib/Eval.mli | 1 | ||||
| -rw-r--r-- | lib/Quote.ml | 47 | ||||
| -rw-r--r-- | lib/Quote.mli | 2 |
5 files changed, 56 insertions, 1 deletions
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 |