Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Newer
Older
100644 59 lines (52 sloc) 2.439 kB
4c34b3b @andrejbauer Comments
authored
1 (** Pretty-printing of expressions with the Ocaml [Format] library. *)
9c6ca0f @andrejbauer Initial version
authored
2
4c34b3b @andrejbauer Comments
authored
3 (** Print an expression, possibly placing parentheses around it. We always
4 print things at a given "level" [at_level]. If the level exceeds the
5 maximum allowed level [max_level] then the expression should be parenthesized.
6
7 Let us consider an example. When printing nested applications, we should print [App
8 (App (e1, e2), e3)] as ["e1 e2 e3"] and [App(e1, App(e2, e3))] as ["e1 (e2 e3)"]. So
9 if we assign level 1 to applications, then during printing of [App (e1, e2)] we should
10 print [e1] at [max_level] 1 and [e2] at [max_level] 0.
11 *)
9c6ca0f @andrejbauer Initial version
authored
12 let print ?(max_level=9999) ?(at_level=0) ppf =
13 if max_level < at_level then
14 begin
8d7985f @andrejbauer Better printout and other improvements
authored
15 Format.fprintf ppf "(@[" ;
9c6ca0f @andrejbauer Initial version
authored
16 Format.kfprintf (fun ppf -> Format.fprintf ppf "@])") ppf
17 end
18 else
19 begin
8d7985f @andrejbauer Better printout and other improvements
authored
20 Format.fprintf ppf "@[" ;
9c6ca0f @andrejbauer Initial version
authored
21 Format.kfprintf (fun ppf -> Format.fprintf ppf "@]") ppf
22 end
23
4c34b3b @andrejbauer Comments
authored
24 (** Print the name of a variable. *)
9c6ca0f @andrejbauer Initial version
authored
25 let variable x ppf =
26 match x with
4c34b3b @andrejbauer Comments
authored
27 | Syntax.Dummy -> assert false (* should never happen *)
8a0ef44 @andrejbauer Abstract syntax with variable names.
authored
28 | Syntax.String x -> print ppf "%s" x
29 | Syntax.Gensym (x, k) -> print ppf "%s_%d" x k
9c6ca0f @andrejbauer Initial version
authored
30
4c34b3b @andrejbauer Comments
authored
31 (** [expr e ppf] prints (beautified) expression [e] using formatter [ppf]. *)
4eb5bb5 @andrejbauer Must go, but hunting down a bug in normalization
authored
32 let expr e ppf =
8d7985f @andrejbauer Better printout and other improvements
authored
33 let rec expr ?max_level e ppf =
9c6ca0f @andrejbauer Initial version
authored
34 let print ?at_level = print ?max_level ?at_level ppf in
8d7985f @andrejbauer Better printout and other improvements
authored
35 match e with
8a0ef44 @andrejbauer Abstract syntax with variable names.
authored
36 | Syntax.Var x -> variable x ppf
37 | Syntax.Universe k -> print "Type %d" k
38 | Syntax.Pi (Syntax.Dummy, t1, t2) -> print ~at_level:3 "%t ->@;%t" (expr ~max_level:2 t1) (expr t2)
39 | Syntax.Pi (x, t1, t2) -> print ~at_level:3 "forall %t : %t,@;%t" (variable x) (expr ~max_level:4 t1) (expr t2)
40 | Syntax.Lambda (x, t, e) -> print ~at_level:3 "fun %t : %t =>@;%t" (variable x) (expr t) (expr e)
41 | Syntax.App (e1, e2) -> print ~at_level:1 "%t %t" (expr ~max_level:1 e1) (expr ~max_level:0 e2)
9c6ca0f @andrejbauer Initial version
authored
42 in
8a0ef44 @andrejbauer Abstract syntax with variable names.
authored
43 expr (Beautify.beautify e) ppf
8d7985f @andrejbauer Better printout and other improvements
authored
44
4c34b3b @andrejbauer Comments
authored
45 (** Support for printing of errors, warning and debugging information. *)
9c6ca0f @andrejbauer Initial version
authored
46 let verbosity = ref 3
47 let message msg_type v =
48 if v <= !verbosity then
49 begin
50 Format.eprintf "@[%s: " msg_type;
4c34b3b @andrejbauer Comments
authored
51 Format.kfprintf (fun ppf -> Format.fprintf ppf "@]@.") Format.err_formatter
9c6ca0f @andrejbauer Initial version
authored
52 end
53 else
54 Format.ifprintf Format.err_formatter
55
56 let error (err_type, msg) = message (err_type) 1 "%s" msg
4c34b3b @andrejbauer Comments
authored
57 let warning msg = message "Warning" 2 msg
58 let debug msg = message "Debug" 3 msg
Something went wrong with that request. Please try again.