Permalink
Browse files

Minor changes to match with the blog post

  • Loading branch information...
1 parent abab9f1 commit dcd1ac55b2d0a8711e7e34be2375e37bc1c1d05f @andrejbauer andrejbauer committed Nov 8, 2012
Showing with 20 additions and 23 deletions.
  1. +1 −1 README.markdown
  2. +6 −7 ctx.ml
  3. +11 −10 infer.ml
  4. +2 −5 syntax.ml
View
@@ -15,7 +15,7 @@ The hierarchy of universes is not commulative, i.e., even though `Type k` has ty
## Compilation
-You need `ocamlbuild` and `make`. You can type
+You need `ocamlbuild`, which is part of OCaml, `menhir`, and `make`. You can type
* `make` to make the `tt.native` executable.
* `make clean` to clean up.
View
13 ctx.ml
@@ -1,17 +1,16 @@
-(** Handling of contexts.
+(** Handling of contexts. *)
- A context is represented as an associative list which maps a variable [x]
- to a pair [(t,e)] where [t] is its type and [e] is its value (optional).
+(** A context is represented as an associative list which maps a variable [x] to a pair
+ [(t,e)] where [t] is its type and [e] is its value (optional).
*)
-
-let lookup = List.assoc
+type context = (Syntax.variable * (Syntax.expr * Syntax.expr option)) list
(** [lookup_ty x ctx] returns the type of [x] in context [ctx]. *)
-let lookup_ty x ctx = fst (lookup x ctx)
+let lookup_ty x ctx = fst (List.assoc x ctx)
(** [lookup_ty x ctx] returns the value of [x] in context [ctx], or [None]
if [x] has no assigned value. *)
-let lookup_value x ctx = snd (lookup x ctx)
+let lookup_value x ctx = snd (List.assoc x ctx)
(** [extend x t ctx] returns [ctx] extended with variable [x] of type [t],
whereas [extend x t ~value:e ctx] returns [ctx] extended with variable [x]
View
@@ -1,13 +1,14 @@
(** Type inference and normalization. *)
open Syntax
+open Ctx
(** [normalize ctx e] normalizes the given expression [e] in context [ctx]. It removes
all redexes and it unfolds all definitions. It performs normalization under binders. *)
let rec normalize ctx = function
| Var x ->
(match
- (try Ctx.lookup_value x ctx
+ (try lookup_value x ctx
with Not_found -> Error.runtime "unkown identifier %t" (Print.variable x))
with
| None -> Var x
@@ -23,7 +24,7 @@ let rec normalize ctx = function
and normalize_abstraction ctx (x, t, e) =
let t = normalize ctx t in
- (x, t, normalize (Ctx.extend x t ctx) e)
+ (x, t, normalize (extend x t ctx) e)
(** [equal ctx e1 e2] determines whether normalized [e1] and [e2] are equal up to renaming
of bound variables. *)
@@ -32,7 +33,7 @@ let equal ctx e1 e2 =
match e1, e2 with
| Var x1, Var x2 -> x1 = x2
| App (e11, e12), App (e21, e22) -> equal e11 e21 && equal e12 e22
- | Universe u1, Universe u2 -> u1 = u2
+ | Universe k1, Universe k2 -> k1 = k2
| Pi a1, Pi a2 -> equal_abstraction a1 a2
| Lambda a1, Lambda a2 -> equal_abstraction a1 a2
| (Var _ | App _ | Universe _ | Pi _ | Lambda _), _ -> false
@@ -44,16 +45,16 @@ let equal ctx e1 e2 =
(** [infer_type ctx e] infers the type of expression [e] in context [ctx]. *)
let rec infer_type ctx = function
| Var x ->
- (try Ctx.lookup_ty x ctx
+ (try lookup_ty x ctx
with Not_found -> Error.typing "unkown identifier %t" (Print.variable x))
- | Universe u -> Universe (u + 1)
+ | Universe k -> Universe (k + 1)
| Pi (x, t1, t2) ->
- let u1 = infer_universe ctx t1 in
- let u2 = infer_universe (Ctx.extend x t1 ctx) t2 in
- Universe (max u1 u2)
+ let k1 = infer_universe ctx t1 in
+ let k2 = infer_universe (extend x t1 ctx) t2 in
+ Universe (max k1 k2)
| Lambda (x, t, e) ->
let _ = infer_universe ctx t in
- let te = infer_type (Ctx.extend x t ctx) e in
+ let te = infer_type (extend x t ctx) e in
Pi (x, t, te)
| App (e1, e2) ->
let (x, s, t) = infer_pi ctx e1 in
@@ -65,7 +66,7 @@ let rec infer_type ctx = function
and infer_universe ctx t =
let u = infer_type ctx t in
match normalize ctx u with
- | Universe u -> u
+ | Universe k -> k
| App _ | Var _ | Pi _ | Lambda _ -> Error.typing "type expected"
(** [infer_pi ctx e] infers the type of [e] in context [ctx], verifies that it is
View
@@ -11,17 +11,14 @@ type variable =
| Gensym of string * int
| Dummy
-(** Universes are indexed by numerals. *)
-type universe = int
-
(** Abstract syntax of expressions. *)
type expr =
| Var of variable
- | Universe of universe
+ | Universe of int
| Pi of abstraction
| Lambda of abstraction
| App of expr * expr
-
+
(** An abstraction [(x,t,e)] indicates that [x] of type [t] is bound in [e]. *)
and abstraction = variable * expr * expr

0 comments on commit dcd1ac5

Please sign in to comment.