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