fall back on P.term_group, to avoid problems with inner_syntax markup (due to CodeName.read_const_exprs);
1 (* Title: Tools/code/code_target.ML
3 Author: Florian Haftmann, TU Muenchen
5 Serializer from intermediate language ("Thin-gol")
6 to target languages (like SML or Haskell).
9 signature CODE_TARGET =
11 include BASIC_CODE_THINGOL;
13 val add_syntax_class: string -> class
14 -> (string * (string * string) list) option -> theory -> theory;
15 val add_syntax_inst: string -> string * class -> bool -> theory -> theory;
16 val add_syntax_tycoP: string -> string -> OuterParse.token list
17 -> (theory -> theory) * OuterParse.token list;
18 val add_syntax_constP: string -> string -> OuterParse.token list
19 -> (theory -> theory) * OuterParse.token list;
21 val add_undefined: string -> string -> string -> theory -> theory;
22 val add_pretty_list: string -> string -> string -> theory -> theory;
23 val add_pretty_list_string: string -> string -> string
24 -> string -> string list -> theory -> theory;
25 val add_pretty_char: string -> string -> string list -> theory -> theory
26 val add_pretty_numeral: string -> bool -> bool -> string -> string -> string
27 -> string -> string -> theory -> theory;
28 val add_pretty_message: string -> string -> string list -> string
29 -> string -> string -> theory -> theory;
31 val allow_abort: string -> theory -> theory;
35 val add_target: string * serializer -> theory -> theory;
36 val extend_target: string * (string * (CodeThingol.program -> CodeThingol.program))
38 val assert_target: theory -> string -> string;
39 val serialize: theory -> string -> string option -> Args.T list
40 -> CodeThingol.program -> string list -> serialization;
41 val compile: serialization -> unit;
42 val export: serialization -> unit;
43 val file: Path.T -> serialization -> unit;
44 val string: string list -> serialization -> string;
46 val code_of: theory -> string -> string -> string list -> string list -> string;
47 val eval_conv: string * (unit -> thm) option ref
48 -> theory -> cterm -> string list -> thm;
49 val eval_term: string * (unit -> 'a) option ref
50 -> theory -> term -> string list -> 'a;
51 val shell_command: string (*theory name*) -> string (*cg expr*) -> unit;
53 val setup: theory -> theory;
54 val code_width: int ref;
56 val ml_code_of: theory -> CodeThingol.program -> string list -> string * string list;
59 structure CodeTarget : CODE_TARGET =
62 open BasicCodeThingol;
69 fun xs @| y = xs @ [y];
70 val str = PrintMode.setmp [] Pretty.str;
71 val concat = Pretty.block o Pretty.breaks;
72 val brackets = Pretty.enclose "(" ")" o Pretty.breaks;
73 fun semicolon ps = Pretty.block [concat ps, str ";"];
74 fun enum_default default sep opn cls [] = str default
75 | enum_default default sep opn cls xs = Pretty.enum sep opn cls xs;
77 datatype destination = Compile | Export | File of Path.T | String of string list;
78 type serialization = destination -> (string * string list) option;
80 val code_width = ref 80; (*FIXME after Pretty module no longer depends on print mode*)
81 fun code_setmp f = PrintMode.setmp [] (Pretty.setmp_margin (!code_width) f);
82 fun code_of_pretty p = code_setmp Pretty.string_of p ^ "\n";
83 fun code_writeln p = Pretty.setmp_margin (!code_width) Pretty.writeln p;
85 (*FIXME why another code_setmp?*)
86 fun compile f = (code_setmp f Compile; ());
87 fun export f = (code_setmp f Export; ());
88 fun file p f = (code_setmp f (File p); ());
89 fun string cs f = fst (the (code_setmp f (String cs)));
91 fun stmt_names_of_destination (String stmts) = stmts
92 | stmt_names_of_destination _ = [];
95 (** generic syntax **)
97 datatype lrx = L | R | X;
102 | INFX of (int * lrx);
104 val APP = INFX (~1, L);
106 fun fixity_lrx L L = false
107 | fixity_lrx R R = false
108 | fixity_lrx _ _ = true;
110 fun fixity NOBR _ = false
111 | fixity _ NOBR = false
112 | fixity (INFX (pr, lr)) (INFX (pr_ctxt, lr_ctxt)) =
115 andalso fixity_lrx lr lr_ctxt
117 | fixity BR (INFX _) = false
120 fun gen_brackify _ [p] = p
121 | gen_brackify true (ps as _::_) = Pretty.enclose "(" ")" ps
122 | gen_brackify false (ps as _::_) = Pretty.block ps;
124 fun brackify fxy_ctxt =
125 gen_brackify (fixity BR fxy_ctxt) o Pretty.breaks;
127 fun brackify_infix infx fxy_ctxt =
128 gen_brackify (fixity (INFX infx) fxy_ctxt) o Pretty.breaks;
130 type class_syntax = string * (string -> string option);
131 type typ_syntax = int * ((fixity -> itype -> Pretty.T)
132 -> fixity -> itype list -> Pretty.T);
133 type term_syntax = int * ((CodeName.var_ctxt -> fixity -> iterm -> Pretty.T)
134 -> thm -> bool -> CodeName.var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
136 datatype name_syntax_table = NameSyntaxTable of {
137 class: class_syntax Symtab.table,
138 inst: unit Symtab.table,
139 tyco: typ_syntax Symtab.table,
140 const: term_syntax Symtab.table
146 val target_SML = "SML";
147 val target_OCaml = "OCaml";
148 val target_Haskell = "Haskell";
150 fun mk_name_syntax_table ((class, inst), (tyco, const)) =
151 NameSyntaxTable { class = class, inst = inst, tyco = tyco, const = const };
152 fun map_name_syntax_table f (NameSyntaxTable { class, inst, tyco, const }) =
153 mk_name_syntax_table (f ((class, inst), (tyco, const)));
154 fun merge_name_syntax_table (NameSyntaxTable { class = class1, inst = inst1, tyco = tyco1, const = const1 },
155 NameSyntaxTable { class = class2, inst = inst2, tyco = tyco2, const = const2 }) =
156 mk_name_syntax_table (
157 (Symtab.join (K snd) (class1, class2),
158 Symtab.join (K snd) (inst1, inst2)),
159 (Symtab.join (K snd) (tyco1, tyco2),
160 Symtab.join (K snd) (const1, const2))
164 string option (*module name*)
165 -> Args.T list (*arguments*)
166 -> (string -> string) (*labelled_name*)
167 -> string list (*reserved symbols*)
168 -> (string * Pretty.T) list (*includes*)
169 -> (string -> string option) (*module aliasses*)
170 -> (string -> class_syntax option)
171 -> (string -> typ_syntax option)
172 -> (string -> term_syntax option)
173 -> CodeThingol.program
174 -> string list (*selected statements*)
177 datatype serializer_entry = Serializer of serializer
178 | Extends of string * (CodeThingol.program -> CodeThingol.program);
180 datatype target = Target of {
182 serializer: serializer_entry,
183 reserved: string list,
184 includes: Pretty.T Symtab.table,
185 name_syntax_table: name_syntax_table,
186 module_alias: string Symtab.table
189 fun mk_target ((serial, serializer), ((reserved, includes), (name_syntax_table, module_alias))) =
190 Target { serial = serial, serializer = serializer, reserved = reserved,
191 includes = includes, name_syntax_table = name_syntax_table, module_alias = module_alias };
192 fun map_target f ( Target { serial, serializer, reserved, includes, name_syntax_table, module_alias } ) =
193 mk_target (f ((serial, serializer), ((reserved, includes), (name_syntax_table, module_alias))));
194 fun merge_target strict target (Target { serial = serial1, serializer = serializer,
195 reserved = reserved1, includes = includes1,
196 name_syntax_table = name_syntax_table1, module_alias = module_alias1 },
197 Target { serial = serial2, serializer = _,
198 reserved = reserved2, includes = includes2,
199 name_syntax_table = name_syntax_table2, module_alias = module_alias2 }) =
200 if serial1 = serial2 orelse not strict then
201 mk_target ((serial1, serializer),
202 ((merge (op =) (reserved1, reserved2), Symtab.merge (op =) (includes1, includes2)),
203 (merge_name_syntax_table (name_syntax_table1, name_syntax_table2),
204 Symtab.join (K snd) (module_alias1, module_alias2))
207 error ("Incompatible serializers: " ^ quote target);
209 structure CodeTargetData = TheoryDataFun
211 type T = target Symtab.table * string list;
212 val empty = (Symtab.empty, []);
215 fun merge _ ((target1, exc1) : T, (target2, exc2)) =
216 (Symtab.join (merge_target true) (target1, target2), Library.merge (op =) (exc1, exc2));
219 fun the_serializer (Target { serializer, ... }) = serializer;
220 fun the_reserved (Target { reserved, ... }) = reserved;
221 fun the_includes (Target { includes, ... }) = includes;
222 fun the_name_syntax (Target { name_syntax_table = NameSyntaxTable x, ... }) = x;
223 fun the_module_alias (Target { module_alias , ... }) = module_alias;
225 val abort_allowed = snd o CodeTargetData.get;
227 fun assert_target thy target =
228 case Symtab.lookup (fst (CodeTargetData.get thy)) target
229 of SOME data => target
230 | NONE => error ("Unknown code target language: " ^ quote target);
232 fun put_target (target, seri) thy =
234 val defined_target = is_some o Symtab.lookup (fst (CodeTargetData.get thy));
236 of Extends (super, _) => if defined_target super then ()
237 else error ("Unknown code target language: " ^ quote super)
239 val _ = if defined_target target
240 then warning ("Overwriting existing target " ^ quote target)
244 |> (CodeTargetData.map o apfst oo Symtab.map_default)
245 (target, mk_target ((serial (), seri), (([], Symtab.empty),
246 (mk_name_syntax_table ((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)),
248 ((map_target o apfst o apsnd o K) seri)
251 fun add_target (target, seri) = put_target (target, Serializer seri);
252 fun extend_target (target, (super, modify)) =
253 put_target (target, Extends (super, modify));
255 fun map_target_data target f thy =
257 val _ = assert_target thy target;
260 |> (CodeTargetData.map o apfst o Symtab.map_entry target o map_target) f
263 fun map_reserved target =
264 map_target_data target o apsnd o apfst o apfst;
265 fun map_includes target =
266 map_target_data target o apsnd o apfst o apsnd;
267 fun map_name_syntax target =
268 map_target_data target o apsnd o apsnd o apfst o map_name_syntax_table;
269 fun map_module_alias target =
270 map_target_data target o apsnd o apsnd o apsnd;
272 fun invoke_serializer thy modify abortable serializer reserved includes
273 module_alias class inst tyco const module args program1 cs1 =
275 val program2 = modify program1;
276 val hidden = Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const;
277 val cs2 = subtract (op =) hidden cs1;
278 val program3 = Graph.subgraph (not o member (op =) hidden) program2;
279 val all_cs = Graph.all_succs program2 cs2;
280 val program4 = Graph.subgraph (member (op =) all_cs) program3;
281 val empty_funs = filter_out (member (op =) abortable)
282 (CodeThingol.empty_funs program3);
283 val _ = if null empty_funs then () else error ("No defining equations for "
284 ^ commas (map (CodeName.labelled_name thy) empty_funs));
286 serializer module args (CodeName.labelled_name thy) reserved includes
287 (Symtab.lookup module_alias) (Symtab.lookup class)
288 (Symtab.lookup tyco) (Symtab.lookup const)
292 fun mount_serializer thy alt_serializer target =
294 val (targets, abortable) = CodeTargetData.get thy;
295 fun collapse_hierarchy target =
297 val data = case Symtab.lookup targets target
299 | NONE => error ("Unknown code target language: " ^ quote target);
300 in case the_serializer data
301 of Serializer _ => (I, data)
302 | Extends (super, modify) => let
303 val (modify', data') = collapse_hierarchy super
304 in (modify' #> modify, merge_target false target (data', data)) end
306 val (modify, data) = collapse_hierarchy target;
307 val serializer = the_default (case the_serializer data
308 of Serializer seri => seri) alt_serializer;
309 val reserved = the_reserved data;
310 val includes = Symtab.dest (the_includes data);
311 val module_alias = the_module_alias data;
312 val { class, inst, tyco, const } = the_name_syntax data;
314 invoke_serializer thy modify abortable serializer reserved
315 includes module_alias class inst tyco const
318 fun serialize thy = mount_serializer thy NONE;
320 fun parse_args f args =
321 case Scan.read Args.stopper f args
323 | NONE => error "Bad serializer arguments";
326 (** generic code combinators **)
328 (* list, char, string, numeral and monad abstract syntax transformations *)
330 fun nerror thm s = error (s ^ ",\nin equation " ^ Display.string_of_thm thm);
332 fun implode_list c_nil c_cons t =
334 fun dest_cons (IConst (c, _) `$ t1 `$ t2) =
338 | dest_cons _ = NONE;
339 val (ts, t') = CodeThingol.unfoldr dest_cons t;
341 of IConst (c, _) => if c = c_nil then SOME ts else NONE
345 fun decode_char c_nibbles (IConst (c1, _), IConst (c2, _)) =
347 fun idx c = find_index (curry (op =) c) c_nibbles;
348 fun decode ~1 _ = NONE
350 | decode n m = SOME (chr (n * 16 + m));
351 in decode (idx c1) (idx c2) end
352 | decode_char _ _ = NONE;
354 fun implode_string c_char c_nibbles mk_char mk_string ts =
356 fun implode_char (IConst (c, _) `$ t1 `$ t2) =
357 if c = c_char then decode_char c_nibbles (t1, t2) else NONE
358 | implode_char _ = NONE;
359 val ts' = map implode_char ts;
360 in if forall is_some ts'
361 then (SOME o str o mk_string o implode o map_filter I) ts'
365 fun implode_numeral thm negative c_pls c_min c_bit0 c_bit1 =
367 fun dest_bit (IConst (c, _)) = if c = c_bit0 then 0
368 else if c = c_bit1 then 1
369 else nerror thm "Illegal numeral expression: illegal bit"
370 | dest_bit _ = nerror thm "Illegal numeral expression: illegal bit";
371 fun dest_numeral (IConst (c, _)) = if c = c_pls then SOME 0
372 else if c = c_min then
373 if negative then SOME ~1 else NONE
374 else nerror thm "Illegal numeral expression: illegal leading digit"
375 | dest_numeral (t1 `$ t2) =
376 let val (n, b) = (dest_numeral t2, dest_bit t1)
377 in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
378 | dest_numeral _ = nerror thm "Illegal numeral expression: illegal term";
379 in dest_numeral #> the_default 0 end;
381 fun implode_monad c_bind t =
383 fun dest_monad (IConst (c, _) `$ t1 `$ t2) =
385 then case CodeThingol.split_abs t2
386 of SOME (((v, pat), ty), t') =>
387 SOME ((SOME (((SOME v, pat), ty), true), t1), t')
390 | dest_monad t = case CodeThingol.split_let t
391 of SOME (((pat, ty), tbind), t') =>
392 SOME ((SOME (((NONE, SOME pat), ty), false), tbind), t')
394 in CodeThingol.unfoldr dest_monad t end;
397 (* applications and bindings *)
399 fun gen_pr_app pr_app pr_term syntax_const is_cons thm pat
400 vars fxy (app as ((c, (_, tys)), ts)) =
402 of NONE => if pat andalso not (is_cons c) then
403 nerror thm "Non-constructor in pattern"
404 else brackify fxy (pr_app thm pat vars app)
407 val k = if i < 0 then length tys else i;
408 fun pr' fxy ts = pr (pr_term thm pat) thm pat vars fxy (ts ~~ curry Library.take k tys);
411 else if k < length ts
412 then case chop k ts of (ts1, ts2) =>
413 brackify fxy (pr' APP ts1 :: map (pr_term thm pat vars BR) ts2)
414 else pr_term thm pat vars fxy (CodeThingol.eta_expand k app)
417 fun gen_pr_bind pr_bind pr_term thm (fxy : fixity) ((v, pat), ty : itype) vars =
420 of SOME pat => CodeThingol.fold_varnames (insert (op =)) pat []
422 val vars' = CodeName.intro_vars (the_list v) vars;
423 val vars'' = CodeName.intro_vars vs vars';
424 val v' = Option.map (CodeName.lookup_var vars') v;
425 val pat' = Option.map (pr_term thm true vars'' fxy) pat;
426 in (pr_bind ((v', pat'), ty), vars'') end;
431 val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
432 val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
435 apfst NameSpace.implode o split_last o fst o split_last o NameSpace.explode;
437 fun mk_name_module reserved_names module_prefix module_alias program =
439 fun mk_alias name = case module_alias name
440 of SOME name' => name'
443 |> map (fn name => (the_single o fst) (Name.variants [name] reserved_names))
444 |> NameSpace.implode;
445 fun mk_prefix name = case module_prefix
446 of SOME module_prefix => NameSpace.append module_prefix name
450 |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))
451 o fst o dest_name o fst)
453 in the o Symtab.lookup tab end;
457 (** SML/OCaml serializer **)
460 MLFuns of (string * (typscheme * ((iterm list * iterm) * thm) list)) list
461 | MLDatas of (string * ((vname * sort) list * (string * itype list) list)) list
462 | MLClass of string * (vname * ((class * string) list * (string * itype) list))
463 | MLClassinst of string * ((class * (string * (vname * sort) list))
464 * ((class * (string * (string * dict list list))) list
465 * ((string * const) * thm) list));
467 fun stmt_names_of (MLFuns fs) = map fst fs
468 | stmt_names_of (MLDatas ds) = map fst ds
469 | stmt_names_of (MLClass (c, _)) = [c]
470 | stmt_names_of (MLClassinst (i, _)) = [i];
472 fun pr_sml_stmt syntax_tyco syntax_const labelled_name reserved_names deresolve is_cons =
474 val pr_label_classrel = translate_string (fn "." => "__" | c => c)
475 o NameSpace.qualifier;
476 val pr_label_classparam = NameSpace.base o NameSpace.qualifier;
477 fun pr_dicts fxy ds =
479 fun pr_dictvar (v, (_, 1)) = first_upper v ^ "_"
480 | pr_dictvar (v, (i, _)) = first_upper v ^ string_of_int (i+1) ^ "_";
485 | pr_proj (ps as _ :: _) p =
486 brackets [Pretty.enum " o" "(" ")" ps, p];
487 fun pr_dict fxy (DictConst (inst, dss)) =
488 brackify fxy ((str o deresolve) inst :: map (pr_dicts BR) dss)
489 | pr_dict fxy (DictVar (classrels, v)) =
490 pr_proj (map (str o deresolve) classrels) ((str o pr_dictvar) v)
493 | [d] => pr_dict fxy d
494 | _ :: _ => (Pretty.list "(" ")" o map (pr_dict NOBR)) ds
496 fun pr_tyvar_dicts vs =
498 |> map (fn (v, sort) => map_index (fn (i, _) =>
499 DictVar ([], (v, (i, length sort)))) sort)
500 |> map (pr_dicts BR);
501 fun pr_tycoexpr fxy (tyco, tys) =
503 val tyco' = (str o deresolve) tyco
504 in case map (pr_typ BR) tys
506 | [p] => Pretty.block [p, Pretty.brk 1, tyco']
507 | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
509 and pr_typ fxy (tyco `%% tys) = (case syntax_tyco tyco
510 of NONE => pr_tycoexpr fxy (tyco, tys)
511 | SOME (i, pr) => pr pr_typ fxy tys)
512 | pr_typ fxy (ITyVar v) = str ("'" ^ v);
513 fun pr_term thm pat vars fxy (IConst c) =
514 pr_app thm pat vars fxy (c, [])
515 | pr_term thm pat vars fxy (IVar v) =
516 str (CodeName.lookup_var vars v)
517 | pr_term thm pat vars fxy (t as t1 `$ t2) =
518 (case CodeThingol.unfold_const_app t
519 of SOME c_ts => pr_app thm pat vars fxy c_ts
521 brackify fxy [pr_term thm pat vars NOBR t1, pr_term thm pat vars BR t2])
522 | pr_term thm pat vars fxy (t as _ `|-> _) =
524 val (binds, t') = CodeThingol.unfold_abs t;
525 fun pr ((v, pat), ty) =
526 pr_bind thm NOBR ((SOME v, pat), ty)
527 #>> (fn p => concat [str "fn", p, str "=>"]);
528 val (ps, vars') = fold_map pr binds vars;
529 in brackets (ps @ [pr_term thm pat vars' NOBR t']) end
530 | pr_term thm pat vars fxy (ICase (cases as (_, t0))) =
531 (case CodeThingol.unfold_const_app t0
532 of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
533 then pr_case thm vars fxy cases
534 else pr_app thm pat vars fxy c_ts
535 | NONE => pr_case thm vars fxy cases)
536 and pr_app' thm pat vars (app as ((c, (iss, tys)), ts)) =
537 if is_cons c then let
540 (str o deresolve) c :: map (pr_term thm pat vars BR) ts
541 else if k = length ts then
542 [(str o deresolve) c, Pretty.enum "," "(" ")" (map (pr_term thm pat vars NOBR) ts)]
543 else [pr_term thm pat vars BR (CodeThingol.eta_expand k app)] end else
545 :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts
546 and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons thm pat vars
547 and pr_bind' ((NONE, NONE), _) = str "_"
548 | pr_bind' ((SOME v, NONE), _) = str v
549 | pr_bind' ((NONE, SOME p), _) = p
550 | pr_bind' ((SOME v, SOME p), _) = concat [str v, str "as", p]
551 and pr_bind thm = gen_pr_bind pr_bind' pr_term thm
552 and pr_case thm vars fxy (cases as ((_, [_]), _)) =
554 val (binds, t') = CodeThingol.unfold_let (ICase cases);
555 fun pr ((pat, ty), t) vars =
557 |> pr_bind thm NOBR ((NONE, SOME pat), ty)
558 |>> (fn p => semicolon [str "val", p, str "=", pr_term thm false vars NOBR t])
559 val (ps, vars') = fold_map pr binds vars;
562 [str ("let"), Pretty.fbrk, Pretty.chunks ps] |> Pretty.block,
563 [str ("in"), Pretty.fbrk, pr_term thm false vars' NOBR t'] |> Pretty.block,
567 | pr_case thm vars fxy (((td, ty), b::bs), _) =
569 fun pr delim (pat, t) =
571 val (p, vars') = pr_bind thm NOBR ((NONE, SOME pat), ty) vars;
573 concat [str delim, p, str "=>", pr_term thm false vars' NOBR t]
576 (Pretty.enclose "(" ")" o single o brackify fxy) (
578 :: pr_term thm false vars NOBR td
583 | pr_case thm vars fxy ((_, []), _) = str "raise Fail \"empty case\"";
584 fun pr_stmt (MLFuns (funns as (funn :: funns'))) =
588 fun no_args _ (((ts, _), _) :: _) = length ts
589 | no_args ty [] = (length o fst o CodeThingol.unfold_fun) ty;
591 | mk 0 vs = if (null o filter_out (null o snd)) vs
592 then "val" else "fun"
594 fun chk (_, ((vs, ty), eqs)) NONE = SOME (mk (no_args ty eqs) vs)
595 | chk (_, ((vs, ty), eqs)) (SOME defi) =
596 if defi = mk (no_args ty eqs) vs then SOME defi
597 else error ("Mixing simultaneous vals and funs not implemented: "
598 ^ commas (map (labelled_name o fst) funns));
599 in the (fold chk funns NONE) end;
600 fun pr_funn definer (name, ((vs, ty), [])) =
602 val vs_dict = filter_out (null o snd) vs;
603 val n = length vs_dict + (length o fst o CodeThingol.unfold_fun) ty;
605 (ML_Syntax.print_string o NameSpace.base o NameSpace.qualifier) name;
609 :: (str o deresolve) name
610 :: map str (replicate n "_")
614 @@ str (exc_str ^ ")")
617 | pr_funn definer (name, ((vs, ty), eqs as eq :: eqs')) =
619 val vs_dict = filter_out (null o snd) vs;
620 val shift = if null eqs' then I else
621 map (Pretty.block o single o Pretty.block o single);
622 fun pr_eq definer ((ts, t), thm) =
624 val consts = map_filter
625 (fn c => if (is_some o syntax_const) c
626 then NONE else (SOME o NameSpace.base o deresolve) c)
627 ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);
628 val vars = reserved_names
629 |> CodeName.intro_vars consts
630 |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)
631 (insert (op =)) ts []);
634 [str definer, (str o deresolve) name]
635 @ (if null ts andalso null vs_dict
636 then [str ":", pr_typ NOBR ty]
638 pr_tyvar_dicts vs_dict
639 @ map (pr_term thm true vars BR) ts)
640 @ [str "=", pr_term thm false vars NOBR t]
644 (Pretty.block o Pretty.fbreaks o shift) (
646 :: map (pr_eq "|") eqs'
649 val (ps, p) = split_last (pr_funn definer funn :: map (pr_funn "and") funns');
650 in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end
651 | pr_stmt (MLDatas (datas as (data :: datas'))) =
659 Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys)
661 fun pr_data definer (tyco, (vs, [])) =
664 :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
668 | pr_data definer (tyco, (vs, cos)) =
671 :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
673 :: separate (str "|") (map pr_co cos)
675 val (ps, p) = split_last
676 (pr_data "datatype" data :: map (pr_data "and") datas');
677 in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end
678 | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
680 val w = first_upper v ^ "_";
681 fun pr_superclass_field (class, classrel) =
683 pr_label_classrel classrel, ":", "'" ^ v, deresolve class
685 fun pr_classparam_field (classparam, ty) =
687 (str o pr_label_classparam) classparam, str ":", pr_typ NOBR ty
689 fun pr_classparam_proj (classparam, _) =
692 (str o deresolve) classparam,
693 Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolve class)],
695 str ("#" ^ pr_label_classparam classparam),
698 fun pr_superclass_proj (_, classrel) =
701 (str o deresolve) classrel,
702 Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolve class)],
704 str ("#" ^ pr_label_classrel classrel),
711 (str o deresolve) class,
713 Pretty.enum "," "{" "};" (
714 map pr_superclass_field superclasses @ map pr_classparam_field classparams
717 :: map pr_superclass_proj superclasses
718 @ map pr_classparam_proj classparams
721 | pr_stmt (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =
723 fun pr_superclass (_, (classrel, dss)) =
725 (str o pr_label_classrel) classrel,
727 pr_dicts NOBR [DictConst dss]
729 fun pr_classparam ((classparam, c_inst), thm) =
731 (str o pr_label_classparam) classparam,
733 pr_app thm false reserved_names NOBR (c_inst, [])
737 str (if null arity then "val" else "fun"),
738 (str o deresolve) inst ] @
739 pr_tyvar_dicts arity @ [
741 Pretty.enum "," "{" "}"
742 (map pr_superclass superarities @ map pr_classparam classparam_insts),
744 pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
749 fun pr_sml_module name content =
751 str ("structure " ^ name ^ " = ")
756 @@ str ("end; (*struct " ^ name ^ "*)")
759 fun pr_ocaml_stmt syntax_tyco syntax_const labelled_name reserved_names deresolve is_cons =
761 fun pr_dicts fxy ds =
763 fun pr_dictvar (v, (_, 1)) = "_" ^ first_upper v
764 | pr_dictvar (v, (i, _)) = "_" ^ first_upper v ^ string_of_int (i+1);
766 fold_rev (fn p2 => fn p1 => Pretty.block [p1, str ".", str p2]) ps p
767 fun pr_dict fxy (DictConst (inst, dss)) =
768 brackify fxy ((str o deresolve) inst :: map (pr_dicts BR) dss)
769 | pr_dict fxy (DictVar (classrels, v)) =
770 pr_proj (map deresolve classrels) ((str o pr_dictvar) v)
773 | [d] => pr_dict fxy d
774 | _ :: _ => (Pretty.list "(" ")" o map (pr_dict NOBR)) ds
776 fun pr_tyvar_dicts vs =
778 |> map (fn (v, sort) => map_index (fn (i, _) =>
779 DictVar ([], (v, (i, length sort)))) sort)
780 |> map (pr_dicts BR);
781 fun pr_tycoexpr fxy (tyco, tys) =
783 val tyco' = (str o deresolve) tyco
784 in case map (pr_typ BR) tys
786 | [p] => Pretty.block [p, Pretty.brk 1, tyco']
787 | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
789 and pr_typ fxy (tyco `%% tys) = (case syntax_tyco tyco
790 of NONE => pr_tycoexpr fxy (tyco, tys)
791 | SOME (i, pr) => pr pr_typ fxy tys)
792 | pr_typ fxy (ITyVar v) = str ("'" ^ v);
793 fun pr_term thm pat vars fxy (IConst c) =
794 pr_app thm pat vars fxy (c, [])
795 | pr_term thm pat vars fxy (IVar v) =
796 str (CodeName.lookup_var vars v)
797 | pr_term thm pat vars fxy (t as t1 `$ t2) =
798 (case CodeThingol.unfold_const_app t
799 of SOME c_ts => pr_app thm pat vars fxy c_ts
801 brackify fxy [pr_term thm pat vars NOBR t1, pr_term thm pat vars BR t2])
802 | pr_term thm pat vars fxy (t as _ `|-> _) =
804 val (binds, t') = CodeThingol.unfold_abs t;
805 fun pr ((v, pat), ty) = pr_bind thm BR ((SOME v, pat), ty);
806 val (ps, vars') = fold_map pr binds vars;
807 in brackets (str "fun" :: ps @ str "->" @@ pr_term thm pat vars' NOBR t') end
808 | pr_term thm pat vars fxy (ICase (cases as (_, t0))) = (case CodeThingol.unfold_const_app t0
809 of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
810 then pr_case thm vars fxy cases
811 else pr_app thm pat vars fxy c_ts
812 | NONE => pr_case thm vars fxy cases)
813 and pr_app' thm pat vars (app as ((c, (iss, tys)), ts)) =
815 if length tys = length ts
817 of [] => [(str o deresolve) c]
818 | [t] => [(str o deresolve) c, pr_term thm pat vars BR t]
819 | _ => [(str o deresolve) c, Pretty.enum "," "(" ")"
820 (map (pr_term thm pat vars NOBR) ts)]
821 else [pr_term thm pat vars BR (CodeThingol.eta_expand (length tys) app)]
822 else (str o deresolve) c
823 :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts)
824 and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons thm pat vars
825 and pr_bind' ((NONE, NONE), _) = str "_"
826 | pr_bind' ((SOME v, NONE), _) = str v
827 | pr_bind' ((NONE, SOME p), _) = p
828 | pr_bind' ((SOME v, SOME p), _) = brackets [p, str "as", str v]
829 and pr_bind thm = gen_pr_bind pr_bind' pr_term thm
830 and pr_case thm vars fxy (cases as ((_, [_]), _)) =
832 val (binds, t') = CodeThingol.unfold_let (ICase cases);
833 fun pr ((pat, ty), t) vars =
835 |> pr_bind thm NOBR ((NONE, SOME pat), ty)
837 [str "let", p, str "=", pr_term thm false vars NOBR t, str "in"])
838 val (ps, vars') = fold_map pr binds vars;
839 in Pretty.chunks (ps @| pr_term thm false vars' NOBR t') end
840 | pr_case thm vars fxy (((td, ty), b::bs), _) =
842 fun pr delim (pat, t) =
844 val (p, vars') = pr_bind thm NOBR ((NONE, SOME pat), ty) vars;
845 in concat [str delim, p, str "->", pr_term thm false vars' NOBR t] end;
847 (Pretty.enclose "(" ")" o single o brackify fxy) (
849 :: pr_term thm false vars NOBR td
854 | pr_case thm vars fxy ((_, []), _) = str "failwith \"empty case\"";
855 fun fish_params vars eqs =
857 fun fish_param _ (w as SOME _) = w
858 | fish_param (IVar v) NONE = SOME v
859 | fish_param _ NONE = NONE;
860 fun fillup_param _ (_, SOME v) = v
861 | fillup_param x (i, NONE) = x ^ string_of_int i;
862 val fished1 = fold (map2 fish_param) eqs (replicate (length (hd eqs)) NONE);
863 val x = Name.variant (map_filter I fished1) "x";
864 val fished2 = map_index (fillup_param x) fished1;
865 val (fished3, _) = Name.variants fished2 Name.context;
866 val vars' = CodeName.intro_vars fished3 vars;
867 in map (CodeName.lookup_var vars') fished3 end;
868 fun pr_stmt (MLFuns (funns as funn :: funns')) =
870 fun pr_eq ((ts, t), thm) =
872 val consts = map_filter
873 (fn c => if (is_some o syntax_const) c
874 then NONE else (SOME o NameSpace.base o deresolve) c)
875 ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);
876 val vars = reserved_names
877 |> CodeName.intro_vars consts
878 |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)
879 (insert (op =)) ts []);
881 (Pretty.block o Pretty.commas) (map (pr_term thm true vars NOBR) ts),
883 pr_term thm false vars NOBR t
885 fun pr_eqs name ty [] =
887 val n = (length o fst o CodeThingol.unfold_fun) ty;
889 (ML_Syntax.print_string o NameSpace.base o NameSpace.qualifier) name;
892 map str (replicate n "_")
898 | pr_eqs _ _ [((ts, t), thm)] =
900 val consts = map_filter
901 (fn c => if (is_some o syntax_const) c
902 then NONE else (SOME o NameSpace.base o deresolve) c)
903 ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);
904 val vars = reserved_names
905 |> CodeName.intro_vars consts
906 |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)
907 (insert (op =)) ts []);
910 map (pr_term thm true vars BR) ts
912 @@ pr_term thm false vars NOBR t
915 | pr_eqs _ _ (eqs as (eq as (([_], _), _)) :: eqs') =
922 :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
923 o single o pr_eq) eqs'
925 | pr_eqs _ _ (eqs as eq :: eqs') =
927 val consts = map_filter
928 (fn c => if (is_some o syntax_const) c
929 then NONE else (SOME o NameSpace.base o deresolve) c)
930 ((fold o CodeThingol.fold_constnames)
931 (insert (op =)) (map (snd o fst) eqs) []);
932 val vars = reserved_names
933 |> CodeName.intro_vars consts;
934 val dummy_parms = (map str o fish_params vars o map (fst o fst)) eqs;
937 Pretty.breaks dummy_parms
943 :: (Pretty.block o Pretty.commas) dummy_parms
948 :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
949 o single o pr_eq) eqs'
952 fun pr_funn definer (name, ((vs, ty), eqs)) =
955 :: (str o deresolve) name
956 :: pr_tyvar_dicts (filter_out (null o snd) vs)
957 @| pr_eqs name ty eqs
959 val (ps, p) = split_last
960 (pr_funn "let rec" funn :: map (pr_funn "and") funns');
961 in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end
962 | pr_stmt (MLDatas (datas as (data :: datas'))) =
970 Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys)
972 fun pr_data definer (tyco, (vs, [])) =
975 :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
979 | pr_data definer (tyco, (vs, cos)) =
982 :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
984 :: separate (str "|") (map pr_co cos)
986 val (ps, p) = split_last
987 (pr_data "type" data :: map (pr_data "and") datas');
988 in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end
989 | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
991 val w = "_" ^ first_upper v;
992 fun pr_superclass_field (class, classrel) =
994 deresolve classrel, ":", "'" ^ v, deresolve class
996 fun pr_classparam_field (classparam, ty) =
998 (str o deresolve) classparam, str ":", pr_typ NOBR ty
1000 fun pr_classparam_proj (classparam, _) =
1003 (str o deresolve) classparam,
1006 str (w ^ "." ^ deresolve classparam ^ ";;")
1011 (str o deresolve) class,
1013 enum_default "();;" ";" "{" "};;" (
1014 map pr_superclass_field superclasses
1015 @ map pr_classparam_field classparams
1018 :: map pr_classparam_proj classparams
1020 | pr_stmt (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =
1022 fun pr_superclass (_, (classrel, dss)) =
1024 (str o deresolve) classrel,
1026 pr_dicts NOBR [DictConst dss]
1028 fun pr_classparam_inst ((classparam, c_inst), thm) =
1030 (str o deresolve) classparam,
1032 pr_app thm false reserved_names NOBR (c_inst, [])
1037 :: (str o deresolve) inst
1038 :: pr_tyvar_dicts arity
1040 @@ (Pretty.enclose "(" ");;" o Pretty.breaks) [
1041 enum_default "()" ";" "{" "}" (map pr_superclass superarities
1042 @ map pr_classparam_inst classparam_insts),
1044 pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
1050 fun pr_ocaml_module name content =
1052 str ("module " ^ name ^ " = ")
1057 @@ str ("end;; (*struct " ^ name ^ "*)")
1064 | Stmt of string * ml_stmt
1065 | Module of string * ((Name.context * Name.context) * ml_node Graph.T);
1069 fun ml_node_of_program labelled_name module_name reserved_names raw_module_alias program =
1071 val module_alias = if is_some module_name then K module_name else raw_module_alias;
1072 val reserved_names = Name.make_context reserved_names;
1073 val empty_module = ((reserved_names, reserved_names), Graph.empty);
1074 fun map_node [] f = f
1075 | map_node (m::ms) f =
1076 Graph.default_node (m, Module (m, empty_module))
1077 #> Graph.map_node m (fn (Module (module_name, (nsp, nodes))) =>
1078 Module (module_name, (nsp, map_node ms f nodes)));
1079 fun map_nsp_yield [] f (nsp, nodes) =
1081 val (x, nsp') = f nsp
1082 in (x, (nsp', nodes)) end
1083 | map_nsp_yield (m::ms) f (nsp, nodes) =
1087 |> Graph.default_node (m, Module (m, empty_module))
1088 |> Graph.map_node_yield m (fn Module (d_module_name, nsp_nodes) =>
1090 val (x, nsp_nodes') = map_nsp_yield ms f nsp_nodes
1091 in (x, Module (d_module_name, nsp_nodes')) end)
1092 in (x, (nsp, nodes')) end;
1093 fun map_nsp_fun_yield f (nsp_fun, nsp_typ) =
1095 val (x, nsp_fun') = f nsp_fun
1096 in (x, (nsp_fun', nsp_typ)) end;
1097 fun map_nsp_typ_yield f (nsp_fun, nsp_typ) =
1099 val (x, nsp_typ') = f nsp_typ
1100 in (x, (nsp_fun, nsp_typ')) end;
1101 val mk_name_module = mk_name_module reserved_names NONE module_alias program;
1102 fun mk_name_stmt upper name nsp =
1104 val (_, base) = dest_name name;
1105 val base' = if upper then first_upper base else base;
1106 val ([base''], nsp') = Name.variants [base'] nsp;
1107 in (base'', nsp') end;
1108 fun add_funs stmts =
1110 (fn (name, CodeThingol.Fun stmt) =>
1111 map_nsp_fun_yield (mk_name_stmt false name) #>>
1114 error ("Function block containing illegal statement: " ^ labelled_name name)
1116 #>> (split_list #> apsnd MLFuns);
1117 fun add_datatypes stmts =
1119 (fn (name, CodeThingol.Datatype stmt) =>
1120 map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt))
1121 | (name, CodeThingol.Datatypecons _) =>
1122 map_nsp_fun_yield (mk_name_stmt true name) #>> rpair NONE
1124 error ("Datatype block containing illegal statement: " ^ labelled_name name)
1126 #>> (split_list #> apsnd (map_filter I
1127 #> (fn [] => error ("Datatype block without data statement: "
1128 ^ (commas o map (labelled_name o fst)) stmts)
1129 | stmts => MLDatas stmts)));
1130 fun add_class stmts =
1132 (fn (name, CodeThingol.Class info) =>
1133 map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, info))
1134 | (name, CodeThingol.Classrel _) =>
1135 map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
1136 | (name, CodeThingol.Classparam _) =>
1137 map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
1139 error ("Class block containing illegal statement: " ^ labelled_name name)
1141 #>> (split_list #> apsnd (map_filter I
1142 #> (fn [] => error ("Class block without class statement: "
1143 ^ (commas o map (labelled_name o fst)) stmts)
1144 | [stmt] => MLClass stmt)));
1145 fun add_inst [(name, CodeThingol.Classinst stmt)] =
1146 map_nsp_fun_yield (mk_name_stmt false name)
1147 #>> (fn base => ([base], MLClassinst (name, stmt)));
1148 fun add_stmts ((stmts as (_, CodeThingol.Fun _)::_)) =
1150 | add_stmts ((stmts as (_, CodeThingol.Datatypecons _)::_)) =
1152 | add_stmts ((stmts as (_, CodeThingol.Datatype _)::_)) =
1154 | add_stmts ((stmts as (_, CodeThingol.Class _)::_)) =
1156 | add_stmts ((stmts as (_, CodeThingol.Classrel _)::_)) =
1158 | add_stmts ((stmts as (_, CodeThingol.Classparam _)::_)) =
1160 | add_stmts ((stmts as [(_, CodeThingol.Classinst _)])) =
1162 | add_stmts stmts = error ("Illegal mutual dependencies: " ^
1163 (commas o map (labelled_name o fst)) stmts);
1164 fun add_stmts' stmts nsp_nodes =
1166 val names as (name :: names') = map fst stmts;
1169 |> fold (fold (insert (op =)) o Graph.imm_succs program) names
1170 |> subtract (op =) names;
1171 val (module_names, _) = (split_list o map dest_name) names;
1172 val module_name = (the_single o distinct (op =) o map mk_name_module) module_names
1174 error ("Different namespace prefixes for mutual dependencies:\n"
1175 ^ commas (map labelled_name names)
1177 ^ commas module_names);
1178 val module_name_path = NameSpace.explode module_name;
1179 fun add_dep name name' =
1181 val module_name' = (mk_name_module o fst o dest_name) name';
1182 in if module_name = module_name' then
1183 map_node module_name_path (Graph.add_edge (name, name'))
1185 val (common, (diff1::_, diff2::_)) = chop_prefix (op =)
1186 (module_name_path, NameSpace.explode module_name');
1189 (fn node => Graph.add_edge_acyclic (diff1, diff2) node
1190 handle Graph.CYCLES _ => error ("Dependency "
1191 ^ quote name ^ " -> " ^ quote name'
1192 ^ " would result in module dependency cycle"))
1196 |> map_nsp_yield module_name_path (add_stmts stmts)
1197 |-> (fn (base' :: bases', stmt') =>
1198 apsnd (map_node module_name_path (Graph.new_node (name, (Stmt (base', stmt')))
1199 #> fold2 (fn name' => fn base' =>
1200 Graph.new_node (name', (Dummy base'))) names' bases')))
1201 |> apsnd (fold (fn name => fold (add_dep name) deps) names)
1202 |> apsnd (fold_product (curry (map_node module_name_path o Graph.add_edge)) names names)
1204 val (_, nodes) = empty_module
1205 |> fold add_stmts' (map (AList.make (Graph.get_node program))
1206 (rev (Graph.strong_conn program)));
1207 fun deresolver prefix name =
1209 val module_name = (fst o dest_name) name;
1210 val module_name' = (NameSpace.explode o mk_name_module) module_name;
1211 val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name');
1214 |> fold (fn name => fn node => case Graph.get_node node name
1215 of Module (_, (_, node)) => node) module_name'
1216 |> (fn node => case Graph.get_node node name of Stmt (stmt_name, _) => stmt_name
1217 | Dummy stmt_name => stmt_name);
1219 NameSpace.implode (remainder @ [stmt_name])
1220 end handle Graph.UNDEF _ =>
1221 error ("Unknown statement name: " ^ labelled_name name);
1222 in (deresolver, nodes) end;
1224 fun serialize_ml compile pr_module pr_stmt raw_module_name labelled_name reserved_names includes raw_module_alias
1225 _ syntax_tyco syntax_const program cs destination =
1227 val is_cons = CodeThingol.is_cons program;
1228 val stmt_names = stmt_names_of_destination destination;
1229 val module_name = if null stmt_names then raw_module_name else SOME "Code";
1230 val (deresolver, nodes) = ml_node_of_program labelled_name module_name
1231 reserved_names raw_module_alias program;
1232 val reserved_names = CodeName.make_vars reserved_names;
1233 fun pr_node prefix (Dummy _) =
1235 | pr_node prefix (Stmt (_, stmt)) = if null stmt_names orelse
1236 (not o null o filter (member (op =) stmt_names) o stmt_names_of) stmt then SOME
1237 (pr_stmt syntax_tyco syntax_const labelled_name reserved_names
1238 (deresolver prefix) is_cons stmt)
1240 | pr_node prefix (Module (module_name, (_, nodes))) =
1242 val ps = separate (str "")
1243 ((map_filter (pr_node (prefix @ [module_name]) o Graph.get_node nodes)
1244 o rev o flat o Graph.strong_conn) nodes)
1245 in SOME (case destination of String _ => Pretty.chunks ps
1246 | _ => pr_module module_name ps)
1248 val cs' = map_filter (try (deresolver (if is_some module_name then the_list module_name else [])))
1250 val p = Pretty.chunks (separate (str "") (map snd includes @ (map_filter
1251 (pr_node [] o Graph.get_node nodes) o rev o flat o Graph.strong_conn) nodes));
1252 fun output Compile = K NONE o compile o code_of_pretty
1253 | output Export = K NONE o code_writeln
1254 | output (File file) = K NONE o File.write file o code_of_pretty
1255 | output (String _) = SOME o rpair cs' o code_of_pretty;
1256 in output destination p end;
1260 (* ML (system language) code for evaluation and instrumentalization *)
1262 fun ml_code_of thy program cs = mount_serializer thy
1263 (SOME (fn _ => fn [] => serialize_ml (K ()) (K Pretty.chunks) pr_sml_stmt (SOME "")))
1264 target_SML NONE [] program cs (String [])
1267 (* generic entry points for SML/OCaml *)
1269 fun isar_seri_sml module_name =
1270 parse_args (Scan.succeed ())
1271 #> (fn () => serialize_ml (use_text (1, "generated code") Output.ml_output false)
1272 pr_sml_module pr_sml_stmt module_name);
1274 fun isar_seri_ocaml module_name =
1275 parse_args (Scan.succeed ())
1276 #> (fn () => serialize_ml (fn _ => error "OCaml: no internal compilation")
1277 pr_ocaml_module pr_ocaml_stmt module_name);
1280 (** Haskell serializer **)
1282 fun pr_haskell_bind pr_term =
1284 fun pr_bind ((NONE, NONE), _) = str "_"
1285 | pr_bind ((SOME v, NONE), _) = str v
1286 | pr_bind ((NONE, SOME p), _) = p
1287 | pr_bind ((SOME v, SOME p), _) = brackets [str v, str "@", p];
1288 in gen_pr_bind pr_bind pr_term end;
1290 fun pr_haskell_stmt syntax_class syntax_tyco syntax_const labelled_name
1291 init_syms deresolve is_cons contr_classparam_typs deriving_show =
1293 val deresolve_base = NameSpace.base o deresolve;
1294 fun class_name class = case syntax_class class
1295 of NONE => deresolve class
1296 | SOME (class, _) => class;
1297 fun classparam_name class classparam = case syntax_class class
1298 of NONE => deresolve_base classparam
1299 | SOME (_, classparam_syntax) => case classparam_syntax classparam
1300 of NONE => (snd o dest_name) classparam
1301 | SOME classparam => classparam;
1302 fun pr_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs
1304 | classbinds => Pretty.enum "," "(" ")" (
1305 map (fn (v, class) =>
1306 str (class_name class ^ " " ^ CodeName.lookup_var tyvars v)) classbinds)
1308 fun pr_typforall tyvars vs = case map fst vs
1310 | vnames => str "forall " :: Pretty.breaks
1311 (map (str o CodeName.lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
1312 fun pr_tycoexpr tyvars fxy (tyco, tys) =
1313 brackify fxy (str tyco :: map (pr_typ tyvars BR) tys)
1314 and pr_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco
1315 of NONE => pr_tycoexpr tyvars fxy (deresolve tyco, tys)
1316 | SOME (i, pr) => pr (pr_typ tyvars) fxy tys)
1317 | pr_typ tyvars fxy (ITyVar v) = (str o CodeName.lookup_var tyvars) v;
1318 fun pr_typdecl tyvars (vs, tycoexpr) =
1319 Pretty.block (pr_typcontext tyvars vs @| pr_tycoexpr tyvars NOBR tycoexpr);
1320 fun pr_typscheme tyvars (vs, ty) =
1321 Pretty.block (pr_typforall tyvars vs @ pr_typcontext tyvars vs @| pr_typ tyvars NOBR ty);
1322 fun pr_term tyvars thm pat vars fxy (IConst c) =
1323 pr_app tyvars thm pat vars fxy (c, [])
1324 | pr_term tyvars thm pat vars fxy (t as (t1 `$ t2)) =
1325 (case CodeThingol.unfold_const_app t
1326 of SOME app => pr_app tyvars thm pat vars fxy app
1329 pr_term tyvars thm pat vars NOBR t1,
1330 pr_term tyvars thm pat vars BR t2
1332 | pr_term tyvars thm pat vars fxy (IVar v) =
1333 (str o CodeName.lookup_var vars) v
1334 | pr_term tyvars thm pat vars fxy (t as _ `|-> _) =
1336 val (binds, t') = CodeThingol.unfold_abs t;
1337 fun pr ((v, pat), ty) = pr_bind tyvars thm BR ((SOME v, pat), ty);
1338 val (ps, vars') = fold_map pr binds vars;
1339 in brackets (str "\\" :: ps @ str "->" @@ pr_term tyvars thm pat vars' NOBR t') end
1340 | pr_term tyvars thm pat vars fxy (ICase (cases as (_, t0))) =
1341 (case CodeThingol.unfold_const_app t0
1342 of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
1343 then pr_case tyvars thm vars fxy cases
1344 else pr_app tyvars thm pat vars fxy c_ts
1345 | NONE => pr_case tyvars thm vars fxy cases)
1346 and pr_app' tyvars thm pat vars ((c, (_, tys)), ts) = case contr_classparam_typs c
1347 of [] => (str o deresolve) c :: map (pr_term tyvars thm pat vars BR) ts
1348 | fingerprint => let
1349 val ts_fingerprint = ts ~~ curry Library.take (length ts) fingerprint;
1350 val needs_annotation = forall (fn (_, NONE) => true | (t, SOME _) =>
1351 (not o CodeThingol.locally_monomorphic) t) ts_fingerprint;
1352 fun pr_term_anno (t, NONE) _ = pr_term tyvars thm pat vars BR t
1353 | pr_term_anno (t, SOME _) ty =
1354 brackets [pr_term tyvars thm pat vars NOBR t, str "::", pr_typ tyvars NOBR ty];
1356 if needs_annotation then
1357 (str o deresolve) c :: map2 pr_term_anno ts_fingerprint (curry Library.take (length ts) tys)
1358 else (str o deresolve) c :: map (pr_term tyvars thm pat vars BR) ts
1360 and pr_app tyvars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const is_cons
1361 and pr_bind tyvars = pr_haskell_bind (pr_term tyvars)
1362 and pr_case tyvars thm vars fxy (cases as ((_, [_]), _)) =
1364 val (binds, t) = CodeThingol.unfold_let (ICase cases);
1365 fun pr ((pat, ty), t) vars =
1367 |> pr_bind tyvars thm BR ((NONE, SOME pat), ty)
1368 |>> (fn p => semicolon [p, str "=", pr_term tyvars thm false vars NOBR t])
1369 val (ps, vars') = fold_map pr binds vars;
1371 Pretty.block_enclose (
1373 concat [str "}", str "in", pr_term tyvars thm false vars' NOBR t]
1376 | pr_case tyvars thm vars fxy (((td, ty), bs as _ :: _), _) =
1380 val (p, vars') = pr_bind tyvars thm NOBR ((NONE, SOME pat), ty) vars;
1381 in semicolon [p, str "->", pr_term tyvars thm false vars' NOBR t] end;
1383 Pretty.block_enclose (
1384 concat [str "(case", pr_term tyvars thm false vars NOBR td, str "of", str "{"],
1388 | pr_case tyvars thm vars fxy ((_, []), _) = str "error \"empty case\"";
1389 fun pr_stmt (name, CodeThingol.Fun ((vs, ty), [])) =
1391 val tyvars = CodeName.intro_vars (map fst vs) init_syms;
1392 val n = (length o fst o CodeThingol.unfold_fun) ty;
1396 (str o suffix " ::" o deresolve_base) name,
1398 pr_typscheme tyvars (vs, ty),
1402 (str o deresolve_base) name
1403 :: map str (replicate n "_")
1406 @@ (str o (fn s => s ^ ";") o ML_Syntax.print_string
1407 o NameSpace.base o NameSpace.qualifier) name
1411 | pr_stmt (name, CodeThingol.Fun ((vs, ty), eqs)) =
1413 val tyvars = CodeName.intro_vars (map fst vs) init_syms;
1414 fun pr_eq ((ts, t), thm) =
1416 val consts = map_filter
1417 (fn c => if (is_some o syntax_const) c
1418 then NONE else (SOME o NameSpace.base o deresolve) c)
1419 ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);
1420 val vars = init_syms
1421 |> CodeName.intro_vars consts
1422 |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)
1423 (insert (op =)) ts []);
1426 (str o deresolve_base) name
1427 :: map (pr_term tyvars thm true vars BR) ts
1429 @@ pr_term tyvars thm false vars NOBR t
1435 (str o suffix " ::" o deresolve_base) name,
1437 pr_typscheme tyvars (vs, ty),
1443 | pr_stmt (name, CodeThingol.Datatype (vs, [])) =
1445 val tyvars = CodeName.intro_vars (map fst vs) init_syms;
1449 pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
1452 | pr_stmt (name, CodeThingol.Datatype (vs, [(co, [ty])])) =
1454 val tyvars = CodeName.intro_vars (map fst vs) init_syms;
1458 :: pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
1460 :: (str o deresolve_base) co
1461 :: pr_typ tyvars BR ty
1462 :: (if deriving_show name then [str "deriving (Read, Show)"] else [])
1465 | pr_stmt (name, CodeThingol.Datatype (vs, co :: cos)) =
1467 val tyvars = CodeName.intro_vars (map fst vs) init_syms;
1468 fun pr_co (co, tys) =
1470 (str o deresolve_base) co
1471 :: map (pr_typ tyvars BR) tys
1476 :: pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
1479 :: map ((fn p => Pretty.block [str "| ", p]) o pr_co) cos
1480 @ (if deriving_show name then [str "deriving (Read, Show)"] else [])
1483 | pr_stmt (name, CodeThingol.Class (v, (superclasses, classparams))) =
1485 val tyvars = CodeName.intro_vars [v] init_syms;
1486 fun pr_classparam (classparam, ty) =
1488 (str o classparam_name name) classparam,
1490 pr_typ tyvars NOBR ty
1493 Pretty.block_enclose (
1496 Pretty.block (pr_typcontext tyvars [(v, map fst superclasses)]),
1497 str (deresolve_base name ^ " " ^ CodeName.lookup_var tyvars v),
1501 ) (map pr_classparam classparams)
1503 | pr_stmt (_, CodeThingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =
1505 val tyvars = CodeName.intro_vars (map fst vs) init_syms;
1506 fun pr_instdef ((classparam, c_inst), thm) =
1508 (str o classparam_name class) classparam,
1510 pr_app tyvars thm false init_syms NOBR (c_inst, [])
1513 Pretty.block_enclose (
1516 Pretty.block (pr_typcontext tyvars vs),
1517 str (class_name class ^ " "),
1518 pr_typ tyvars BR (tyco `%% map (ITyVar o fst) vs),
1522 ) (map pr_instdef classparam_insts)
1526 fun pretty_haskell_monad c_bind =
1528 fun pretty pr thm pat vars fxy [(t, _)] =
1530 val pr_bind = pr_haskell_bind (K (K pr)) thm;
1531 fun pr_monad (NONE, t) vars =
1532 (semicolon [pr vars NOBR t], vars)
1533 | pr_monad (SOME (bind, true), t) vars = vars
1534 |> pr_bind NOBR bind
1535 |>> (fn p => semicolon [p, str "<-", pr vars NOBR t])
1536 | pr_monad (SOME (bind, false), t) vars = vars
1537 |> pr_bind NOBR bind
1538 |>> (fn p => semicolon [str "let", p, str "=", pr vars NOBR t]);
1539 val (binds, t) = implode_monad c_bind t;
1540 val (ps, vars') = fold_map pr_monad binds vars;
1541 fun brack p = if fixity BR fxy then Pretty.block [str "(", p, str ")"] else p;
1542 in (brack o Pretty.block_enclose (str "do {", str "}")) (ps @| pr vars' NOBR t) end;
1545 fun haskell_program_of_program labelled_name module_name module_prefix reserved_names raw_module_alias program =
1547 val module_alias = if is_some module_name then K module_name else raw_module_alias;
1548 val reserved_names = Name.make_context reserved_names;
1549 val mk_name_module = mk_name_module reserved_names module_prefix module_alias program;
1550 fun add_stmt (name, (stmt, deps)) =
1552 val (module_name, base) = dest_name name;
1553 val module_name' = mk_name_module module_name;
1554 val mk_name_stmt = yield_singleton Name.variants;
1555 fun add_fun upper (nsp_fun, nsp_typ) =
1557 val (base', nsp_fun') =
1558 mk_name_stmt (if upper then first_upper base else base) nsp_fun
1559 in (base', (nsp_fun', nsp_typ)) end;
1560 fun add_typ (nsp_fun, nsp_typ) =
1562 val (base', nsp_typ') = mk_name_stmt (first_upper base) nsp_typ
1563 in (base', (nsp_fun, nsp_typ')) end;
1564 val add_name = case stmt
1565 of CodeThingol.Fun _ => add_fun false
1566 | CodeThingol.Datatype _ => add_typ
1567 | CodeThingol.Datatypecons _ => add_fun true
1568 | CodeThingol.Class _ => add_typ
1569 | CodeThingol.Classrel _ => pair base
1570 | CodeThingol.Classparam _ => add_fun false
1571 | CodeThingol.Classinst _ => pair base;
1572 fun add_stmt' base' = case stmt
1573 of CodeThingol.Datatypecons _ =>
1574 cons (name, (NameSpace.append module_name' base', NONE))
1575 | CodeThingol.Classrel _ => I
1576 | CodeThingol.Classparam _ =>
1577 cons (name, (NameSpace.append module_name' base', NONE))
1578 | _ => cons (name, (NameSpace.append module_name' base', SOME stmt));
1580 Symtab.map_default (module_name', ([], ([], (reserved_names, reserved_names))))
1581 (apfst (fold (insert (op = : string * string -> bool)) deps))
1582 #> `(fn program => add_name ((snd o snd o the o Symtab.lookup program) module_name'))
1583 #-> (fn (base', names) =>
1584 (Symtab.map_entry module_name' o apsnd) (fn (stmts, _) =>
1585 (add_stmt' base' stmts, names)))
1587 val hs_program = fold add_stmt (AList.make (fn name =>
1588 (Graph.get_node program name, Graph.imm_succs program name))
1589 (Graph.strong_conn program |> flat)) Symtab.empty;
1590 fun deresolver name =
1591 (fst o the o AList.lookup (op =) ((fst o snd o the
1592 o Symtab.lookup hs_program) ((mk_name_module o fst o dest_name) name))) name
1593 handle Option => error ("Unknown statement name: " ^ labelled_name name);
1594 in (deresolver, hs_program) end;
1596 fun serialize_haskell module_prefix raw_module_name string_classes labelled_name
1597 reserved_names includes raw_module_alias
1598 syntax_class syntax_tyco syntax_const program cs destination =
1600 val stmt_names = stmt_names_of_destination destination;
1601 val module_name = if null stmt_names then raw_module_name else SOME "Code";
1602 val (deresolver, hs_program) = haskell_program_of_program labelled_name
1603 module_name module_prefix reserved_names raw_module_alias program;
1604 val is_cons = CodeThingol.is_cons program;
1605 val contr_classparam_typs = CodeThingol.contr_classparam_typs program;
1606 fun deriving_show tyco =
1608 fun deriv _ "fun" = false
1609 | deriv tycos tyco = member (op =) tycos tyco orelse
1610 case try (Graph.get_node program) tyco
1611 of SOME (CodeThingol.Datatype (_, cs)) => forall (deriv' (tyco :: tycos))
1614 and deriv' tycos (tyco `%% tys) = deriv tycos tyco
1615 andalso forall (deriv' tycos) tys
1616 | deriv' _ (ITyVar _) = true
1617 in deriv [] tyco end;
1618 val reserved_names = CodeName.make_vars reserved_names;
1619 fun pr_stmt qualified = pr_haskell_stmt syntax_class syntax_tyco
1620 syntax_const labelled_name reserved_names
1621 (if qualified then deresolver else NameSpace.base o deresolver)
1622 is_cons contr_classparam_typs
1623 (if string_classes then deriving_show else K false);
1624 fun pr_module name content =
1625 (name, Pretty.chunks [
1626 str ("module " ^ name ^ " where {"),
1632 fun serialize_module1 (module_name', (deps, (stmts, _))) =
1634 val stmt_names = map fst stmts;
1635 val deps' = subtract (op =) stmt_names deps
1637 |> map_filter (try deresolver);
1638 val qualified = is_none module_name andalso
1639 map deresolver stmt_names @ deps'
1640 |> map NameSpace.base
1641 |> has_duplicates (op =);
1643 |> map NameSpace.qualifier
1645 fun pr_import_include (name, _) = str ("import " ^ name ^ ";");
1646 val pr_import_module = str o (if qualified
1647 then prefix "import qualified "
1648 else prefix "import ") o suffix ";";
1649 val content = Pretty.chunks (
1650 map pr_import_include includes
1651 @ map pr_import_module imports
1653 :: separate (str "") (map_filter
1654 (fn (name, (_, SOME stmt)) => SOME (pr_stmt qualified (name, stmt))
1655 | (_, (_, NONE)) => NONE) stmts)
1657 in pr_module module_name' content end;
1658 fun serialize_module2 (_, (_, (stmts, _))) = Pretty.chunks (
1659 separate (str "") (map_filter
1660 (fn (name, (_, SOME stmt)) => if null stmt_names
1661 orelse member (op =) stmt_names name
1662 then SOME (pr_stmt false (name, stmt))
1664 | (_, (_, NONE)) => NONE) stmts));
1665 val serialize_module = case destination of String _ => pair "" o serialize_module2
1666 | _ => serialize_module1;
1667 fun write_module destination (modlname, content) =
1669 val filename = case modlname
1670 of "" => Path.explode "Main.hs"
1671 | _ => (Path.ext "hs" o Path.explode o implode o separate "/"
1672 o NameSpace.explode) modlname;
1673 val pathname = Path.append destination filename;
1674 val _ = File.mkdir (Path.dir pathname);
1675 in File.write pathname (code_of_pretty content) end
1676 fun output Compile = error ("Haskell: no internal compilation")
1677 | output Export = K NONE o map (code_writeln o snd)
1678 | output (File destination) = K NONE o map (write_module destination)
1679 | output (String _) = SOME o rpair [] o cat_lines o map (code_of_pretty o snd);
1681 output destination (map (uncurry pr_module) includes
1682 @ map serialize_module (Symtab.dest hs_program))
1685 fun isar_seri_haskell module =
1686 parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name)
1687 -- Scan.optional (Args.$$$ "string_classes" >> K true) false
1688 >> (fn (module_prefix, string_classes) =>
1689 serialize_haskell module_prefix module string_classes));
1692 (** optional pretty serialization **)
1700 val xs = string_of_int i;
1701 val ys = replicate_string (3 - length (explode xs)) "0";
1702 in "\\" ^ ys ^ xs end;
1704 val s = if i < 32 orelse i = 34 orelse i = 39 orelse i = 92 orelse i > 126
1708 fun haskell_char c =
1710 val s = ML_Syntax.print_char c;
1711 in if s = "'" then "\\'" else s end;
1713 val pretty : (string * {
1714 pretty_char: string -> string,
1715 pretty_string: string -> string,
1716 pretty_numeral: bool -> int -> string,
1717 pretty_list: Pretty.T list -> Pretty.T,
1718 infix_cons: int * string
1720 ("SML", { pretty_char = prefix "#" o quote o ML_Syntax.print_char,
1721 pretty_string = quote o translate_string ML_Syntax.print_char,
1722 pretty_numeral = fn unbounded => fn k =>
1723 if unbounded then "(" ^ string_of_int k ^ " : IntInf.int)"
1724 else string_of_int k,
1725 pretty_list = Pretty.enum "," "[" "]",
1726 infix_cons = (7, "::")}),
1727 ("OCaml", { pretty_char = enclose "'" "'" o ocaml_char,
1728 pretty_string = quote o translate_string ocaml_char,
1729 pretty_numeral = fn unbounded => fn k => if k >= 0 then
1731 "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
1732 else string_of_int k
1735 "(Big_int.big_int_of_int " ^ (enclose "(" ")" o prefix "-"
1736 o string_of_int o op ~) k ^ ")"
1737 else (enclose "(" ")" o prefix "-" o string_of_int o op ~) k,
1738 pretty_list = Pretty.enum ";" "[" "]",
1739 infix_cons = (6, "::")}),
1740 ("Haskell", { pretty_char = enclose "'" "'" o haskell_char,
1741 pretty_string = quote o translate_string haskell_char,
1742 pretty_numeral = fn unbounded => fn k => if k >= 0 then string_of_int k
1743 else enclose "(" ")" (signed_string_of_int k),
1744 pretty_list = Pretty.enum "," "[" "]",
1745 infix_cons = (5, ":")})
1750 fun pr_pretty target = case AList.lookup (op =) pretty target
1752 | NONE => error ("Unknown code target language: " ^ quote target);
1754 fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
1755 brackify_infix (target_fxy, R) fxy [
1756 pr (INFX (target_fxy, X)) t1,
1758 pr (INFX (target_fxy, R)) t2
1761 fun pretty_list c_nil c_cons target =
1763 val pretty_ops = pr_pretty target;
1764 val mk_list = #pretty_list pretty_ops;
1765 fun pretty pr thm pat vars fxy [(t1, _), (t2, _)] =
1766 case Option.map (cons t1) (implode_list c_nil c_cons t2)
1767 of SOME ts => mk_list (map (pr vars NOBR) ts)
1768 | NONE => default_list (#infix_cons pretty_ops) (pr vars) fxy t1 t2;
1771 fun pretty_list_string c_nil c_cons c_char c_nibbles target =
1773 val pretty_ops = pr_pretty target;
1774 val mk_list = #pretty_list pretty_ops;
1775 val mk_char = #pretty_char pretty_ops;
1776 val mk_string = #pretty_string pretty_ops;
1777 fun pretty pr thm pat vars fxy [(t1, _), (t2, _)] =
1778 case Option.map (cons t1) (implode_list c_nil c_cons t2)
1779 of SOME ts => (case implode_string c_char c_nibbles mk_char mk_string ts
1781 | NONE => mk_list (map (pr vars NOBR) ts))
1782 | NONE => default_list (#infix_cons pretty_ops) (pr vars) fxy t1 t2;
1785 fun pretty_char c_char c_nibbles target =
1787 val mk_char = #pretty_char (pr_pretty target);
1788 fun pretty _ thm _ _ _ [(t1, _), (t2, _)] =
1789 case decode_char c_nibbles (t1, t2)
1790 of SOME c => (str o mk_char) c
1791 | NONE => nerror thm "Illegal character expression";
1794 fun pretty_numeral unbounded negative c_pls c_min c_bit0 c_bit1 target =
1796 val mk_numeral = #pretty_numeral (pr_pretty target);
1797 fun pretty _ thm _ _ _ [(t, _)] =
1798 (str o mk_numeral unbounded o implode_numeral thm negative c_pls c_min c_bit0 c_bit1) t;
1801 fun pretty_message c_char c_nibbles c_nil c_cons target =
1803 val pretty_ops = pr_pretty target;
1804 val mk_char = #pretty_char pretty_ops;
1805 val mk_string = #pretty_string pretty_ops;
1806 fun pretty _ thm _ _ _ [(t, _)] =
1807 case implode_list c_nil c_cons t
1808 of SOME ts => (case implode_string c_char c_nibbles mk_char mk_string ts
1810 | NONE => nerror thm "Illegal message expression")
1811 | NONE => nerror thm "Illegal message expression";
1817 (** serializer use cases **)
1821 fun eval eval'' term_of reff thy ct args =
1823 val _ = if null (term_frees (term_of ct)) then () else error ("Term "
1824 ^ quote (Syntax.string_of_term_global thy (term_of ct))
1825 ^ " to be evaluated contains free variables");
1826 fun eval' program ((vs, ty), t) deps =
1828 val _ = if CodeThingol.contains_dictvar t then
1829 error "Term to be evaluated constains free dictionaries" else ();
1830 val program' = program
1831 |> Graph.new_node (CodeName.value_name, CodeThingol.Fun (([], ty), [(([], t), Drule.dummy_thm)]))
1832 |> fold (curry Graph.add_edge CodeName.value_name) deps;
1833 val (value_code, [value_name']) = ml_code_of thy program' [CodeName.value_name];
1834 val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
1835 ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
1836 in ML_Context.evaluate Output.ml_output false reff sml_code end;
1837 in eval'' thy (fn t => (t, eval')) ct end;
1839 fun eval_conv reff = eval CodeThingol.eval_conv Thm.term_of reff;
1840 fun eval_term reff = eval CodeThingol.eval_term I reff;
1843 (* instrumentalization by antiquotation *)
1847 structure CodeAntiqData = ProofDataFun
1849 type T = string list * (bool * (string * (string * (string * string) list) Susp.T));
1850 fun init _ = ([], (true, ("", Susp.value ("", []))));
1853 val is_first_occ = fst o snd o CodeAntiqData.get;
1855 fun delayed_code thy consts () =
1857 val (consts', program) = CodeThingol.consts_program thy consts;
1858 val (ml_code, consts'') = ml_code_of thy program consts';
1859 val _ = if length consts <> length consts'' then
1860 error ("One of the constants " ^ commas (map (quote o CodeUnit.string_of_const thy) consts)
1861 ^ "\nhas a user-defined serialization") else ();
1862 in (ml_code, consts ~~ consts'') end;
1864 fun register_const const ctxt =
1866 val (consts, (_, (struct_name, _))) = CodeAntiqData.get ctxt;
1867 val consts' = insert (op =) const consts;
1868 val (struct_name', ctxt') = if struct_name = ""
1869 then ML_Antiquote.variant "Code" ctxt
1870 else (struct_name, ctxt);
1871 val acc_code = Susp.delay (delayed_code (ProofContext.theory_of ctxt) consts');
1872 in CodeAntiqData.put (consts', (false, (struct_name', acc_code))) ctxt' end;
1874 fun print_code struct_name is_first const ctxt =
1876 val (consts, (_, (struct_code_name, acc_code))) = CodeAntiqData.get ctxt;
1877 val (raw_ml_code, consts_map) = Susp.force acc_code;
1878 val const'' = NameSpace.append (NameSpace.append struct_name struct_code_name)
1879 ((the o AList.lookup (op =) consts_map) const);
1880 val ml_code = if is_first then "\nstructure " ^ struct_code_name
1881 ^ " =\nstruct\n\n" ^ raw_ml_code ^ "\nend;\n\n"
1883 in (ml_code, const'') end;
1887 fun ml_code_antiq raw_const {struct_name, background} =
1889 val const = CodeUnit.check_const (ProofContext.theory_of background) raw_const;
1890 val is_first = is_first_occ background;
1891 val background' = register_const const background;
1892 in (print_code struct_name is_first const, background') end;
1897 (* code presentation *)
1899 fun code_of thy target module_name cs stmt_names =
1901 val (cs', program) = CodeThingol.consts_program thy cs;
1903 string stmt_names (serialize thy target (SOME module_name) [] program cs')
1907 (* code generation *)
1909 fun read_const_exprs thy cs =
1911 val (cs1, cs2) = CodeName.read_const_exprs thy cs;
1912 val (cs3, program) = CodeThingol.consts_program thy cs2;
1913 val cs4 = CodeThingol.transitivly_non_empty_funs program (abort_allowed thy);
1914 val cs5 = map_filter
1915 (fn (c, c') => if member (op =) cs4 c' then SOME c else NONE) (cs2 ~~ cs3);
1916 in fold (insert (op =)) cs5 cs1 end;
1918 fun cached_program thy =
1920 val program = CodeThingol.cached_program thy;
1921 in (CodeThingol.transitivly_non_empty_funs program (abort_allowed thy), program) end
1923 fun export_code thy cs seris =
1925 val (cs', program) = if null cs then cached_program thy
1926 else CodeThingol.consts_program thy cs;
1927 fun mk_seri_dest dest = case dest
1929 | SOME "-" => export
1930 | SOME f => file (Path.explode f)
1931 val _ = map (fn (((target, module), dest), args) =>
1932 (mk_seri_dest dest (serialize thy target module args program cs'))) seris;
1935 fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs) seris;
1938 (** serializer data **)
1942 datatype 'a mixfix =
1944 | Pretty of Pretty.T;
1946 fun mk_mixfix prep_arg (fixity_this, mfx) =
1948 fun is_arg (Arg _) = true
1950 val i = (length o filter is_arg) mfx;
1951 fun fillin _ [] [] =
1953 | fillin pr (Arg fxy :: mfx) (a :: args) =
1954 (pr fxy o prep_arg) a :: fillin pr mfx args
1955 | fillin pr (Pretty p :: mfx) args =
1956 p :: fillin pr mfx args;
1958 (i, fn pr => fn fixity_ctxt => fn args =>
1959 gen_brackify (fixity fixity_this fixity_ctxt) (fillin pr mfx args))
1962 fun parse_infix prep_arg (x, i) s =
1964 val l = case x of L => INFX (i, L) | _ => INFX (i, X);
1965 val r = case x of R => INFX (i, R) | _ => INFX (i, X);
1967 mk_mixfix prep_arg (INFX (i, x),
1968 [Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r])
1976 fun cert_class thy class =
1978 val _ = AxClass.get_info thy class;
1981 fun read_class thy = cert_class thy o Sign.intern_class thy;
1983 fun cert_tyco thy tyco =
1985 val _ = if Sign.declared_tyname thy tyco then ()
1986 else error ("No such type constructor: " ^ quote tyco);
1989 fun read_tyco thy = cert_tyco thy o Sign.intern_type thy;
1991 fun gen_add_syntax_class prep_class prep_const target raw_class raw_syn thy =
1993 val class = prep_class thy raw_class;
1994 val class' = CodeName.class thy class;
1995 fun mk_classparam c = case AxClass.class_of_param thy c
1996 of SOME class'' => if class = class'' then CodeName.const thy c
1997 else error ("Not a class operation for class " ^ quote class ^ ": " ^ quote c)
1998 | NONE => error ("Not a class operation: " ^ quote c);
1999 fun mk_syntax_params raw_params = AList.lookup (op =)
2000 ((map o apfst) (mk_classparam o prep_const thy) raw_params);
2002 of SOME (syntax, raw_params) =>
2004 |> (map_name_syntax target o apfst o apfst)
2005 (Symtab.update (class', (syntax, mk_syntax_params raw_params)))
2008 |> (map_name_syntax target o apfst o apfst)
2009 (Symtab.delete_safe class')
2012 fun gen_add_syntax_inst prep_class prep_tyco target (raw_tyco, raw_class) add_del thy =
2014 val inst = CodeName.instance thy (prep_class thy raw_class, prep_tyco thy raw_tyco);
2017 |> (map_name_syntax target o apfst o apsnd)
2018 (Symtab.update (inst, ()))
2021 |> (map_name_syntax target o apfst o apsnd)
2022 (Symtab.delete_safe inst)
2025 fun gen_add_syntax_tyco prep_tyco target raw_tyco raw_syn thy =
2027 val tyco = prep_tyco thy raw_tyco;
2028 val tyco' = if tyco = "fun" then "fun" else CodeName.tyco thy tyco;
2029 fun check_args (syntax as (n, _)) = if n <> Sign.arity_number thy tyco
2030 then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
2035 |> (map_name_syntax target o apsnd o apfst)
2036 (Symtab.update (tyco', check_args syntax))
2039 |> (map_name_syntax target o apsnd o apfst)
2040 (Symtab.delete_safe tyco')
2043 fun simple_const_syntax x = (Option.map o apsnd)
2044 (fn pretty => fn pr => fn thm => fn pat => fn vars => pretty (pr vars)) x;
2046 fun gen_add_syntax_const prep_const target raw_c raw_syn thy =
2048 val c = prep_const thy raw_c;
2049 val c' = CodeName.const thy c;
2050 fun check_args (syntax as (n, _)) = if n > CodeUnit.no_args thy c
2051 then error ("Too many arguments in syntax for constant " ^ quote c)
2056 |> (map_name_syntax target o apsnd o apsnd)
2057 (Symtab.update (c', check_args syntax))
2060 |> (map_name_syntax target o apsnd o apsnd)
2061 (Symtab.delete_safe c')
2064 fun add_reserved target =
2066 fun add sym syms = if member (op =) syms sym
2067 then error ("Reserved symbol " ^ quote sym ^ " already declared")
2068 else insert (op =) sym syms
2069 in map_reserved target o add end;
2071 fun add_include target =
2073 fun add (name, SOME content) incls =
2075 val _ = if Symtab.defined incls name
2076 then warning ("Overwriting existing include " ^ name)
2078 in Symtab.update (name, str content) incls end
2079 | add (name, NONE) incls =
2080 Symtab.delete name incls;
2081 in map_includes target o add end;
2083 fun add_module_alias target =
2084 map_module_alias target o Symtab.update o apsnd CodeName.check_modulename;
2086 fun add_monad target raw_c_run raw_c_bind thy =
2088 val c_run = CodeUnit.read_const thy raw_c_run;
2089 val c_bind = CodeUnit.read_const thy raw_c_bind;
2090 val c_bind' = CodeName.const thy c_bind;
2091 in if target = target_Haskell then
2093 |> gen_add_syntax_const (K I) target_Haskell c_run
2094 (SOME (pretty_haskell_monad c_bind'))
2095 |> gen_add_syntax_const (K I) target_Haskell c_bind
2096 (simple_const_syntax (SOME (parse_infix fst (L, 1) ">>=")))
2097 else error "Only Haskell target allows for monad syntax" end;
2099 fun gen_allow_abort prep_cs raw_c thy =
2101 val c = prep_cs thy raw_c;
2102 val c' = CodeName.const thy c;
2103 in thy |> (CodeTargetData.map o apsnd) (insert (op =) c') end;
2105 fun zip_list (x::xs) f g =
2108 fold_map (fn x => g |-- f >> pair x) xs
2109 #-> (fn xys => pair ((x, y) :: xys)));
2112 (* concrete syntax *)
2114 structure P = OuterParse
2115 and K = OuterKeyword
2117 fun parse_multi_syntax parse_thing parse_syntax =
2118 P.and_list1 parse_thing
2119 #-> (fn things => Scan.repeat1 (P.$$$ "(" |-- P.name --
2120 (zip_list things parse_syntax (P.$$$ "and")) --| P.$$$ ")"));
2122 val (infixK, infixlK, infixrK) = ("infix", "infixl", "infixr");
2124 fun parse_mixfix prep_arg s =
2126 val sym_any = Scan.one Symbol.is_regular;
2127 val parse = Scan.optional ($$ "!" >> K true) false -- Scan.repeat (
2128 ($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR))
2129 || ($$ "_" >> K (Arg BR))
2130 || ($$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length))
2132 ( $$ "'" |-- sym_any
2133 || Scan.unless ($$ "_" || $$ "/" || $$ "(" |-- $$ "_" |-- $$ ")")
2134 sym_any) >> (Pretty o str o implode)));
2135 in case Scan.finite Symbol.stopper parse (Symbol.explode s)
2136 of ((_, p as [_]), []) => mk_mixfix prep_arg (NOBR, p)
2137 | ((b, p as _ :: _ :: _), []) => mk_mixfix prep_arg (if b then NOBR else BR, p)
2139 (the_default ("malformed mixfix annotation: " ^ quote s) o snd) Scan.fail ()
2142 fun parse_syntax prep_arg xs =
2144 ((P.$$$ infixK >> K X)
2145 || (P.$$$ infixlK >> K L)
2146 || (P.$$$ infixrK >> K R))
2147 -- P.nat >> parse_infix prep_arg
2148 || Scan.succeed (parse_mixfix prep_arg))
2150 >> (fn (parse, s) => parse s)) xs;
2154 val parse_syntax = parse_syntax;
2156 val add_syntax_class = gen_add_syntax_class cert_class (K I);
2157 val add_syntax_inst = gen_add_syntax_inst cert_class cert_tyco;
2158 val add_syntax_tyco = gen_add_syntax_tyco cert_tyco;
2159 val add_syntax_const = gen_add_syntax_const (K I);
2160 val allow_abort = gen_allow_abort (K I);
2162 val add_syntax_class_cmd = gen_add_syntax_class read_class CodeUnit.read_const;
2163 val add_syntax_inst_cmd = gen_add_syntax_inst read_class read_tyco;
2164 val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco;
2165 val add_syntax_const_cmd = gen_add_syntax_const CodeUnit.read_const;
2166 val allow_abort_cmd = gen_allow_abort CodeUnit.read_const;
2168 fun add_syntax_tycoP target tyco = parse_syntax I >> add_syntax_tyco_cmd target tyco;
2169 fun add_syntax_constP target c = parse_syntax fst >> (add_syntax_const_cmd target c o simple_const_syntax);
2171 fun add_undefined target undef target_undefined thy =
2173 fun pr _ _ _ _ _ _ = str target_undefined;
2176 |> add_syntax_const target undef (SOME (~1, pr))
2179 fun add_pretty_list target nill cons thy =
2181 val nil' = CodeName.const thy nill;
2182 val cons' = CodeName.const thy cons;
2183 val pr = pretty_list nil' cons' target;
2186 |> add_syntax_const target cons (SOME pr)
2189 fun add_pretty_list_string target nill cons charr nibbles thy =
2191 val nil' = CodeName.const thy nill;
2192 val cons' = CodeName.const thy cons;
2193 val charr' = CodeName.const thy charr;
2194 val nibbles' = map (CodeName.const thy) nibbles;
2195 val pr = pretty_list_string nil' cons' charr' nibbles' target;
2198 |> add_syntax_const target cons (SOME pr)
2201 fun add_pretty_char target charr nibbles thy =
2203 val charr' = CodeName.const thy charr;
2204 val nibbles' = map (CodeName.const thy) nibbles;
2205 val pr = pretty_char charr' nibbles' target;
2208 |> add_syntax_const target charr (SOME pr)
2211 fun add_pretty_numeral target unbounded negative number_of pls min bit0 bit1 thy =
2213 val pls' = CodeName.const thy pls;
2214 val min' = CodeName.const thy min;
2215 val bit0' = CodeName.const thy bit0;
2216 val bit1' = CodeName.const thy bit1;
2217 val pr = pretty_numeral unbounded negative pls' min' bit0' bit1' target;
2220 |> add_syntax_const target number_of (SOME pr)
2223 fun add_pretty_message target charr nibbles nill cons str thy =
2225 val charr' = CodeName.const thy charr;
2226 val nibbles' = map (CodeName.const thy) nibbles;
2227 val nil' = CodeName.const thy nill;
2228 val cons' = CodeName.const thy cons;
2229 val pr = pretty_message charr' nibbles' nil' cons' target;
2232 |> add_syntax_const target str (SOME pr)
2239 val (inK, module_nameK, fileK) = ("in", "module_name", "file");
2241 fun code_exprP cmd =
2242 (Scan.repeat P.term_group
2243 -- Scan.repeat (P.$$$ inK |-- P.name
2244 -- Scan.option (P.$$$ module_nameK |-- P.name)
2245 -- Scan.option (P.$$$ fileK |-- P.name)
2246 -- Scan.optional (P.$$$ "(" |-- P.arguments --| P.$$$ ")") []
2247 ) >> (fn (raw_cs, seris) => cmd raw_cs seris));
2249 val _ = List.app OuterKeyword.keyword [infixK, infixlK, infixrK, inK, module_nameK, fileK];
2252 OuterSyntax.command "code_class" "define code syntax for class" K.thy_decl (
2253 parse_multi_syntax P.xname
2254 (Scan.option (P.string -- Scan.optional (P.$$$ "where" |-- Scan.repeat1
2255 (P.term_group --| (P.$$$ "\<equiv>" || P.$$$ "==") -- P.string)) []))
2256 >> (Toplevel.theory oo fold) (fn (target, syns) =>
2257 fold (fn (raw_class, syn) => add_syntax_class_cmd target raw_class syn) syns)
2261 OuterSyntax.command "code_instance" "define code syntax for instance" K.thy_decl (
2262 parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname)
2263 ((P.minus >> K true) || Scan.succeed false)
2264 >> (Toplevel.theory oo fold) (fn (target, syns) =>
2265 fold (fn (raw_inst, add_del) => add_syntax_inst_cmd target raw_inst add_del) syns)
2269 OuterSyntax.command "code_type" "define code syntax for type constructor" K.thy_decl (
2270 parse_multi_syntax P.xname (parse_syntax I)
2271 >> (Toplevel.theory oo fold) (fn (target, syns) =>
2272 fold (fn (raw_tyco, syn) => add_syntax_tyco_cmd target raw_tyco syn) syns)
2276 OuterSyntax.command "code_const" "define code syntax for constant" K.thy_decl (
2277 parse_multi_syntax P.term_group (parse_syntax fst)
2278 >> (Toplevel.theory oo fold) (fn (target, syns) =>
2279 fold (fn (raw_const, syn) => add_syntax_const_cmd target raw_const (simple_const_syntax syn)) syns)
2283 OuterSyntax.command "code_monad" "define code syntax for monads" K.thy_decl (
2284 P.term_group -- P.term_group -- P.name
2285 >> (fn ((raw_run, raw_bind), target) => Toplevel.theory
2286 (add_monad target raw_run raw_bind))
2290 OuterSyntax.command "code_reserved" "declare words as reserved for target language" K.thy_decl (
2291 P.name -- Scan.repeat1 P.name
2292 >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds)
2296 OuterSyntax.command "code_include" "declare piece of code to be included in generated code" K.thy_decl (
2297 P.name -- P.name -- (P.text >> (fn "-" => NONE | s => SOME s))
2298 >> (fn ((target, name), content) => (Toplevel.theory o add_include target)
2303 OuterSyntax.command "code_modulename" "alias module to other name" K.thy_decl (
2304 P.name -- Scan.repeat1 (P.name -- P.name)
2305 >> (fn (target, modlnames) => (Toplevel.theory o fold (add_module_alias target)) modlnames)
2309 OuterSyntax.command "code_abort" "permit constant to be implemented as program abort" K.thy_decl (
2310 Scan.repeat1 P.term_group >> (Toplevel.theory o fold allow_abort_cmd)
2314 OuterSyntax.command "export_code" "generate executable code for constants"
2315 K.diag (P.!!! (code_exprP export_code_cmd) >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
2317 fun shell_command thyname cmd = Toplevel.program (fn _ =>
2318 (use_thy thyname; case Scan.read OuterLex.stopper (P.!!! (code_exprP export_code_cmd)) ((filter OuterLex.is_proper o OuterSyntax.scan) cmd)
2319 of SOME f => (writeln "Now generating code..."; f (theory thyname))
2320 | NONE => error ("Bad directive " ^ quote cmd)))
2321 handle TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
2323 val _ = ML_Context.add_antiq "code" (Args.term >> ml_code_antiq);
2326 (* serializer setup, including serializer defaults *)
2329 add_target (target_SML, isar_seri_sml)
2330 #> add_target (target_OCaml, isar_seri_ocaml)
2331 #> add_target (target_Haskell, isar_seri_haskell)
2332 #> add_syntax_tyco "SML" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
2333 brackify_infix (1, R) fxy [
2334 pr_typ (INFX (1, X)) ty1,
2336 pr_typ (INFX (1, R)) ty2
2338 #> add_syntax_tyco "OCaml" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
2339 brackify_infix (1, R) fxy [
2340 pr_typ (INFX (1, X)) ty1,
2342 pr_typ (INFX (1, R)) ty2
2344 #> add_syntax_tyco "Haskell" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
2345 brackify_infix (1, R) fxy [
2346 pr_typ (INFX (1, X)) ty1,
2348 pr_typ (INFX (1, R)) ty2
2350 #> fold (add_reserved "SML") ML_Syntax.reserved_names
2351 #> fold (add_reserved "SML")
2352 ["o" (*dictionary projections use it already*), "Fail", "div", "mod" (*standard infixes*)]
2353 #> fold (add_reserved "OCaml") [
2354 "and", "as", "assert", "begin", "class",
2355 "constraint", "do", "done", "downto", "else", "end", "exception",
2356 "external", "false", "for", "fun", "function", "functor", "if",
2357 "in", "include", "inherit", "initializer", "lazy", "let", "match", "method",
2358 "module", "mutable", "new", "object", "of", "open", "or", "private", "rec",
2359 "sig", "struct", "then", "to", "true", "try", "type", "val",
2360 "virtual", "when", "while", "with"
2362 #> fold (add_reserved "OCaml") ["failwith", "mod"]
2363 #> fold (add_reserved "Haskell") [
2364 "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
2365 "import", "default", "forall", "let", "in", "class", "qualified", "data",
2366 "newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
2368 #> fold (add_reserved "Haskell") [
2369 "Prelude", "Main", "Bool", "Maybe", "Either", "Ordering", "Char", "String", "Int",
2370 "Integer", "Float", "Double", "Rational", "IO", "Eq", "Ord", "Enum", "Bounded",
2371 "Num", "Real", "Integral", "Fractional", "Floating", "RealFloat", "Monad", "Functor",
2372 "AlreadyExists", "ArithException", "ArrayException", "AssertionFailed", "AsyncException",
2373 "BlockedOnDeadMVar", "Deadlock", "Denormal", "DivideByZero", "DotNetException", "DynException",
2374 "Dynamic", "EOF", "EQ", "EmptyRec", "ErrorCall", "ExitException", "ExitFailure",
2375 "ExitSuccess", "False", "GT", "HeapOverflow",
2376 "IOError", "IOException", "IllegalOperation",
2377 "IndexOutOfBounds", "Just", "Key", "LT", "Left", "LossOfPrecision", "NoMethodError",
2378 "NoSuchThing", "NonTermination", "Nothing", "Obj", "OtherError", "Overflow",
2379 "PatternMatchFail", "PermissionDenied", "ProtocolError", "RecConError", "RecSelError",
2380 "RecUpdError", "ResourceBusy", "ResourceExhausted", "Right", "StackOverflow",
2381 "ThreadKilled", "True", "TyCon", "TypeRep", "UndefinedElement", "Underflow",
2382 "UnsupportedOperation", "UserError", "abs", "absReal", "acos", "acosh", "all",
2383 "and", "any", "appendFile", "asTypeOf", "asciiTab", "asin", "asinh", "atan",
2384 "atan2", "atanh", "basicIORun", "blockIO", "boundedEnumFrom", "boundedEnumFromThen",
2385 "boundedEnumFromThenTo", "boundedEnumFromTo", "boundedPred", "boundedSucc", "break",
2386 "catch", "catchException", "ceiling", "compare", "concat", "concatMap", "const",
2387 "cos", "cosh", "curry", "cycle", "decodeFloat", "denominator", "div", "divMod",
2388 "doubleToRatio", "doubleToRational", "drop", "dropWhile", "either", "elem",
2389 "emptyRec", "encodeFloat", "enumFrom", "enumFromThen", "enumFromThenTo",
2390 "enumFromTo", "error", "even", "exp", "exponent", "fail", "filter", "flip",
2391 "floatDigits", "floatProperFraction", "floatRadix", "floatRange", "floatToRational",
2392 "floor", "fmap", "foldl", "foldl'", "foldl1", "foldr", "foldr1", "fromDouble",
2393 "fromEnum", "fromEnum_0", "fromInt", "fromInteger", "fromIntegral", "fromObj",
2394 "fromRational", "fst", "gcd", "getChar", "getContents", "getLine", "head",
2395 "id", "inRange", "index", "init", "intToRatio", "interact", "ioError", "isAlpha",
2396 "isAlphaNum", "isDenormalized", "isDigit", "isHexDigit", "isIEEE", "isInfinite",
2397 "isLower", "isNaN", "isNegativeZero", "isOctDigit", "isSpace", "isUpper", "iterate", "iterate'",
2398 "last", "lcm", "length", "lex", "lexDigits", "lexLitChar", "lexmatch", "lines", "log",
2399 "logBase", "lookup", "loop", "map", "mapM", "mapM_", "max", "maxBound", "maximum",
2400 "maybe", "min", "minBound", "minimum", "mod", "negate", "nonnull", "not", "notElem",
2401 "null", "numerator", "numericEnumFrom", "numericEnumFromThen", "numericEnumFromThenTo",
2402 "numericEnumFromTo", "odd", "or", "otherwise", "pi", "pred",
2403 "print", "product", "properFraction", "protectEsc", "putChar", "putStr", "putStrLn",
2404 "quot", "quotRem", "range", "rangeSize", "rationalToDouble", "rationalToFloat",
2405 "rationalToRealFloat", "read", "readDec", "readField", "readFieldName", "readFile",
2406 "readFloat", "readHex", "readIO", "readInt", "readList", "readLitChar", "readLn",
2407 "readOct", "readParen", "readSigned", "reads", "readsPrec", "realFloatToRational",
2408 "realToFrac", "recip", "reduce", "rem", "repeat", "replicate", "return", "reverse",
2409 "round", "scaleFloat", "scanl", "scanl1", "scanr", "scanr1", "seq", "sequence",
2410 "sequence_", "show", "showChar", "showException", "showField", "showList",
2411 "showLitChar", "showParen", "showString", "shows", "showsPrec", "significand",
2412 "signum", "signumReal", "sin", "sinh", "snd", "span", "splitAt", "sqrt", "subtract",
2413 "succ", "sum", "tail", "take", "takeWhile", "takeWhile1", "tan", "tanh", "threadToIOResult",
2414 "throw", "toEnum", "toInt", "toInteger", "toObj", "toRational", "truncate", "uncurry",
2415 "undefined", "unlines", "unsafeCoerce", "unsafeIndex", "unsafeRangeSize", "until", "unwords",
2416 "unzip", "unzip3", "userError", "words", "writeFile", "zip", "zip3", "zipWith", "zipWith3"
2417 ] (*due to weird handling of ':', we can't do anything else than to import *all* prelude symbols*);