src/Tools/code/code_target.ML
author haftmann
Fri Jul 11 09:02:33 2008 +0200 (2008-07-11)
changeset 27550 e97d61a67063
parent 27437 727297fcf7c8
child 27710 29702aa892a5
permissions -rw-r--r--
simple inheritance concept
     1 (*  Title:      Tools/code/code_target.ML
     2     ID:         $Id$
     3     Author:     Florian Haftmann, TU Muenchen
     4 
     5 Serializer from intermediate language ("Thin-gol")
     6 to target languages (like SML or Haskell).
     7 *)
     8 
     9 signature CODE_TARGET =
    10 sig
    11   include BASIC_CODE_THINGOL;
    12 
    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;
    20 
    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;
    30 
    31   val allow_abort: string -> theory -> theory;
    32 
    33   type serialization;
    34   type serializer;
    35   val add_target: string * serializer -> theory -> theory;
    36   val extend_target: string * (string * (CodeThingol.program -> CodeThingol.program))
    37     -> theory -> theory;
    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;
    45 
    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;
    52 
    53   val setup: theory -> theory;
    54   val code_width: int ref;
    55 
    56   val ml_code_of: theory -> CodeThingol.program -> string list -> string * string list;
    57 end;
    58 
    59 structure CodeTarget : CODE_TARGET =
    60 struct
    61 
    62 open BasicCodeThingol;
    63 
    64 (** basics **)
    65 
    66 infixr 5 @@;
    67 infixr 5 @|;
    68 fun x @@ y = [x, y];
    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;
    76 
    77 datatype destination = Compile | Export | File of Path.T | String of string list;
    78 type serialization = destination -> (string * string list) option;
    79 
    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;
    84 
    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)));
    90 
    91 fun stmt_names_of_destination (String stmts) = stmts
    92   | stmt_names_of_destination _ = [];
    93 
    94 
    95 (** generic syntax **)
    96 
    97 datatype lrx = L | R | X;
    98 
    99 datatype fixity =
   100     BR
   101   | NOBR
   102   | INFX of (int * lrx);
   103 
   104 val APP = INFX (~1, L);
   105 
   106 fun fixity_lrx L L = false
   107   | fixity_lrx R R = false
   108   | fixity_lrx _ _ = true;
   109 
   110 fun fixity NOBR _ = false
   111   | fixity _ NOBR = false
   112   | fixity (INFX (pr, lr)) (INFX (pr_ctxt, lr_ctxt)) =
   113       pr < pr_ctxt
   114       orelse pr = pr_ctxt
   115         andalso fixity_lrx lr lr_ctxt
   116       orelse pr_ctxt = ~1
   117   | fixity BR (INFX _) = false
   118   | fixity _ _ = true;
   119 
   120 fun gen_brackify _ [p] = p
   121   | gen_brackify true (ps as _::_) = Pretty.enclose "(" ")" ps
   122   | gen_brackify false (ps as _::_) = Pretty.block ps;
   123 
   124 fun brackify fxy_ctxt =
   125   gen_brackify (fixity BR fxy_ctxt) o Pretty.breaks;
   126 
   127 fun brackify_infix infx fxy_ctxt =
   128   gen_brackify (fixity (INFX infx) fxy_ctxt) o Pretty.breaks;
   129 
   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);
   135 
   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
   141 };
   142 
   143 
   144 (** theory data **)
   145 
   146 val target_SML = "SML";
   147 val target_OCaml = "OCaml";
   148 val target_Haskell = "Haskell";
   149 
   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))
   161   );
   162 
   163 type serializer =
   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*)
   175   -> serialization;
   176 
   177 datatype serializer_entry = Serializer of serializer
   178   | Extends of string * (CodeThingol.program -> CodeThingol.program);
   179 
   180 datatype target = Target of {
   181   serial: serial,
   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
   187 };
   188 
   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))
   205     ))
   206   else
   207     error ("Incompatible serializers: " ^ quote target);
   208 
   209 structure CodeTargetData = TheoryDataFun
   210 (
   211   type T = target Symtab.table * string list;
   212   val empty = (Symtab.empty, []);
   213   val copy = I;
   214   val extend = I;
   215   fun merge _ ((target1, exc1) : T, (target2, exc2)) =
   216     (Symtab.join (merge_target true) (target1, target2), Library.merge (op =) (exc1, exc2));
   217 );
   218 
   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;
   224 
   225 val abort_allowed = snd o CodeTargetData.get;
   226 
   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);
   231 
   232 fun put_target (target, seri) thy =
   233   let
   234     val defined_target = is_some o Symtab.lookup (fst (CodeTargetData.get thy));
   235     val _ = case seri
   236      of Extends (super, _) => if defined_target super then ()
   237           else error ("No such target: " ^ quote super)
   238       | _ => ();
   239     val _ = if defined_target target
   240       then warning ("Overwriting existing target " ^ quote target)
   241       else ();
   242   in
   243     thy
   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)),
   247               Symtab.empty))))
   248           ((map_target o apfst o apsnd o K) seri)
   249   end;
   250 
   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));
   254 
   255 fun map_target_data target f thy =
   256   let
   257     val _ = assert_target thy target;
   258   in
   259     thy
   260     |> (CodeTargetData.map o apfst o Symtab.map_entry target o map_target) f
   261   end;
   262 
   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;
   271 
   272 fun invoke_serializer thy modify abortable serializer reserved includes 
   273     module_alias class inst tyco const module args program1 cs1 =
   274   let
   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));
   285   in
   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)
   289       program4 cs2
   290   end;
   291 
   292 fun mount_serializer thy alt_serializer target =
   293   let
   294     val (targets, abortable) = CodeTargetData.get thy;
   295     fun collapse_hierarchy target =
   296       let
   297         val data = case Symtab.lookup targets target
   298          of SOME data => data
   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
   305       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;
   313   in
   314     invoke_serializer thy modify abortable serializer reserved
   315       includes module_alias class inst tyco const
   316   end;
   317 
   318 fun serialize thy = mount_serializer thy NONE;
   319 
   320 fun parse_args f args =
   321   case Scan.read Args.stopper f args
   322    of SOME x => x
   323     | NONE => error "Bad serializer arguments";
   324 
   325 
   326 (** generic code combinators **)
   327 
   328 (* list, char, string, numeral and monad abstract syntax transformations *)
   329 
   330 fun nerror thm s = error (s ^ ",\nin equation " ^ Display.string_of_thm thm);
   331 
   332 fun implode_list c_nil c_cons t =
   333   let
   334     fun dest_cons (IConst (c, _) `$ t1 `$ t2) =
   335           if c = c_cons
   336           then SOME (t1, t2)
   337           else NONE
   338       | dest_cons _ = NONE;
   339     val (ts, t') = CodeThingol.unfoldr dest_cons t;
   340   in case t'
   341    of IConst (c, _) => if c = c_nil then SOME ts else NONE
   342     | _ => NONE
   343   end;
   344 
   345 fun decode_char c_nibbles (IConst (c1, _), IConst (c2, _)) =
   346       let
   347         fun idx c = find_index (curry (op =) c) c_nibbles;
   348         fun decode ~1 _ = NONE
   349           | decode _ ~1 = NONE
   350           | decode n m = SOME (chr (n * 16 + m));
   351       in decode (idx c1) (idx c2) end
   352   | decode_char _ _ = NONE;
   353 
   354 fun implode_string c_char c_nibbles mk_char mk_string ts =
   355   let
   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'
   362     else NONE
   363   end;
   364 
   365 fun implode_numeral thm negative c_pls c_min c_bit0 c_bit1 =
   366   let
   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;
   380 
   381 fun implode_monad c_bind t =
   382   let
   383     fun dest_monad (IConst (c, _) `$ t1 `$ t2) =
   384           if c = c_bind
   385             then case CodeThingol.split_abs t2
   386              of SOME (((v, pat), ty), t') =>
   387                   SOME ((SOME (((SOME v, pat), ty), true), t1), t')
   388               | NONE => NONE
   389             else NONE
   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')
   393             | NONE => NONE;
   394   in CodeThingol.unfoldr dest_monad t end;
   395 
   396 
   397 (* applications and bindings *)
   398 
   399 fun gen_pr_app pr_app pr_term syntax_const is_cons thm pat
   400     vars fxy (app as ((c, (_, tys)), ts)) =
   401   case syntax_const c
   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)
   405     | SOME (i, pr) =>
   406         let
   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);
   409         in if k = length ts
   410           then pr' fxy ts
   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 app k)
   415         end;
   416 
   417 fun gen_pr_bind pr_bind pr_term thm (fxy : fixity) ((v, pat), ty : itype) vars =
   418   let
   419     val vs = case pat
   420      of SOME pat => CodeThingol.fold_varnames (insert (op =)) pat []
   421       | NONE => [];
   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;
   427 
   428 
   429 (* name auxiliary *)
   430 
   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;
   433 
   434 val dest_name =
   435   apfst NameSpace.implode o split_last o fst o split_last o NameSpace.explode;
   436 
   437 fun mk_name_module reserved_names module_prefix module_alias program =
   438   let
   439     fun mk_alias name = case module_alias name
   440      of SOME name' => name'
   441       | NONE => name
   442           |> NameSpace.explode
   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
   447       | NONE => name;
   448     val tab =
   449       Symtab.empty
   450       |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))
   451            o fst o dest_name o fst)
   452              program
   453   in the o Symtab.lookup tab end;
   454 
   455 
   456 
   457 (** SML/OCaml serializer **)
   458 
   459 datatype ml_stmt =
   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));
   466 
   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];
   471 
   472 fun pr_sml_stmt syntax_tyco syntax_const labelled_name reserved_names deresolve is_cons =
   473   let
   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 =
   478       let
   479         fun pr_dictvar (v, (_, 1)) = first_upper v ^ "_"
   480           | pr_dictvar (v, (i, _)) = first_upper v ^ string_of_int (i+1) ^ "_";
   481         fun pr_proj [] p =
   482               p
   483           | pr_proj [p'] p =
   484               brackets [p', p]
   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)
   491       in case ds
   492        of [] => str "()"
   493         | [d] => pr_dict fxy d
   494         | _ :: _ => (Pretty.list "(" ")" o map (pr_dict NOBR)) ds
   495       end;
   496     fun pr_tyvar_dicts vs =
   497       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) =
   502       let
   503         val tyco' = (str o deresolve) tyco
   504       in case map (pr_typ BR) tys
   505        of [] => tyco'
   506         | [p] => Pretty.block [p, Pretty.brk 1, tyco']
   507         | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
   508       end
   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
   520             | NONE =>
   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 _ `|-> _) =
   523           let
   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
   538         val k = length tys
   539       in if k < 2 then 
   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 app k)] end else
   544         (str o deresolve) c
   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 ((_, [_]), _)) =
   553           let
   554             val (binds, t') = CodeThingol.unfold_let (ICase cases);
   555             fun pr ((pat, ty), t) vars =
   556               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;
   560           in
   561             Pretty.chunks [
   562               [str ("let"), Pretty.fbrk, Pretty.chunks ps] |> Pretty.block,
   563               [str ("in"), Pretty.fbrk, pr_term thm false vars' NOBR t'] |> Pretty.block,
   564               str ("end")
   565             ]
   566           end
   567       | pr_case thm vars fxy (((td, ty), b::bs), _) =
   568           let
   569             fun pr delim (pat, t) =
   570               let
   571                 val (p, vars') = pr_bind thm NOBR ((NONE, SOME pat), ty) vars;
   572               in
   573                 concat [str delim, p, str "=>", pr_term thm false vars' NOBR t]
   574               end;
   575           in
   576             (Pretty.enclose "(" ")" o single o brackify fxy) (
   577               str "case"
   578               :: pr_term thm false vars NOBR td
   579               :: pr "of" b
   580               :: map (pr "|") bs
   581             )
   582           end
   583       | pr_case thm vars fxy ((_, []), _) = str "raise Fail \"empty case\"";
   584     fun pr_stmt (MLFuns (funns as (funn :: funns'))) =
   585           let
   586             val definer =
   587               let
   588                 fun no_args _ (((ts, _), _) :: _) = length ts
   589                   | no_args ty [] = (length o fst o CodeThingol.unfold_fun) ty;
   590                 fun mk 0 [] = "val"
   591                   | mk 0 vs = if (null o filter_out (null o snd)) vs
   592                       then "val" else "fun"
   593                   | mk k _ = "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), [])) =
   601                   let
   602                     val vs_dict = filter_out (null o snd) vs;
   603                     val n = length vs_dict + (length o fst o CodeThingol.unfold_fun) ty;
   604                     val exc_str =
   605                       (ML_Syntax.print_string o NameSpace.base o NameSpace.qualifier) name;
   606                   in
   607                     concat (
   608                       str definer
   609                       :: (str o deresolve) name
   610                       :: map str (replicate n "_")
   611                       @ str "="
   612                       :: str "raise"
   613                       :: str "(Fail"
   614                       @@ str (exc_str ^ ")")
   615                     )
   616                   end
   617               | pr_funn definer (name, ((vs, ty), eqs as eq :: eqs')) =
   618                   let
   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) =
   623                       let
   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 []);
   632                       in
   633                         concat (
   634                           [str definer, (str o deresolve) name]
   635                           @ (if null ts andalso null vs_dict
   636                              then [str ":", pr_typ NOBR ty]
   637                              else
   638                                pr_tyvar_dicts vs_dict
   639                                @ map (pr_term thm true vars BR) ts)
   640                        @ [str "=", pr_term thm false vars NOBR t]
   641                         )
   642                       end
   643                   in
   644                     (Pretty.block o Pretty.fbreaks o shift) (
   645                       pr_eq definer eq
   646                       :: map (pr_eq "|") eqs'
   647                     )
   648                   end;
   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'))) =
   652           let
   653             fun pr_co (co, []) =
   654                   str (deresolve co)
   655               | pr_co (co, tys) =
   656                   concat [
   657                     str (deresolve co),
   658                     str "of",
   659                     Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys)
   660                   ];
   661             fun pr_data definer (tyco, (vs, [])) =
   662                   concat (
   663                     str definer
   664                     :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
   665                     :: str "="
   666                     @@ str "EMPTY__" 
   667                   )
   668               | pr_data definer (tyco, (vs, cos)) =
   669                   concat (
   670                     str definer
   671                     :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
   672                     :: str "="
   673                     :: separate (str "|") (map pr_co cos)
   674                   );
   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)))) =
   679           let
   680             val w = first_upper v ^ "_";
   681             fun pr_superclass_field (class, classrel) =
   682               (concat o map str) [
   683                 pr_label_classrel classrel, ":", "'" ^ v, deresolve class
   684               ];
   685             fun pr_classparam_field (classparam, ty) =
   686               concat [
   687                 (str o pr_label_classparam) classparam, str ":", pr_typ NOBR ty
   688               ];
   689             fun pr_classparam_proj (classparam, _) =
   690               semicolon [
   691                 str "fun",
   692                 (str o deresolve) classparam,
   693                 Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolve class)],
   694                 str "=",
   695                 str ("#" ^ pr_label_classparam classparam),
   696                 str w
   697               ];
   698             fun pr_superclass_proj (_, classrel) =
   699               semicolon [
   700                 str "fun",
   701                 (str o deresolve) classrel,
   702                 Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolve class)],
   703                 str "=",
   704                 str ("#" ^ pr_label_classrel classrel),
   705                 str w
   706               ];
   707           in
   708             Pretty.chunks (
   709               concat [
   710                 str ("type '" ^ v),
   711                 (str o deresolve) class,
   712                 str "=",
   713                 Pretty.enum "," "{" "};" (
   714                   map pr_superclass_field superclasses @ map pr_classparam_field classparams
   715                 )
   716               ]
   717               :: map pr_superclass_proj superclasses
   718               @ map pr_classparam_proj classparams
   719             )
   720           end
   721      | pr_stmt (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =
   722           let
   723             fun pr_superclass (_, (classrel, dss)) =
   724               concat [
   725                 (str o pr_label_classrel) classrel,
   726                 str "=",
   727                 pr_dicts NOBR [DictConst dss]
   728               ];
   729             fun pr_classparam ((classparam, c_inst), thm) =
   730               concat [
   731                 (str o pr_label_classparam) classparam,
   732                 str "=",
   733                 pr_app thm false reserved_names NOBR (c_inst, [])
   734               ];
   735           in
   736             semicolon ([
   737               str (if null arity then "val" else "fun"),
   738               (str o deresolve) inst ] @
   739               pr_tyvar_dicts arity @ [
   740               str "=",
   741               Pretty.enum "," "{" "}"
   742                 (map pr_superclass superarities @ map pr_classparam classparam_insts),
   743               str ":",
   744               pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
   745             ])
   746           end;
   747   in pr_stmt end;
   748 
   749 fun pr_sml_module name content =
   750   Pretty.chunks (
   751     str ("structure " ^ name ^ " = ")
   752     :: str "struct"
   753     :: str ""
   754     :: content
   755     @ str ""
   756     @@ str ("end; (*struct " ^ name ^ "*)")
   757   );
   758 
   759 fun pr_ocaml_stmt syntax_tyco syntax_const labelled_name reserved_names deresolve is_cons =
   760   let
   761     fun pr_dicts fxy ds =
   762       let
   763         fun pr_dictvar (v, (_, 1)) = "_" ^ first_upper v
   764           | pr_dictvar (v, (i, _)) = "_" ^ first_upper v ^ string_of_int (i+1);
   765         fun pr_proj ps p =
   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)
   771       in case ds
   772        of [] => str "()"
   773         | [d] => pr_dict fxy d
   774         | _ :: _ => (Pretty.list "(" ")" o map (pr_dict NOBR)) ds
   775       end;
   776     fun pr_tyvar_dicts vs =
   777       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) =
   782       let
   783         val tyco' = (str o deresolve) tyco
   784       in case map (pr_typ BR) tys
   785        of [] => tyco'
   786         | [p] => Pretty.block [p, Pretty.brk 1, tyco']
   787         | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
   788       end
   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
   800             | NONE =>
   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 _ `|-> _) =
   803           let
   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)) =
   814       if is_cons c then
   815         if length tys = length ts
   816         then case 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 app (length tys))]
   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 ((_, [_]), _)) =
   831           let
   832             val (binds, t') = CodeThingol.unfold_let (ICase cases);
   833             fun pr ((pat, ty), t) vars =
   834               vars
   835               |> pr_bind thm NOBR ((NONE, SOME pat), ty)
   836               |>> (fn p => concat
   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), _) =
   841           let
   842             fun pr delim (pat, t) =
   843               let
   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;
   846           in
   847             (Pretty.enclose "(" ")" o single o brackify fxy) (
   848               str "match"
   849               :: pr_term thm false vars NOBR td
   850               :: pr "with" b
   851               :: map (pr "|") bs
   852             )
   853           end
   854       | pr_case thm vars fxy ((_, []), _) = str "failwith \"empty case\"";
   855     fun fish_params vars eqs =
   856       let
   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')) =
   869           let
   870             fun pr_eq ((ts, t), thm) =
   871               let
   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 []);
   880               in concat [
   881                 (Pretty.block o Pretty.commas) (map (pr_term thm true vars NOBR) ts),
   882                 str "->",
   883                 pr_term thm false vars NOBR t
   884               ] end;
   885             fun pr_eqs name ty [] =
   886                   let
   887                     val n = (length o fst o CodeThingol.unfold_fun) ty;
   888                     val exc_str =
   889                       (ML_Syntax.print_string o NameSpace.base o NameSpace.qualifier) name;
   890                   in
   891                     concat (
   892                       map str (replicate n "_")
   893                       @ str "="
   894                       :: str "failwith"
   895                       @@ str exc_str
   896                     )
   897                   end
   898               | pr_eqs _ _ [((ts, t), thm)] =
   899                   let
   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 []);
   908                   in
   909                     concat (
   910                       map (pr_term thm true vars BR) ts
   911                       @ str "="
   912                       @@ pr_term thm false vars NOBR t
   913                     )
   914                   end
   915               | pr_eqs _ _ (eqs as (eq as (([_], _), _)) :: eqs') =
   916                   Pretty.block (
   917                     str "="
   918                     :: Pretty.brk 1
   919                     :: str "function"
   920                     :: Pretty.brk 1
   921                     :: pr_eq eq
   922                     :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
   923                           o single o pr_eq) eqs'
   924                   )
   925               | pr_eqs _ _ (eqs as eq :: eqs') =
   926                   let
   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;
   935                   in
   936                     Pretty.block (
   937                       Pretty.breaks dummy_parms
   938                       @ Pretty.brk 1
   939                       :: str "="
   940                       :: Pretty.brk 1
   941                       :: str "match"
   942                       :: Pretty.brk 1
   943                       :: (Pretty.block o Pretty.commas) dummy_parms
   944                       :: Pretty.brk 1
   945                       :: str "with"
   946                       :: Pretty.brk 1
   947                       :: pr_eq eq
   948                       :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
   949                            o single o pr_eq) eqs'
   950                     )
   951                   end;
   952             fun pr_funn definer (name, ((vs, ty), eqs)) =
   953               concat (
   954                 str definer
   955                 :: (str o deresolve) name
   956                 :: pr_tyvar_dicts (filter_out (null o snd) vs)
   957                 @| pr_eqs name ty eqs
   958               );
   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'))) =
   963           let
   964             fun pr_co (co, []) =
   965                   str (deresolve co)
   966               | pr_co (co, tys) =
   967                   concat [
   968                     str (deresolve co),
   969                     str "of",
   970                     Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys)
   971                   ];
   972             fun pr_data definer (tyco, (vs, [])) =
   973                   concat (
   974                     str definer
   975                     :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
   976                     :: str "="
   977                     @@ str "EMPTY_"
   978                   )
   979               | pr_data definer (tyco, (vs, cos)) =
   980                   concat (
   981                     str definer
   982                     :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
   983                     :: str "="
   984                     :: separate (str "|") (map pr_co cos)
   985                   );
   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)))) =
   990           let
   991             val w = "_" ^ first_upper v;
   992             fun pr_superclass_field (class, classrel) =
   993               (concat o map str) [
   994                 deresolve classrel, ":", "'" ^ v, deresolve class
   995               ];
   996             fun pr_classparam_field (classparam, ty) =
   997               concat [
   998                 (str o deresolve) classparam, str ":", pr_typ NOBR ty
   999               ];
  1000             fun pr_classparam_proj (classparam, _) =
  1001               concat [
  1002                 str "let",
  1003                 (str o deresolve) classparam,
  1004                 str w,
  1005                 str "=",
  1006                 str (w ^ "." ^ deresolve classparam ^ ";;")
  1007               ];
  1008           in Pretty.chunks (
  1009             concat [
  1010               str ("type '" ^ v),
  1011               (str o deresolve) class,
  1012               str "=",
  1013               enum_default "();;" ";" "{" "};;" (
  1014                 map pr_superclass_field superclasses
  1015                 @ map pr_classparam_field classparams
  1016               )
  1017             ]
  1018             :: map pr_classparam_proj classparams
  1019           ) end
  1020      | pr_stmt (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =
  1021           let
  1022             fun pr_superclass (_, (classrel, dss)) =
  1023               concat [
  1024                 (str o deresolve) classrel,
  1025                 str "=",
  1026                 pr_dicts NOBR [DictConst dss]
  1027               ];
  1028             fun pr_classparam_inst ((classparam, c_inst), thm) =
  1029               concat [
  1030                 (str o deresolve) classparam,
  1031                 str "=",
  1032                 pr_app thm false reserved_names NOBR (c_inst, [])
  1033               ];
  1034           in
  1035             concat (
  1036               str "let"
  1037               :: (str o deresolve) inst
  1038               :: pr_tyvar_dicts arity
  1039               @ str "="
  1040               @@ (Pretty.enclose "(" ");;" o Pretty.breaks) [
  1041                 enum_default "()" ";" "{" "}" (map pr_superclass superarities
  1042                   @ map pr_classparam_inst classparam_insts),
  1043                 str ":",
  1044                 pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
  1045               ]
  1046             )
  1047           end;
  1048   in pr_stmt end;
  1049 
  1050 fun pr_ocaml_module name content =
  1051   Pretty.chunks (
  1052     str ("module " ^ name ^ " = ")
  1053     :: str "struct"
  1054     :: str ""
  1055     :: content
  1056     @ str ""
  1057     @@ str ("end;; (*struct " ^ name ^ "*)")
  1058   );
  1059 
  1060 local
  1061 
  1062 datatype ml_node =
  1063     Dummy of string
  1064   | Stmt of string * ml_stmt
  1065   | Module of string * ((Name.context * Name.context) * ml_node Graph.T);
  1066 
  1067 in
  1068 
  1069 fun ml_node_of_program labelled_name module_name reserved_names raw_module_alias program =
  1070   let
  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) =
  1080           let
  1081             val (x, nsp') = f nsp
  1082           in (x, (nsp', nodes)) end
  1083       | map_nsp_yield (m::ms) f (nsp, nodes) =
  1084           let
  1085             val (x, nodes') =
  1086               nodes
  1087               |> Graph.default_node (m, Module (m, empty_module))
  1088               |> Graph.map_node_yield m (fn Module (d_module_name, nsp_nodes) => 
  1089                   let
  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) =
  1094       let
  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) =
  1098       let
  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 =
  1103       let
  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 =
  1109       fold_map
  1110         (fn (name, CodeThingol.Fun stmt) =>
  1111               map_nsp_fun_yield (mk_name_stmt false name) #>>
  1112                 rpair (name, stmt)
  1113           | (name, _) =>
  1114               error ("Function block containing illegal statement: " ^ labelled_name name)
  1115         ) stmts
  1116       #>> (split_list #> apsnd MLFuns);
  1117     fun add_datatypes stmts =
  1118       fold_map
  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
  1123           | (name, _) =>
  1124               error ("Datatype block containing illegal statement: " ^ labelled_name name)
  1125         ) stmts
  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 =
  1131       fold_map
  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
  1138           | (name, _) =>
  1139               error ("Class block containing illegal statement: " ^ labelled_name name)
  1140         ) stmts
  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 _)::_)) =
  1149           add_funs stmts
  1150       | add_stmts ((stmts as (_, CodeThingol.Datatypecons _)::_)) =
  1151           add_datatypes stmts
  1152       | add_stmts ((stmts as (_, CodeThingol.Datatype _)::_)) =
  1153           add_datatypes stmts
  1154       | add_stmts ((stmts as (_, CodeThingol.Class _)::_)) =
  1155           add_class stmts
  1156       | add_stmts ((stmts as (_, CodeThingol.Classrel _)::_)) =
  1157           add_class stmts
  1158       | add_stmts ((stmts as (_, CodeThingol.Classparam _)::_)) =
  1159           add_class stmts
  1160       | add_stmts ((stmts as [(_, CodeThingol.Classinst _)])) =
  1161           add_inst stmts
  1162       | add_stmts stmts = error ("Illegal mutual dependencies: " ^
  1163           (commas o map (labelled_name o fst)) stmts);
  1164     fun add_stmts' stmts nsp_nodes =
  1165       let
  1166         val names as (name :: names') = map fst stmts;
  1167         val deps =
  1168           []
  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
  1173           handle Empty =>
  1174             error ("Different namespace prefixes for mutual dependencies:\n"
  1175               ^ commas (map labelled_name names)
  1176               ^ "\n"
  1177               ^ commas module_names);
  1178         val module_name_path = NameSpace.explode module_name;
  1179         fun add_dep name name' =
  1180           let
  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'))
  1184           else let
  1185             val (common, (diff1::_, diff2::_)) = chop_prefix (op =)
  1186               (module_name_path, NameSpace.explode module_name');
  1187           in
  1188             map_node common
  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"))
  1193           end end;
  1194       in
  1195         nsp_nodes
  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)
  1203       end;
  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 = 
  1208       let
  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');
  1212         val stmt_name =
  1213           nodes
  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);
  1218       in
  1219         NameSpace.implode (remainder @ [stmt_name])
  1220       end handle Graph.UNDEF _ =>
  1221         error ("Unknown statement name: " ^ labelled_name name);
  1222   in (deresolver, nodes) end;
  1223 
  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 =
  1226   let
  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 _) =
  1234           NONE
  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)
  1239           else NONE
  1240       | pr_node prefix (Module (module_name, (_, nodes))) =
  1241           let
  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)
  1247           end;
  1248     val cs' = map_filter (try (deresolver (if is_some module_name then the_list module_name else [])))
  1249       cs;
  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;
  1257 
  1258 end; (*local*)
  1259 
  1260 (* ML (system language) code for evaluation and instrumentalization *)
  1261 
  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 [])
  1265   |> the;
  1266 
  1267 (* generic entry points for SML/OCaml *)
  1268 
  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);
  1273 
  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);
  1278 
  1279 
  1280 (** Haskell serializer **)
  1281 
  1282 fun pr_haskell_bind pr_term =
  1283   let
  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;
  1289 
  1290 fun pr_haskell_stmt syntax_class syntax_tyco syntax_const labelled_name
  1291     init_syms deresolve is_cons contr_classparam_typs deriving_show =
  1292   let
  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
  1303      of [] => []
  1304       | classbinds => Pretty.enum "," "(" ")" (
  1305           map (fn (v, class) =>
  1306             str (class_name class ^ " " ^ CodeName.lookup_var tyvars v)) classbinds)
  1307           @@ str " => ";
  1308     fun pr_typforall tyvars vs = case map fst vs
  1309      of [] => []
  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
  1327             | _ =>
  1328                 brackify fxy [
  1329                   pr_term tyvars thm pat vars NOBR t1,
  1330                   pr_term tyvars thm pat vars BR t2
  1331                 ])
  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 _ `|-> _) =
  1335           let
  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];
  1355         in
  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
  1359         end
  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 ((_, [_]), _)) =
  1363           let
  1364             val (binds, t) = CodeThingol.unfold_let (ICase cases);
  1365             fun pr ((pat, ty), t) vars =
  1366               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;
  1370           in
  1371             Pretty.block_enclose (
  1372               str "let {",
  1373               concat [str "}", str "in", pr_term tyvars thm false vars' NOBR t]
  1374             ) ps
  1375           end
  1376       | pr_case tyvars thm vars fxy (((td, ty), bs as _ :: _), _) =
  1377           let
  1378             fun pr (pat, t) =
  1379               let
  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;
  1382           in
  1383             Pretty.block_enclose (
  1384               concat [str "(case", pr_term tyvars thm false vars NOBR td, str "of", str "{"],
  1385               str "})"
  1386             ) (map pr bs)
  1387           end
  1388       | pr_case tyvars thm vars fxy ((_, []), _) = str "error \"empty case\"";
  1389     fun pr_stmt (name, CodeThingol.Fun ((vs, ty), [])) =
  1390           let
  1391             val tyvars = CodeName.intro_vars (map fst vs) init_syms;
  1392             val n = (length o fst o CodeThingol.unfold_fun) ty;
  1393           in
  1394             Pretty.chunks [
  1395               Pretty.block [
  1396                 (str o suffix " ::" o deresolve_base) name,
  1397                 Pretty.brk 1,
  1398                 pr_typscheme tyvars (vs, ty),
  1399                 str ";"
  1400               ],
  1401               concat (
  1402                 (str o deresolve_base) name
  1403                 :: map str (replicate n "_")
  1404                 @ str "="
  1405                 :: str "error"
  1406                 @@ (str o (fn s => s ^ ";") o ML_Syntax.print_string
  1407                     o NameSpace.base o NameSpace.qualifier) name
  1408               )
  1409             ]
  1410           end
  1411       | pr_stmt (name, CodeThingol.Fun ((vs, ty), eqs)) =
  1412           let
  1413             val tyvars = CodeName.intro_vars (map fst vs) init_syms;
  1414             fun pr_eq ((ts, t), thm) =
  1415               let
  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 []);
  1424               in
  1425                 semicolon (
  1426                   (str o deresolve_base) name
  1427                   :: map (pr_term tyvars thm true vars BR) ts
  1428                   @ str "="
  1429                   @@ pr_term tyvars thm false vars NOBR t
  1430                 )
  1431               end;
  1432           in
  1433             Pretty.chunks (
  1434               Pretty.block [
  1435                 (str o suffix " ::" o deresolve_base) name,
  1436                 Pretty.brk 1,
  1437                 pr_typscheme tyvars (vs, ty),
  1438                 str ";"
  1439               ]
  1440               :: map pr_eq eqs
  1441             )
  1442           end
  1443       | pr_stmt (name, CodeThingol.Datatype (vs, [])) =
  1444           let
  1445             val tyvars = CodeName.intro_vars (map fst vs) init_syms;
  1446           in
  1447             semicolon [
  1448               str "data",
  1449               pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
  1450             ]
  1451           end
  1452       | pr_stmt (name, CodeThingol.Datatype (vs, [(co, [ty])])) =
  1453           let
  1454             val tyvars = CodeName.intro_vars (map fst vs) init_syms;
  1455           in
  1456             semicolon (
  1457               str "newtype"
  1458               :: pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
  1459               :: str "="
  1460               :: (str o deresolve_base) co
  1461               :: pr_typ tyvars BR ty
  1462               :: (if deriving_show name then [str "deriving (Read, Show)"] else [])
  1463             )
  1464           end
  1465       | pr_stmt (name, CodeThingol.Datatype (vs, co :: cos)) =
  1466           let
  1467             val tyvars = CodeName.intro_vars (map fst vs) init_syms;
  1468             fun pr_co (co, tys) =
  1469               concat (
  1470                 (str o deresolve_base) co
  1471                 :: map (pr_typ tyvars BR) tys
  1472               )
  1473           in
  1474             semicolon (
  1475               str "data"
  1476               :: pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
  1477               :: str "="
  1478               :: pr_co co
  1479               :: map ((fn p => Pretty.block [str "| ", p]) o pr_co) cos
  1480               @ (if deriving_show name then [str "deriving (Read, Show)"] else [])
  1481             )
  1482           end
  1483       | pr_stmt (name, CodeThingol.Class (v, (superclasses, classparams))) =
  1484           let
  1485             val tyvars = CodeName.intro_vars [v] init_syms;
  1486             fun pr_classparam (classparam, ty) =
  1487               semicolon [
  1488                 (str o classparam_name name) classparam,
  1489                 str "::",
  1490                 pr_typ tyvars NOBR ty
  1491               ]
  1492           in
  1493             Pretty.block_enclose (
  1494               Pretty.block [
  1495                 str "class ",
  1496                 Pretty.block (pr_typcontext tyvars [(v, map fst superclasses)]),
  1497                 str (deresolve_base name ^ " " ^ CodeName.lookup_var tyvars v),
  1498                 str " where {"
  1499               ],
  1500               str "};"
  1501             ) (map pr_classparam classparams)
  1502           end
  1503       | pr_stmt (_, CodeThingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =
  1504           let
  1505             val tyvars = CodeName.intro_vars (map fst vs) init_syms;
  1506             fun pr_instdef ((classparam, c_inst), thm) =
  1507               semicolon [
  1508                 (str o classparam_name class) classparam,
  1509                 str "=",
  1510                 pr_app tyvars thm false init_syms NOBR (c_inst, [])
  1511               ];
  1512           in
  1513             Pretty.block_enclose (
  1514               Pretty.block [
  1515                 str "instance ",
  1516                 Pretty.block (pr_typcontext tyvars vs),
  1517                 str (class_name class ^ " "),
  1518                 pr_typ tyvars BR (tyco `%% map (ITyVar o fst) vs),
  1519                 str " where {"
  1520               ],
  1521               str "};"
  1522             ) (map pr_instdef classparam_insts)
  1523           end;
  1524   in pr_stmt end;
  1525 
  1526 fun pretty_haskell_monad c_bind =
  1527   let
  1528     fun pretty pr thm pat vars fxy [(t, _)] =
  1529       let
  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;
  1543   in (1, pretty) end;
  1544 
  1545 fun haskell_program_of_program labelled_name module_name module_prefix reserved_names raw_module_alias program =
  1546   let
  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)) =
  1551       let
  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) =
  1556           let
  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) =
  1561           let
  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));
  1579       in
  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)))
  1586       end;
  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;
  1595 
  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 =
  1599   let
  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 =
  1607       let
  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))
  1612                     (maps snd cs)
  1613                  | NONE => true
  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 {"),
  1627         str "",
  1628         content,
  1629         str "",
  1630         str "}"
  1631       ]);
  1632     fun serialize_module1 (module_name', (deps, (stmts, _))) =
  1633       let
  1634         val stmt_names = map fst stmts;
  1635         val deps' = subtract (op =) stmt_names deps
  1636           |> distinct (op =)
  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 =);
  1642         val imports = deps'
  1643           |> map NameSpace.qualifier
  1644           |> distinct (op =);
  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
  1652             @ str ""
  1653             :: separate (str "") (map_filter
  1654               (fn (name, (_, SOME stmt)) => SOME (pr_stmt qualified (name, stmt))
  1655                 | (_, (_, NONE)) => NONE) stmts)
  1656           )
  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))
  1663               else NONE
  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) =
  1668       let
  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);
  1680   in
  1681     output destination (map (uncurry pr_module) includes
  1682       @ map serialize_module (Symtab.dest hs_program))
  1683   end;
  1684 
  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));
  1690 
  1691 
  1692 (** optional pretty serialization **)
  1693 
  1694 local
  1695 
  1696 fun ocaml_char c =
  1697   let
  1698     fun chr i =
  1699       let
  1700         val xs = string_of_int i;
  1701         val ys = replicate_string (3 - length (explode xs)) "0";
  1702       in "\\" ^ ys ^ xs end;
  1703     val i = ord c;
  1704     val s = if i < 32 orelse i = 34 orelse i = 39 orelse i = 92 orelse i > 126
  1705       then chr i else c
  1706   in s end;
  1707 
  1708 fun haskell_char c =
  1709   let
  1710     val s = ML_Syntax.print_char c;
  1711   in if s = "'" then "\\'" else s end;
  1712 
  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
  1719   }) list = [
  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
  1730             if unbounded then
  1731               "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
  1732             else string_of_int k
  1733           else
  1734             if unbounded then
  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, ":")})
  1746 ];
  1747 
  1748 in
  1749 
  1750 fun pr_pretty target = case AList.lookup (op =) pretty target
  1751  of SOME x => x
  1752   | NONE => error ("Unknown code target language: " ^ quote target);
  1753 
  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,
  1757     str target_cons,
  1758     pr (INFX (target_fxy, R)) t2
  1759   ];
  1760 
  1761 fun pretty_list c_nil c_cons target =
  1762   let
  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;
  1769   in (2, pretty) end;
  1770 
  1771 fun pretty_list_string c_nil c_cons c_char c_nibbles target =
  1772   let
  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
  1780            of SOME p => p
  1781             | NONE => mk_list (map (pr vars NOBR) ts))
  1782         | NONE => default_list (#infix_cons pretty_ops) (pr vars) fxy t1 t2;
  1783   in (2, pretty) end;
  1784 
  1785 fun pretty_char c_char c_nibbles target =
  1786   let
  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";
  1792   in (2, pretty) end;
  1793 
  1794 fun pretty_numeral unbounded negative c_pls c_min c_bit0 c_bit1 target =
  1795   let
  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;
  1799   in (1, pretty) end;
  1800 
  1801 fun pretty_message c_char c_nibbles c_nil c_cons target =
  1802   let
  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
  1809            of SOME p => p
  1810             | NONE => nerror thm "Illegal message expression")
  1811         | NONE => nerror thm "Illegal message expression";
  1812   in (1, pretty) end;
  1813 
  1814 fun pretty_imperative_monad_bind bind' return' unit' =
  1815   let
  1816     val dummy_name = "";
  1817     val dummy_type = ITyVar dummy_name;
  1818     val dummy_case_term = IVar dummy_name;
  1819     (*assumption: dummy values are not relevant for serialization*)
  1820     val unitt = IConst (unit', ([], []));
  1821     fun dest_abs ((v, ty) `|-> t, _) = ((v, ty), t)
  1822       | dest_abs (t, ty) =
  1823           let
  1824             val vs = CodeThingol.fold_varnames cons t [];
  1825             val v = Name.variant vs "x";
  1826             val ty' = (hd o fst o CodeThingol.unfold_fun) ty;
  1827           in ((v, ty'), t `$ IVar v) end;
  1828     fun force (t as IConst (c, _) `$ t') = if c = return'
  1829           then t' else t `$ unitt
  1830       | force t = t `$ unitt;
  1831     fun tr_bind' [(t1, _), (t2, ty2)] =
  1832       let
  1833         val ((v, ty), t) = dest_abs (t2, ty2);
  1834       in ICase (((force t1, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end
  1835     and tr_bind'' t = case CodeThingol.unfold_app t
  1836          of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if c = bind'
  1837               then tr_bind' [(x1, ty1), (x2, ty2)]
  1838               else force t
  1839           | _ => force t;
  1840     fun tr_bind ts = (dummy_name, dummy_type)
  1841       `|-> ICase (((IVar dummy_name, dummy_type), [(unitt, tr_bind' ts)]), dummy_case_term);
  1842     fun pretty pr thm pat vars fxy ts = pr vars fxy (tr_bind ts);
  1843   in (2, pretty) end;
  1844 
  1845 end; (*local*)
  1846 
  1847 
  1848 (** serializer use cases **)
  1849 
  1850 (* evaluation *)
  1851 
  1852 fun eval eval'' term_of reff thy ct args =
  1853   let
  1854     val _ = if null (term_frees (term_of ct)) then () else error ("Term "
  1855       ^ quote (Syntax.string_of_term_global thy (term_of ct))
  1856       ^ " to be evaluated contains free variables");
  1857     fun eval' program ((vs, ty), t) deps =
  1858       let
  1859         val _ = if CodeThingol.contains_dictvar t then
  1860           error "Term to be evaluated constains free dictionaries" else ();
  1861         val program' = program
  1862           |> Graph.new_node (CodeName.value_name, CodeThingol.Fun (([], ty), [(([], t), Drule.dummy_thm)]))
  1863           |> fold (curry Graph.add_edge CodeName.value_name) deps;
  1864         val (value_code, [value_name']) = ml_code_of thy program' [CodeName.value_name];
  1865         val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
  1866           ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
  1867       in ML_Context.evaluate Output.ml_output false reff sml_code end;
  1868   in eval'' thy (fn t => (t, eval')) ct end;
  1869 
  1870 fun eval_conv reff = eval CodeThingol.eval_conv Thm.term_of reff;
  1871 fun eval_term reff = eval CodeThingol.eval_term I reff;
  1872 
  1873 
  1874 (* instrumentalization by antiquotation *)
  1875 
  1876 local
  1877 
  1878 structure CodeAntiqData = ProofDataFun
  1879 (
  1880   type T = string list * (bool * (string * (string * (string * string) list) Susp.T));
  1881   fun init _ = ([], (true, ("", Susp.value ("", []))));
  1882 );
  1883 
  1884 val is_first_occ = fst o snd o CodeAntiqData.get;
  1885 
  1886 fun delayed_code thy consts () =
  1887   let
  1888     val (consts', program) = CodeThingol.consts_program thy consts;
  1889     val (ml_code, consts'') = ml_code_of thy program consts';
  1890     val _ = if length consts <> length consts'' then
  1891       error ("One of the constants " ^ commas (map (quote o CodeUnit.string_of_const thy) consts)
  1892         ^ "\nhas a user-defined serialization") else ();
  1893   in (ml_code, consts ~~ consts'') end;
  1894 
  1895 fun register_const const ctxt =
  1896   let
  1897     val (consts, (_, (struct_name, _))) = CodeAntiqData.get ctxt;
  1898     val consts' = insert (op =) const consts;
  1899     val (struct_name', ctxt') = if struct_name = ""
  1900       then ML_Antiquote.variant "Code" ctxt
  1901       else (struct_name, ctxt);
  1902     val acc_code = Susp.delay (delayed_code (ProofContext.theory_of ctxt) consts');
  1903   in CodeAntiqData.put (consts', (false, (struct_name', acc_code))) ctxt' end;
  1904 
  1905 fun print_code struct_name is_first const ctxt =
  1906   let
  1907     val (consts, (_, (struct_code_name, acc_code))) = CodeAntiqData.get ctxt;
  1908     val (raw_ml_code, consts_map) = Susp.force acc_code;
  1909     val const'' = NameSpace.append (NameSpace.append struct_name struct_code_name)
  1910       ((the o AList.lookup (op =) consts_map) const);
  1911     val ml_code = if is_first then "\nstructure " ^ struct_code_name
  1912         ^ " =\nstruct\n\n" ^ raw_ml_code ^ "\nend;\n\n"
  1913       else "";
  1914   in (ml_code, const'') end;
  1915 
  1916 in
  1917 
  1918 fun ml_code_antiq raw_const {struct_name, background} =
  1919   let
  1920     val const = CodeUnit.check_const (ProofContext.theory_of background) raw_const;
  1921     val is_first = is_first_occ background;
  1922     val background' = register_const const background;
  1923   in (print_code struct_name is_first const, background') end;
  1924 
  1925 end; (*local*)
  1926 
  1927 
  1928 (* code presentation *)
  1929 
  1930 fun code_of thy target module_name cs stmt_names =
  1931   let
  1932     val (cs', program) = CodeThingol.consts_program thy cs;
  1933   in
  1934     string stmt_names (serialize thy target (SOME module_name) [] program cs')
  1935   end;
  1936 
  1937 
  1938 (* code generation *)
  1939 
  1940 fun read_const_exprs thy cs =
  1941   let
  1942     val (cs1, cs2) = CodeName.read_const_exprs thy cs;
  1943     val (cs3, program) = CodeThingol.consts_program thy cs2;
  1944     val cs4 = CodeThingol.transitivly_non_empty_funs program (abort_allowed thy);
  1945     val cs5 = map_filter
  1946       (fn (c, c') => if member (op =) cs4 c' then SOME c else NONE) (cs2 ~~ cs3);
  1947   in fold (insert (op =)) cs5 cs1 end;
  1948 
  1949 fun cached_program thy = 
  1950   let
  1951     val program = CodeThingol.cached_program thy;
  1952   in (CodeThingol.transitivly_non_empty_funs program (abort_allowed thy), program) end
  1953 
  1954 fun export_code thy cs seris =
  1955   let
  1956     val (cs', program) = if null cs then cached_program thy
  1957       else CodeThingol.consts_program thy cs;
  1958     fun mk_seri_dest dest = case dest
  1959      of NONE => compile
  1960       | SOME "-" => export
  1961       | SOME f => file (Path.explode f)
  1962     val _ = map (fn (((target, module), dest), args) =>
  1963       (mk_seri_dest dest (serialize thy target module args program cs'))) seris;
  1964   in () end;
  1965 
  1966 fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs) seris;
  1967 
  1968 
  1969 (** serializer data **)
  1970 
  1971 (* infix syntax *)
  1972 
  1973 datatype 'a mixfix =
  1974     Arg of fixity
  1975   | Pretty of Pretty.T;
  1976 
  1977 fun mk_mixfix prep_arg (fixity_this, mfx) =
  1978   let
  1979     fun is_arg (Arg _) = true
  1980       | is_arg _ = false;
  1981     val i = (length o filter is_arg) mfx;
  1982     fun fillin _ [] [] =
  1983           []
  1984       | fillin pr (Arg fxy :: mfx) (a :: args) =
  1985           (pr fxy o prep_arg) a :: fillin pr mfx args
  1986       | fillin pr (Pretty p :: mfx) args =
  1987           p :: fillin pr mfx args;
  1988   in
  1989     (i, fn pr => fn fixity_ctxt => fn args =>
  1990       gen_brackify (fixity fixity_this fixity_ctxt) (fillin pr mfx args))
  1991   end;
  1992 
  1993 fun parse_infix prep_arg (x, i) s =
  1994   let
  1995     val l = case x of L => INFX (i, L) | _ => INFX (i, X);
  1996     val r = case x of R => INFX (i, R) | _ => INFX (i, X);
  1997   in
  1998     mk_mixfix prep_arg (INFX (i, x),
  1999       [Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r])
  2000   end;
  2001 
  2002 
  2003 (* data access *)
  2004 
  2005 local
  2006 
  2007 fun cert_class thy class =
  2008   let
  2009     val _ = AxClass.get_info thy class;
  2010   in class end;
  2011 
  2012 fun read_class thy = cert_class thy o Sign.intern_class thy;
  2013 
  2014 fun cert_tyco thy tyco =
  2015   let
  2016     val _ = if Sign.declared_tyname thy tyco then ()
  2017       else error ("No such type constructor: " ^ quote tyco);
  2018   in tyco end;
  2019 
  2020 fun read_tyco thy = cert_tyco thy o Sign.intern_type thy;
  2021 
  2022 fun gen_add_syntax_class prep_class prep_const target raw_class raw_syn thy =
  2023   let
  2024     val class = prep_class thy raw_class;
  2025     val class' = CodeName.class thy class;
  2026     fun mk_classparam c = case AxClass.class_of_param thy c
  2027      of SOME class'' => if class = class'' then CodeName.const thy c
  2028           else error ("Not a class operation for class " ^ quote class ^ ": " ^ quote c)
  2029       | NONE => error ("Not a class operation: " ^ quote c);
  2030     fun mk_syntax_params raw_params = AList.lookup (op =)
  2031       ((map o apfst) (mk_classparam o prep_const thy) raw_params);
  2032   in case raw_syn
  2033    of SOME (syntax, raw_params) =>
  2034       thy
  2035       |> (map_name_syntax target o apfst o apfst)
  2036            (Symtab.update (class', (syntax, mk_syntax_params raw_params)))
  2037     | NONE =>
  2038       thy
  2039       |> (map_name_syntax target o apfst o apfst)
  2040            (Symtab.delete_safe class')
  2041   end;
  2042 
  2043 fun gen_add_syntax_inst prep_class prep_tyco target (raw_tyco, raw_class) add_del thy =
  2044   let
  2045     val inst = CodeName.instance thy (prep_class thy raw_class, prep_tyco thy raw_tyco);
  2046   in if add_del then
  2047     thy
  2048     |> (map_name_syntax target o apfst o apsnd)
  2049         (Symtab.update (inst, ()))
  2050   else
  2051     thy
  2052     |> (map_name_syntax target o apfst o apsnd)
  2053         (Symtab.delete_safe inst)
  2054   end;
  2055 
  2056 fun gen_add_syntax_tyco prep_tyco target raw_tyco raw_syn thy =
  2057   let
  2058     val tyco = prep_tyco thy raw_tyco;
  2059     val tyco' = if tyco = "fun" then "fun" else CodeName.tyco thy tyco;
  2060     fun check_args (syntax as (n, _)) = if n <> Sign.arity_number thy tyco
  2061       then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
  2062       else syntax
  2063   in case raw_syn
  2064    of SOME syntax =>
  2065       thy
  2066       |> (map_name_syntax target o apsnd o apfst)
  2067            (Symtab.update (tyco', check_args syntax))
  2068    | NONE =>
  2069       thy
  2070       |> (map_name_syntax target o apsnd o apfst)
  2071            (Symtab.delete_safe tyco')
  2072   end;
  2073 
  2074 fun simple_const_syntax x = (Option.map o apsnd)
  2075   (fn pretty => fn pr => fn thm => fn pat => fn vars => pretty (pr vars)) x;
  2076 
  2077 fun gen_add_syntax_const prep_const target raw_c raw_syn thy =
  2078   let
  2079     val c = prep_const thy raw_c;
  2080     val c' = CodeName.const thy c;
  2081     fun check_args (syntax as (n, _)) = if n > CodeUnit.no_args thy c
  2082       then error ("Too many arguments in syntax for constant " ^ quote c)
  2083       else syntax;
  2084   in case raw_syn
  2085    of SOME syntax =>
  2086       thy
  2087       |> (map_name_syntax target o apsnd o apsnd)
  2088            (Symtab.update (c', check_args syntax))
  2089    | NONE =>
  2090       thy
  2091       |> (map_name_syntax target o apsnd o apsnd)
  2092            (Symtab.delete_safe c')
  2093   end;
  2094 
  2095 fun add_reserved target =
  2096   let
  2097     fun add sym syms = if member (op =) syms sym
  2098       then error ("Reserved symbol " ^ quote sym ^ " already declared")
  2099       else insert (op =) sym syms
  2100   in map_reserved target o add end;
  2101 
  2102 fun add_include target =
  2103   let
  2104     fun add (name, SOME content) incls =
  2105           let
  2106             val _ = if Symtab.defined incls name
  2107               then warning ("Overwriting existing include " ^ name)
  2108               else ();
  2109           in Symtab.update (name, str content) incls end
  2110       | add (name, NONE) incls =
  2111           Symtab.delete name incls;
  2112   in map_includes target o add end;
  2113 
  2114 fun add_module_alias target =
  2115   map_module_alias target o Symtab.update o apsnd CodeName.check_modulename;
  2116 
  2117 fun add_monad target raw_c_run raw_c_bind raw_c_return_unit thy =
  2118   let
  2119     val c_run = CodeUnit.read_const thy raw_c_run;
  2120     val c_bind = CodeUnit.read_const thy raw_c_bind;
  2121     val c_bind' = CodeName.const thy c_bind;
  2122     val c_return_unit' = (Option.map o pairself)
  2123       (CodeName.const thy o CodeUnit.read_const thy) raw_c_return_unit;
  2124     val is_haskell = target = target_Haskell;
  2125     val _ = if is_haskell andalso is_some c_return_unit'
  2126       then error ("No unit entry may be given for Haskell monad")
  2127       else ();
  2128     val _ = if not is_haskell andalso is_none c_return_unit'
  2129       then error ("Unit entry must be given for SML/OCaml monad")
  2130       else ();
  2131   in if target = target_Haskell then
  2132     thy
  2133     |> gen_add_syntax_const (K I) target_Haskell c_run
  2134           (SOME (pretty_haskell_monad c_bind'))
  2135     |> gen_add_syntax_const (K I) target_Haskell c_bind
  2136           (simple_const_syntax (SOME (parse_infix fst (L, 1) ">>=")))
  2137   else
  2138     thy
  2139     |> gen_add_syntax_const (K I) target c_bind
  2140           (SOME (pretty_imperative_monad_bind c_bind'
  2141             ((fst o the) c_return_unit') ((snd o the) c_return_unit')))
  2142   end;
  2143 
  2144 fun gen_allow_abort prep_cs raw_c thy =
  2145   let
  2146     val c = prep_cs thy raw_c;
  2147     val c' = CodeName.const thy c;
  2148   in thy |> (CodeTargetData.map o apsnd) (insert (op =) c') end;
  2149 
  2150 fun zip_list (x::xs) f g =
  2151   f
  2152   #-> (fn y =>
  2153     fold_map (fn x => g |-- f >> pair x) xs
  2154     #-> (fn xys => pair ((x, y) :: xys)));
  2155 
  2156 
  2157 (* concrete syntax *)
  2158 
  2159 structure P = OuterParse
  2160 and K = OuterKeyword
  2161 
  2162 fun parse_multi_syntax parse_thing parse_syntax =
  2163   P.and_list1 parse_thing
  2164   #-> (fn things => Scan.repeat1 (P.$$$ "(" |-- P.name --
  2165         (zip_list things parse_syntax (P.$$$ "and")) --| P.$$$ ")"));
  2166 
  2167 val (infixK, infixlK, infixrK) = ("infix", "infixl", "infixr");
  2168 
  2169 fun parse_mixfix prep_arg s =
  2170   let
  2171     val sym_any = Scan.one Symbol.is_regular;
  2172     val parse = Scan.optional ($$ "!" >> K true) false -- Scan.repeat (
  2173          ($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR))
  2174       || ($$ "_" >> K (Arg BR))
  2175       || ($$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length))
  2176       || (Scan.repeat1
  2177            (   $$ "'" |-- sym_any
  2178             || Scan.unless ($$ "_" || $$ "/" || $$ "(" |-- $$ "_" |-- $$ ")")
  2179                  sym_any) >> (Pretty o str o implode)));
  2180   in case Scan.finite Symbol.stopper parse (Symbol.explode s)
  2181    of ((_, p as [_]), []) => mk_mixfix prep_arg (NOBR, p)
  2182     | ((b, p as _ :: _ :: _), []) => mk_mixfix prep_arg (if b then NOBR else BR, p)
  2183     | _ => Scan.!!
  2184         (the_default ("malformed mixfix annotation: " ^ quote s) o snd) Scan.fail ()
  2185   end;
  2186 
  2187 fun parse_syntax prep_arg xs =
  2188   Scan.option ((
  2189       ((P.$$$ infixK  >> K X)
  2190         || (P.$$$ infixlK >> K L)
  2191         || (P.$$$ infixrK >> K R))
  2192         -- P.nat >> parse_infix prep_arg
  2193       || Scan.succeed (parse_mixfix prep_arg))
  2194       -- P.string
  2195       >> (fn (parse, s) => parse s)) xs;
  2196 
  2197 in
  2198 
  2199 val parse_syntax = parse_syntax;
  2200 
  2201 val add_syntax_class = gen_add_syntax_class cert_class (K I);
  2202 val add_syntax_inst = gen_add_syntax_inst cert_class cert_tyco;
  2203 val add_syntax_tyco = gen_add_syntax_tyco cert_tyco;
  2204 val add_syntax_const = gen_add_syntax_const (K I);
  2205 val allow_abort = gen_allow_abort (K I);
  2206 
  2207 val add_syntax_class_cmd = gen_add_syntax_class read_class CodeUnit.read_const;
  2208 val add_syntax_inst_cmd = gen_add_syntax_inst read_class read_tyco;
  2209 val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco;
  2210 val add_syntax_const_cmd = gen_add_syntax_const CodeUnit.read_const;
  2211 val allow_abort_cmd = gen_allow_abort CodeUnit.read_const;
  2212 
  2213 fun add_syntax_tycoP target tyco = parse_syntax I >> add_syntax_tyco_cmd target tyco;
  2214 fun add_syntax_constP target c = parse_syntax fst >> (add_syntax_const_cmd target c o simple_const_syntax);
  2215 
  2216 fun add_undefined target undef target_undefined thy =
  2217   let
  2218     fun pr _ _ _ _ _ _ = str target_undefined;
  2219   in
  2220     thy
  2221     |> add_syntax_const target undef (SOME (~1, pr))
  2222   end;
  2223 
  2224 fun add_pretty_list target nill cons thy =
  2225   let
  2226     val nil' = CodeName.const thy nill;
  2227     val cons' = CodeName.const thy cons;
  2228     val pr = pretty_list nil' cons' target;
  2229   in
  2230     thy
  2231     |> add_syntax_const target cons (SOME pr)
  2232   end;
  2233 
  2234 fun add_pretty_list_string target nill cons charr nibbles thy =
  2235   let
  2236     val nil' = CodeName.const thy nill;
  2237     val cons' = CodeName.const thy cons;
  2238     val charr' = CodeName.const thy charr;
  2239     val nibbles' = map (CodeName.const thy) nibbles;
  2240     val pr = pretty_list_string nil' cons' charr' nibbles' target;
  2241   in
  2242     thy
  2243     |> add_syntax_const target cons (SOME pr)
  2244   end;
  2245 
  2246 fun add_pretty_char target charr nibbles thy =
  2247   let
  2248     val charr' = CodeName.const thy charr;
  2249     val nibbles' = map (CodeName.const thy) nibbles;
  2250     val pr = pretty_char charr' nibbles' target;
  2251   in
  2252     thy
  2253     |> add_syntax_const target charr (SOME pr)
  2254   end;
  2255 
  2256 fun add_pretty_numeral target unbounded negative number_of pls min bit0 bit1 thy =
  2257   let
  2258     val pls' = CodeName.const thy pls;
  2259     val min' = CodeName.const thy min;
  2260     val bit0' = CodeName.const thy bit0;
  2261     val bit1' = CodeName.const thy bit1;
  2262     val pr = pretty_numeral unbounded negative pls' min' bit0' bit1' target;
  2263   in
  2264     thy
  2265     |> add_syntax_const target number_of (SOME pr)
  2266   end;
  2267 
  2268 fun add_pretty_message target charr nibbles nill cons str thy =
  2269   let
  2270     val charr' = CodeName.const thy charr;
  2271     val nibbles' = map (CodeName.const thy) nibbles;
  2272     val nil' = CodeName.const thy nill;
  2273     val cons' = CodeName.const thy cons;
  2274     val pr = pretty_message charr' nibbles' nil' cons' target;
  2275   in
  2276     thy
  2277     |> add_syntax_const target str (SOME pr)
  2278   end;
  2279 
  2280 
  2281 
  2282 (** Isar setup **)
  2283 
  2284 val (inK, module_nameK, fileK) = ("in", "module_name", "file");
  2285 
  2286 fun code_exprP cmd =
  2287   (Scan.repeat P.term
  2288   -- Scan.repeat (P.$$$ inK |-- P.name
  2289      -- Scan.option (P.$$$ module_nameK |-- P.name)
  2290      -- Scan.option (P.$$$ fileK |-- P.name)
  2291      -- Scan.optional (P.$$$ "(" |-- P.arguments --| P.$$$ ")") []
  2292   ) >> (fn (raw_cs, seris) => cmd raw_cs seris));
  2293 
  2294 val _ = List.app OuterKeyword.keyword [infixK, infixlK, infixrK, inK, module_nameK, fileK];
  2295 
  2296 val _ =
  2297   OuterSyntax.command "code_class" "define code syntax for class" K.thy_decl (
  2298     parse_multi_syntax P.xname
  2299       (Scan.option (P.string -- Scan.optional (P.$$$ "where" |-- Scan.repeat1
  2300         (P.term --| (P.$$$ "\<equiv>" || P.$$$ "==") -- P.string)) []))
  2301     >> (Toplevel.theory oo fold) (fn (target, syns) =>
  2302           fold (fn (raw_class, syn) => add_syntax_class_cmd target raw_class syn) syns)
  2303   );
  2304 
  2305 val _ =
  2306   OuterSyntax.command "code_instance" "define code syntax for instance" K.thy_decl (
  2307     parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname)
  2308       ((P.minus >> K true) || Scan.succeed false)
  2309     >> (Toplevel.theory oo fold) (fn (target, syns) =>
  2310           fold (fn (raw_inst, add_del) => add_syntax_inst_cmd target raw_inst add_del) syns)
  2311   );
  2312 
  2313 val _ =
  2314   OuterSyntax.command "code_type" "define code syntax for type constructor" K.thy_decl (
  2315     parse_multi_syntax P.xname (parse_syntax I)
  2316     >> (Toplevel.theory oo fold) (fn (target, syns) =>
  2317           fold (fn (raw_tyco, syn) => add_syntax_tyco_cmd target raw_tyco syn) syns)
  2318   );
  2319 
  2320 val _ =
  2321   OuterSyntax.command "code_const" "define code syntax for constant" K.thy_decl (
  2322     parse_multi_syntax P.term (parse_syntax fst)
  2323     >> (Toplevel.theory oo fold) (fn (target, syns) =>
  2324           fold (fn (raw_const, syn) => add_syntax_const_cmd target raw_const (simple_const_syntax syn)) syns)
  2325   );
  2326 
  2327 val _ =
  2328   OuterSyntax.command "code_monad" "define code syntax for monads" K.thy_decl (
  2329     P.term -- P.term -- ((P.term -- P.term >> SOME) -- Scan.repeat1 P.name
  2330       || Scan.succeed NONE -- Scan.repeat1 P.name)
  2331     >> (fn ((raw_run, raw_bind), (raw_unit_return, targets)) => Toplevel.theory 
  2332           (fold (fn target => add_monad target raw_run raw_bind raw_unit_return) targets))
  2333   );
  2334 
  2335 val _ =
  2336   OuterSyntax.command "code_reserved" "declare words as reserved for target language" K.thy_decl (
  2337     P.name -- Scan.repeat1 P.name
  2338     >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds)
  2339   );
  2340 
  2341 val _ =
  2342   OuterSyntax.command "code_include" "declare piece of code to be included in generated code" K.thy_decl (
  2343     P.name -- P.name -- (P.text >> (fn "-" => NONE | s => SOME s))
  2344     >> (fn ((target, name), content) => (Toplevel.theory o add_include target)
  2345       (name, content))
  2346   );
  2347 
  2348 val _ =
  2349   OuterSyntax.command "code_modulename" "alias module to other name" K.thy_decl (
  2350     P.name -- Scan.repeat1 (P.name -- P.name)
  2351     >> (fn (target, modlnames) => (Toplevel.theory o fold (add_module_alias target)) modlnames)
  2352   );
  2353 
  2354 val _ =
  2355   OuterSyntax.command "code_abort" "permit constant to be implemented as program abort" K.thy_decl (
  2356     Scan.repeat1 P.term >> (Toplevel.theory o fold allow_abort_cmd)
  2357   );
  2358 
  2359 val _ =
  2360   OuterSyntax.command "export_code" "generate executable code for constants"
  2361     K.diag (P.!!! (code_exprP export_code_cmd) >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
  2362 
  2363 fun shell_command thyname cmd = Toplevel.program (fn _ =>
  2364   (use_thy thyname; case Scan.read OuterLex.stopper (P.!!! (code_exprP export_code_cmd)) ((filter OuterLex.is_proper o OuterSyntax.scan) cmd)
  2365    of SOME f => (writeln "Now generating code..."; f (theory thyname))
  2366     | NONE => error ("Bad directive " ^ quote cmd)))
  2367   handle TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
  2368 
  2369 val _ = ML_Context.add_antiq "code" (Args.term >> ml_code_antiq);
  2370 
  2371 
  2372 (* serializer setup, including serializer defaults *)
  2373 
  2374 val setup =
  2375   add_target (target_SML, isar_seri_sml)
  2376   #> add_target (target_OCaml, isar_seri_ocaml)
  2377   #> add_target (target_Haskell, isar_seri_haskell)
  2378   #> add_syntax_tyco "SML" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
  2379       brackify_infix (1, R) fxy [
  2380         pr_typ (INFX (1, X)) ty1,
  2381         str "->",
  2382         pr_typ (INFX (1, R)) ty2
  2383       ]))
  2384   #> add_syntax_tyco "OCaml" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
  2385       brackify_infix (1, R) fxy [
  2386         pr_typ (INFX (1, X)) ty1,
  2387         str "->",
  2388         pr_typ (INFX (1, R)) ty2
  2389       ]))
  2390   #> add_syntax_tyco "Haskell" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
  2391       brackify_infix (1, R) fxy [
  2392         pr_typ (INFX (1, X)) ty1,
  2393         str "->",
  2394         pr_typ (INFX (1, R)) ty2
  2395       ]))
  2396   #> fold (add_reserved "SML") ML_Syntax.reserved_names
  2397   #> fold (add_reserved "SML")
  2398       ["o" (*dictionary projections use it already*), "Fail", "div", "mod" (*standard infixes*)]
  2399   #> fold (add_reserved "OCaml") [
  2400       "and", "as", "assert", "begin", "class",
  2401       "constraint", "do", "done", "downto", "else", "end", "exception",
  2402       "external", "false", "for", "fun", "function", "functor", "if",
  2403       "in", "include", "inherit", "initializer", "lazy", "let", "match", "method",
  2404       "module", "mutable", "new", "object", "of", "open", "or", "private", "rec",
  2405       "sig", "struct", "then", "to", "true", "try", "type", "val",
  2406       "virtual", "when", "while", "with"
  2407     ]
  2408   #> fold (add_reserved "OCaml") ["failwith", "mod"]
  2409   #> fold (add_reserved "Haskell") [
  2410       "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
  2411       "import", "default", "forall", "let", "in", "class", "qualified", "data",
  2412       "newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
  2413     ]
  2414   #> fold (add_reserved "Haskell") [
  2415       "Prelude", "Main", "Bool", "Maybe", "Either", "Ordering", "Char", "String", "Int",
  2416       "Integer", "Float", "Double", "Rational", "IO", "Eq", "Ord", "Enum", "Bounded",
  2417       "Num", "Real", "Integral", "Fractional", "Floating", "RealFloat", "Monad", "Functor",
  2418       "AlreadyExists", "ArithException", "ArrayException", "AssertionFailed", "AsyncException",
  2419       "BlockedOnDeadMVar", "Deadlock", "Denormal", "DivideByZero", "DotNetException", "DynException",
  2420       "Dynamic", "EOF", "EQ", "EmptyRec", "ErrorCall", "ExitException", "ExitFailure",
  2421       "ExitSuccess", "False", "GT", "HeapOverflow",
  2422       "IOError", "IOException", "IllegalOperation",
  2423       "IndexOutOfBounds", "Just", "Key", "LT", "Left", "LossOfPrecision", "NoMethodError",
  2424       "NoSuchThing", "NonTermination", "Nothing", "Obj", "OtherError", "Overflow",
  2425       "PatternMatchFail", "PermissionDenied", "ProtocolError", "RecConError", "RecSelError",
  2426       "RecUpdError", "ResourceBusy", "ResourceExhausted", "Right", "StackOverflow",
  2427       "ThreadKilled", "True", "TyCon", "TypeRep", "UndefinedElement", "Underflow",
  2428       "UnsupportedOperation", "UserError", "abs", "absReal", "acos", "acosh", "all",
  2429       "and", "any", "appendFile", "asTypeOf", "asciiTab", "asin", "asinh", "atan",
  2430       "atan2", "atanh", "basicIORun", "blockIO", "boundedEnumFrom", "boundedEnumFromThen",
  2431       "boundedEnumFromThenTo", "boundedEnumFromTo", "boundedPred", "boundedSucc", "break",
  2432       "catch", "catchException", "ceiling", "compare", "concat", "concatMap", "const",
  2433       "cos", "cosh", "curry", "cycle", "decodeFloat", "denominator", "div", "divMod",
  2434       "doubleToRatio", "doubleToRational", "drop", "dropWhile", "either", "elem",
  2435       "emptyRec", "encodeFloat", "enumFrom", "enumFromThen", "enumFromThenTo",
  2436       "enumFromTo", "error", "even", "exp", "exponent", "fail", "filter", "flip",
  2437       "floatDigits", "floatProperFraction", "floatRadix", "floatRange", "floatToRational",
  2438       "floor", "fmap", "foldl", "foldl'", "foldl1", "foldr", "foldr1", "fromDouble",
  2439       "fromEnum", "fromEnum_0", "fromInt", "fromInteger", "fromIntegral", "fromObj",
  2440       "fromRational", "fst", "gcd", "getChar", "getContents", "getLine", "head",
  2441       "id", "inRange", "index", "init", "intToRatio", "interact", "ioError", "isAlpha",
  2442       "isAlphaNum", "isDenormalized", "isDigit", "isHexDigit", "isIEEE", "isInfinite",
  2443       "isLower", "isNaN", "isNegativeZero", "isOctDigit", "isSpace", "isUpper", "iterate", "iterate'",
  2444       "last", "lcm", "length", "lex", "lexDigits", "lexLitChar", "lexmatch", "lines", "log",
  2445       "logBase", "lookup", "loop", "map", "mapM", "mapM_", "max", "maxBound", "maximum",
  2446       "maybe", "min", "minBound", "minimum", "mod", "negate", "nonnull", "not", "notElem",
  2447       "null", "numerator", "numericEnumFrom", "numericEnumFromThen", "numericEnumFromThenTo",
  2448       "numericEnumFromTo", "odd", "or", "otherwise", "pi", "pred", 
  2449       "print", "product", "properFraction", "protectEsc", "putChar", "putStr", "putStrLn",
  2450       "quot", "quotRem", "range", "rangeSize", "rationalToDouble", "rationalToFloat",
  2451       "rationalToRealFloat", "read", "readDec", "readField", "readFieldName", "readFile",
  2452       "readFloat", "readHex", "readIO", "readInt", "readList", "readLitChar", "readLn",
  2453       "readOct", "readParen", "readSigned", "reads", "readsPrec", "realFloatToRational",
  2454       "realToFrac", "recip", "reduce", "rem", "repeat", "replicate", "return", "reverse",
  2455       "round", "scaleFloat", "scanl", "scanl1", "scanr", "scanr1", "seq", "sequence",
  2456       "sequence_", "show", "showChar", "showException", "showField", "showList",
  2457       "showLitChar", "showParen", "showString", "shows", "showsPrec", "significand",
  2458       "signum", "signumReal", "sin", "sinh", "snd", "span", "splitAt", "sqrt", "subtract",
  2459       "succ", "sum", "tail", "take", "takeWhile", "takeWhile1", "tan", "tanh", "threadToIOResult",
  2460       "throw", "toEnum", "toInt", "toInteger", "toObj", "toRational", "truncate", "uncurry",
  2461       "undefined", "unlines", "unsafeCoerce", "unsafeIndex", "unsafeRangeSize", "until", "unwords",
  2462       "unzip", "unzip3", "userError", "words", "writeFile", "zip", "zip3", "zipWith", "zipWith3"
  2463     ] (*due to weird handling of ':', we can't do anything else than to import *all* prelude symbols*);
  2464 
  2465 end; (*local*)
  2466 
  2467 end; (*struct*)