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
|
haftmann@37744
|
9 |
val target: string
|
haftmann@28054
|
10 |
val setup: theory -> theory
|
haftmann@28054
|
11 |
end;
|
haftmann@28054
|
12 |
|
haftmann@28054
|
13 |
structure Code_Haskell : CODE_HASKELL =
|
haftmann@28054
|
14 |
struct
|
haftmann@28054
|
15 |
|
haftmann@28054
|
16 |
val target = "Haskell";
|
haftmann@28054
|
17 |
|
haftmann@28054
|
18 |
open Basic_Code_Thingol;
|
haftmann@28054
|
19 |
open Code_Printer;
|
haftmann@28054
|
20 |
|
haftmann@28054
|
21 |
infixr 5 @@;
|
haftmann@28054
|
22 |
infixr 5 @|;
|
haftmann@28054
|
23 |
|
haftmann@28054
|
24 |
|
haftmann@28054
|
25 |
(** Haskell serializer **)
|
haftmann@28054
|
26 |
|
haftmann@39149
|
27 |
fun print_haskell_stmt labelled_name class_syntax tyco_syntax const_syntax
|
haftmann@32924
|
28 |
reserved deresolve contr_classparam_typs deriving_show =
|
haftmann@28054
|
29 |
let
|
haftmann@39149
|
30 |
fun class_name class = case class_syntax class
|
haftmann@28054
|
31 |
of NONE => deresolve class
|
haftmann@28687
|
32 |
| SOME class => class;
|
haftmann@33988
|
33 |
fun print_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs
|
haftmann@28054
|
34 |
of [] => []
|
haftmann@37359
|
35 |
| constraints => enum "," "(" ")" (
|
haftmann@28054
|
36 |
map (fn (v, class) =>
|
haftmann@37359
|
37 |
str (class_name class ^ " " ^ lookup_var tyvars v)) constraints)
|
haftmann@28054
|
38 |
@@ str " => ";
|
haftmann@33988
|
39 |
fun print_typforall tyvars vs = case map fst vs
|
haftmann@28054
|
40 |
of [] => []
|
haftmann@28054
|
41 |
| vnames => str "forall " :: Pretty.breaks
|
haftmann@32924
|
42 |
(map (str o lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
|
haftmann@33988
|
43 |
fun print_tyco_expr tyvars fxy (tyco, tys) =
|
haftmann@33988
|
44 |
brackify fxy (str tyco :: map (print_typ tyvars BR) tys)
|
haftmann@39149
|
45 |
and print_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case tyco_syntax tyco
|
haftmann@33988
|
46 |
of NONE => print_tyco_expr tyvars fxy (deresolve tyco, tys)
|
haftmann@33988
|
47 |
| SOME (i, print) => print (print_typ tyvars) fxy tys)
|
haftmann@33988
|
48 |
| print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v;
|
haftmann@33988
|
49 |
fun print_typdecl tyvars (vs, tycoexpr) =
|
haftmann@33988
|
50 |
Pretty.block (print_typcontext tyvars vs @| print_tyco_expr tyvars NOBR tycoexpr);
|
haftmann@33988
|
51 |
fun print_typscheme tyvars (vs, ty) =
|
haftmann@33988
|
52 |
Pretty.block (print_typforall tyvars vs @ print_typcontext tyvars vs @| print_typ tyvars NOBR ty);
|
haftmann@35228
|
53 |
fun print_term tyvars some_thm vars fxy (IConst c) =
|
haftmann@35228
|
54 |
print_app tyvars some_thm vars fxy (c, [])
|
haftmann@35228
|
55 |
| print_term tyvars some_thm vars fxy (t as (t1 `$ t2)) =
|
haftmann@28054
|
56 |
(case Code_Thingol.unfold_const_app t
|
haftmann@35228
|
57 |
of SOME app => print_app tyvars some_thm vars fxy app
|
haftmann@28054
|
58 |
| _ =>
|
haftmann@28054
|
59 |
brackify fxy [
|
haftmann@35228
|
60 |
print_term tyvars some_thm vars NOBR t1,
|
haftmann@35228
|
61 |
print_term tyvars some_thm vars BR t2
|
haftmann@28054
|
62 |
])
|
haftmann@35228
|
63 |
| print_term tyvars some_thm vars fxy (IVar NONE) =
|
haftmann@31889
|
64 |
str "_"
|
haftmann@35228
|
65 |
| print_term tyvars some_thm vars fxy (IVar (SOME v)) =
|
haftmann@32924
|
66 |
(str o lookup_var vars) v
|
haftmann@35228
|
67 |
| print_term tyvars some_thm vars fxy (t as _ `|=> _) =
|
haftmann@28054
|
68 |
let
|
haftmann@31873
|
69 |
val (binds, t') = Code_Thingol.unfold_pat_abs t;
|
haftmann@35228
|
70 |
val (ps, vars') = fold_map (print_bind tyvars some_thm BR o fst) binds vars;
|
haftmann@35228
|
71 |
in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars some_thm vars' NOBR t') end
|
haftmann@35228
|
72 |
| print_term tyvars some_thm vars fxy (ICase (cases as (_, t0))) =
|
haftmann@28054
|
73 |
(case Code_Thingol.unfold_const_app t0
|
haftmann@39149
|
74 |
of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
|
haftmann@35228
|
75 |
then print_case tyvars some_thm vars fxy cases
|
haftmann@35228
|
76 |
else print_app tyvars some_thm vars fxy c_ts
|
haftmann@35228
|
77 |
| NONE => print_case tyvars some_thm vars fxy cases)
|
haftmann@37424
|
78 |
and print_app_expr tyvars some_thm vars ((c, (_, function_typs)), ts) = case contr_classparam_typs c
|
haftmann@35228
|
79 |
of [] => (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts
|
haftmann@28054
|
80 |
| fingerprint => let
|
haftmann@33956
|
81 |
val ts_fingerprint = ts ~~ take (length ts) fingerprint;
|
haftmann@28054
|
82 |
val needs_annotation = forall (fn (_, NONE) => true | (t, SOME _) =>
|
haftmann@28054
|
83 |
(not o Code_Thingol.locally_monomorphic) t) ts_fingerprint;
|
haftmann@35228
|
84 |
fun print_term_anno (t, NONE) _ = print_term tyvars some_thm vars BR t
|
haftmann@33988
|
85 |
| print_term_anno (t, SOME _) ty =
|
haftmann@35228
|
86 |
brackets [print_term tyvars some_thm vars NOBR t, str "::", print_typ tyvars NOBR ty];
|
haftmann@28054
|
87 |
in
|
haftmann@28054
|
88 |
if needs_annotation then
|
haftmann@37424
|
89 |
(str o deresolve) c :: map2 print_term_anno ts_fingerprint (take (length ts) function_typs)
|
haftmann@35228
|
90 |
else (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts
|
haftmann@28054
|
91 |
end
|
haftmann@39149
|
92 |
and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) const_syntax
|
haftmann@35228
|
93 |
and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p
|
haftmann@35228
|
94 |
and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
|
haftmann@28054
|
95 |
let
|
haftmann@29889
|
96 |
val (binds, body) = Code_Thingol.unfold_let (ICase cases);
|
haftmann@33988
|
97 |
fun print_match ((pat, ty), t) vars =
|
haftmann@28054
|
98 |
vars
|
haftmann@35228
|
99 |
|> print_bind tyvars some_thm BR pat
|
haftmann@35228
|
100 |
|>> (fn p => semicolon [p, str "=", print_term tyvars some_thm vars NOBR t])
|
haftmann@33988
|
101 |
val (ps, vars') = fold_map print_match binds vars;
|
haftmann@31665
|
102 |
in brackify_block fxy (str "let {")
|
haftmann@31665
|
103 |
ps
|
haftmann@35228
|
104 |
(concat [str "}", str "in", print_term tyvars some_thm vars' NOBR body])
|
haftmann@28054
|
105 |
end
|
haftmann@35228
|
106 |
| print_case tyvars some_thm vars fxy (((t, ty), clauses as _ :: _), _) =
|
haftmann@28054
|
107 |
let
|
haftmann@33988
|
108 |
fun print_select (pat, body) =
|
haftmann@28054
|
109 |
let
|
haftmann@35228
|
110 |
val (p, vars') = print_bind tyvars some_thm NOBR pat vars;
|
haftmann@35228
|
111 |
in semicolon [p, str "->", print_term tyvars some_thm vars' NOBR body] end;
|
haftmann@36574
|
112 |
in Pretty.block_enclose
|
haftmann@36574
|
113 |
(concat [str "(case", print_term tyvars some_thm vars NOBR t, str "of", str "{"], str "})")
|
haftmann@33988
|
114 |
(map print_select clauses)
|
haftmann@28054
|
115 |
end
|
haftmann@35228
|
116 |
| print_case tyvars some_thm vars fxy ((_, []), _) =
|
haftmann@31376
|
117 |
(brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""];
|
haftmann@37412
|
118 |
fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
|
haftmann@28054
|
119 |
let
|
haftmann@32924
|
120 |
val tyvars = intro_vars (map fst vs) reserved;
|
haftmann@34262
|
121 |
fun print_err n =
|
haftmann@33988
|
122 |
semicolon (
|
haftmann@39437
|
123 |
(str o deresolve) name
|
haftmann@28054
|
124 |
:: map str (replicate n "_")
|
haftmann@28054
|
125 |
@ str "="
|
haftmann@28054
|
126 |
:: str "error"
|
haftmann@33988
|
127 |
@@ (str o ML_Syntax.print_string
|
wenzelm@30364
|
128 |
o Long_Name.base_name o Long_Name.qualifier) name
|
haftmann@34262
|
129 |
);
|
haftmann@35228
|
130 |
fun print_eqn ((ts, t), (some_thm, _)) =
|
haftmann@28054
|
131 |
let
|
haftmann@32913
|
132 |
val consts = fold Code_Thingol.add_constnames (t :: ts) [];
|
haftmann@32924
|
133 |
val vars = reserved
|
haftmann@32924
|
134 |
|> intro_base_names
|
haftmann@39149
|
135 |
(is_none o const_syntax) deresolve consts
|
haftmann@32924
|
136 |
|> intro_vars ((fold o Code_Thingol.fold_varnames)
|
haftmann@32925
|
137 |
(insert (op =)) ts []);
|
haftmann@28054
|
138 |
in
|
haftmann@28054
|
139 |
semicolon (
|
haftmann@39437
|
140 |
(str o deresolve) name
|
haftmann@35228
|
141 |
:: map (print_term tyvars some_thm vars BR) ts
|
haftmann@28054
|
142 |
@ str "="
|
haftmann@35228
|
143 |
@@ print_term tyvars some_thm vars NOBR t
|
haftmann@28054
|
144 |
)
|
haftmann@28054
|
145 |
end;
|
haftmann@28054
|
146 |
in
|
haftmann@28054
|
147 |
Pretty.chunks (
|
haftmann@33988
|
148 |
semicolon [
|
haftmann@39437
|
149 |
(str o suffix " ::" o deresolve) name,
|
haftmann@33988
|
150 |
print_typscheme tyvars (vs, ty)
|
haftmann@28054
|
151 |
]
|
haftmann@34262
|
152 |
:: (case filter (snd o snd) raw_eqs
|
haftmann@34262
|
153 |
of [] => [print_err ((length o fst o Code_Thingol.unfold_fun) ty)]
|
haftmann@34262
|
154 |
| eqs => map print_eqn eqs)
|
haftmann@28054
|
155 |
)
|
haftmann@28054
|
156 |
end
|
haftmann@33988
|
157 |
| print_stmt (name, Code_Thingol.Datatype (_, (vs, []))) =
|
haftmann@28054
|
158 |
let
|
haftmann@32924
|
159 |
val tyvars = intro_vars (map fst vs) reserved;
|
haftmann@28054
|
160 |
in
|
haftmann@28054
|
161 |
semicolon [
|
haftmann@28054
|
162 |
str "data",
|
haftmann@39437
|
163 |
print_typdecl tyvars (vs, (deresolve name, map (ITyVar o fst) vs))
|
haftmann@28054
|
164 |
]
|
haftmann@28054
|
165 |
end
|
haftmann@37424
|
166 |
| print_stmt (name, Code_Thingol.Datatype (_, (vs, [((co, _), [ty])]))) =
|
haftmann@28054
|
167 |
let
|
haftmann@32924
|
168 |
val tyvars = intro_vars (map fst vs) reserved;
|
haftmann@28054
|
169 |
in
|
haftmann@28054
|
170 |
semicolon (
|
haftmann@28054
|
171 |
str "newtype"
|
haftmann@39437
|
172 |
:: print_typdecl tyvars (vs, (deresolve name, map (ITyVar o fst) vs))
|
haftmann@28054
|
173 |
:: str "="
|
haftmann@39437
|
174 |
:: (str o deresolve) co
|
haftmann@33988
|
175 |
:: print_typ tyvars BR ty
|
haftmann@28054
|
176 |
:: (if deriving_show name then [str "deriving (Read, Show)"] else [])
|
haftmann@28054
|
177 |
)
|
haftmann@28054
|
178 |
end
|
haftmann@33988
|
179 |
| print_stmt (name, Code_Thingol.Datatype (_, (vs, co :: cos))) =
|
haftmann@28054
|
180 |
let
|
haftmann@32924
|
181 |
val tyvars = intro_vars (map fst vs) reserved;
|
haftmann@37424
|
182 |
fun print_co ((co, _), tys) =
|
haftmann@28054
|
183 |
concat (
|
haftmann@39437
|
184 |
(str o deresolve) co
|
haftmann@33988
|
185 |
:: map (print_typ tyvars BR) tys
|
haftmann@28054
|
186 |
)
|
haftmann@28054
|
187 |
in
|
haftmann@28054
|
188 |
semicolon (
|
haftmann@28054
|
189 |
str "data"
|
haftmann@39437
|
190 |
:: print_typdecl tyvars (vs, (deresolve name, map (ITyVar o fst) vs))
|
haftmann@28054
|
191 |
:: str "="
|
haftmann@33988
|
192 |
:: print_co co
|
haftmann@33988
|
193 |
:: map ((fn p => Pretty.block [str "| ", p]) o print_co) cos
|
haftmann@28054
|
194 |
@ (if deriving_show name then [str "deriving (Read, Show)"] else [])
|
haftmann@28054
|
195 |
)
|
haftmann@28054
|
196 |
end
|
haftmann@37422
|
197 |
| print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
|
haftmann@28054
|
198 |
let
|
haftmann@32924
|
199 |
val tyvars = intro_vars [v] reserved;
|
haftmann@33988
|
200 |
fun print_classparam (classparam, ty) =
|
haftmann@28054
|
201 |
semicolon [
|
haftmann@39437
|
202 |
(str o deresolve) classparam,
|
haftmann@28054
|
203 |
str "::",
|
haftmann@33988
|
204 |
print_typ tyvars NOBR ty
|
haftmann@28054
|
205 |
]
|
haftmann@28054
|
206 |
in
|
haftmann@28054
|
207 |
Pretty.block_enclose (
|
haftmann@28054
|
208 |
Pretty.block [
|
haftmann@28054
|
209 |
str "class ",
|
haftmann@37359
|
210 |
Pretty.block (print_typcontext tyvars [(v, map fst super_classes)]),
|
haftmann@39437
|
211 |
str (deresolve name ^ " " ^ lookup_var tyvars v),
|
haftmann@28054
|
212 |
str " where {"
|
haftmann@28054
|
213 |
],
|
haftmann@28054
|
214 |
str "};"
|
haftmann@33988
|
215 |
) (map print_classparam classparams)
|
haftmann@28054
|
216 |
end
|
haftmann@37424
|
217 |
| print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, (classparam_instances, _)))) =
|
haftmann@28054
|
218 |
let
|
haftmann@32924
|
219 |
val tyvars = intro_vars (map fst vs) reserved;
|
haftmann@39149
|
220 |
fun requires_args classparam = case const_syntax classparam
|
haftmann@39437
|
221 |
of NONE => NONE
|
haftmann@39437
|
222 |
| SOME (Code_Printer.Plain_const_syntax _) => SOME 0
|
haftmann@39437
|
223 |
| SOME (Code_Printer.Complex_const_syntax (k,_ )) => SOME k;
|
haftmann@37854
|
224 |
fun print_classparam_instance ((classparam, const), (thm, _)) =
|
haftmann@37854
|
225 |
case requires_args classparam
|
haftmann@39437
|
226 |
of NONE => semicolon [
|
haftmann@39437
|
227 |
(str o Long_Name.base_name o deresolve) classparam,
|
haftmann@28687
|
228 |
str "=",
|
haftmann@37854
|
229 |
print_app tyvars (SOME thm) reserved NOBR (const, [])
|
haftmann@28687
|
230 |
]
|
haftmann@39437
|
231 |
| SOME k =>
|
haftmann@37854
|
232 |
let
|
haftmann@37854
|
233 |
val (c, (_, tys)) = const;
|
haftmann@37854
|
234 |
val (vs, rhs) = (apfst o map) fst
|
haftmann@37854
|
235 |
(Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
|
haftmann@39149
|
236 |
val s = if (is_some o const_syntax) c
|
haftmann@37854
|
237 |
then NONE else (SOME o Long_Name.base_name o deresolve) c;
|
haftmann@37854
|
238 |
val vars = reserved
|
haftmann@37854
|
239 |
|> intro_vars (map_filter I (s :: vs));
|
haftmann@37854
|
240 |
val lhs = IConst (classparam, (([], []), tys)) `$$ map IVar vs;
|
haftmann@37854
|
241 |
(*dictionaries are not relevant at this late stage*)
|
haftmann@37854
|
242 |
in
|
haftmann@37854
|
243 |
semicolon [
|
haftmann@37854
|
244 |
print_term tyvars (SOME thm) vars NOBR lhs,
|
haftmann@37854
|
245 |
str "=",
|
haftmann@37854
|
246 |
print_term tyvars (SOME thm) vars NOBR rhs
|
haftmann@37854
|
247 |
]
|
haftmann@37854
|
248 |
end;
|
haftmann@28054
|
249 |
in
|
haftmann@28054
|
250 |
Pretty.block_enclose (
|
haftmann@28054
|
251 |
Pretty.block [
|
haftmann@28054
|
252 |
str "instance ",
|
haftmann@33988
|
253 |
Pretty.block (print_typcontext tyvars vs),
|
haftmann@28054
|
254 |
str (class_name class ^ " "),
|
haftmann@33988
|
255 |
print_typ tyvars BR (tyco `%% map (ITyVar o fst) vs),
|
haftmann@28054
|
256 |
str " where {"
|
haftmann@28054
|
257 |
],
|
haftmann@28054
|
258 |
str "};"
|
haftmann@37359
|
259 |
) (map print_classparam_instance classparam_instances)
|
haftmann@28054
|
260 |
end;
|
haftmann@33988
|
261 |
in print_stmt end;
|
haftmann@28054
|
262 |
|
haftmann@39432
|
263 |
fun haskell_program_of_program labelled_name module_alias module_prefix reserved =
|
haftmann@39432
|
264 |
let
|
haftmann@39432
|
265 |
fun namify_fun upper base (nsp_fun, nsp_typ) =
|
haftmann@39432
|
266 |
let
|
haftmann@39432
|
267 |
val (base', nsp_fun') = yield_singleton Name.variants
|
haftmann@39432
|
268 |
(if upper then first_upper base else base) nsp_fun;
|
haftmann@39432
|
269 |
in (base', (nsp_fun', nsp_typ)) end;
|
haftmann@39432
|
270 |
fun namify_typ base (nsp_fun, nsp_typ) =
|
haftmann@39432
|
271 |
let
|
haftmann@39432
|
272 |
val (base', nsp_typ') = yield_singleton Name.variants
|
haftmann@39432
|
273 |
(first_upper base) nsp_typ
|
haftmann@39432
|
274 |
in (base', (nsp_fun, nsp_typ')) end;
|
haftmann@39432
|
275 |
fun namify_stmt (Code_Thingol.Fun (_, (_, SOME _))) = pair
|
haftmann@39432
|
276 |
| namify_stmt (Code_Thingol.Fun _) = namify_fun false
|
haftmann@39432
|
277 |
| namify_stmt (Code_Thingol.Datatype _) = namify_typ
|
haftmann@39432
|
278 |
| namify_stmt (Code_Thingol.Datatypecons _) = namify_fun true
|
haftmann@39432
|
279 |
| namify_stmt (Code_Thingol.Class _) = namify_typ
|
haftmann@39432
|
280 |
| namify_stmt (Code_Thingol.Classrel _) = pair
|
haftmann@39432
|
281 |
| namify_stmt (Code_Thingol.Classparam _) = namify_fun false
|
haftmann@39432
|
282 |
| namify_stmt (Code_Thingol.Classinst _) = pair;
|
haftmann@39432
|
283 |
fun select_stmt (Code_Thingol.Fun (_, (_, SOME _))) = false
|
haftmann@39432
|
284 |
| select_stmt (Code_Thingol.Fun _) = true
|
haftmann@39432
|
285 |
| select_stmt (Code_Thingol.Datatype _) = true
|
haftmann@39432
|
286 |
| select_stmt (Code_Thingol.Datatypecons _) = false
|
haftmann@39432
|
287 |
| select_stmt (Code_Thingol.Class _) = true
|
haftmann@39432
|
288 |
| select_stmt (Code_Thingol.Classrel _) = false
|
haftmann@39432
|
289 |
| select_stmt (Code_Thingol.Classparam _) = false
|
haftmann@39432
|
290 |
| select_stmt (Code_Thingol.Classinst _) = true;
|
haftmann@39432
|
291 |
in
|
haftmann@39436
|
292 |
Code_Namespace.flat_program labelled_name
|
haftmann@39432
|
293 |
{ module_alias = module_alias, module_prefix = module_prefix,
|
haftmann@39432
|
294 |
reserved = reserved, empty_nsp = (reserved, reserved), namify_stmt = namify_stmt,
|
haftmann@39432
|
295 |
modify_stmt = fn stmt => if select_stmt stmt then SOME stmt else NONE }
|
haftmann@39432
|
296 |
end;
|
haftmann@39432
|
297 |
|
haftmann@39381
|
298 |
fun serialize_haskell module_prefix string_classes { labelled_name, reserved_syms,
|
haftmann@41591
|
299 |
includes, module_alias, class_syntax, tyco_syntax, const_syntax } program =
|
haftmann@28054
|
300 |
let
|
haftmann@39434
|
301 |
|
haftmann@39434
|
302 |
(* build program *)
|
haftmann@39152
|
303 |
val reserved = fold (insert (op =) o fst) includes reserved_syms;
|
haftmann@39434
|
304 |
val { deresolver, flat_program = haskell_program } = haskell_program_of_program
|
haftmann@39434
|
305 |
labelled_name module_alias module_prefix (Name.make_context reserved) program;
|
haftmann@39434
|
306 |
|
haftmann@39434
|
307 |
(* print statements *)
|
haftmann@28054
|
308 |
val contr_classparam_typs = Code_Thingol.contr_classparam_typs program;
|
haftmann@28054
|
309 |
fun deriving_show tyco =
|
haftmann@28054
|
310 |
let
|
haftmann@28054
|
311 |
fun deriv _ "fun" = false
|
haftmann@34085
|
312 |
| deriv tycos tyco = not (tyco = Code_Thingol.fun_tyco)
|
haftmann@34085
|
313 |
andalso (member (op =) tycos tyco
|
haftmann@34085
|
314 |
orelse case try (Graph.get_node program) tyco
|
haftmann@28663
|
315 |
of SOME (Code_Thingol.Datatype (_, (_, cs))) => forall (deriv' (tyco :: tycos))
|
haftmann@28054
|
316 |
(maps snd cs)
|
haftmann@34085
|
317 |
| NONE => true)
|
haftmann@28054
|
318 |
and deriv' tycos (tyco `%% tys) = deriv tycos tyco
|
haftmann@28054
|
319 |
andalso forall (deriv' tycos) tys
|
haftmann@28054
|
320 |
| deriv' _ (ITyVar _) = true
|
haftmann@28054
|
321 |
in deriv [] tyco end;
|
haftmann@39434
|
322 |
fun print_stmt deresolve = print_haskell_stmt labelled_name
|
haftmann@39434
|
323 |
class_syntax tyco_syntax const_syntax (make_vars reserved)
|
haftmann@39434
|
324 |
deresolve contr_classparam_typs
|
haftmann@28054
|
325 |
(if string_classes then deriving_show else K false);
|
haftmann@39434
|
326 |
|
haftmann@39434
|
327 |
(* print modules *)
|
haftmann@39434
|
328 |
val import_includes_ps =
|
haftmann@39434
|
329 |
map (fn (name, _) => str ("import qualified " ^ name ^ ";")) includes;
|
haftmann@39434
|
330 |
fun print_module_frame module_name ps =
|
haftmann@39434
|
331 |
(module_name, Pretty.chunks2 (
|
haftmann@39439
|
332 |
str ("module " ^ module_name ^ " where {")
|
haftmann@39434
|
333 |
:: ps
|
haftmann@39434
|
334 |
@| str "}"
|
haftmann@39434
|
335 |
));
|
haftmann@39434
|
336 |
fun print_module module_name (gr, imports) =
|
haftmann@28054
|
337 |
let
|
haftmann@39434
|
338 |
val deresolve = deresolver module_name
|
haftmann@39434
|
339 |
fun print_import module_name = (semicolon o map str) ["import qualified", module_name];
|
haftmann@39434
|
340 |
val import_ps = import_includes_ps @ map (print_import o fst) imports;
|
haftmann@39434
|
341 |
fun print_stmt' gr name = case Graph.get_node gr name
|
haftmann@39434
|
342 |
of (_, NONE) => NONE
|
haftmann@39434
|
343 |
| (_, SOME stmt) => SOME (markup_stmt name (print_stmt deresolve (name, stmt)));
|
haftmann@39434
|
344 |
val body_ps = map_filter (print_stmt' gr) ((flat o rev o Graph.strong_conn) gr);
|
haftmann@39434
|
345 |
in
|
haftmann@39434
|
346 |
print_module_frame module_name
|
haftmann@39434
|
347 |
((if null import_ps then [] else [Pretty.chunks import_ps]) @ body_ps)
|
haftmann@39434
|
348 |
end;
|
haftmann@39434
|
349 |
|
haftmann@39434
|
350 |
(*serialization*)
|
haftmann@39434
|
351 |
fun write_module width (SOME destination) (module_name, content) =
|
haftmann@39141
|
352 |
let
|
haftmann@39141
|
353 |
val _ = File.check destination;
|
haftmann@39434
|
354 |
val filepath = (Path.append destination o Path.ext "hs" o Path.explode o implode
|
haftmann@39434
|
355 |
o separate "/" o Long_Name.explode) module_name;
|
haftmann@41487
|
356 |
val _ = Isabelle_System.mkdirs (Path.dir filepath);
|
haftmann@39439
|
357 |
in
|
haftmann@39439
|
358 |
(File.write filepath o format [] width o Pretty.chunks2)
|
haftmann@41050
|
359 |
[str "{-# LANGUAGE ScopedTypeVariables #-}", content]
|
haftmann@39439
|
360 |
end
|
haftmann@39290
|
361 |
| write_module width NONE (_, content) = writeln (format [] width content);
|
haftmann@28054
|
362 |
in
|
haftmann@39142
|
363 |
Code_Target.serialization
|
haftmann@39141
|
364 |
(fn width => fn destination => K () o map (write_module width destination))
|
haftmann@40953
|
365 |
(fn present => fn width => rpair (try (deresolver ""))
|
haftmann@39434
|
366 |
o format present width o Pretty.chunks o map snd)
|
haftmann@39434
|
367 |
(map (uncurry print_module_frame o apsnd single) includes
|
haftmann@39434
|
368 |
@ map (fn module_name => print_module module_name (Graph.get_node haskell_program module_name))
|
haftmann@39434
|
369 |
((flat o rev o Graph.strong_conn) haskell_program))
|
haftmann@28054
|
370 |
end;
|
haftmann@28054
|
371 |
|
haftmann@39192
|
372 |
val serializer : Code_Target.serializer =
|
haftmann@39436
|
373 |
Code_Target.parse_args (Scan.optional (Args.$$$ "root" -- Args.colon |-- Args.name) ""
|
haftmann@39192
|
374 |
-- Scan.optional (Args.$$$ "string_classes" >> K true) false
|
haftmann@39192
|
375 |
>> (fn (module_prefix, string_classes) =>
|
haftmann@39192
|
376 |
serialize_haskell module_prefix string_classes));
|
haftmann@39192
|
377 |
|
haftmann@28064
|
378 |
val literals = let
|
haftmann@28064
|
379 |
fun char_haskell c =
|
haftmann@28064
|
380 |
let
|
haftmann@28064
|
381 |
val s = ML_Syntax.print_char c;
|
haftmann@28064
|
382 |
in if s = "'" then "\\'" else s end;
|
haftmann@34931
|
383 |
fun numeral_haskell k = if k >= 0 then string_of_int k
|
haftmann@34931
|
384 |
else Library.enclose "(" ")" (signed_string_of_int k);
|
haftmann@28064
|
385 |
in Literals {
|
haftmann@34178
|
386 |
literal_char = Library.enclose "'" "'" o char_haskell,
|
haftmann@28064
|
387 |
literal_string = quote o translate_string char_haskell,
|
haftmann@34931
|
388 |
literal_numeral = numeral_haskell,
|
haftmann@34931
|
389 |
literal_positive_numeral = numeral_haskell,
|
haftmann@38195
|
390 |
literal_alternative_numeral = numeral_haskell,
|
haftmann@34931
|
391 |
literal_naive_numeral = numeral_haskell,
|
haftmann@34178
|
392 |
literal_list = enum "," "[" "]",
|
haftmann@28064
|
393 |
infix_cons = (5, ":")
|
haftmann@28064
|
394 |
} end;
|
haftmann@28064
|
395 |
|
haftmann@28054
|
396 |
|
haftmann@28054
|
397 |
(** optional monad syntax **)
|
haftmann@28054
|
398 |
|
haftmann@28054
|
399 |
fun pretty_haskell_monad c_bind =
|
haftmann@28054
|
400 |
let
|
haftmann@31873
|
401 |
fun dest_bind t1 t2 = case Code_Thingol.split_pat_abs t2
|
haftmann@31889
|
402 |
of SOME ((pat, ty), t') =>
|
haftmann@31889
|
403 |
SOME ((SOME ((pat, ty), true), t1), t')
|
haftmann@28145
|
404 |
| NONE => NONE;
|
haftmann@28663
|
405 |
fun dest_monad c_bind_name (IConst (c, _) `$ t1 `$ t2) =
|
haftmann@28663
|
406 |
if c = c_bind_name then dest_bind t1 t2
|
haftmann@28145
|
407 |
else NONE
|
haftmann@28663
|
408 |
| dest_monad _ t = case Code_Thingol.split_let t
|
haftmann@28145
|
409 |
of SOME (((pat, ty), tbind), t') =>
|
haftmann@31889
|
410 |
SOME ((SOME ((pat, ty), false), tbind), t')
|
haftmann@28145
|
411 |
| NONE => NONE;
|
haftmann@28663
|
412 |
fun implode_monad c_bind_name = Code_Thingol.unfoldr (dest_monad c_bind_name);
|
haftmann@33988
|
413 |
fun print_monad print_bind print_term (NONE, t) vars =
|
haftmann@33988
|
414 |
(semicolon [print_term vars NOBR t], vars)
|
haftmann@33988
|
415 |
| print_monad print_bind print_term (SOME ((bind, _), true), t) vars = vars
|
haftmann@33988
|
416 |
|> print_bind NOBR bind
|
haftmann@33988
|
417 |
|>> (fn p => semicolon [p, str "<-", print_term vars NOBR t])
|
haftmann@33988
|
418 |
| print_monad print_bind print_term (SOME ((bind, _), false), t) vars = vars
|
haftmann@33988
|
419 |
|> print_bind NOBR bind
|
haftmann@37832
|
420 |
|>> (fn p => semicolon [str "let", str "{", p, str "=", print_term vars NOBR t, str "}"]);
|
haftmann@33988
|
421 |
fun pretty _ [c_bind'] print_term thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
|
haftmann@28145
|
422 |
of SOME (bind, t') => let
|
haftmann@31054
|
423 |
val (binds, t'') = implode_monad c_bind' t'
|
haftmann@33988
|
424 |
val (ps, vars') = fold_map (print_monad (gen_print_bind (K print_term) thm) print_term)
|
haftmann@33988
|
425 |
(bind :: binds) vars;
|
haftmann@33988
|
426 |
in
|
haftmann@37833
|
427 |
(brackify fxy o single o enclose "do { " " }" o Pretty.breaks)
|
haftmann@33988
|
428 |
(ps @| print_term vars' NOBR t'')
|
haftmann@33988
|
429 |
end
|
haftmann@28145
|
430 |
| NONE => brackify_infix (1, L) fxy
|
haftmann@37239
|
431 |
(print_term vars (INFX (1, L)) t1, str ">>=", print_term vars (INFX (1, X)) t2)
|
haftmann@31054
|
432 |
in (2, ([c_bind], pretty)) end;
|
haftmann@28054
|
433 |
|
haftmann@28145
|
434 |
fun add_monad target' raw_c_bind thy =
|
haftmann@28054
|
435 |
let
|
haftmann@31156
|
436 |
val c_bind = Code.read_const thy raw_c_bind;
|
haftmann@28054
|
437 |
in if target = target' then
|
haftmann@28054
|
438 |
thy
|
haftmann@39149
|
439 |
|> Code_Target.add_const_syntax target c_bind
|
haftmann@37854
|
440 |
(SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind)))
|
haftmann@28054
|
441 |
else error "Only Haskell target allows for monad syntax" end;
|
haftmann@28054
|
442 |
|
haftmann@28054
|
443 |
|
haftmann@28054
|
444 |
(** Isar setup **)
|
haftmann@28054
|
445 |
|
haftmann@28054
|
446 |
val _ =
|
wenzelm@36970
|
447 |
Outer_Syntax.command "code_monad" "define code syntax for monads" Keyword.thy_decl (
|
wenzelm@36970
|
448 |
Parse.term_group -- Parse.name >> (fn (raw_bind, target) =>
|
haftmann@28145
|
449 |
Toplevel.theory (add_monad target raw_bind))
|
haftmann@28054
|
450 |
);
|
haftmann@28054
|
451 |
|
haftmann@28054
|
452 |
val setup =
|
haftmann@37821
|
453 |
Code_Target.add_target
|
haftmann@39192
|
454 |
(target, { serializer = serializer, literals = literals,
|
haftmann@37822
|
455 |
check = { env_var = "EXEC_GHC", make_destination = I,
|
haftmann@39092
|
456 |
make_command = fn ghc => fn module_name =>
|
haftmann@37822
|
457 |
ghc ^ " -fglasgow-exts -odir build -hidir build -stubdir build -e \"\" " ^ module_name ^ ".hs" } })
|
haftmann@39149
|
458 |
#> Code_Target.add_tyco_syntax target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
|
haftmann@37239
|
459 |
brackify_infix (1, R) fxy (
|
haftmann@33988
|
460 |
print_typ (INFX (1, X)) ty1,
|
haftmann@28054
|
461 |
str "->",
|
haftmann@33988
|
462 |
print_typ (INFX (1, R)) ty2
|
haftmann@37239
|
463 |
)))
|
haftmann@28054
|
464 |
#> fold (Code_Target.add_reserved target) [
|
haftmann@28054
|
465 |
"hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
|
haftmann@28054
|
466 |
"import", "default", "forall", "let", "in", "class", "qualified", "data",
|
haftmann@28054
|
467 |
"newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
|
haftmann@28054
|
468 |
]
|
haftmann@28054
|
469 |
#> fold (Code_Target.add_reserved target) [
|
haftmann@28054
|
470 |
"Prelude", "Main", "Bool", "Maybe", "Either", "Ordering", "Char", "String", "Int",
|
haftmann@28054
|
471 |
"Integer", "Float", "Double", "Rational", "IO", "Eq", "Ord", "Enum", "Bounded",
|
haftmann@28054
|
472 |
"Num", "Real", "Integral", "Fractional", "Floating", "RealFloat", "Monad", "Functor",
|
haftmann@28054
|
473 |
"AlreadyExists", "ArithException", "ArrayException", "AssertionFailed", "AsyncException",
|
haftmann@28054
|
474 |
"BlockedOnDeadMVar", "Deadlock", "Denormal", "DivideByZero", "DotNetException", "DynException",
|
haftmann@28054
|
475 |
"Dynamic", "EOF", "EQ", "EmptyRec", "ErrorCall", "ExitException", "ExitFailure",
|
haftmann@28054
|
476 |
"ExitSuccess", "False", "GT", "HeapOverflow",
|
haftmann@28054
|
477 |
"IOError", "IOException", "IllegalOperation",
|
haftmann@28054
|
478 |
"IndexOutOfBounds", "Just", "Key", "LT", "Left", "LossOfPrecision", "NoMethodError",
|
haftmann@28054
|
479 |
"NoSuchThing", "NonTermination", "Nothing", "Obj", "OtherError", "Overflow",
|
haftmann@28054
|
480 |
"PatternMatchFail", "PermissionDenied", "ProtocolError", "RecConError", "RecSelError",
|
haftmann@28054
|
481 |
"RecUpdError", "ResourceBusy", "ResourceExhausted", "Right", "StackOverflow",
|
haftmann@28054
|
482 |
"ThreadKilled", "True", "TyCon", "TypeRep", "UndefinedElement", "Underflow",
|
haftmann@28054
|
483 |
"UnsupportedOperation", "UserError", "abs", "absReal", "acos", "acosh", "all",
|
haftmann@28054
|
484 |
"and", "any", "appendFile", "asTypeOf", "asciiTab", "asin", "asinh", "atan",
|
haftmann@28054
|
485 |
"atan2", "atanh", "basicIORun", "blockIO", "boundedEnumFrom", "boundedEnumFromThen",
|
haftmann@28054
|
486 |
"boundedEnumFromThenTo", "boundedEnumFromTo", "boundedPred", "boundedSucc", "break",
|
haftmann@28054
|
487 |
"catch", "catchException", "ceiling", "compare", "concat", "concatMap", "const",
|
haftmann@28054
|
488 |
"cos", "cosh", "curry", "cycle", "decodeFloat", "denominator", "div", "divMod",
|
haftmann@28054
|
489 |
"doubleToRatio", "doubleToRational", "drop", "dropWhile", "either", "elem",
|
haftmann@28054
|
490 |
"emptyRec", "encodeFloat", "enumFrom", "enumFromThen", "enumFromThenTo",
|
haftmann@28054
|
491 |
"enumFromTo", "error", "even", "exp", "exponent", "fail", "filter", "flip",
|
haftmann@28054
|
492 |
"floatDigits", "floatProperFraction", "floatRadix", "floatRange", "floatToRational",
|
haftmann@28054
|
493 |
"floor", "fmap", "foldl", "foldl'", "foldl1", "foldr", "foldr1", "fromDouble",
|
haftmann@28054
|
494 |
"fromEnum", "fromEnum_0", "fromInt", "fromInteger", "fromIntegral", "fromObj",
|
haftmann@28054
|
495 |
"fromRational", "fst", "gcd", "getChar", "getContents", "getLine", "head",
|
haftmann@28054
|
496 |
"id", "inRange", "index", "init", "intToRatio", "interact", "ioError", "isAlpha",
|
haftmann@28054
|
497 |
"isAlphaNum", "isDenormalized", "isDigit", "isHexDigit", "isIEEE", "isInfinite",
|
haftmann@28054
|
498 |
"isLower", "isNaN", "isNegativeZero", "isOctDigit", "isSpace", "isUpper", "iterate", "iterate'",
|
haftmann@28054
|
499 |
"last", "lcm", "length", "lex", "lexDigits", "lexLitChar", "lexmatch", "lines", "log",
|
haftmann@28054
|
500 |
"logBase", "lookup", "loop", "map", "mapM", "mapM_", "max", "maxBound", "maximum",
|
haftmann@28054
|
501 |
"maybe", "min", "minBound", "minimum", "mod", "negate", "nonnull", "not", "notElem",
|
haftmann@28054
|
502 |
"null", "numerator", "numericEnumFrom", "numericEnumFromThen", "numericEnumFromThenTo",
|
haftmann@28054
|
503 |
"numericEnumFromTo", "odd", "or", "otherwise", "pi", "pred",
|
haftmann@28054
|
504 |
"print", "product", "properFraction", "protectEsc", "putChar", "putStr", "putStrLn",
|
haftmann@28054
|
505 |
"quot", "quotRem", "range", "rangeSize", "rationalToDouble", "rationalToFloat",
|
haftmann@28054
|
506 |
"rationalToRealFloat", "read", "readDec", "readField", "readFieldName", "readFile",
|
haftmann@28054
|
507 |
"readFloat", "readHex", "readIO", "readInt", "readList", "readLitChar", "readLn",
|
haftmann@28054
|
508 |
"readOct", "readParen", "readSigned", "reads", "readsPrec", "realFloatToRational",
|
haftmann@28054
|
509 |
"realToFrac", "recip", "reduce", "rem", "repeat", "replicate", "return", "reverse",
|
haftmann@28054
|
510 |
"round", "scaleFloat", "scanl", "scanl1", "scanr", "scanr1", "seq", "sequence",
|
haftmann@28054
|
511 |
"sequence_", "show", "showChar", "showException", "showField", "showList",
|
haftmann@28054
|
512 |
"showLitChar", "showParen", "showString", "shows", "showsPrec", "significand",
|
haftmann@28054
|
513 |
"signum", "signumReal", "sin", "sinh", "snd", "span", "splitAt", "sqrt", "subtract",
|
haftmann@28054
|
514 |
"succ", "sum", "tail", "take", "takeWhile", "takeWhile1", "tan", "tanh", "threadToIOResult",
|
haftmann@28054
|
515 |
"throw", "toEnum", "toInt", "toInteger", "toObj", "toRational", "truncate", "uncurry",
|
haftmann@28054
|
516 |
"undefined", "unlines", "unsafeCoerce", "unsafeIndex", "unsafeRangeSize", "until", "unwords",
|
haftmann@28054
|
517 |
"unzip", "unzip3", "userError", "words", "writeFile", "zip", "zip3", "zipWith", "zipWith3"
|
haftmann@28054
|
518 |
] (*due to weird handling of ':', we can't do anything else than to import *all* prelude symbols*);
|
haftmann@28054
|
519 |
|
haftmann@28054
|
520 |
end; (*struct*)
|