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
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
|
open Bwd
open Bwd.Infix
module S = Syntax
module D = Domain
module Internal =
struct
module Eff = Algaeff.Reader.Make (struct type nonrec t = D.env end)
let make_clo body = D.Clo { body; env = Eff.read() }
let rec inst_clo (D.Clo { body; env }) arg =
let env = env <: arg in
Eff.run ~env @@ fun () -> eval body
and app v w = match v with
| D.Lam (_, clo) -> inst_clo clo w
| D.Neutral (hd, frms) ->
D.Neutral (hd, frms <: D.App w)
| D.Unfold (hd, frms, v) ->
D.Unfold (hd, frms <: D.App w, Lazy.map (fun v -> app v w) v)
| _ -> invalid_arg "Eval.app"
and fst = function
| D.Pair (v, _) -> v
| D.Neutral (hd, frms) ->
D.Neutral (hd, frms <: D.Fst)
| D.Unfold (hd, frms, v) ->
D.Unfold (hd, frms <: D.Fst, Lazy.map (fun v -> fst v) v)
| _ -> invalid_arg "Eval.fst"
and snd = function
| D.Pair (_, v) -> v
| D.Neutral (hd, frms) ->
D.Neutral (hd, frms <: D.Snd)
| D.Unfold (hd, frms, v) ->
D.Unfold (hd, frms <: D.Snd, Lazy.map (fun v -> snd v) v)
| _ -> invalid_arg "Eval.snd"
and bool_elim motive_var motive true_case false_case = function
| D.True -> true_case
| D.False -> false_case
| D.Neutral (hd, frms) ->
D.Neutral (hd, frms <: D.BoolElim { motive_var; motive; true_case; false_case })
| D.Unfold (hd, frms, v) ->
D.Unfold (hd, frms <: D.BoolElim { motive_var; motive; true_case; false_case },
Lazy.map (fun v -> bool_elim motive_var motive true_case false_case v) v)
| _ -> invalid_arg "Eval.bool_elim"
and eval = function
| S.Var i -> Bwd.nth (Eff.read()) i
| S.Def (p, v) -> D.def p v
| S.Pi (name, base, fam) -> D.Pi (name, eval base, make_clo fam)
| S.Lam (name, body) -> D.Lam (name, make_clo body)
| S.App (a, b) -> app (eval a) (eval b)
| S.Sg (name, base, fam) -> D.Sg (name, eval base, make_clo fam)
| S.Pair (a, b) -> D.Pair (eval a, eval b)
| S.Fst a -> fst (eval a)
| S.Snd a -> snd (eval a)
| S.Type -> D.Type
| S.Bool -> D.Bool
| S.True -> D.True
| S.False -> D.False
| S.BoolElim { motive_var; motive; true_case; false_case; scrut } ->
bool_elim motive_var (make_clo motive) (eval true_case) (eval false_case) (eval scrut)
end
let eval ~env tm = Internal.Eff.run ~env @@ fun () -> Internal.eval tm
let eval_toplevel tm = eval ~env:Emp tm
let inst_clo = Internal.inst_clo
let rec force_all = function
| D.Unfold (_, _, v) -> force_all (Lazy.force v)
| v -> v
|