blob: d2f94d30b3ae98e1c9c975bbf330107ed8819230 (
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
|
open Bwd
(** Syntactic terms *)
type syn =
| Var of int
| 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;
}
(** Semantic domain *)
type value =
| Neutral of ne
| 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 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 }
|