blob: 8589ea54663d6eac1046d3fe95fd1c2c918470d4 (
plain)
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
|
open Bwd
type syn =
| Var of int
| Def of Ident.t * value Lazy.t
| Pi of Ident.local * syn * (* BINDS *) syn
| Lam of Ident.local * (* BINDS *) syn
| App of syn * syn
| Sg of Ident.local * syn * (* BINDS *) syn
| Pair of syn * syn
| Fst of syn
| Snd of syn
| Type
| Bool
| True
| False
| BoolElim of {
motive_var : Ident.local;
motive : (* BINDS *) syn;
true_case : syn;
false_case : syn;
scrut : syn;
}
and value =
| Neutral of ne
| Unfold of unfold
| Pi of Ident.local * value * clo
| Lam of Ident.local * clo
| Sg of Ident.local * value * clo
| Pair of value * value
| Type
| Bool
| True
| False
and ne = ne_head * frm bwd
and ne_head =
| Var of int (* De Bruijn levels *)
and unfold = unfold_head * frm bwd * value Lazy.t
and unfold_head =
| Def of Ident.t * value Lazy.t
and frm =
| App of value
| Fst
| Snd
| BoolElim of {
motive_var : Ident.local;
motive: clo;
true_case: value;
false_case: value;
}
and env = value bwd
and clo = Clo of { body : syn; env : env }
|