Permalink
Browse files

Abstract syntax with variable names.

While de Bruijn indices are The Right Thing to implement,
we opt for "pedestrian" syntax with variable names and
substitutions. This is extremely inefficient, but is much
easier to understand, as it is closer to theory.
  • Loading branch information...
1 parent 3fd7142 commit 8a0ef44683a9ce03686b6f3b037f7879b764e365 @andrejbauer andrejbauer committed Nov 7, 2012
Showing with 69 additions and 162 deletions.
  1. +0 −83 concrete.ml
  2. +14 −21 infer.ml
  3. +2 −2 parser.mly
  4. +10 −11 print.ml
  5. +31 −29 syntax.ml
  6. +12 −16 tt.ml
View
@@ -1,83 +0,0 @@
-type variable =
- | String of string
- | Gensym of string * int
- | Dummy
-
-type universe = int
-
-type expr =
- | Var of variable
- | Universe of universe
- | Pi of abstraction
- | Lambda of abstraction
- | App of expr * expr
-
-and abstraction = variable * expr * expr
-
-type directive =
- | Quit
- | Help
- | Context
- | Parameter of variable * expr
- | Definition of variable * expr
- | Check of expr
- | Eval of expr
-
-let fresh_var =
- let k = ref 0 in
- function
- | String x | Gensym (x, _) -> (incr k ; Gensym (x, !k))
- | Dummy -> (incr k ; Gensym ("_", !k))
-
-let rec occurs x = function
- | Var y -> x = y
- | Universe _ -> false
- | Pi (y, e1, e2)
- | Lambda (y, e1, e2) -> occurs x e1 || (x <> y && occurs x e2)
- | App (e1, e2) -> occurs x e1 || occurs x e2
-
-(* This nasty function is used to rename bound variables before
- they are shown to the user. *)
-let beautify =
- (* Split a variable name into base and numerical postfix. *)
- let split s =
- let n = String.length s in
- let i = ref (n - 1) in
- while !i >= 0 && '0' <= s.[!i] && s.[!i] <= '9' do decr i done ;
- if !i < 0 || !i = n - 1
- then (s, None)
- else
- let k = int_of_string (String.sub s (!i+1) (n - !i - 1)) in
- (String.sub s 0 (!i+1), Some k)
- in
- let rec used x = function
- | [] -> false
- | (_, (String y | Gensym (y, _))) :: lst -> x = y || used x lst
- | (_, Dummy) :: lst -> used x lst
- in
- let find_available x sbst =
- let x = (match x with String x | Gensym (x, _) -> x | Dummy -> "_") in
- if not (used x sbst)
- then x
- else
- let (y, k) = split x in
- let k = ref (match k with Some k -> k | None -> 0) in
- while used (y ^ string_of_int !k) sbst do incr k done ;
- y ^ string_of_int !k
- in
- let rec beautify sbst = function
- | Var x -> (try Var (List.assoc x sbst) with Not_found -> Var x)
- | Universe k -> Universe k
- | Pi a -> Pi (beautify_abstraction sbst a)
- | Lambda a -> Lambda (beautify_abstraction sbst a)
- | App (e1, e2) -> App (beautify sbst e1, beautify sbst e2)
- and beautify_abstraction sbst (x, e1, e2) =
- let e1 = beautify sbst e1 in
- let y =
- if occurs x e2
- then String (find_available x sbst)
- else Dummy
- in
- (y, e1, beautify ((x,y) :: sbst) e2)
- in
- beautify []
View
@@ -5,24 +5,22 @@ 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 Not_found -> Error.runtime "shit, 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)
+ | Lambda (x, _, e1') -> normalize ctx (subst [(x,e2)] e1')
| 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) =
+and normalize_abstraction ctx (x, t, e) =
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)
+ (x, t, normalize (Ctx.extend x t ctx) e)
(* Equality of expressions. *)
let rec equal ctx e1 e2 =
@@ -34,10 +32,9 @@ let rec equal ctx e1 e2 =
| Lambda a1, Lambda a2 -> equal_abstraction ctx a1 a2
| (Var _ | App _ | Universe _ | Pi _ | Lambda _), _ -> false
-and equal_abstraction ctx (x, t1, f1) (_, t2, f2) =
+and equal_abstraction ctx (x, t1, e1) (y, t2, e2) =
equal ctx t1 t2 &&
- (let x = Concrete.fresh_var x in
- equal (Ctx.extend x t1 ctx) (f1 (Var x)) (f2 (Var x)))
+ (equal (Ctx.extend x t1 ctx) e1 (subst [(y, Var x)] e2))
(* Type inference. *)
let rec infer_type ctx = function
@@ -47,21 +44,17 @@ let rec infer_type ctx = function
| 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
+ let u2 = infer_universe (Ctx.extend x t1 ctx) t2 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)
+ let te = infer_type (Ctx.extend x t ctx) e in
+ Pi (x, t, te)
| 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
+ let (x, s, t) = infer_pi ctx e1 in
+ let te = infer_type ctx e2 in
+ check_equal ctx s te ;
+ subst [(x, e2)] t
and infer_universe ctx t =
let u = infer_type ctx t in
@@ -72,7 +65,7 @@ and infer_universe ctx t =
and infer_pi ctx e =
let t = infer_type ctx e in
match normalize ctx t with
- | Pi (_, t, f) -> (t, f)
+ | Pi a -> a
| Var _ | App _ | Universe _ | Lambda _ -> Error.typing "function expected"
and check_equal ctx t1 t2 =
View
@@ -1,5 +1,5 @@
%{
- open Concrete
+ open Syntax
%}
%token FORALL FUN TYPE
@@ -11,7 +11,7 @@
%token QUIT HELP PARAMETER CHECK EVAL CONTEXT DEFINITION
%token EOF
-%start <Concrete.directive list> directives
+%start <Syntax.directive list> directives
%%
View
@@ -14,23 +14,22 @@ let print ?(max_level=9999) ?(at_level=0) ppf =
let variable x ppf =
match x with
- | Concrete.Dummy -> print ppf "_"
- | Concrete.String x -> print ppf "%s" x
- | Concrete.Gensym (x, k) -> print ppf "%s_%d" x k
+ | Syntax.Dummy -> print ppf "_"
+ | Syntax.String x -> print ppf "%s" x
+ | Syntax.Gensym (x, k) -> print ppf "%s_%d" x k
let expr e ppf =
- let e = Syntax.uncompile e in
let rec expr ?max_level e ppf =
let print ?at_level = print ?max_level ?at_level ppf in
match e with
- | Concrete.Var x -> variable x ppf
- | Concrete.Universe k -> print "Type %d" k
- | Concrete.Pi (Concrete.Dummy, t1, t2) -> print ~at_level:3 "%t ->@;%t" (expr ~max_level:2 t1) (expr t2)
- | Concrete.Pi (x, t1, t2) -> print ~at_level:3 "forall %t : %t,@;%t" (variable x) (expr ~max_level:4 t1) (expr t2)
- | Concrete.Lambda (x, t, e) -> print ~at_level:3 "fun %t : %t =>@;%t" (variable x) (expr t) (expr e)
- | Concrete.App (e1, e2) -> print ~at_level:1 "%t %t" (expr ~max_level:1 e1) (expr ~max_level:0 e2)
+ | Syntax.Var x -> variable x ppf
+ | Syntax.Universe k -> print "Type %d" k
+ | Syntax.Pi (Syntax.Dummy, t1, t2) -> print ~at_level:3 "%t ->@;%t" (expr ~max_level:2 t1) (expr t2)
+ | Syntax.Pi (x, t1, t2) -> print ~at_level:3 "forall %t : %t,@;%t" (variable x) (expr ~max_level:4 t1) (expr t2)
+ | Syntax.Lambda (x, t, e) -> print ~at_level:3 "fun %t : %t =>@;%t" (variable x) (expr t) (expr e)
+ | Syntax.App (e1, e2) -> print ~at_level:1 "%t %t" (expr ~max_level:1 e1) (expr ~max_level:0 e2)
in
- expr (Concrete.beautify e) ppf
+ expr (Beautify.beautify e) ppf
let verbosity = ref 3
let message msg_type v =
View
@@ -1,39 +1,41 @@
-type variable = Concrete.variable
+type variable =
+ | String of string
+ | Gensym of string * int
+ | Dummy
-type universe = Concrete.universe
+type universe = int
type expr =
| Var of variable
- | Bound of int
- | App of expr * expr
| Universe of universe
| Pi of abstraction
| Lambda of abstraction
+ | App of expr * expr
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
- | Var x -> Concrete.Var x
- | App (e1, e2) -> Concrete.App (uncompile e1, uncompile e2)
- | Universe u -> Concrete.Universe u
- | Pi a -> Concrete.Pi (uncompile_vabstraction a)
- | Lambda a -> Concrete.Lambda (uncompile_vabstraction a)
-
-and uncompile_vabstraction (x, t, f) =
- let x = Concrete.fresh_var x in
- (x, uncompile t, uncompile (f (Var x)))
+type directive =
+ | Quit
+ | Help
+ | Context
+ | Parameter of variable * expr
+ | Definition of variable * expr
+ | Check of expr
+ | Eval of expr
+
+let refresh =
+ let k = ref 0 in
+ function
+ | String x | Gensym (x, _) -> (incr k ; Gensym (x, !k))
+ | Dummy -> (incr k ; Gensym ("_", !k))
+
+let rec subst s = function
+ | Var x -> (try List.assoc x s with Not_found -> Var x)
+ | Universe k -> Universe k
+ | Pi a -> Pi (subst_abstraction s a)
+ | Lambda a -> Lambda (subst_abstraction s a)
+ | App (e1, e2) -> App (subst s e1, subst s e2)
+
+and subst_abstraction s (x, t, e) =
+ let x' = refresh x in
+ (x', subst s t, subst ((x, Var x') :: s) e)
View
@@ -60,43 +60,39 @@ let initial_ctx = []
and return the new environment. *)
let rec exec_cmd interactive ctx e =
match e with
- | Concrete.Eval e ->
- let e = Syntax.compile e in
+ | Syntax.Eval e ->
let t = Infer.infer_type ctx e in
let e = Infer.normalize ctx e in
if interactive then Format.printf " = @[%t@]@\n : @[%t@]@."
(Print.expr e)
(Print.expr t) ;
ctx
- | Concrete.Context ->
+ | Syntax.Context ->
List.iter
(function
| (x, (t, None)) -> Format.printf "@[%t : @[%t@]@]@." (Print.variable x) (Print.expr t)
| (x, (t, Some e)) -> Format.printf "@[%t = %t@]@\n : @[%t@]@."
(Print.variable x) (Print.expr e) (Print.expr t))
ctx ;
ctx
- | Concrete.Parameter (x, t) ->
- let t = Syntax.compile t in
- ignore (Infer.infer_universe ctx t) ;
- if interactive then
- Format.printf "@[%t is assumed@]@." (Print.variable x) ;
- Infer.extend x t ctx
- | Concrete.Definition (x, e) ->
+ | Syntax.Parameter (x, t) ->
+ ignore (Infer.infer_universe ctx t) ;
+ if interactive then
+ Format.printf "@[%t is assumed@]@." (Print.variable x) ;
+ Ctx.extend x t ctx
+ | Syntax.Definition (x, e) ->
if List.mem_assoc x ctx then Error.typing "%t already exists" (Print.variable x) ;
- let e = Syntax.compile e in
let t = Infer.infer_type ctx e in
if interactive then
Format.printf "@[%t is defined@]@." (Print.variable x) ;
- Infer.extend x t ~value:e ctx
- | Concrete.Check e ->
- let e = Syntax.compile e in
+ Ctx.extend x t ~value:e ctx
+ | Syntax.Check e ->
let t = Infer.infer_type ctx e in
Format.printf "@[%t@]@\n : @[%t@]@." (Print.expr e) (Print.expr t) ;
ctx
- | Concrete.Help ->
+ | Syntax.Help ->
print_endline help_text ; ctx
- | Concrete.Quit -> exit 0
+ | Syntax.Quit -> exit 0
and use_file ctx (filename, interactive) =
let cmds = Lexer.read_file (parse Parser.directives) filename in

0 comments on commit 8a0ef44

Please sign in to comment.