haftmann@37744
|
1 |
(* Title: Tools/Code/code_haskell.ML
|
haftmann@28054
|
2 |
Author: Florian Haftmann, TU Muenchen
|
haftmann@28054
|
3 |
|
haftmann@28054
|
4 |
Serializer for Haskell.
|
haftmann@28054
|
5 |
*)
|
haftmann@28054
|
6 |
|
haftmann@28054
|
7 |
signature CODE_HASKELL =
|
haftmann@28054
|
8 |
sig
|
noschinl@45797
|
9 |
val language_params: string
|
haftmann@37744
|
10 |
val target: string
|
haftmann@28054
|
11 |
val setup: theory -> theory
|
haftmann@28054
|
12 |
end;
|
haftmann@28054
|
13 |
|
haftmann@28054
|
14 |
structure Code_Haskell : CODE_HASKELL =
|
haftmann@28054
|
15 |
struct
|
haftmann@28054
|
16 |
|
haftmann@28054
|
17 |
val target = "Haskell";
|
haftmann@28054
|
18 |
|
noschinl@45797
|
19 |
val language_extensions =
|
noschinl@45811
|
20 |
["EmptyDataDecls", "RankNTypes", "ScopedTypeVariables"];
|
noschinl@45797
|
21 |
|
noschinl@45797
|
22 |
val language_pragma =
|
noschinl@45811
|
23 |
"{-# LANGUAGE " ^ commas language_extensions ^ " #-}";
|
noschinl@45797
|
24 |
|
noschinl@45797
|
25 |
val language_params =
|
noschinl@45811
|
26 |
space_implode " " (map (prefix "-X") language_extensions);
|
noschinl@45797
|
27 |
|
haftmann@28054
|
28 |
open Basic_Code_Thingol;
|
haftmann@28054
|
29 |
open Code_Printer;
|
haftmann@28054
|
30 |
|
haftmann@28054
|
31 |
infixr 5 @@;
|
haftmann@28054
|
32 |
infixr 5 @|;
|
haftmann@28054
|
33 |
|
haftmann@28054
|
34 |
|
haftmann@28054
|
35 |
(** Haskell serializer **)
|
haftmann@28054
|
36 |
|
haftmann@48472
|
37 |
fun print_haskell_stmt class_syntax tyco_syntax const_syntax
|
bulwahn@45661
|
38 |
reserved deresolve deriving_show =
|
haftmann@28054
|
39 |
let
|
haftmann@39149
|
40 |
fun class_name class = case class_syntax class
|
haftmann@28054
|
41 |
of NONE => deresolve class
|
haftmann@28687
|
42 |
| SOME class => class;
|
haftmann@33988
|
43 |
fun print_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs
|
haftmann@28054
|
44 |
of [] => []
|
haftmann@37359
|
45 |
| constraints => enum "," "(" ")" (
|
haftmann@28054
|
46 |
map (fn (v, class) =>
|
haftmann@37359
|
47 |
str (class_name class ^ " " ^ lookup_var tyvars v)) constraints)
|
haftmann@28054
|
48 |
@@ str " => ";
|
haftmann@33988
|
49 |
fun print_typforall tyvars vs = case map fst vs
|
haftmann@28054
|
50 |
of [] => []
|
haftmann@28054
|
51 |
| vnames => str "forall " :: Pretty.breaks
|
haftmann@32924
|
52 |
(map (str o lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
|
haftmann@33988
|
53 |
fun print_tyco_expr tyvars fxy (tyco, tys) =
|
haftmann@33988
|
54 |
brackify fxy (str tyco :: map (print_typ tyvars BR) tys)
|
haftmann@48472
|
55 |
and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco
|
haftmann@33988
|
56 |
of NONE => print_tyco_expr tyvars fxy (deresolve tyco, tys)
|
haftmann@48472
|
57 |
| SOME (_, print) => print (print_typ tyvars) fxy tys)
|
haftmann@33988
|
58 |
| print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v;
|
haftmann@49018
|
59 |
fun print_typdecl tyvars (tyco, vs) =
|
haftmann@49018
|
60 |
print_tyco_expr tyvars NOBR (tyco, map ITyVar vs);
|
haftmann@33988
|
61 |
fun print_typscheme tyvars (vs, ty) =
|
haftmann@33988
|
62 |
Pretty.block (print_typforall tyvars vs @ print_typcontext tyvars vs @| print_typ tyvars NOBR ty);
|
haftmann@49087
|
63 |
fun print_term tyvars some_thm vars fxy (IConst const) =
|
haftmann@49087
|
64 |
print_app tyvars some_thm vars fxy (const, [])
|
haftmann@35228
|
65 |
| print_term tyvars some_thm vars fxy (t as (t1 `$ t2)) =
|
haftmann@28054
|
66 |
(case Code_Thingol.unfold_const_app t
|
haftmann@35228
|
67 |
of SOME app => print_app tyvars some_thm vars fxy app
|
haftmann@28054
|
68 |
| _ =>
|
haftmann@28054
|
69 |
brackify fxy [
|
haftmann@35228
|
70 |
print_term tyvars some_thm vars NOBR t1,
|
haftmann@35228
|
71 |
print_term tyvars some_thm vars BR t2
|
haftmann@28054
|
72 |
])
|
haftmann@35228
|
73 |
| print_term tyvars some_thm vars fxy (IVar NONE) =
|
haftmann@31889
|
74 |
str "_"
|
haftmann@35228
|
75 |
| print_term tyvars some_thm vars fxy (IVar (SOME v)) =
|
haftmann@32924
|
76 |
(str o lookup_var vars) v
|
haftmann@35228
|
77 |
| print_term tyvars some_thm vars fxy (t as _ `|=> _) =
|
haftmann@28054
|
78 |
let
|
haftmann@31873
|
79 |
val (binds, t') = Code_Thingol.unfold_pat_abs t;
|
haftmann@35228
|
80 |
val (ps, vars') = fold_map (print_bind tyvars some_thm BR o fst) binds vars;
|
haftmann@35228
|
81 |
in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars some_thm vars' NOBR t') end
|
haftmann@49087
|
82 |
| print_term tyvars some_thm vars fxy (ICase case_expr) =
|
haftmann@49087
|
83 |
(case Code_Thingol.unfold_const_app (#primitive case_expr)
|
haftmann@49087
|
84 |
of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
|
haftmann@49087
|
85 |
then print_case tyvars some_thm vars fxy case_expr
|
haftmann@49087
|
86 |
else print_app tyvars some_thm vars fxy app
|
haftmann@49087
|
87 |
| NONE => print_case tyvars some_thm vars fxy case_expr)
|
haftmann@49087
|
88 |
and print_app_expr tyvars some_thm vars ({ name = c, dom, range, annotate, ... }, ts) =
|
bulwahn@45660
|
89 |
let
|
haftmann@49087
|
90 |
val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (dom, range)
|
bulwahn@45880
|
91 |
val printed_const =
|
bulwahn@45880
|
92 |
if annotate then
|
bulwahn@45880
|
93 |
brackets [(str o deresolve) c, str "::", print_typ tyvars NOBR ty]
|
bulwahn@45880
|
94 |
else
|
bulwahn@45880
|
95 |
(str o deresolve) c
|
bulwahn@45660
|
96 |
in
|
bulwahn@45880
|
97 |
printed_const :: map (print_term tyvars some_thm vars BR) ts
|
bulwahn@45660
|
98 |
end
|
haftmann@39149
|
99 |
and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) const_syntax
|
haftmann@35228
|
100 |
and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p
|
haftmann@49087
|
101 |
and print_case tyvars some_thm vars fxy { clauses = [], ... } =
|
haftmann@49087
|
102 |
(brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""]
|
haftmann@49087
|
103 |
| print_case tyvars some_thm vars fxy (case_expr as { clauses = [_], ... }) =
|
haftmann@28054
|
104 |
let
|
haftmann@49087
|
105 |
val (binds, body) = Code_Thingol.unfold_let (ICase case_expr);
|
haftmann@48472
|
106 |
fun print_match ((pat, _), t) vars =
|
haftmann@28054
|
107 |
vars
|
haftmann@35228
|
108 |
|> print_bind tyvars some_thm BR pat
|
haftmann@35228
|
109 |
|>> (fn p => semicolon [p, str "=", print_term tyvars some_thm vars NOBR t])
|
haftmann@33988
|
110 |
val (ps, vars') = fold_map print_match binds vars;
|
haftmann@31665
|
111 |
in brackify_block fxy (str "let {")
|
haftmann@31665
|
112 |
ps
|
haftmann@35228
|
113 |
(concat [str "}", str "in", print_term tyvars some_thm vars' NOBR body])
|
haftmann@28054
|
114 |
end
|
haftmann@49087
|
115 |
| print_case tyvars some_thm vars fxy { term = t, typ = ty, clauses = clauses as _ :: _, ... } =
|
haftmann@28054
|
116 |
let
|
haftmann@33988
|
117 |
fun print_select (pat, body) =
|
haftmann@28054
|
118 |
let
|
haftmann@35228
|
119 |
val (p, vars') = print_bind tyvars some_thm NOBR pat vars;
|
haftmann@35228
|
120 |
in semicolon [p, str "->", print_term tyvars some_thm vars' NOBR body] end;
|
haftmann@36574
|
121 |
in Pretty.block_enclose
|
haftmann@36574
|
122 |
(concat [str "(case", print_term tyvars some_thm vars NOBR t, str "of", str "{"], str "})")
|
haftmann@33988
|
123 |
(map print_select clauses)
|
haftmann@49087
|
124 |
end;
|
haftmann@37412
|
125 |
fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
|
haftmann@28054
|
126 |
let
|
haftmann@32924
|
127 |
val tyvars = intro_vars (map fst vs) reserved;
|
haftmann@34262
|
128 |
fun print_err n =
|
haftmann@33988
|
129 |
semicolon (
|
haftmann@39437
|
130 |
(str o deresolve) name
|
haftmann@28054
|
131 |
:: map str (replicate n "_")
|
haftmann@28054
|
132 |
@ str "="
|
haftmann@28054
|
133 |
:: str "error"
|
haftmann@33988
|
134 |
@@ (str o ML_Syntax.print_string
|
wenzelm@30364
|
135 |
o Long_Name.base_name o Long_Name.qualifier) name
|
haftmann@34262
|
136 |
);
|
haftmann@35228
|
137 |
fun print_eqn ((ts, t), (some_thm, _)) =
|
haftmann@28054
|
138 |
let
|
haftmann@32913
|
139 |
val consts = fold Code_Thingol.add_constnames (t :: ts) [];
|
haftmann@32924
|
140 |
val vars = reserved
|
haftmann@32924
|
141 |
|> intro_base_names
|
haftmann@39149
|
142 |
(is_none o const_syntax) deresolve consts
|
haftmann@32924
|
143 |
|> intro_vars ((fold o Code_Thingol.fold_varnames)
|
haftmann@32925
|
144 |
(insert (op =)) ts []);
|
haftmann@28054
|
145 |
in
|
haftmann@28054
|
146 |
semicolon (
|
haftmann@39437
|
147 |
(str o deresolve) name
|
haftmann@35228
|
148 |
:: map (print_term tyvars some_thm vars BR) ts
|
haftmann@28054
|
149 |
@ str "="
|
haftmann@35228
|
150 |
@@ print_term tyvars some_thm vars NOBR t
|
haftmann@28054
|
151 |
)
|
haftmann@28054
|
152 |
end;
|
haftmann@28054
|
153 |
in
|
haftmann@28054
|
154 |
Pretty.chunks (
|
haftmann@33988
|
155 |
semicolon [
|
haftmann@39437
|
156 |
(str o suffix " ::" o deresolve) name,
|
haftmann@33988
|
157 |
print_typscheme tyvars (vs, ty)
|
haftmann@28054
|
158 |
]
|
haftmann@34262
|
159 |
:: (case filter (snd o snd) raw_eqs
|
haftmann@34262
|
160 |
of [] => [print_err ((length o fst o Code_Thingol.unfold_fun) ty)]
|
haftmann@34262
|
161 |
| eqs => map print_eqn eqs)
|
haftmann@28054
|
162 |
)
|
haftmann@28054
|
163 |
end
|
haftmann@33988
|
164 |
| print_stmt (name, Code_Thingol.Datatype (_, (vs, []))) =
|
haftmann@28054
|
165 |
let
|
haftmann@49018
|
166 |
val tyvars = intro_vars vs reserved;
|
haftmann@28054
|
167 |
in
|
haftmann@28054
|
168 |
semicolon [
|
haftmann@28054
|
169 |
str "data",
|
haftmann@49018
|
170 |
print_typdecl tyvars (deresolve name, vs)
|
haftmann@28054
|
171 |
]
|
haftmann@28054
|
172 |
end
|
haftmann@37424
|
173 |
| print_stmt (name, Code_Thingol.Datatype (_, (vs, [((co, _), [ty])]))) =
|
haftmann@28054
|
174 |
let
|
haftmann@49018
|
175 |
val tyvars = intro_vars vs reserved;
|
haftmann@28054
|
176 |
in
|
haftmann@28054
|
177 |
semicolon (
|
haftmann@28054
|
178 |
str "newtype"
|
haftmann@49018
|
179 |
:: print_typdecl tyvars (deresolve name, vs)
|
haftmann@28054
|
180 |
:: str "="
|
haftmann@39437
|
181 |
:: (str o deresolve) co
|
haftmann@33988
|
182 |
:: print_typ tyvars BR ty
|
haftmann@28054
|
183 |
:: (if deriving_show name then [str "deriving (Read, Show)"] else [])
|
haftmann@28054
|
184 |
)
|
haftmann@28054
|
185 |
end
|
haftmann@33988
|
186 |
| print_stmt (name, Code_Thingol.Datatype (_, (vs, co :: cos))) =
|
haftmann@28054
|
187 |
let
|
haftmann@49018
|
188 |
val tyvars = intro_vars vs reserved;
|
haftmann@37424
|
189 |
fun print_co ((co, _), tys) =
|
haftmann@28054
|
190 |
concat (
|
haftmann@39437
|
191 |
(str o deresolve) co
|
haftmann@33988
|
192 |
:: map (print_typ tyvars BR) tys
|
haftmann@28054
|
193 |
)
|
haftmann@28054
|
194 |
in
|
haftmann@28054
|
195 |
semicolon (
|
haftmann@28054
|
196 |
str "data"
|
haftmann@49018
|
197 |
:: print_typdecl tyvars (deresolve name, vs)
|
haftmann@28054
|
198 |
:: str "="
|
haftmann@33988
|
199 |
:: print_co co
|
haftmann@33988
|
200 |
:: map ((fn p => Pretty.block [str "| ", p]) o print_co) cos
|
haftmann@28054
|
201 |
@ (if deriving_show name then [str "deriving (Read, Show)"] else [])
|
haftmann@28054
|
202 |
)
|
haftmann@28054
|
203 |
end
|
haftmann@37422
|
204 |
| print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
|
haftmann@28054
|
205 |
let
|
haftmann@32924
|
206 |
val tyvars = intro_vars [v] reserved;
|
haftmann@33988
|
207 |
fun print_classparam (classparam, ty) =
|
haftmann@28054
|
208 |
semicolon [
|
haftmann@39437
|
209 |
(str o deresolve) classparam,
|
haftmann@28054
|
210 |
str "::",
|
haftmann@33988
|
211 |
print_typ tyvars NOBR ty
|
haftmann@28054
|
212 |
]
|
haftmann@28054
|
213 |
in
|
haftmann@28054
|
214 |
Pretty.block_enclose (
|
haftmann@28054
|
215 |
Pretty.block [
|
haftmann@28054
|
216 |
str "class ",
|
haftmann@37359
|
217 |
Pretty.block (print_typcontext tyvars [(v, map fst super_classes)]),
|
haftmann@39437
|
218 |
str (deresolve name ^ " " ^ lookup_var tyvars v),
|
haftmann@28054
|
219 |
str " where {"
|
haftmann@28054
|
220 |
],
|
haftmann@28054
|
221 |
str "};"
|
haftmann@33988
|
222 |
) (map print_classparam classparams)
|
haftmann@28054
|
223 |
end
|
haftmann@49087
|
224 |
| print_stmt (_, Code_Thingol.Classinst { class, tyco, vs, inst_params, ... }) =
|
haftmann@28054
|
225 |
let
|
haftmann@32924
|
226 |
val tyvars = intro_vars (map fst vs) reserved;
|
haftmann@39149
|
227 |
fun requires_args classparam = case const_syntax classparam
|
haftmann@39437
|
228 |
of NONE => NONE
|
haftmann@39437
|
229 |
| SOME (Code_Printer.Plain_const_syntax _) => SOME 0
|
haftmann@39437
|
230 |
| SOME (Code_Printer.Complex_const_syntax (k,_ )) => SOME k;
|
haftmann@37854
|
231 |
fun print_classparam_instance ((classparam, const), (thm, _)) =
|
haftmann@37854
|
232 |
case requires_args classparam
|
haftmann@39437
|
233 |
of NONE => semicolon [
|
haftmann@39437
|
234 |
(str o Long_Name.base_name o deresolve) classparam,
|
haftmann@28687
|
235 |
str "=",
|
haftmann@37854
|
236 |
print_app tyvars (SOME thm) reserved NOBR (const, [])
|
haftmann@28687
|
237 |
]
|
haftmann@39437
|
238 |
| SOME k =>
|
haftmann@37854
|
239 |
let
|
haftmann@49087
|
240 |
val { name = c, dom, range, ... } = const;
|
haftmann@37854
|
241 |
val (vs, rhs) = (apfst o map) fst
|
haftmann@37854
|
242 |
(Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
|
haftmann@39149
|
243 |
val s = if (is_some o const_syntax) c
|
haftmann@37854
|
244 |
then NONE else (SOME o Long_Name.base_name o deresolve) c;
|
haftmann@37854
|
245 |
val vars = reserved
|
haftmann@37854
|
246 |
|> intro_vars (map_filter I (s :: vs));
|
haftmann@49087
|
247 |
val lhs = IConst { name = classparam, typargs = [],
|
haftmann@49087
|
248 |
dicts = [], dom = dom, range = range, annotate = false } `$$ map IVar vs;
|
bulwahn@45880
|
249 |
(*dictionaries are not relevant at this late stage,
|
bulwahn@45880
|
250 |
and these consts never need type annotations for disambiguation *)
|
haftmann@37854
|
251 |
in
|
haftmann@37854
|
252 |
semicolon [
|
haftmann@37854
|
253 |
print_term tyvars (SOME thm) vars NOBR lhs,
|
haftmann@37854
|
254 |
str "=",
|
haftmann@37854
|
255 |
print_term tyvars (SOME thm) vars NOBR rhs
|
haftmann@37854
|
256 |
]
|
haftmann@37854
|
257 |
end;
|
haftmann@28054
|
258 |
in
|
haftmann@28054
|
259 |
Pretty.block_enclose (
|
haftmann@28054
|
260 |
Pretty.block [
|
haftmann@28054
|
261 |
str "instance ",
|
haftmann@33988
|
262 |
Pretty.block (print_typcontext tyvars vs),
|
haftmann@28054
|
263 |
str (class_name class ^ " "),
|
haftmann@33988
|
264 |
print_typ tyvars BR (tyco `%% map (ITyVar o fst) vs),
|
haftmann@28054
|
265 |
str " where {"
|
haftmann@28054
|
266 |
],
|
haftmann@28054
|
267 |
str "};"
|
haftmann@49087
|
268 |
) (map print_classparam_instance inst_params)
|
haftmann@28054
|
269 |
end;
|
haftmann@33988
|
270 |
in print_stmt end;
|
haftmann@28054
|
271 |
|
haftmann@39432
|
272 |
fun haskell_program_of_program labelled_name module_alias module_prefix reserved =
|
haftmann@39432
|
273 |
let
|
haftmann@39432
|
274 |
fun namify_fun upper base (nsp_fun, nsp_typ) =
|
haftmann@39432
|
275 |
let
|
wenzelm@44208
|
276 |
val (base', nsp_fun') =
|
wenzelm@44208
|
277 |
Name.variant (if upper then first_upper base else base) nsp_fun;
|
haftmann@39432
|
278 |
in (base', (nsp_fun', nsp_typ)) end;
|
haftmann@39432
|
279 |
fun namify_typ base (nsp_fun, nsp_typ) =
|
haftmann@39432
|
280 |
let
|
wenzelm@44208
|
281 |
val (base', nsp_typ') = Name.variant (first_upper base) nsp_typ;
|
haftmann@39432
|
282 |
in (base', (nsp_fun, nsp_typ')) end;
|
haftmann@39432
|
283 |
fun namify_stmt (Code_Thingol.Fun (_, (_, SOME _))) = pair
|
haftmann@39432
|
284 |
| namify_stmt (Code_Thingol.Fun _) = namify_fun false
|
haftmann@39432
|
285 |
| namify_stmt (Code_Thingol.Datatype _) = namify_typ
|
haftmann@39432
|
286 |
| namify_stmt (Code_Thingol.Datatypecons _) = namify_fun true
|
haftmann@39432
|
287 |
| namify_stmt (Code_Thingol.Class _) = namify_typ
|
haftmann@39432
|
288 |
| namify_stmt (Code_Thingol.Classrel _) = pair
|
haftmann@39432
|
289 |
| namify_stmt (Code_Thingol.Classparam _) = namify_fun false
|
haftmann@39432
|
290 |
| namify_stmt (Code_Thingol.Classinst _) = pair;
|
haftmann@39432
|
291 |
fun select_stmt (Code_Thingol.Fun (_, (_, SOME _))) = false
|
haftmann@39432
|
292 |
| select_stmt (Code_Thingol.Fun _) = true
|
haftmann@39432
|
293 |
| select_stmt (Code_Thingol.Datatype _) = true
|
haftmann@39432
|
294 |
| select_stmt (Code_Thingol.Datatypecons _) = false
|
haftmann@39432
|
295 |
| select_stmt (Code_Thingol.Class _) = true
|
haftmann@39432
|
296 |
| select_stmt (Code_Thingol.Classrel _) = false
|
haftmann@39432
|
297 |
| select_stmt (Code_Thingol.Classparam _) = false
|
haftmann@39432
|
298 |
| select_stmt (Code_Thingol.Classinst _) = true;
|
haftmann@39432
|
299 |
in
|
haftmann@39436
|
300 |
Code_Namespace.flat_program labelled_name
|
haftmann@39432
|
301 |
{ module_alias = module_alias, module_prefix = module_prefix,
|
haftmann@39432
|
302 |
reserved = reserved, empty_nsp = (reserved, reserved), namify_stmt = namify_stmt,
|
haftmann@39432
|
303 |
modify_stmt = fn stmt => if select_stmt stmt then SOME stmt else NONE }
|
haftmann@39432
|
304 |
end;
|
haftmann@39432
|
305 |
|
haftmann@49446
|
306 |
val prelude_import_operators = [
|
haftmann@49446
|
307 |
"==", "/=", "<", "<=", ">=", ">", "+", "-", "*", "/", "**", ">>=", ">>", "=<<", "&&", "||", "^", "^^", ".", "$", "$!", "++", "!!"
|
haftmann@49446
|
308 |
];
|
haftmann@49446
|
309 |
|
haftmann@49446
|
310 |
val prelude_import_unqualified = [
|
haftmann@49446
|
311 |
"Eq",
|
haftmann@49446
|
312 |
"error",
|
haftmann@49446
|
313 |
"id",
|
haftmann@49446
|
314 |
"return",
|
haftmann@49446
|
315 |
"not",
|
haftmann@49446
|
316 |
"fst", "snd",
|
haftmann@49446
|
317 |
"map", "filter", "concat", "concatMap", "reverse", "zip", "null", "takeWhile", "dropWhile", "all", "any",
|
haftmann@49446
|
318 |
"Integer", "negate", "abs", "divMod",
|
haftmann@49446
|
319 |
"String"
|
haftmann@49446
|
320 |
];
|
haftmann@49446
|
321 |
|
haftmann@49446
|
322 |
val prelude_import_unqualified_constr = [
|
haftmann@49446
|
323 |
("Bool", ["True", "False"]),
|
haftmann@49446
|
324 |
("Maybe", ["Nothing", "Just"])
|
haftmann@49446
|
325 |
];
|
haftmann@49446
|
326 |
|
haftmann@39381
|
327 |
fun serialize_haskell module_prefix string_classes { labelled_name, reserved_syms,
|
haftmann@41591
|
328 |
includes, module_alias, class_syntax, tyco_syntax, const_syntax } program =
|
haftmann@28054
|
329 |
let
|
haftmann@39434
|
330 |
|
haftmann@39434
|
331 |
(* build program *)
|
haftmann@39152
|
332 |
val reserved = fold (insert (op =) o fst) includes reserved_syms;
|
haftmann@39434
|
333 |
val { deresolver, flat_program = haskell_program } = haskell_program_of_program
|
haftmann@39434
|
334 |
labelled_name module_alias module_prefix (Name.make_context reserved) program;
|
haftmann@39434
|
335 |
|
haftmann@39434
|
336 |
(* print statements *)
|
haftmann@28054
|
337 |
fun deriving_show tyco =
|
haftmann@28054
|
338 |
let
|
haftmann@28054
|
339 |
fun deriv _ "fun" = false
|
haftmann@34085
|
340 |
| deriv tycos tyco = not (tyco = Code_Thingol.fun_tyco)
|
haftmann@34085
|
341 |
andalso (member (op =) tycos tyco
|
haftmann@34085
|
342 |
orelse case try (Graph.get_node program) tyco
|
haftmann@28663
|
343 |
of SOME (Code_Thingol.Datatype (_, (_, cs))) => forall (deriv' (tyco :: tycos))
|
haftmann@28054
|
344 |
(maps snd cs)
|
haftmann@34085
|
345 |
| NONE => true)
|
haftmann@28054
|
346 |
and deriv' tycos (tyco `%% tys) = deriv tycos tyco
|
haftmann@28054
|
347 |
andalso forall (deriv' tycos) tys
|
haftmann@28054
|
348 |
| deriv' _ (ITyVar _) = true
|
haftmann@28054
|
349 |
in deriv [] tyco end;
|
haftmann@48472
|
350 |
fun print_stmt deresolve = print_haskell_stmt
|
haftmann@39434
|
351 |
class_syntax tyco_syntax const_syntax (make_vars reserved)
|
bulwahn@45880
|
352 |
deresolve (if string_classes then deriving_show else K false);
|
haftmann@39434
|
353 |
|
haftmann@39434
|
354 |
(* print modules *)
|
haftmann@39434
|
355 |
fun print_module_frame module_name ps =
|
haftmann@39434
|
356 |
(module_name, Pretty.chunks2 (
|
haftmann@39439
|
357 |
str ("module " ^ module_name ^ " where {")
|
haftmann@39434
|
358 |
:: ps
|
haftmann@39434
|
359 |
@| str "}"
|
haftmann@39434
|
360 |
));
|
haftmann@49446
|
361 |
fun print_qualified_import module_name = semicolon [str "import qualified", str module_name];
|
haftmann@49446
|
362 |
val import_common_ps =
|
haftmann@49446
|
363 |
enclose "import Prelude (" ");" (commas (map str
|
haftmann@49446
|
364 |
(map (Library.enclose "(" ")") prelude_import_operators @ prelude_import_unqualified)
|
haftmann@49446
|
365 |
@ map (fn (tyco, constrs) => (enclose (tyco ^ "(") ")" o commas o map str) constrs) prelude_import_unqualified_constr))
|
haftmann@49446
|
366 |
:: print_qualified_import "Prelude"
|
haftmann@49446
|
367 |
:: map (print_qualified_import o fst) includes;
|
haftmann@39434
|
368 |
fun print_module module_name (gr, imports) =
|
haftmann@28054
|
369 |
let
|
haftmann@49446
|
370 |
val deresolve = deresolver module_name;
|
haftmann@39434
|
371 |
fun print_import module_name = (semicolon o map str) ["import qualified", module_name];
|
haftmann@49446
|
372 |
val import_ps = import_common_ps @ map (print_qualified_import o fst) imports;
|
haftmann@49446
|
373 |
fun print_stmt' name = case Graph.get_node gr name
|
haftmann@39434
|
374 |
of (_, NONE) => NONE
|
haftmann@39434
|
375 |
| (_, SOME stmt) => SOME (markup_stmt name (print_stmt deresolve (name, stmt)));
|
haftmann@49446
|
376 |
val body_ps = map_filter print_stmt' ((flat o rev o Graph.strong_conn) gr);
|
haftmann@39434
|
377 |
in
|
haftmann@39434
|
378 |
print_module_frame module_name
|
haftmann@39434
|
379 |
((if null import_ps then [] else [Pretty.chunks import_ps]) @ body_ps)
|
haftmann@39434
|
380 |
end;
|
haftmann@39434
|
381 |
|
haftmann@39434
|
382 |
(*serialization*)
|
haftmann@39434
|
383 |
fun write_module width (SOME destination) (module_name, content) =
|
haftmann@39141
|
384 |
let
|
wenzelm@42874
|
385 |
val _ = File.check_dir destination;
|
haftmann@39434
|
386 |
val filepath = (Path.append destination o Path.ext "hs" o Path.explode o implode
|
haftmann@39434
|
387 |
o separate "/" o Long_Name.explode) module_name;
|
haftmann@41487
|
388 |
val _ = Isabelle_System.mkdirs (Path.dir filepath);
|
haftmann@39439
|
389 |
in
|
haftmann@39439
|
390 |
(File.write filepath o format [] width o Pretty.chunks2)
|
noschinl@45797
|
391 |
[str language_pragma, content]
|
haftmann@39439
|
392 |
end
|
haftmann@39290
|
393 |
| write_module width NONE (_, content) = writeln (format [] width content);
|
haftmann@28054
|
394 |
in
|
haftmann@39142
|
395 |
Code_Target.serialization
|
haftmann@39141
|
396 |
(fn width => fn destination => K () o map (write_module width destination))
|
haftmann@40953
|
397 |
(fn present => fn width => rpair (try (deresolver ""))
|
haftmann@39434
|
398 |
o format present width o Pretty.chunks o map snd)
|
haftmann@39434
|
399 |
(map (uncurry print_module_frame o apsnd single) includes
|
haftmann@39434
|
400 |
@ map (fn module_name => print_module module_name (Graph.get_node haskell_program module_name))
|
haftmann@39434
|
401 |
((flat o rev o Graph.strong_conn) haskell_program))
|
haftmann@28054
|
402 |
end;
|
haftmann@28054
|
403 |
|
haftmann@39192
|
404 |
val serializer : Code_Target.serializer =
|
haftmann@39436
|
405 |
Code_Target.parse_args (Scan.optional (Args.$$$ "root" -- Args.colon |-- Args.name) ""
|
haftmann@39192
|
406 |
-- Scan.optional (Args.$$$ "string_classes" >> K true) false
|
haftmann@39192
|
407 |
>> (fn (module_prefix, string_classes) =>
|
haftmann@39192
|
408 |
serialize_haskell module_prefix string_classes));
|
haftmann@39192
|
409 |
|
haftmann@28064
|
410 |
val literals = let
|
haftmann@28064
|
411 |
fun char_haskell c =
|
haftmann@28064
|
412 |
let
|
haftmann@28064
|
413 |
val s = ML_Syntax.print_char c;
|
haftmann@28064
|
414 |
in if s = "'" then "\\'" else s end;
|
haftmann@34931
|
415 |
fun numeral_haskell k = if k >= 0 then string_of_int k
|
haftmann@34931
|
416 |
else Library.enclose "(" ")" (signed_string_of_int k);
|
haftmann@28064
|
417 |
in Literals {
|
haftmann@34178
|
418 |
literal_char = Library.enclose "'" "'" o char_haskell,
|
haftmann@28064
|
419 |
literal_string = quote o translate_string char_haskell,
|
haftmann@34931
|
420 |
literal_numeral = numeral_haskell,
|
haftmann@34931
|
421 |
literal_positive_numeral = numeral_haskell,
|
haftmann@38195
|
422 |
literal_alternative_numeral = numeral_haskell,
|
haftmann@34931
|
423 |
literal_naive_numeral = numeral_haskell,
|
haftmann@34178
|
424 |
literal_list = enum "," "[" "]",
|
haftmann@28064
|
425 |
infix_cons = (5, ":")
|
haftmann@28064
|
426 |
} end;
|
haftmann@28064
|
427 |
|
haftmann@28054
|
428 |
|
haftmann@28054
|
429 |
(** optional monad syntax **)
|
haftmann@28054
|
430 |
|
haftmann@28054
|
431 |
fun pretty_haskell_monad c_bind =
|
haftmann@28054
|
432 |
let
|
haftmann@31873
|
433 |
fun dest_bind t1 t2 = case Code_Thingol.split_pat_abs t2
|
haftmann@31889
|
434 |
of SOME ((pat, ty), t') =>
|
haftmann@31889
|
435 |
SOME ((SOME ((pat, ty), true), t1), t')
|
haftmann@28145
|
436 |
| NONE => NONE;
|
haftmann@49087
|
437 |
fun dest_monad c_bind_name (IConst { name = c, ... } `$ t1 `$ t2) =
|
haftmann@28663
|
438 |
if c = c_bind_name then dest_bind t1 t2
|
haftmann@28145
|
439 |
else NONE
|
haftmann@28663
|
440 |
| dest_monad _ t = case Code_Thingol.split_let t
|
haftmann@28145
|
441 |
of SOME (((pat, ty), tbind), t') =>
|
haftmann@31889
|
442 |
SOME ((SOME ((pat, ty), false), tbind), t')
|
haftmann@28145
|
443 |
| NONE => NONE;
|
haftmann@28663
|
444 |
fun implode_monad c_bind_name = Code_Thingol.unfoldr (dest_monad c_bind_name);
|
haftmann@33988
|
445 |
fun print_monad print_bind print_term (NONE, t) vars =
|
haftmann@33988
|
446 |
(semicolon [print_term vars NOBR t], vars)
|
haftmann@33988
|
447 |
| print_monad print_bind print_term (SOME ((bind, _), true), t) vars = vars
|
haftmann@33988
|
448 |
|> print_bind NOBR bind
|
haftmann@33988
|
449 |
|>> (fn p => semicolon [p, str "<-", print_term vars NOBR t])
|
haftmann@33988
|
450 |
| print_monad print_bind print_term (SOME ((bind, _), false), t) vars = vars
|
haftmann@33988
|
451 |
|> print_bind NOBR bind
|
haftmann@37832
|
452 |
|>> (fn p => semicolon [str "let", str "{", p, str "=", print_term vars NOBR t, str "}"]);
|
haftmann@33988
|
453 |
fun pretty _ [c_bind'] print_term thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
|
haftmann@28145
|
454 |
of SOME (bind, t') => let
|
haftmann@31054
|
455 |
val (binds, t'') = implode_monad c_bind' t'
|
haftmann@33988
|
456 |
val (ps, vars') = fold_map (print_monad (gen_print_bind (K print_term) thm) print_term)
|
haftmann@33988
|
457 |
(bind :: binds) vars;
|
haftmann@33988
|
458 |
in
|
haftmann@37833
|
459 |
(brackify fxy o single o enclose "do { " " }" o Pretty.breaks)
|
haftmann@33988
|
460 |
(ps @| print_term vars' NOBR t'')
|
haftmann@33988
|
461 |
end
|
haftmann@28145
|
462 |
| NONE => brackify_infix (1, L) fxy
|
haftmann@37239
|
463 |
(print_term vars (INFX (1, L)) t1, str ">>=", print_term vars (INFX (1, X)) t2)
|
haftmann@31054
|
464 |
in (2, ([c_bind], pretty)) end;
|
haftmann@28054
|
465 |
|
haftmann@28145
|
466 |
fun add_monad target' raw_c_bind thy =
|
haftmann@28054
|
467 |
let
|
haftmann@31156
|
468 |
val c_bind = Code.read_const thy raw_c_bind;
|
haftmann@28054
|
469 |
in if target = target' then
|
haftmann@28054
|
470 |
thy
|
haftmann@39149
|
471 |
|> Code_Target.add_const_syntax target c_bind
|
haftmann@37854
|
472 |
(SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind)))
|
haftmann@28054
|
473 |
else error "Only Haskell target allows for monad syntax" end;
|
haftmann@28054
|
474 |
|
haftmann@28054
|
475 |
|
haftmann@28054
|
476 |
(** Isar setup **)
|
haftmann@28054
|
477 |
|
haftmann@28054
|
478 |
val _ =
|
wenzelm@47836
|
479 |
Outer_Syntax.command @{command_spec "code_monad"} "define code syntax for monads"
|
wenzelm@47836
|
480 |
(Parse.term_group -- Parse.name >> (fn (raw_bind, target) =>
|
wenzelm@47836
|
481 |
Toplevel.theory (add_monad target raw_bind)));
|
haftmann@28054
|
482 |
|
haftmann@28054
|
483 |
val setup =
|
haftmann@37821
|
484 |
Code_Target.add_target
|
haftmann@39192
|
485 |
(target, { serializer = serializer, literals = literals,
|
wenzelm@42823
|
486 |
check = { env_var = "ISABELLE_GHC", make_destination = I,
|
wenzelm@42811
|
487 |
make_command = fn module_name =>
|
noschinl@45797
|
488 |
"\"$ISABELLE_GHC\" " ^ language_params ^ " -odir build -hidir build -stubdir build -e \"\" " ^
|
wenzelm@42811
|
489 |
module_name ^ ".hs" } })
|
haftmann@39149
|
490 |
#> Code_Target.add_tyco_syntax target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
|
haftmann@37239
|
491 |
brackify_infix (1, R) fxy (
|
haftmann@33988
|
492 |
print_typ (INFX (1, X)) ty1,
|
haftmann@28054
|
493 |
str "->",
|
haftmann@33988
|
494 |
print_typ (INFX (1, R)) ty2
|
haftmann@37239
|
495 |
)))
|
haftmann@28054
|
496 |
#> fold (Code_Target.add_reserved target) [
|
haftmann@28054
|
497 |
"hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
|
haftmann@28054
|
498 |
"import", "default", "forall", "let", "in", "class", "qualified", "data",
|
haftmann@28054
|
499 |
"newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
|
haftmann@28054
|
500 |
]
|
haftmann@49446
|
501 |
#> fold (Code_Target.add_reserved target) prelude_import_unqualified
|
haftmann@49446
|
502 |
#> fold (Code_Target.add_reserved target o fst) prelude_import_unqualified_constr
|
haftmann@49446
|
503 |
#> fold (fold (Code_Target.add_reserved target) o snd) prelude_import_unqualified_constr;
|
haftmann@28054
|
504 |
|
haftmann@28054
|
505 |
end; (*struct*)
|