blob: 88560c208b63633ecefd539d96b6a32127866bba (
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
|
open Bwd
type value =
| Neutral of ne
| Pi of value * clos
| Lam of clos
| Sg of value * clos
| Pair of value * value
| Type
| Bool
| True
| False
and ne = ne_head * frame bwd
and ne_head = Var of int (* De Bruijn levels *)
and frame =
| BoolElim of {
cmot: clos;
vtrue: value;
vfalse: value;
}
| App of value
| Fst
| Snd
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)
|