rachel/implicitt
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

did work on evaluation

Browse Source
This commit is contained in:
Rachel Lambda Samuelsson 2022-08-30 16:12:47 +02:00
parent 75f4dea650
commit 354705afe5
3 changed files with 58 additions and 35 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

84
lib/Eval.ml
View File

@ -1,34 +1,58 @@
module V = Value module V = Value
module T = Term module T = Term
let rec index : V.env -> int -> V.value let rec index (env : V.env) (i : int) =
= fun env i -> match env with
match env with | [] -> failwith "Can't happen"
| [] -> failwith "Can't happen" | x :: xs -> if i < 1 then x else index xs (i-1)
| x :: xs -> if i < 1 then x else index xs (i-1)
let rec eval : V.env -> t.term -> V.value let rec eval (env : V.env) (tr : T.term) =
= fun env tr -> match tr with
match tr with | Var (Ix i) -> index env i
| Var i -> index env i | Type -> V.Type
| Type -> V.Type | T0 -> V.T0
| T0 -> V.T0 | Ind0 (B b, t) -> begin
| Ind0 (B b, t) -> failwith "todo" match eval env t with
| T1 -> V.T1 | Stuck (s , T0) -> V.Stuck (V.Ind0 (V.C (env, b), s), V.T0)
| T1tr -> V.T1tr | _ -> failwith "eval Ind0 impossible error"
| Ind1 (B b, t1 tr) -> failwith "todo" end
| TNat -> V.TNat | T1 -> V.T1
| Zero -> V.Zero | T1tr -> V.T1vl
| Suc n -> failwith "todo" | TNat -> V.TNat
| IndN (B b, tz, B B ts, n) -> failwith "todo" | Zero -> V.Zero
| TBool -> failwith "todo" | Suc n -> V.Suc (eval env n)
| True -> failwith "todo" | IndN (B b, tz, B B ts, n) -> indN env b (eval env tz) ts (eval env n)
| False -> failwith "todo" | TBool -> V.TBool
| IndB (B b, tt, tf, b) -> failwith "todo" | True -> V.True
| Pi (dom, B cod) -> failwith "todo" | False -> V.False
| Lam (B body) -> failwith "todo" | IndB (B b, t, f, bo) -> begin
| App (f, x) -> failwith "todo" match eval env bo with
| Sg (ty, tr) -> failwith "todo" | True -> eval env t
| Pair (x, y) -> failwith "todo" | False -> eval env f
| Fst tr -> failwith "todo" | Stuck (s, TBool) -> V.Stuck (V.IndB (V.C (env, b), eval env t, eval env f, s), V.TBool)
| Snd tr -> failwith "todo" | _ -> failwith "eval IndB impossible error"
end
| Pi (dom, B cod) -> V.Pi (eval env dom, V.C (env, cod))
| Lam (B scope) -> V.Lam (C (env, scope))
| App (f, x) -> app (eval env f) (eval env x)
| Sg (ty, B tr) -> V.Sg (eval env ty, V.C (env, tr))
| Pair (x, y) -> V.Pair (eval env x, eval env y)
| Fst tr -> fst (eval env tr)
| Snd tr -> snd (eval env tr)
(* B b, B B ts *)
and indN (env : V.env) (b : T.term) (tz : V.value) (ts : T.term) (n : V.value) =
match n with
| Zero -> tz
| Suc m -> eval (indN env b tz ts m :: m :: env) ts
| Stuck (s, TNat) -> V.Stuck (V.IndN (V.C (env, b), tz, V.C2 (env, ts), s), V.TNat)
| _ -> failwith "eval IndN impossible error"
and app (f : V.value) (x : V.value) =
failwith "todo"
and fst (p : V.value) =
failwith "todo"
and snd (p : V.value) =
failwith "todo"

3
lib/Term.ml
View File

@ -11,8 +11,7 @@ type term
| Ind0 of term binder * term | Ind0 of term binder * term
| T1 | T1
| T1tr | T1tr (* Unit eta rule instead of elimination principle *)
| Ind1 of term binder * term * term
| TNat | TNat
| Zero | Zero

6
lib/Value.ml
View File

@ -2,7 +2,8 @@ module T = Term
type lvl = Lvl of int type lvl = Lvl of int
type closure = C of env * T.term type closure = C of env * T.term
and closure2 = C2 of env * T.term (* 2 variables missing *)
and env = value list and env = value list
@ -26,8 +27,7 @@ and value
and stuck and stuck
= Var of lvl = Var of lvl
| Ind0 of closure * stuck | Ind0 of closure * stuck
| Ind1 of closure * value * stuck | IndN of closure * value * closure2 * stuck
| IndN of closure * value * closure * stuck
| IndB of closure * value * value * stuck | IndB of closure * value * value * stuck
| App of stuck * value * value (* fn; val; type of fn *) | App of stuck * value * value (* fn; val; type of fn *)
| Fst of stuck | Fst of stuck