Permalink
Browse files

Separated values and evaluation from inference

  • Loading branch information...
1 parent 167af4b commit 388b323fe070ea6146544df671d03a1a9f223dcd @andrejbauer andrejbauer committed Nov 5, 2012
Showing with 104 additions and 103 deletions.
  1. +2 −0 common.ml
  2. +0 −94 eval.ml
  3. +43 −0 infer.ml
  4. +2 −2 tt.ml
  5. +57 −7 value.ml
View
@@ -2,3 +2,5 @@ let lookup x lst =
try
Some (List.assoc x lst)
with Not_found -> None
+
+let extend x y lst = (x,y) :: lst
View
94 eval.ml
@@ -1,94 +0,0 @@
-open Syntax
-open Value
-
-let disable_typing = ref false
-
-let lookup_var x ctx =
- match Common.lookup x ctx with
- | Some y -> y
- | None -> Error.typing "unkown identifier %t" (Print.variable x)
-
-let extend x y lst = (x,y) :: lst
-
-let rec eval env = function
- | Var x ->
- (match Common.lookup x env with
- | Some v -> v
- | None -> VNeutral (VVar x))
- | Universe u -> VUniverse u
- | Pi a -> VPi (eval_abstraction env a)
- | Lambda a -> VLambda (eval_abstraction env a)
- | App (e1, e2) ->
- let v2 = eval env e2 in
- (match eval env e1 with
- | VLambda (_, _, f) -> f v2
- | VNeutral n -> VNeutral (VApp (n, v2))
- | _ -> Error.runtime "function expected")
-
-and eval_abstraction env (x, t, e) =
- (eval env t, x, fun v -> eval (extend x v env) e)
-
-let rec uneval = function
- | VNeutral n -> uneval_neutral n
- | VUniverse u -> Universe u
- | VPi a -> Pi (uneval_vabstraction a)
- | VLambda a -> Lambda (uneval_vabstraction a)
-
-and uneval_neutral = function
- | VVar x -> Var x
- | VApp (n, v) -> App (uneval_neutral n, uneval v)
-
-and uneval_vabstraction (t, x, f) =
- let x = fresh_var x in
- (x, uneval t, uneval (f (VNeutral (VVar x))))
-
-let rec equal_value v1 v2 =
- match v1, v2 with
- | VNeutral n1, VNeutral n2 -> equal_neutral n1 n2
- | VUniverse u1, VUniverse u2 -> u1 = u2
- | VPi a1, VPi a2 -> equal_vabstraction a1 a2
- | VLambda a1, VLambda a2 -> equal_vabstraction a1 a2
- | (VNeutral _ | VUniverse _ | VPi _ | VLambda _), _ -> false
-
-and equal_vabstraction (v1, x, f1) (v2, _, f2) =
- v1 = v2 && (let x = VNeutral (VVar (fresh_var x)) in equal_value (f1 x) (f2 x))
-
-and equal_neutral n1 n2 =
- match n1, n2 with
- | VVar x, VVar y -> x = y
- | VApp (m1, v1), VApp (m2, v2) -> equal_neutral m1 m2 && equal_value v1 v2
- | (VVar _ | VApp _), _ -> false
-
-let rec infer_type ctx = function
- | Var x -> lookup_var x ctx
- | Universe u -> Universe (u + 1)
- | Pi (x, t1, t2) ->
- let u1 = infer_universe ctx t1 in
- let u2 = infer_universe (extend x t1 ctx) t2 in
- Universe (max u1 u2)
- | Lambda (x, t, e) ->
- check_type ctx t ;
- let s = infer_type (extend x t ctx) e in
- Pi (x, t, s)
- | App (e1, e2) ->
- let (t, f) = infer_pi ctx e1 in
- let r = infer_type ctx e2 in
- check_equal t r ;
- f e2
-
-and infer_universe ctx t =
- let u = infer_type ctx t in
- match eval [] u with
- | VUniverse u -> u
- | VNeutral _ | VPi _ | VLambda _ -> Error.typing "type expected"
-
-and check_type ctx t = ignore (infer_universe ctx t)
-
-and infer_pi ctx e =
- let t = infer_type ctx e in
- match eval [] t with
- | VPi (t, _, f) -> (uneval t, fun e -> uneval (f (eval [] e)))
- | VUniverse _ | VNeutral _ | VLambda _ -> Error.typing "function expected"
-
-and check_equal t1 t2 =
- if not (equal_value (eval [] t1) (eval [] t2)) then Error.typing "type mismatch"
View
@@ -0,0 +1,43 @@
+open Syntax
+
+let disable_typing = ref false
+
+let lookup_var x ctx =
+ match Common.lookup x ctx with
+ | Some y -> y
+ | None -> Error.typing "unkown identifier %t" (Print.variable x)
+
+let rec infer_type ctx = function
+ | Var x -> lookup_var x ctx
+ | Universe u -> Universe (u + 1)
+ | Pi (x, t1, t2) ->
+ let u1 = infer_universe ctx t1 in
+ let u2 = infer_universe (Common.extend x t1 ctx) t2 in
+ Universe (max u1 u2)
+ | Lambda (x, t, e) ->
+ check_type ctx t ;
+ let s = infer_type (Common.extend x t ctx) e in
+ Pi (x, t, s)
+ | App (e1, e2) ->
+ let (t, f) = infer_pi ctx e1 in
+ let r = infer_type ctx e2 in
+ check_equal t r ;
+ f e2
+
+and infer_universe ctx t =
+ let u = infer_type ctx t in
+ match Value.eval [] u with
+ | Value.Universe u -> u
+ | Value.Neutral _ | Value.Pi _ | Value.Lambda _ -> Error.typing "type expected"
+
+and check_type ctx t = ignore (infer_universe ctx t)
+
+and infer_pi ctx e =
+ let t = infer_type ctx e in
+ match Value.eval [] t with
+ | Value.Pi (t, _, f) -> (Value.uneval t, fun e -> Value.uneval (f (Value.eval [] e)))
+ | Value.Universe _ | Value.Neutral _ | Value.Lambda _ -> Error.typing "function expected"
+
+and check_equal t1 t2 =
+ if not (Value.equal_value (Value.eval [] t1) (Value.eval [] t2))
+ then Error.typing "type mismatch"
View
4 tt.ml
@@ -63,8 +63,8 @@ let rec exec_cmd interactive ctx e =
match e with
| Syntax.Eval e ->
let t = Infer.infer_type ctx e in
- let v = Infer.eval [] e in
- let e' = Infer.uneval v in
+ let v = Value.eval [] e in
+ let e' = Value.uneval v in
if interactive then Format.printf " = @[%t@]@\n : @[%t@]@."
(Print.expr e')
(Print.expr t) ;
View
@@ -3,13 +3,63 @@ type variable = Syntax.variable
type universe = int
type value =
- | VNeutral of neutral
- | VUniverse of universe
- | VPi of vabstraction
- | VLambda of vabstraction
+ | Neutral of neutral
+ | Universe of universe
+ | Pi of abstraction
+ | Lambda of abstraction
and neutral =
- | VVar of variable
- | VApp of neutral * value
+ | Var of variable
+ | App of neutral * value
+
+and abstraction = value * variable * (value -> value)
+
+let rec eval env = function
+ | Syntax.Var x ->
+ (match Common.lookup x env with
+ | Some v -> v
+ | None -> Neutral (Var x))
+ | Syntax.Universe u -> Universe u
+ | Syntax.Pi a -> Pi (eval_abstraction env a)
+ | Syntax.Lambda a -> Lambda (eval_abstraction env a)
+ | Syntax.App (e1, e2) ->
+ let v2 = eval env e2 in
+ (match eval env e1 with
+ | Lambda (_, _, f) -> f v2
+ | Neutral n -> Neutral (App (n, v2))
+ | _ -> Error.runtime "function expected")
+
+and eval_abstraction env (x, t, e) =
+ (eval env t, x, fun v -> eval (Common.extend x v env) e)
+
+let rec equal_value v1 v2 =
+ match v1, v2 with
+ | Neutral n1, Neutral n2 -> equal_neutral n1 n2
+ | Universe u1, Universe u2 -> u1 = u2
+ | Pi a1, Pi a2 -> equal_abstraction a1 a2
+ | Lambda a1, Lambda a2 -> equal_abstraction a1 a2
+ | (Neutral _ | Universe _ | Pi _ | Lambda _), _ -> false
+
+and equal_abstraction (v1, x, f1) (v2, _, f2) =
+ v1 = v2 && (let x = Neutral (Var (Syntax.fresh_var x)) in equal_value (f1 x) (f2 x))
+
+and equal_neutral n1 n2 =
+ match n1, n2 with
+ | Var x, Var y -> x = y
+ | App (m1, v1), App (m2, v2) -> equal_neutral m1 m2 && equal_value v1 v2
+ | (Var _ | App _), _ -> false
+
+let rec uneval = function
+ | Neutral n -> uneval_neutral n
+ | Universe u -> Syntax.Universe u
+ | Pi a -> Syntax.Pi (uneval_vabstraction a)
+ | Lambda a -> Syntax.Lambda (uneval_vabstraction a)
+
+and uneval_neutral = function
+ | Var x -> Syntax.Var x
+ | App (n, v) -> Syntax.App (uneval_neutral n, uneval v)
+
+and uneval_vabstraction (t, x, f) =
+ let x = Syntax.fresh_var x in
+ (x, uneval t, uneval (f (Neutral (Var x))))
-and vabstraction = value * variable * (value -> value)

0 comments on commit 388b323

Please sign in to comment.