Permalink
Browse files

Commit before getting rid of two levels of syntax

  • Loading branch information...
1 parent 0c0b6af commit 3fd7142d3068926474931864ac4dbb5acde6ad72 @andrejbauer andrejbauer committed Nov 7, 2012
Showing with 39 additions and 29 deletions.
  1. +17 −0 ctx.ml
  2. +6 −15 infer.ml
  3. +16 −14 syntax.ml
View
17 ctx.ml
@@ -0,0 +1,17 @@
+(* Contexts *)
+let lookup = List.assoc
+
+let index x ctx =
+ let rec index k = function
+ | [] -> raise Not_found
+ | y :: ys -> if x = y then k else index (k+1) ys
+ in
+ index 0 ctx
+
+let lookup_ty x ctx = fst (lookup x ctx)
+
+let lookup_value x ctx = snd (lookup x ctx)
+
+let extend x t ?value ctx = (x, (t, value)) :: ctx
+
+
View
21 infer.ml
@@ -1,19 +1,10 @@
open Syntax
-(* Contexts *)
-let lookup x ctx = List.assoc x ctx
-
-let lookup_ty x ctx = fst (lookup x ctx)
-
-let lookup_value x ctx = snd (lookup x ctx)
-
-let extend x t ?value ctx = (x, (t, value)) :: ctx
-
(* Normalization. *)
let rec normalize ctx = function
| Var x ->
(match
- (try lookup_value x ctx
+ (try Ctx.lookup_value x ctx
with Not_found -> Error.runtime "unkown identifier %t" (Print.variable x))
with
| None -> Var x
@@ -30,7 +21,7 @@ let rec normalize ctx = function
and normalize_abstraction ctx (x, t, f) =
let t = normalize ctx t in
let x = Concrete.fresh_var x in
- let f v = normalize (extend x t ~value:v ctx) (f (Var x)) in
+ let f v = normalize (Ctx.extend x t ~value:v ctx) (f (Var x)) in
(x, t, f)
(* Equality of expressions. *)
@@ -46,25 +37,25 @@ let rec equal ctx e1 e2 =
and equal_abstraction ctx (x, t1, f1) (_, t2, f2) =
equal ctx t1 t2 &&
(let x = Concrete.fresh_var x in
- equal (extend x t1 ctx) (f1 (Var x)) (f2 (Var x)))
+ equal (Ctx.extend x t1 ctx) (f1 (Var x)) (f2 (Var x)))
(* Type inference. *)
let rec infer_type ctx = function
| Var x ->
- (try lookup_ty x ctx
+ (try Ctx.lookup_ty x ctx
with Not_found -> Error.typing "unkown identifier %t" (Print.variable x))
| Universe u -> Universe (u + 1)
| Pi (x, t1, t2) ->
let u1 = infer_universe ctx t1 in
let x = Concrete.fresh_var x in
- let ctx = extend x t1 ctx in
+ let ctx = Ctx.extend x t1 ctx in
let u2 = infer_universe ctx (t2 (Var x)) in
Universe (max u1 u2)
| Lambda (x, t, e) ->
let _ = infer_universe ctx t in
let x = Concrete.fresh_var x in
(* XXX: bug, infer_type does not get called immediately. *)
- let f v = infer_type (extend x t ~value:v ctx) (e (Var x)) in
+ let f v = infer_type (Ctx.extend x t ~value:v ctx) (e (Var x)) in
Pi (x, t, f)
| App (e1, e2) ->
let (t1, f1) = infer_pi ctx e1 in
View
30 syntax.ml
@@ -4,25 +4,27 @@ type universe = Concrete.universe
type expr =
| Var of variable
+ | Bound of int
| App of expr * expr
| Universe of universe
| Pi of abstraction
| Lambda of abstraction
-and abstraction = variable * expr * (expr -> expr)
-
-(* Compilation from concrete. *)
-let compile e =
- let rec compile env = function
- | Concrete.Var x -> (try List.assoc x env with Not_found -> Var x)
- | Concrete.Universe u -> Universe u
- | Concrete.Pi a -> Pi (compile_abstraction env a)
- | Concrete.Lambda a -> Lambda (compile_abstraction env a)
- | Concrete.App (e1, e2) -> App (compile env e1, compile env e2)
- and compile_abstraction env (x, t, e) =
- (x, compile env t, fun v -> compile ((x,v)::env) e)
- in
- compile [] e
+and abstraction = variable * expr * expr
+
+(* Compilation from concrete syntax. *)
+let compile ctx e =
+ let rec compile k
+
+ function
+ | Concrete.Var x -> (try List.assoc x ctx with Not_found -> Var x)
+ | Concrete.Universe u -> Universe u
+ | Concrete.Pi a -> Pi (compile_abstraction env a)
+ | Concrete.Lambda a -> Lambda (compile_abstraction env a)
+ | Concrete.App (e1, e2) -> App (compile env e1, compile env e2)
+
+and compile_abstraction env (x, t, e) =
+ (x, compile env t, fun v -> compile ((x,v)::env) e)
(* Conversion back to concrete syntax, for pretty-printing. *)
let rec uncompile = function

0 comments on commit 3fd7142

Please sign in to comment.