blob: 19ca67da3c2306bc41cbbdac21096a3a041ed47d (
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
|
open Bwd
(** Syntactic terms *)
type syn =
| Var of int
| Pi of syn * (* BINDS *) syn
| Lam of (* BINDS *) syn
| App of syn * syn
| Sg of syn * (* BINDS *) syn
| Pair of syn * syn
| Fst of syn
| Snd of syn
| Type
| Bool
| True
| False
| BoolElim of {
motive : (* BINDS *) syn;
true_case : syn;
false_case : syn;
scrut : syn;
}
(** Semantic domain *)
type value =
| Neutral of ne
| Pi of value * clo
| Lam of clo
| Sg of 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 frm =
| App of value
| Fst
| Snd
| BoolElim of {
cmot: clo;
vtrue: value;
vfalse: value;
}
and env = value bwd
and clo = Clo of { body : syn; env : env }
|