Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Comments

  • Loading branch information...
commit 4c34b3ba9cb6c29ce0e8bbd38ad507ef324f1e6e 1 parent 8fab532
@andrejbauer authored
Showing with 143 additions and 95 deletions.
  1. +37 −29 beautify.ml
  2. +4 −0 error.ml
  3. +27 −18 infer.ml
  4. +17 −6 print.ml
  5. +13 −0 syntax.ml
  6. +45 −42 tt.ml
View
66 beautify.ml
@@ -1,34 +1,30 @@
-(* This nasty function is used to rename bound variables before
- they are shown to the user. *)
+(** Renaming of bound variables for pretty printing. *)
open Syntax
-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 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
- in
- let find_available x sbst =
- let x = (match x with String x | Gensym (x, _) -> x | Dummy -> "_") in
+(** Split a variable name into base and numerical postfix, e.g.,
+ ["x42"] is split into [("x", 42)]. *)
+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)
+
+(** Given a variable [x] and substitution of variables to variables, does [x] appear
+ in the codomain of the substitution? *)
+let rec used x = function
+ | [] -> false
+ | (_, (String y | Gensym (y, _))) :: lst -> x = y || used x lst
+ | (_, Dummy) :: lst -> used x lst
+
+(** Given a variable [x] and a substitution of variables to variables, find a variant of
+ [x] which does not appear in the codomain of the substitution. *)
+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
@@ -36,13 +32,25 @@ let beautify =
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
+
+(** Does [x] occur freely in the given expression? *)
+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
+
+(** Rename bound variables in the given expression for the purposes of
+ pretty printing. *)
+let beautify =
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 =
View
4 error.ml
@@ -1,3 +1,7 @@
+(** Error reporting. *)
+
+(** Exception [Error (err, msg)] indicates an error of type [err] with
+ error message [msg]. *)
exception Error of (string * string)
(** [error err_type msg] raises an error of type [err_type], and a message [msg]. The
View
45 infer.ml
@@ -1,6 +1,9 @@
+(** Type inference and normalization. *)
+
open Syntax
-(* Normalization. *)
+(** [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
@@ -22,21 +25,23 @@ and normalize_abstraction ctx (x, t, e) =
let t = normalize ctx t in
(x, t, normalize (Ctx.extend x t ctx) e)
-(* 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, e1) (y, t2, e2) =
- equal ctx t1 t2 &&
- (equal (Ctx.extend x t1 ctx) e1 (subst [(y, Var x)] e2))
+(** [equal ctx e1 e2] determines whether normalized [e1] and [e2] are equal up to renaming
+ of bound variables. *)
+let equal ctx e1 e2 =
+ let rec equal 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
+ | Pi a1, Pi a2 -> equal_abstraction a1 a2
+ | Lambda a1, Lambda a2 -> equal_abstraction a1 a2
+ | (Var _ | App _ | Universe _ | Pi _ | Lambda _), _ -> false
+ and equal_abstraction (x, t1, e1) (y, t2, e2) =
+ equal t1 t2 && (equal e1 (subst [(y, Var x)] e2))
+ in
+ equal (normalize ctx e1) (normalize ctx e2)
-(* Type inference. *)
+(** [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
@@ -56,18 +61,22 @@ let rec infer_type ctx = function
check_equal ctx s te ;
subst [(x, e2)] t
+(** [infer_universe ctx t] infers the universe level of type [t] in context [ctx]. *)
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"
+(** [infer_pi ctx e] infers the type of [e] in context [ctx], verifies that it is
+ of the form [Pi (x, t1, t2)] and returns the triple [(x, t1, t2)]. *)
and infer_pi ctx e =
let t = infer_type ctx e in
match normalize ctx t with
| Pi a -> a
| 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)
+(** [check_equal ctx e1 e2] checks that expressions [e1] and [e2] are equal. *)
+and check_equal ctx e1 e2 =
+ if not (equal ctx e1 e2)
+ then Error.typing "expressions %t and %t are not equal" (Print.expr e1) (Print.expr e2)
View
23 print.ml
@@ -1,5 +1,14 @@
-let fprintf = Format.fprintf
+(** Pretty-printing of expressions with the Ocaml [Format] library. *)
+(** Print an expression, possibly placing parentheses around it. We always
+ print things at a given "level" [at_level]. If the level exceeds the
+ maximum allowed level [max_level] then the expression should be parenthesized.
+
+ Let us consider an example. When printing nested applications, we should print [App
+ (App (e1, e2), e3)] as ["e1 e2 e3"] and [App(e1, App(e2, e3))] as ["e1 (e2 e3)"]. So
+ if we assign level 1 to applications, then during printing of [App (e1, e2)] we should
+ print [e1] at [max_level] 1 and [e2] at [max_level] 0.
+*)
let print ?(max_level=9999) ?(at_level=0) ppf =
if max_level < at_level then
begin
@@ -12,12 +21,14 @@ let print ?(max_level=9999) ?(at_level=0) ppf =
Format.kfprintf (fun ppf -> Format.fprintf ppf "@]") ppf
end
+(** Print the name of a variable. *)
let variable x ppf =
match x with
- | Syntax.Dummy -> print ppf "_"
+ | Syntax.Dummy -> assert false (* should never happen *)
| Syntax.String x -> print ppf "%s" x
| Syntax.Gensym (x, k) -> print ppf "%s_%d" x k
+(** [expr e ppf] prints (beautified) expression [e] using formatter [ppf]. *)
let expr e ppf =
let rec expr ?max_level e ppf =
let print ?at_level = print ?max_level ?at_level ppf in
@@ -31,17 +42,17 @@ let expr e ppf =
in
expr (Beautify.beautify e) ppf
+(** Support for printing of errors, warning and debugging information. *)
let verbosity = ref 3
let message msg_type v =
if v <= !verbosity then
begin
Format.eprintf "@[%s: " msg_type;
- Format.kfprintf (fun ppf -> fprintf ppf "@]@.") Format.err_formatter
+ Format.kfprintf (fun ppf -> Format.fprintf ppf "@]@.") Format.err_formatter
end
else
Format.ifprintf Format.err_formatter
let error (err_type, msg) = message (err_type) 1 "%s" msg
-let check msg = message "Check" 2 msg
-let warning msg = message "Warning" 3 msg
-let debug msg = message "Debug" 4 msg
+let warning msg = message "Warning" 2 msg
+let debug msg = message "Debug" 3 msg
View
13 syntax.ml
@@ -1,10 +1,19 @@
+
+(** During substitution we generate fresh variable names. Because we want pretty printing,
+ each freshly generated variable name should "remember" its preferred form. Thus a
+ variable name has three possible form. It can be a string, as originally given by
+ the user, or it can be a generated fresh name consisting of preferred name and a counter,
+ or it can be a dummy, indicating that it is never used.
+*)
type variable =
| String of string
| 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
@@ -14,6 +23,7 @@ type expr =
and abstraction = variable * expr * expr
+(** Toplevel directives. *)
type directive =
| Quit
| Help
@@ -23,12 +33,15 @@ type directive =
| Check of expr
| Eval of expr
+(** [refresh x] generates a fresh variable name whose preferred form is [x]. *)
let refresh =
let k = ref 0 in
function
| String x | Gensym (x, _) -> (incr k ; Gensym (x, !k))
| Dummy -> (incr k ; Gensym ("_", !k))
+(** [subst [(x1,e1); ...; (xn;en)] e] performs the given substitution of
+ expressions [e1], ..., [en] for variables [x1], ..., [xn] in expression [e]. *)
let rec subst s = function
| Var x -> (try List.assoc x s with Not_found -> Var x)
| Universe k -> Universe k
View
87 tt.ml
@@ -1,4 +1,4 @@
-(** TT with pies and universes indexed by numerals *)
+(** Toplevel. *)
let usage = "Usage: tt [option] ... [file] ..."
let interactive_shell = ref true
@@ -12,12 +12,15 @@ Context. print current contex
Help. print this help
Quit. exit" ;;
-(* A list of files to be loaded and run. *)
+(** A list of files to be loaded and run. *)
let files = ref []
+
let add_file interactive filename = (files := (filename, interactive) :: !files)
+
+(** A list of command-line wrappers to look for. *)
let wrapper = ref (Some ["rlwrap"; "ledit"])
-(* Command-line options *)
+(** Command-line options *)
let options = Arg.align [
("--wrapper",
Arg.String (fun str -> wrapper := Some [str]),
@@ -38,12 +41,12 @@ let options = Arg.align [
"<file> Load <file> into the initial environment");
]
-(* Treat anonymous arguments as files to be run. *)
+(** Treat anonymous arguments as files to be run. *)
let anonymous str =
add_file true str;
interactive_shell := false
-(* Parser wrapper *)
+(** Parser wrapper *)
let parse parser lex =
try
parser Lexer.token lex
@@ -55,50 +58,50 @@ let parse parser lex =
let initial_ctx = []
-(* [exec_cmd env c] executes toplevel command [c] in global
- context [ctx]. It prints the result on standard output
- and return the new environment. *)
-let rec exec_cmd interactive ctx e =
- match e with
- | 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) ;
+(** [exec_cmd ctx d] executes toplevel directive [d] in global context [ctx]. It prints the
+ result on standard output and return the new context. *)
+let rec exec_cmd interactive ctx d =
+ match d with
+ | 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
+ | 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
- | 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
- | 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 t = Infer.infer_type ctx e in
+ | Syntax.Parameter (x, t) ->
+ ignore (Infer.infer_universe ctx t) ;
if interactive then
- Format.printf "@[%t is defined@]@." (Print.variable x) ;
- 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
- | Syntax.Help ->
+ 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 t = Infer.infer_type ctx e in
+ if interactive then
+ Format.printf "@[%t is defined@]@." (Print.variable x) ;
+ 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
+ | Syntax.Help ->
print_endline help_text ; ctx
- | Syntax.Quit -> exit 0
+ | Syntax.Quit -> exit 0
+(** Load directives from the given file. *)
and use_file ctx (filename, interactive) =
let cmds = Lexer.read_file (parse Parser.directives) filename in
List.fold_left (exec_cmd interactive) ctx cmds
-(* Interactive toplevel *)
+(** Interactive toplevel *)
let toplevel ctx =
let eof = match Sys.os_type with
| "Unix" | "Cygwin" -> "Ctrl-D"
@@ -119,7 +122,7 @@ let toplevel ctx =
done
with End_of_file -> ()
-(* Main program *)
+(** Main program *)
let main =
Sys.catch_break true;
(* Parse the arguments. *)
Please sign in to comment.
Something went wrong with that request. Please try again.