Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Must go, but hunting down a bug in normalization

  • Loading branch information...
commit 4eb5bb5a17b367fc2a25b5efd10c78b87b88159d 1 parent 1703400
@andrejbauer authored
View
3  Makefile
@@ -1,2 +1,5 @@
all:
ocamlbuild -lib unix -use-menhir tt.native
+
+clean:
+ ocamlbuild -clean
View
6 README.markdown
@@ -33,9 +33,9 @@ session:
The purpose of the implementation is to keep the source uncomplicated and short. The
essential bits of source code can be found in the following files:
-* `syntax.ml` the abstract syntax of the type system
-* `value.ml` auxiliary datatype used during normalization
-* `eval.ml` type checking and normalization
+* `concrete.ml` the abstract syntax
+* `syntax.ml` compiled form of abstract syntax, where abstractions are Ocaml functions, normalization
+* `infer.ml` type checking
The rest of the files are just logistics:
View
6 common.ml
@@ -1,6 +0,0 @@
-let lookup x lst =
- try
- Some (List.assoc x lst)
- with Not_found -> None
-
-let extend x y lst = (x,y) :: lst
View
5 concrete.ml
@@ -65,10 +65,7 @@ let beautify =
y ^ string_of_int !k
in
let rec beautify sbst = function
- | Var x ->
- (match Common.lookup x sbst with
- | Some y -> Var y
- | None -> Var x)
+ | 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)
View
0  ctx.ml
No changes.
View
2  error.ml
@@ -12,5 +12,5 @@ let error err_type =
let fatal msg = error "Fatal error" msg
let syntax msg = error "Syntax error" msg
let typing msg = error "Typing error" msg
-let runtime msg = error "Runtime error" msg
+let runtime msg = error "Normalization error" msg
let exc msg = error "Exception" msg
View
87 infer.ml
@@ -1,41 +1,88 @@
open Syntax
-let lookup_var x ctx =
- match Common.lookup x ctx with
- | Some y -> y
- | None -> Error.typing "unkown identifier %t" (Print.variable x)
+(* 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 lst = (x, (t, value)) :: lst
+
+(* Normalization. *)
+let rec normalize ctx = function
+ | Var x ->
+ (match
+ (try 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 (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 (extend x t1 ctx) (f1 (Var x)) (f2 (Var x)))
+
+(* Type inference. *)
let rec infer_type ctx = function
- | Var x -> lookup_var x ctx
+ | Var x ->
+ (try 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 u2 = infer_universe (Common.extend x t1 ctx) t2 in
+ let x = Concrete.fresh_var x in
+ let ctx = extend x t1 ctx in
+ let u2 = infer_universe ctx (t2 (Var x)) in
Universe (max u1 u2)
| Lambda (x, t, e) ->
- check_type ctx t ;
- let s = infer_type (Common.extend x t ctx) e in
- Pi (x, t, s)
+ let _ = infer_universe ctx t in
+ let x = Concrete.fresh_var x in
+ let f v = infer_type (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 t1 t2 ;
+ check_equal ctx t1 t2 ;
f1 e2
and infer_universe ctx t =
let u = infer_type ctx t in
- match Value.eval [] u with
- | Value.Universe u -> u
- | Value.Neutral _ | Value.Pi _ | Value.Lambda _ -> Error.typing "type expected"
-
-and check_type ctx t = ignore (infer_universe ctx t)
+ 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 Value.eval [] t with
- | Value.Pi (t, _, f) -> (Value.uneval t, fun e -> Value.uneval (f (Value.eval [] e)))
- | Value.Universe _ | Value.Neutral _ | Value.Lambda _ -> Error.typing "function expected"
+ match normalize ctx t with
+ | Pi (_, t, f) -> (t, f)
+ | Var _ | App _ | Universe _ | Lambda _ -> Error.typing "function expected"
-and check_equal t1 t2 =
- if not (Value.equal_value (Value.eval [] t1) (Value.eval [] t2))
+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)
View
12 lexer.mll
@@ -27,12 +27,12 @@ rule token = parse
| [' ' '\r' '\t'] { token lexbuf }
| numeral { NUMERAL (int_of_string (Lexing.lexeme lexbuf)) }
| name { let s = Lexing.lexeme lexbuf in
- match Common.lookup s reserved with
- | Some r -> r
- | None ->
- (match Common.lookup s directives with
- | Some d -> d
- | None -> NAME s)
+ try
+ List.assoc s reserved
+ with Not_found ->
+ (try
+ List.assoc s directives
+ with Not_found -> NAME s)
}
| '(' { LPAREN }
| ')' { RPAREN }
View
4 parser.mly
@@ -1,5 +1,5 @@
%{
- open Syntax
+ open Concrete
%}
%token FORALL FUN TYPE
@@ -11,7 +11,7 @@
%token QUIT HELP PARAMETER CHECK EVAL CONTEXT
%token EOF
-%start <Syntax.directive list> directives
+%start <Concrete.directive list> directives
%%
View
23 print.ml
@@ -14,22 +14,23 @@ let print ?(max_level=9999) ?(at_level=0) ppf =
let variable x ppf =
match x with
- | Syntax.Dummy -> print ppf "_"
- | Syntax.String x -> print ppf "%s" x
- | Syntax.Gensym (x, k) -> print ppf "%s_%d" x k
+ | Concrete.Dummy -> print ppf "_"
+ | Concrete.String x -> print ppf "%s" x
+ | Concrete.Gensym (x, k) -> print ppf "%s_%d" x k
-let rec expr e ppf =
+let expr e ppf =
+ let e = Syntax.uneval e in
let rec expr ?max_level e ppf =
let print ?at_level = print ?max_level ?at_level ppf in
match e with
- | 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)
+ | 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)
in
- expr (Syntax.beautify e) ppf
+ expr (Concrete.beautify e) ppf
let verbosity = ref 3
let message msg_type v =
View
86 syntax.ml
@@ -1,65 +1,37 @@
-type variable = Syntax.variable
+type variable = Concrete.variable
-type universe = Syntax.universe
+type universe = Concrete.universe
type value =
- | Neutral of neutral
+ | Var of variable
+ | App of value * value
| Universe of universe
| Pi of abstraction
| Lambda of abstraction
-and neutral =
- | Var of variable
- | App of neutral * value
-
-and abstraction = value * variable * (value -> value)
-
-let rec eval env = function
- | Syntax.Var x ->
- (match Common.lookup x env with
- | Some v -> v
- | None -> Neutral (Var x))
- | Syntax.Universe u -> Universe u
- | Syntax.Pi a -> Pi (eval_abstraction env a)
- | Syntax.Lambda a -> Lambda (eval_abstraction env a)
- | Syntax.App (e1, e2) ->
- let v2 = eval env e2 in
- (match eval env e1 with
- | Lambda (_, _, f) -> f v2
- | Neutral n -> Neutral (App (n, v2))
- | _ -> Error.runtime "function expected")
-
-and eval_abstraction env (x, t, e) =
- (eval env t, x, fun v -> eval (Common.extend x v env) e)
-
-let rec equal_value v1 v2 =
- match v1, v2 with
- | Neutral n1, Neutral n2 -> equal_neutral n1 n2
- | Universe u1, Universe u2 -> u1 = u2
- | Pi a1, Pi a2 -> equal_abstraction a1 a2
- | Lambda a1, Lambda a2 -> equal_abstraction a1 a2
- | (Neutral _ | Universe _ | Pi _ | Lambda _), _ -> false
-
-and equal_abstraction (v1, x, f1) (v2, _, f2) =
- v1 = v2 && (let x = Neutral (Var (Syntax.fresh_var x)) in equal_value (f1 x) (f2 x))
-
-and equal_neutral n1 n2 =
- match n1, n2 with
- | Var x, Var y -> x = y
- | App (m1, v1), App (m2, v2) -> equal_neutral m1 m2 && equal_value v1 v2
- | (Var _ | App _), _ -> false
-
+and abstraction = variable * value * (value -> value)
+
+(* 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
+
+(* Conversion back to concrete syntax, for pretty-printing. *)
let rec uneval = function
- | Neutral n -> uneval_neutral n
- | Universe u -> Syntax.Universe u
- | Pi a -> Syntax.Pi (uneval_vabstraction a)
- | Lambda a -> Syntax.Lambda (uneval_vabstraction a)
-
-and uneval_neutral = function
- | Var x -> Syntax.Var x
- | App (n, v) -> Syntax.App (uneval_neutral n, uneval v)
-
-and uneval_vabstraction (t, x, f) =
- let x = Syntax.fresh_var x in
- (x, uneval t, uneval (f (Neutral (Var x))))
-
+ | Var x -> Concrete.Var x
+ | App (e1, e2) -> Concrete.App (uneval e1, uneval e2)
+ | Universe u -> Concrete.Universe u
+ | Pi a -> Concrete.Pi (uneval_vabstraction a)
+ | Lambda a -> Concrete.Lambda (uneval_vabstraction a)
+
+and uneval_vabstraction (x, t, f) =
+ let x = Concrete.fresh_var x in
+ (x, uneval t, uneval (f (Var x)))
View
30 tt.ml
@@ -58,31 +58,33 @@ let initial_ctx = []
and return the new environment. *)
let rec exec_cmd interactive ctx e =
match e with
- | Syntax.Eval e ->
+ | Concrete.Eval e ->
+ let e = Syntax.compile e in
let t = Infer.infer_type ctx e in
- let v = Value.eval [] e in
- let e' = Value.uneval v in
+ let e = Infer.normalize ctx e in
if interactive then Format.printf " = @[%t@]@\n : @[%t@]@."
- (Print.expr e')
+ (Print.expr e)
(Print.expr t) ;
ctx
- | Syntax.Context ->
+ | Concrete.Context ->
List.iter
- (fun (x, t) -> Format.printf "@[%t : @[%t@]@]@." (Print.variable x) (Print.expr t))
+ (fun (x, (t, _)) -> Format.printf "@[%t : @[%t@]@]@." (Print.variable x) (Print.expr t))
ctx ;
ctx
- | Syntax.Parameter (x, t) ->
- Infer.check_type ctx t ;
- if interactive then
- Format.printf "@[%t is assumed@]@." (Print.variable x) ;
- (x, t) :: ctx
- | Syntax.Check e ->
+ | 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.Check e ->
+ let e = Syntax.compile e in
let t = Infer.infer_type ctx e in
Format.printf "@[%t@]@\n : @[%t@]@." (Print.expr e) (Print.expr t) ;
ctx
- | Syntax.Help ->
+ | Concrete.Help ->
print_endline help_text ; ctx
- | Syntax.Quit -> exit 0
+ | Concrete.Quit -> exit 0
and use_file ctx (filename, interactive) =
let cmds = Lexer.read_file (parse Parser.directives) filename in
Please sign in to comment.
Something went wrong with that request. Please try again.