35 lines
1.3 KiB
OCaml
35 lines
1.3 KiB
OCaml
|
module V = Value
|
||
|
|
module T = Term
|
||
|
|
|
||
|
|
let rec index : V.env -> int -> V.value
|
||
|
|
= fun env i ->
|
||
|
|
match env with
|
||
|
|
| [] -> failwith "Can't happen"
|
||
|
|
| x :: xs -> if i < 1 then x else index xs (i-1)
|
||
|
|
|
||
|
|
let rec eval : V.env -> t.term -> V.value
|
||
|
|
= fun env tr ->
|
||
|
|
match tr with
|
||
|
|
| Var i -> index env i
|
||
|
|
| Type -> V.Type
|
||
|
|
| T0 -> V.T0
|
||
|
|
| Ind0 (B b, t) -> failwith "todo"
|
||
|
|
| T1 -> V.T1
|
||
|
|
| T1tr -> V.T1tr
|
||
|
|
| Ind1 (B b, t1 tr) -> failwith "todo"
|
||
|
|
| TNat -> V.TNat
|
||
|
|
| Zero -> V.Zero
|
||
|
|
| Suc n -> failwith "todo"
|
||
|
|
| IndN (B b, tz, B B ts, n) -> failwith "todo"
|
||
|
|
| TBool -> failwith "todo"
|
||
|
|
| True -> failwith "todo"
|
||
|
|
| False -> failwith "todo"
|
||
|
|
| IndB (B b, tt, tf, b) -> failwith "todo"
|
||
|
|
| Pi (dom, B cod) -> failwith "todo"
|
||
|
|
| Lam (B body) -> failwith "todo"
|
||
|
|
| App (f, x) -> failwith "todo"
|
||
|
|
| Sg (ty, tr) -> failwith "todo"
|
||
|
|
| Pair (x, y) -> failwith "todo"
|
||
|
|
| Fst tr -> failwith "todo"
|
||
|
|
| Snd tr -> failwith "todo"
|