Skip to content
This repository

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
tree: 3fd7142d30
Fetching contributors…

Octocat-spinner-32-eaf2f5

Cannot retrieve contributors at this time

file 81 lines (72 sloc) 2.695 kb
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80
open Syntax

(* Normalization. *)
let rec normalize ctx = function
  | Var x ->
    (match
        (try Ctx.lookup_value x ctx
         with Not_found -> Error.runtime "unkown identifier %t" (Print.variable x))
     with
       | None -> Var x
       | Some e -> normalize ctx e)
  | App (e1, e2) ->
    let e2 = normalize ctx e2 in
      (match normalize ctx e1 with
        | Lambda (_, _, f) -> normalize ctx (f e2)
        | e1 -> App (e1, e2))
  | Universe k -> Universe k
  | Pi a -> Pi (normalize_abstraction ctx a)
  | Lambda a -> Lambda (normalize_abstraction ctx a)

and normalize_abstraction ctx (x, t, f) =
  let t = normalize ctx t in
  let x = Concrete.fresh_var x in
  let f v = normalize (Ctx.extend x t ~value:v ctx) (f (Var x)) in
    (x, t, f)

(* Equality of expressions. *)
let rec equal ctx e1 e2 =
  match normalize ctx e1, normalize ctx e2 with
    | Var x1, Var x2 -> x1 = x2
    | App (e11, e12), App (e21, e22) -> equal ctx e11 e21 && equal ctx e12 e22
    | Universe u1, Universe u2 -> u1 = u2
    | Pi a1, Pi a2 -> equal_abstraction ctx a1 a2
    | Lambda a1, Lambda a2 -> equal_abstraction ctx a1 a2
    | (Var _ | App _ | Universe _ | Pi _ | Lambda _), _ -> false

and equal_abstraction ctx (x, t1, f1) (_, t2, f2) =
  equal ctx t1 t2 &&
  (let x = Concrete.fresh_var x in
     equal (Ctx.extend x t1 ctx) (f1 (Var x)) (f2 (Var x)))

(* Type inference. *)
let rec infer_type ctx = function
  | Var x ->
    (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 = 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 (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
    let t2 = infer_type ctx e2 in
      check_equal ctx t1 t2 ;
      f1 e2

and infer_universe ctx t =
  let u = infer_type ctx t in
    match normalize ctx u with
      | Universe u -> u
      | App _ | Var _ | Pi _ | Lambda _ -> Error.typing "type expected"

and infer_pi ctx e =
  let t = infer_type ctx e in
    match normalize ctx t with
      | Pi (_, t, f) -> (t, f)
      | Var _ | App _ | Universe _ | Lambda _ -> Error.typing "function expected"

and check_equal ctx t1 t2 =
  if not (equal ctx t1 t2)
  then Error.typing "expressions %t and %t are not equal" (Print.expr t1) (Print.expr t2)
Something went wrong with that request. Please try again.