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
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(*i $Id$ i*)
(*s Production of Haskell syntax. *)
open Pp
open Util
open Names
open Nameops
open Term
open Miniml
open Mlutil
open Options
open Ocaml
open Nametab
(*s Haskell renaming issues. *)
let keywords =
List.fold_right (fun s -> Idset.add (id_of_string s))
[ "case"; "class"; "data"; "default"; "deriving"; "do"; "else";
"if"; "import"; "in"; "infix"; "infixl"; "infixr"; "instance";
"let"; "module"; "newtype"; "of"; "then"; "type"; "where"; "_";
"as"; "qualified"; "hiding" ; "prop" ; "arity" ]
Idset.empty
let preamble prm =
let m = match prm.mod_name with
| None -> "Main"
| Some m -> String.capitalize (string_of_id m)
in
(str "module " ++ str m ++ str " where" ++ fnl () ++ fnl () ++
str "type Prop = ()" ++ fnl () ++
str "prop = ()" ++ fnl () ++ fnl () ++
str "type Arity = ()" ++ fnl () ++
str "arity = ()" ++ fnl () ++ fnl ())
(*s The pretty-printing functor. *)
module Make = functor(P : Mlpp_param) -> struct
let pp_type_global = P.pp_type_global
let pp_global = P.pp_global
let rename_global = P.rename_global
let pr_lower_id id = pr_id (lowercase_id id)
let empty_env () = [], P.globals()
(*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
are needed or not. *)
let rec pp_type par t =
let rec pp_rec par = function
| Tvar id -> pr_lower_id id (* TODO: possible clash with Haskell kw *)
| Tapp l ->
(match collapse_type_app l with
| [] -> assert false
| [t] -> pp_rec par t
| t::l ->
(open_par par ++
pp_rec false t ++ spc () ++
prlist_with_sep (fun () -> (spc ())) (pp_type true) l ++
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 ->
pp_type_global r
| Texn s ->
(string ("() -- " ^ s) ++ fnl ())
| Tprop ->
string "Prop"
| Tarity ->
string "Arity"
in
hov 0 (pp_rec par 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 expr_needs_par = function
| MLlam _ -> true
| MLcase _ -> true
| _ -> false
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 (get_db_name n env))
| MLapp (f,args') ->
let stl = List.map (pp_expr true env []) args' in
pp_expr par env (stl @ args) f
| MLlam _ as a ->
let fl,a' = collect_lams a in
let fl,env' = push_vars fl env in
let st = (pp_abst (List.rev fl) ++ pp_expr false env' [] a') in
if args = [] then
(open_par par ++ st ++ close_par par)
else
apply (str "(" ++ st ++ str ")")
| MLletin (id,a1,a2) ->
let id',env' = push_vars [id] env in
let par' = par || args <> [] in
let par2 = not par' && expr_needs_par a2 in
apply
(hov 0 (open_par par' ++
hov 2 (str "let " ++ pr_id (List.hd id') ++ str " =" ++ spc () ++
pp_expr false env [] a1 ++ spc () ++ str "in") ++
spc () ++
pp_expr par2 env' [] a2 ++
close_par par'))
| MLglob r ->
apply (pp_global r)
| MLcons (r,[]) ->
pp_global r
| MLcons (r,[a]) ->
(open_par par ++ pp_global r ++ spc () ++
pp_expr true env [] a ++ close_par par)
| MLcons (r,args') ->
(open_par par ++ pp_global r ++ spc () ++
prlist_with_sep (fun () -> (spc ())) (pp_expr true env []) args' ++
close_par par)
| MLcase (t, pv) ->
apply
(if args <> [] then (str "(") else open_par par ++
v 0 (str "case " ++ pp_expr false env [] t ++ str " of" ++
fnl () ++ str " " ++ pp_pat env pv) ++
if args <> [] then (str ")") else close_par par)
| MLfix (i,ids,defs) ->
let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
pp_fix par env' (Some i) (Array.of_list (List.rev ids'),defs) args
| MLexn s ->
(open_par par ++ str "error" ++ spc () ++ qs s ++ close_par par)
| MLprop ->
string "prop"
| MLarity ->
string "arity"
| MLcast (a,t) ->
(open_par true ++ pp_expr false env args a ++ spc () ++ str "::" ++ spc () ++
pp_type false 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 =
let pp_one_pat (name,ids,t) =
let ids,env' = push_vars (List.rev ids) env in
let par = expr_needs_par t in
hov 2 (pp_global name ++
begin match ids with
| [] -> (mt ())
| _ -> (str " " ++
prlist_with_sep
(fun () -> (spc ())) pr_id (List.rev ids))
end ++
str " ->" ++ spc () ++ pp_expr par env' [] t)
in
(prvect_with_sep (fun () -> (fnl () ++ str " ")) pp_one_pat pv)
(*s names of the functions ([ids]) are already pushed in [env],
and passed here just for convenience. *)
and pp_fix par env in_p (ids,bl) args =
(open_par par ++
v 0 (str "let { " ++
prvect_with_sep
(fun () -> (str "; " ++ fnl ()))
(fun (fi,ti) -> pp_function env (pr_id fi) ti)
(array_map2 (fun id b -> (id,b)) ids bl) ++
str " }" ++fnl () ++
match in_p with
| Some j ->
hov 2 (str "in " ++ pr_id ids.(j) ++
if args <> [] then
(str " " ++
prlist_with_sep (fun () -> (str " "))
(fun s -> s) args)
else
(mt ()))
| None ->
(mt ())) ++
close_par par)
and pp_function env f t =
let bl,t' = collect_lams t in
let bl,env' = push_vars bl env in
(f ++ pr_binding (List.rev bl) ++
str " =" ++ fnl () ++ str " " ++
hov 2 (pp_expr false env' [] t'))
let pp_ast a = hov 0 (pp_expr false (empty_env ()) [] a)
(*s Pretty-printing of inductive types declaration. *)
let pp_one_inductive (pl,name,cl) =
let pp_constructor (id,l) =
(pp_global id ++
match l with
| [] -> (mt ())
| _ -> (str " " ++
prlist_with_sep
(fun () -> (str " ")) (pp_type true) l))
in
(str (if cl = [] then "type " else "data ") ++
pp_type_global name ++ str " " ++
prlist_with_sep (fun () -> (str " ")) pr_lower_id pl ++
if pl = [] then (mt ()) else (str " ") ++
(v 0 (str "= " ++
prlist_with_sep (fun () -> (fnl () ++ str " | "))
pp_constructor cl)))
let pp_inductive il =
(prlist_with_sep (fun () -> (fnl ())) pp_one_inductive il ++ fnl ())
(*s Pretty-printing of a declaration. *)
let pp_decl = function
| Dtype ([], _) ->
(mt ())
| Dtype (i, _) ->
hov 0 (pp_inductive i)
| Dabbrev (r, l, t) ->
hov 0 (str "type " ++ pp_type_global r ++ spc () ++
prlist_with_sep (fun () -> (str " ")) pr_lower_id l ++
if l <> [] then (str " ") else (mt ()) ++ str "=" ++ spc () ++
pp_type false t ++ fnl ())
| Dglob (r, MLfix (i,ids,defs)) ->
let env = empty_env () in
let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
(prlist_with_sep (fun () -> (fnl ()))
(fun (fi,ti) -> pp_function env' (pr_id fi) ti)
(List.combine (List.rev ids') (Array.to_list defs)) ++
fnl () ++
let id = rename_global r in
let idi = List.nth (List.rev ids') i in
if id <> idi then
(fnl () ++ pr_id id ++ str " = " ++ pr_id idi ++ fnl ())
else
(mt ()))
| Dglob (r, a) ->
hov 0 (pp_function (empty_env ()) (pp_global r) a ++ fnl ())
| Dcustom (r,s) ->
hov 0 (pp_global r ++ str " =" ++
spc () ++ str s ++ fnl ())
let pp_type = pp_type false
end
|
