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
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
|
(*i $Id$ i*)
(*s Production of Ocaml syntax. *)
open Pp
open Util
open Names
open Term
open Miniml
(*s Some utility functions. *)
let string s = [< 'sTR s >]
let open_par = function true -> string "(" | false -> [<>]
let close_par = function true -> string ")" | false -> [<>]
let rec collapse_type_app = function
| (Tapp l1) :: l2 -> collapse_type_app (l1@l2)
| l -> l
let pp_tuple f = function
| [] -> [< >]
| [x] -> f x
| l -> [< 'sTR "(";
prlist_with_sep (fun () -> [< 'sTR ","; 'sPC >]) f l;
'sTR ")" >]
let space_if = function true -> [< 'sPC >] | false -> [<>]
(*s The pretty-printing functor. *)
module Make = functor(P : Mlpp_param) -> struct
(*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
are needed or not. *)
let pp_type t =
let rec pp_rec par = function
| Tvar id ->
string ("'" ^ string_of_id id)
| Tapp l ->
(match collapse_type_app l with
| [] -> assert false
| [t] -> pp_rec par t
| t::l -> [< open_par par; pp_tuple (pp_rec false) l;
space_if (l <>[]); pp_rec false t; close_par par >])
| Tarr (t1,t2) ->
[< open_par par; pp_rec true t1; 'sPC; 'sTR"->"; 'sPC;
pp_rec false t2; close_par par >]
| Tglob r ->
P.pp_global r
| Tprop ->
string "prop"
in
hOV 0 (pp_rec false t)
(*s Pretty-printing of expressions. [par] indicates whether
parentheses are needed or not. [env] is the list of names for the
de Bruijn variables. [args] is the list of collected arguments
(already pretty-printed). *)
let rec pp_expr par env args =
let apply st = match args with
| [] -> st
| _ -> hOV 2 [< open_par par; st; 'sPC;
prlist_with_sep (fun () -> [<'sPC>]) (fun s -> s) args;
close_par par >]
in
function
| MLrel n ->
apply (pr_id (List.nth env (pred n)))
| MLapp (f,args') ->
let stl = List.map (pp_expr true env []) args' in
pp_expr par env (stl @ args) f
| MLlam (id,a) ->
failwith "todo"
(*i
let fl,a' = collect_lambda a in
let fl = rename_bvars env fl in
let st = [< abst (List.rev fl) ; pp_rec false (fl@env) [] a' >] in
if args = [] then
[< open_par par; st; close_par par >]
else
apply [< 'sTR "("; st; 'sTR ")" >]
i*)
| MLglob r ->
apply (P.pp_global r)
| MLcons (_,id,[]) ->
pr_id id
| MLcons (_,id,[a]) ->
[< open_par par; pr_id id; 'sPC; pp_expr true env [] a;
pp_expr true env [] a ; close_par par >]
| MLcons (_,id,args') ->
[< open_par par; pr_id id; 'sPC;
pp_tuple (pp_expr true env []) args'; close_par par >]
| MLcase (t, pv) ->
apply
[< if args<>[] then [< 'sTR"(" >] else open_par par;
v 0 [< 'sTR "match "; pp_expr false env [] t; 'sTR " with";
'fNL; 'sTR " "; pp_pat env pv >] ;
if args<>[] then [< 'sTR")" >] else close_par par >]
| MLfix (i,b,idl,al) ->
pp_fix par env (i,b,idl,al) args
| MLexn id ->
[< open_par par; 'sTR "failwith"; 'sPC;
'qS (string_of_id id); close_par par >]
| MLcast (a,t) ->
[< open_par true; pp_expr false env args a; 'sPC; 'sTR ":"; 'sPC;
pp_type t; close_par true >]
| MLmagic a ->
[< open_par true; 'sTR "Obj.magic"; 'sPC;
pp_expr false env args a; close_par true >]
and pp_pat env pv = failwith "todo"
and pp_fix par env f args = failwith "todo"
let pp_ast = pp_expr false [] []
(*s Pretty-printing of inductive types declaration. *)
let pp_parameters l =
[< pp_tuple (fun id -> string ("'" ^ string_of_id id)) l; space_if (l<>[]) >]
let pp_one_inductive (pl,name,cl) =
let pp_constructor (id,l) =
[< pr_id id;
match l with
| [] -> [< >]
| _ -> [< 'sTR " of " ;
prlist_with_sep
(fun () -> [< 'sPC ; 'sTR "* " >]) pp_type l >] >]
in
[< pp_parameters pl; pr_id name; 'sTR " ="; 'fNL;
v 0 [< 'sTR " " ;
prlist_with_sep (fun () -> [< 'fNL ; 'sTR " | ">])
(fun c -> hOV 2 (pp_constructor c)) cl >] >]
let pp_inductive il =
[< 'sTR "type " ;
prlist_with_sep
(fun () -> [< 'fNL ; 'sTR "and " >])
(fun i -> pp_one_inductive i)
il;
'fNL >]
let pp_decl = function
| Dtype i ->
hOV 0 (pp_inductive i)
| Dabbrev (id, l, t) ->
hOV 0 [< 'sTR "type"; 'sPC; pp_parameters l;
pr_id id; 'sPC; 'sTR "="; 'sPC; pp_type t >]
| Dglob (id, a) ->
hOV 0 [< 'sTR "let"; 'sPC; pr_id id; 'sPC; 'sTR "="; 'sPC; pp_ast a >]
end
|
