Skip to content
This repository
Browse code

Commit before getting rid of two levels of syntax

  • Loading branch information...
commit 3fd7142d3068926474931864ac4dbb5acde6ad72 1 parent 0c0b6af
Andrej Bauer authored

Showing 3 changed files with 39 additions and 29 deletions. Show diff stats Hide diff stats

  1. +17 0 ctx.ml
  2. +6 15 infer.ml
  3. +16 14 syntax.ml
17 ctx.ml
... ... @@ -0,0 +1,17 @@
  1 +(* Contexts *)
  2 +let lookup = List.assoc
  3 +
  4 +let index x ctx =
  5 + let rec index k = function
  6 + | [] -> raise Not_found
  7 + | y :: ys -> if x = y then k else index (k+1) ys
  8 + in
  9 + index 0 ctx
  10 +
  11 +let lookup_ty x ctx = fst (lookup x ctx)
  12 +
  13 +let lookup_value x ctx = snd (lookup x ctx)
  14 +
  15 +let extend x t ?value ctx = (x, (t, value)) :: ctx
  16 +
  17 +
21 infer.ml
... ... @@ -1,19 +1,10 @@
1 1 open Syntax
2 2
3   -(* Contexts *)
4   -let lookup x ctx = List.assoc x ctx
5   -
6   -let lookup_ty x ctx = fst (lookup x ctx)
7   -
8   -let lookup_value x ctx = snd (lookup x ctx)
9   -
10   -let extend x t ?value ctx = (x, (t, value)) :: ctx
11   -
12 3 (* Normalization. *)
13 4 let rec normalize ctx = function
14 5 | Var x ->
15 6 (match
16   - (try lookup_value x ctx
  7 + (try Ctx.lookup_value x ctx
17 8 with Not_found -> Error.runtime "unkown identifier %t" (Print.variable x))
18 9 with
19 10 | None -> Var x
@@ -30,7 +21,7 @@ let rec normalize ctx = function
30 21 and normalize_abstraction ctx (x, t, f) =
31 22 let t = normalize ctx t in
32 23 let x = Concrete.fresh_var x in
33   - let f v = normalize (extend x t ~value:v ctx) (f (Var x)) in
  24 + let f v = normalize (Ctx.extend x t ~value:v ctx) (f (Var x)) in
34 25 (x, t, f)
35 26
36 27 (* Equality of expressions. *)
@@ -46,25 +37,25 @@ let rec equal ctx e1 e2 =
46 37 and equal_abstraction ctx (x, t1, f1) (_, t2, f2) =
47 38 equal ctx t1 t2 &&
48 39 (let x = Concrete.fresh_var x in
49   - equal (extend x t1 ctx) (f1 (Var x)) (f2 (Var x)))
  40 + equal (Ctx.extend x t1 ctx) (f1 (Var x)) (f2 (Var x)))
50 41
51 42 (* Type inference. *)
52 43 let rec infer_type ctx = function
53 44 | Var x ->
54   - (try lookup_ty x ctx
  45 + (try Ctx.lookup_ty x ctx
55 46 with Not_found -> Error.typing "unkown identifier %t" (Print.variable x))
56 47 | Universe u -> Universe (u + 1)
57 48 | Pi (x, t1, t2) ->
58 49 let u1 = infer_universe ctx t1 in
59 50 let x = Concrete.fresh_var x in
60   - let ctx = extend x t1 ctx in
  51 + let ctx = Ctx.extend x t1 ctx in
61 52 let u2 = infer_universe ctx (t2 (Var x)) in
62 53 Universe (max u1 u2)
63 54 | Lambda (x, t, e) ->
64 55 let _ = infer_universe ctx t in
65 56 let x = Concrete.fresh_var x in
66 57 (* XXX: bug, infer_type does not get called immediately. *)
67   - let f v = infer_type (extend x t ~value:v ctx) (e (Var x)) in
  58 + let f v = infer_type (Ctx.extend x t ~value:v ctx) (e (Var x)) in
68 59 Pi (x, t, f)
69 60 | App (e1, e2) ->
70 61 let (t1, f1) = infer_pi ctx e1 in
30 syntax.ml
@@ -4,25 +4,27 @@ type universe = Concrete.universe
4 4
5 5 type expr =
6 6 | Var of variable
  7 + | Bound of int
7 8 | App of expr * expr
8 9 | Universe of universe
9 10 | Pi of abstraction
10 11 | Lambda of abstraction
11 12
12   -and abstraction = variable * expr * (expr -> expr)
13   -
14   -(* Compilation from concrete. *)
15   -let compile e =
16   - let rec compile env = function
17   - | Concrete.Var x -> (try List.assoc x env with Not_found -> Var x)
18   - | Concrete.Universe u -> Universe u
19   - | Concrete.Pi a -> Pi (compile_abstraction env a)
20   - | Concrete.Lambda a -> Lambda (compile_abstraction env a)
21   - | Concrete.App (e1, e2) -> App (compile env e1, compile env e2)
22   - and compile_abstraction env (x, t, e) =
23   - (x, compile env t, fun v -> compile ((x,v)::env) e)
24   - in
25   - compile [] e
  13 +and abstraction = variable * expr * expr
  14 +
  15 +(* Compilation from concrete syntax. *)
  16 +let compile ctx e =
  17 + let rec compile k
  18 +
  19 + function
  20 + | Concrete.Var x -> (try List.assoc x ctx with Not_found -> Var x)
  21 + | Concrete.Universe u -> Universe u
  22 + | Concrete.Pi a -> Pi (compile_abstraction env a)
  23 + | Concrete.Lambda a -> Lambda (compile_abstraction env a)
  24 + | Concrete.App (e1, e2) -> App (compile env e1, compile env e2)
  25 +
  26 +and compile_abstraction env (x, t, e) =
  27 + (x, compile env t, fun v -> compile ((x,v)::env) e)
26 28
27 29 (* Conversion back to concrete syntax, for pretty-printing. *)
28 30 let rec uncompile = function

0 comments on commit 3fd7142

Please sign in to comment.
Something went wrong with that request. Please try again.