From 354705afe535622865731369d7f80703d8dbd41f Mon Sep 17 00:00:00 2001 From: depsterr Date: Tue, 30 Aug 2022 16:12:47 +0200 Subject: [PATCH] did work on evaluation --- lib/Eval.ml | 84 +++++++++++++++++++++++++++++++++------------------- lib/Term.ml | 3 +- lib/Value.ml | 6 ++-- 3 files changed, 58 insertions(+), 35 deletions(-) diff --git a/lib/Eval.ml b/lib/Eval.ml index 4a12c29..99ca9a3 100644 --- a/lib/Eval.ml +++ b/lib/Eval.ml @@ -1,34 +1,58 @@ 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 index (env : V.env) (i : int) = + 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" +let rec eval (env : V.env) (tr : T.term) = + match tr with + | Var (Ix i) -> index env i + | Type -> V.Type + | T0 -> V.T0 + | Ind0 (B b, t) -> begin + match eval env t with + | Stuck (s , T0) -> V.Stuck (V.Ind0 (V.C (env, b), s), V.T0) + | _ -> failwith "eval Ind0 impossible error" + end + | T1 -> V.T1 + | T1tr -> V.T1vl + | TNat -> V.TNat + | Zero -> V.Zero + | Suc n -> V.Suc (eval env n) + | IndN (B b, tz, B B ts, n) -> indN env b (eval env tz) ts (eval env n) + | TBool -> V.TBool + | True -> V.True + | False -> V.False + | IndB (B b, t, f, bo) -> begin + match eval env bo with + | True -> eval env t + | False -> eval env f + | Stuck (s, TBool) -> V.Stuck (V.IndB (V.C (env, b), eval env t, eval env f, s), V.TBool) + | _ -> 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" diff --git a/lib/Term.ml b/lib/Term.ml index 27f0789..b509b6c 100644 --- a/lib/Term.ml +++ b/lib/Term.ml @@ -11,8 +11,7 @@ type term | Ind0 of term binder * term | T1 - | T1tr - | Ind1 of term binder * term * term + | T1tr (* Unit eta rule instead of elimination principle *) | TNat | Zero diff --git a/lib/Value.ml b/lib/Value.ml index b808561..07e3958 100644 --- a/lib/Value.ml +++ b/lib/Value.ml @@ -2,7 +2,8 @@ module T = Term 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 @@ -26,8 +27,7 @@ and value and stuck = Var of lvl | Ind0 of closure * stuck - | Ind1 of closure * value * stuck - | IndN of closure * value * closure * stuck + | IndN of closure * value * closure2 * stuck | IndB of closure * value * value * stuck | App of stuck * value * value (* fn; val; type of fn *) | Fst of stuck