src/Tools/code/code_target.ML
author wenzelm
Wed Jun 25 17:38:32 2008 +0200 (2008-06-25)
changeset 27353 71c4dd53d4cb
parent 27346 b664e5bc95fd
child 27372 29a09358953f
permissions -rw-r--r--
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
     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 assert_target: theory -> string -> string;
    37   val serialize: theory -> string -> string option -> Args.T list
    38     -> CodeThingol.program -> string list -> serialization;
    39   val compile: serialization -> unit;
    40   val export: serialization -> unit;
    41   val file: Path.T -> serialization -> unit;
    42   val string: string list -> serialization -> string;
    43 
    44   val code_of: theory -> string -> string -> string list -> string list -> string;
    45   val eval_conv: string * (unit -> thm) option ref
    46     -> theory -> cterm -> string list -> thm;
    47   val eval_term: string * (unit -> 'a) option ref
    48     -> theory -> term -> string list -> 'a;
    49   val shell_command: string (*theory name*) -> string (*cg expr*) -> unit;
    50 
    51   val setup: theory -> theory;
    52   val code_width: int ref;
    53 end;
    54 
    55 structure CodeTarget : CODE_TARGET =
    56 struct
    57 
    58 open BasicCodeThingol;
    59 
    60 (** basics **)
    61 
    62 infixr 5 @@;
    63 infixr 5 @|;
    64 fun x @@ y = [x, y];
    65 fun xs @| y = xs @ [y];
    66 val str = PrintMode.setmp [] Pretty.str;
    67 val concat = Pretty.block o Pretty.breaks;
    68 val brackets = Pretty.enclose "(" ")" o Pretty.breaks;
    69 fun semicolon ps = Pretty.block [concat ps, str ";"];
    70 fun enum_default default sep opn cls [] = str default
    71   | enum_default default sep opn cls xs = Pretty.enum sep opn cls xs;
    72 
    73 datatype destination = Compile | Export | File of Path.T | String of string list;
    74 type serialization = destination -> string option;
    75 
    76 val code_width = ref 80; (*FIXME after Pretty module no longer depends on print mode*)
    77 fun code_setmp f = PrintMode.setmp [] (Pretty.setmp_margin (!code_width) f);
    78 fun code_of_pretty p = code_setmp Pretty.string_of p ^ "\n";
    79 fun code_writeln p = Pretty.setmp_margin (!code_width) Pretty.writeln p;
    80 
    81 (*FIXME why another code_setmp?*)
    82 fun compile f = (code_setmp f Compile; ());
    83 fun export f = (code_setmp f Export; ());
    84 fun file p f = (code_setmp f (File p); ());
    85 fun string cs f = the (code_setmp f (String cs));
    86 
    87 fun stmt_names_of_destination (String stmts) = stmts
    88   | stmt_names_of_destination _ = [];
    89 
    90 
    91 (** generic syntax **)
    92 
    93 datatype lrx = L | R | X;
    94 
    95 datatype fixity =
    96     BR
    97   | NOBR
    98   | INFX of (int * lrx);
    99 
   100 val APP = INFX (~1, L);
   101 
   102 fun fixity_lrx L L = false
   103   | fixity_lrx R R = false
   104   | fixity_lrx _ _ = true;
   105 
   106 fun fixity NOBR _ = false
   107   | fixity _ NOBR = false
   108   | fixity (INFX (pr, lr)) (INFX (pr_ctxt, lr_ctxt)) =
   109       pr < pr_ctxt
   110       orelse pr = pr_ctxt
   111         andalso fixity_lrx lr lr_ctxt
   112       orelse pr_ctxt = ~1
   113   | fixity BR (INFX _) = false
   114   | fixity _ _ = true;
   115 
   116 fun gen_brackify _ [p] = p
   117   | gen_brackify true (ps as _::_) = Pretty.enclose "(" ")" ps
   118   | gen_brackify false (ps as _::_) = Pretty.block ps;
   119 
   120 fun brackify fxy_ctxt =
   121   gen_brackify (fixity BR fxy_ctxt) o Pretty.breaks;
   122 
   123 fun brackify_infix infx fxy_ctxt =
   124   gen_brackify (fixity (INFX infx) fxy_ctxt) o Pretty.breaks;
   125 
   126 type class_syntax = string * (string -> string option);
   127 type typ_syntax = int * ((fixity -> itype -> Pretty.T)
   128   -> fixity -> itype list -> Pretty.T);
   129 type term_syntax = int * ((CodeName.var_ctxt -> fixity -> iterm -> Pretty.T)
   130   -> thm -> bool -> CodeName.var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
   131 
   132 
   133 (** theory data **)
   134 
   135 val target_SML = "SML";
   136 val target_OCaml = "OCaml";
   137 val target_Haskell = "Haskell";
   138 
   139 datatype name_syntax_table = NameSyntaxTable of {
   140   class: class_syntax Symtab.table,
   141   inst: unit Symtab.table,
   142   tyco: typ_syntax Symtab.table,
   143   const: term_syntax Symtab.table
   144 };
   145 
   146 fun mk_name_syntax_table ((class, inst), (tyco, const)) =
   147   NameSyntaxTable { class = class, inst = inst, tyco = tyco, const = const };
   148 fun map_name_syntax_table f (NameSyntaxTable { class, inst, tyco, const }) =
   149   mk_name_syntax_table (f ((class, inst), (tyco, const)));
   150 fun merge_name_syntax_table (NameSyntaxTable { class = class1, inst = inst1, tyco = tyco1, const = const1 },
   151     NameSyntaxTable { class = class2, inst = inst2, tyco = tyco2, const = const2 }) =
   152   mk_name_syntax_table (
   153     (Symtab.join (K snd) (class1, class2),
   154        Symtab.join (K snd) (inst1, inst2)),
   155     (Symtab.join (K snd) (tyco1, tyco2),
   156        Symtab.join (K snd) (const1, const2))
   157   );
   158 
   159 type serializer =
   160   string option                         (*module name*)
   161   -> Args.T list                        (*arguments*)
   162   -> (string -> string)                 (*labelled_name*)
   163   -> string list                        (*reserved symbols*)
   164   -> (string * Pretty.T) list           (*includes*)
   165   -> (string -> string option)          (*module aliasses*)
   166   -> (string -> class_syntax option)
   167   -> (string -> typ_syntax option)
   168   -> (string -> term_syntax option)
   169   -> CodeThingol.program
   170   -> string list                        (*selected statements*)
   171   -> serialization;
   172 
   173 datatype target = Target of {
   174   serial: serial,
   175   serializer: serializer,
   176   reserved: string list,
   177   includes: Pretty.T Symtab.table,
   178   name_syntax_table: name_syntax_table,
   179   module_alias: string Symtab.table
   180 };
   181 
   182 fun mk_target ((serial, serializer), ((reserved, includes), (name_syntax_table, module_alias))) =
   183   Target { serial = serial, serializer = serializer, reserved = reserved, 
   184     includes = includes, name_syntax_table = name_syntax_table, module_alias = module_alias };
   185 fun map_target f ( Target { serial, serializer, reserved, includes, name_syntax_table, module_alias } ) =
   186   mk_target (f ((serial, serializer), ((reserved, includes), (name_syntax_table, module_alias))));
   187 fun merge_target target (Target { serial = serial1, serializer = serializer,
   188   reserved = reserved1, includes = includes1,
   189   name_syntax_table = name_syntax_table1, module_alias = module_alias1 },
   190     Target { serial = serial2, serializer = _,
   191       reserved = reserved2, includes = includes2,
   192       name_syntax_table = name_syntax_table2, module_alias = module_alias2 }) =
   193   if serial1 = serial2 then
   194     mk_target ((serial1, serializer),
   195       ((merge (op =) (reserved1, reserved2), Symtab.merge (op =) (includes1, includes2)),
   196         (merge_name_syntax_table (name_syntax_table1, name_syntax_table2),
   197           Symtab.join (K snd) (module_alias1, module_alias2))
   198     ))
   199   else
   200     error ("Incompatible serializers: " ^ quote target);
   201 
   202 structure CodeTargetData = TheoryDataFun
   203 (
   204   type T = target Symtab.table * string list;
   205   val empty = (Symtab.empty, []);
   206   val copy = I;
   207   val extend = I;
   208   fun merge _ ((target1, exc1) : T, (target2, exc2)) =
   209     (Symtab.join merge_target (target1, target2), Library.merge (op =) (exc1, exc2));
   210 );
   211 
   212 fun the_serializer (Target { serializer, ... }) = serializer;
   213 fun the_reserved (Target { reserved, ... }) = reserved;
   214 fun the_includes (Target { includes, ... }) = includes;
   215 fun the_name_syntax (Target { name_syntax_table = NameSyntaxTable x, ... }) = x;
   216 fun the_module_alias (Target { module_alias , ... }) = module_alias;
   217 
   218 val abort_allowed = snd o CodeTargetData.get;
   219 
   220 fun assert_target thy target =
   221   case Symtab.lookup (fst (CodeTargetData.get thy)) target
   222    of SOME data => target
   223     | NONE => error ("Unknown code target language: " ^ quote target);
   224 
   225 fun add_target (target, seri) thy =
   226   let
   227     val _ = case Symtab.lookup (fst (CodeTargetData.get thy)) target
   228      of SOME _ => warning ("Overwriting existing serializer " ^ quote target)
   229       | NONE => ();
   230   in
   231     thy
   232     |> (CodeTargetData.map o apfst oo Symtab.map_default)
   233           (target, mk_target ((serial (), seri), (([], Symtab.empty),
   234             (mk_name_syntax_table ((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)),
   235               Symtab.empty))))
   236           ((map_target o apfst o apsnd o K) seri)
   237   end;
   238 
   239 fun map_target_data target f thy =
   240   let
   241     val _ = assert_target thy target;
   242   in
   243     thy
   244     |> (CodeTargetData.map o apfst o Symtab.map_entry target o map_target) f
   245   end;
   246 
   247 fun map_reserved target =
   248   map_target_data target o apsnd o apfst o apfst;
   249 fun map_includes target =
   250   map_target_data target o apsnd o apfst o apsnd;
   251 fun map_name_syntax target =
   252   map_target_data target o apsnd o apsnd o apfst o map_name_syntax_table;
   253 fun map_module_alias target =
   254   map_target_data target o apsnd o apsnd o apsnd;
   255 
   256 fun invoke_serializer thy abortable serializer reserved includes 
   257     module_alias class inst tyco const module args program1 cs1 =
   258   let
   259     val hidden = Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const;
   260     val cs2 = subtract (op =) hidden cs1;
   261     val program2 = Graph.subgraph (not o member (op =) hidden) program1;
   262     val all_cs = Graph.all_succs program2 cs2;
   263     val program3 = Graph.subgraph (member (op =) all_cs) program2;
   264     val empty_funs = filter_out (member (op =) abortable)
   265       (CodeThingol.empty_funs program3);
   266     val _ = if null empty_funs then () else error ("No defining equations for "
   267       ^ commas (map (CodeName.labelled_name thy) empty_funs));
   268   in
   269     serializer module args (CodeName.labelled_name thy) reserved includes
   270       (Symtab.lookup module_alias) (Symtab.lookup class)
   271       (Symtab.lookup tyco) (Symtab.lookup const)
   272       program3 cs2
   273   end;
   274 
   275 fun mount_serializer thy alt_serializer target =
   276   let
   277     val (targets, abortable) = CodeTargetData.get thy;
   278     val data = case Symtab.lookup targets target
   279      of SOME data => data
   280       | NONE => error ("Unknown code target language: " ^ quote target);
   281     val serializer = the_default (the_serializer data) alt_serializer;
   282     val reserved = the_reserved data;
   283     val includes = Symtab.dest (the_includes data);
   284     val module_alias = the_module_alias data;
   285     val { class, inst, tyco, const } = the_name_syntax data;
   286   in
   287     invoke_serializer thy abortable serializer reserved
   288       includes module_alias class inst tyco const
   289   end;
   290 
   291 fun serialize thy = mount_serializer thy NONE;
   292 
   293 fun parse_args f args =
   294   case Scan.read Args.stopper f args
   295    of SOME x => x
   296     | NONE => error "Bad serializer arguments";
   297 
   298 
   299 (** generic code combinators **)
   300 
   301 (* list, char, string, numeral and monad abstract syntax transformations *)
   302 
   303 fun nerror thm s = error (s ^ ",\nin equation " ^ Display.string_of_thm thm);
   304 
   305 fun implode_list c_nil c_cons t =
   306   let
   307     fun dest_cons (IConst (c, _) `$ t1 `$ t2) =
   308           if c = c_cons
   309           then SOME (t1, t2)
   310           else NONE
   311       | dest_cons _ = NONE;
   312     val (ts, t') = CodeThingol.unfoldr dest_cons t;
   313   in case t'
   314    of IConst (c, _) => if c = c_nil then SOME ts else NONE
   315     | _ => NONE
   316   end;
   317 
   318 fun decode_char c_nibbles (IConst (c1, _), IConst (c2, _)) =
   319       let
   320         fun idx c = find_index (curry (op =) c) c_nibbles;
   321         fun decode ~1 _ = NONE
   322           | decode _ ~1 = NONE
   323           | decode n m = SOME (chr (n * 16 + m));
   324       in decode (idx c1) (idx c2) end
   325   | decode_char _ _ = NONE;
   326 
   327 fun implode_string c_char c_nibbles mk_char mk_string ts =
   328   let
   329     fun implode_char (IConst (c, _) `$ t1 `$ t2) =
   330           if c = c_char then decode_char c_nibbles (t1, t2) else NONE
   331       | implode_char _ = NONE;
   332     val ts' = map implode_char ts;
   333   in if forall is_some ts'
   334     then (SOME o str o mk_string o implode o map_filter I) ts'
   335     else NONE
   336   end;
   337 
   338 fun implode_numeral thm negative c_pls c_min c_bit0 c_bit1 =
   339   let
   340     fun dest_bit (IConst (c, _)) = if c = c_bit0 then 0
   341           else if c = c_bit1 then 1
   342           else nerror thm "Illegal numeral expression: illegal bit"
   343       | dest_bit _ = nerror thm "Illegal numeral expression: illegal bit";
   344     fun dest_numeral (IConst (c, _)) = if c = c_pls then SOME 0
   345           else if c = c_min then
   346             if negative then SOME ~1 else NONE
   347           else nerror thm "Illegal numeral expression: illegal leading digit"
   348       | dest_numeral (t1 `$ t2) =
   349           let val (n, b) = (dest_numeral t2, dest_bit t1)
   350           in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
   351       | dest_numeral _ = nerror thm "Illegal numeral expression: illegal term";
   352   in dest_numeral #> the_default 0 end;
   353 
   354 fun implode_monad c_bind t =
   355   let
   356     fun dest_monad (IConst (c, _) `$ t1 `$ t2) =
   357           if c = c_bind
   358             then case CodeThingol.split_abs t2
   359              of SOME (((v, pat), ty), t') =>
   360                   SOME ((SOME (((SOME v, pat), ty), true), t1), t')
   361               | NONE => NONE
   362             else NONE
   363       | dest_monad t = case CodeThingol.split_let t
   364            of SOME (((pat, ty), tbind), t') =>
   365                 SOME ((SOME (((NONE, SOME pat), ty), false), tbind), t')
   366             | NONE => NONE;
   367   in CodeThingol.unfoldr dest_monad t end;
   368 
   369 
   370 (* applications and bindings *)
   371 
   372 fun gen_pr_app pr_app pr_term syntax_const is_cons thm pat
   373     vars fxy (app as ((c, (_, tys)), ts)) =
   374   case syntax_const c
   375    of NONE => if pat andalso not (is_cons c) then
   376         nerror thm "Non-constructor in pattern "
   377         else brackify fxy (pr_app thm pat vars app)
   378     | SOME (i, pr) =>
   379         let
   380           val k = if i < 0 then length tys else i;
   381           fun pr' fxy ts = pr (pr_term thm pat) thm pat vars fxy (ts ~~ curry Library.take k tys);
   382         in if k = length ts
   383           then pr' fxy ts
   384         else if k < length ts
   385           then case chop k ts of (ts1, ts2) =>
   386             brackify fxy (pr' APP ts1 :: map (pr_term thm pat vars BR) ts2)
   387           else pr_term thm pat vars fxy (CodeThingol.eta_expand app k)
   388         end;
   389 
   390 fun gen_pr_bind pr_bind pr_term thm (fxy : fixity) ((v, pat), ty : itype) vars =
   391   let
   392     val vs = case pat
   393      of SOME pat => CodeThingol.fold_varnames (insert (op =)) pat []
   394       | NONE => [];
   395     val vars' = CodeName.intro_vars (the_list v) vars;
   396     val vars'' = CodeName.intro_vars vs vars';
   397     val v' = Option.map (CodeName.lookup_var vars') v;
   398     val pat' = Option.map (pr_term thm true vars'' fxy) pat;
   399   in (pr_bind ((v', pat'), ty), vars'') end;
   400 
   401 
   402 (* name auxiliary *)
   403 
   404 val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
   405 val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
   406 
   407 val dest_name =
   408   apfst NameSpace.implode o split_last o fst o split_last o NameSpace.explode;
   409 
   410 fun mk_name_module reserved_names module_prefix module_alias program =
   411   let
   412     fun mk_alias name = case module_alias name
   413      of SOME name' => name'
   414       | NONE => name
   415           |> NameSpace.explode
   416           |> map (fn name => (the_single o fst) (Name.variants [name] reserved_names))
   417           |> NameSpace.implode;
   418     fun mk_prefix name = case module_prefix
   419      of SOME module_prefix => NameSpace.append module_prefix name
   420       | NONE => name;
   421     val tab =
   422       Symtab.empty
   423       |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))
   424            o fst o dest_name o fst)
   425              program
   426   in the o Symtab.lookup tab end;
   427 
   428 
   429 
   430 (** SML/OCaml serializer **)
   431 
   432 datatype ml_stmt =
   433     MLFuns of (string * (typscheme * ((iterm list * iterm) * thm) list)) list
   434   | MLDatas of (string * ((vname * sort) list * (string * itype list) list)) list
   435   | MLClass of string * (vname * ((class * string) list * (string * itype) list))
   436   | MLClassinst of string * ((class * (string * (vname * sort) list))
   437         * ((class * (string * (string * dict list list))) list
   438       * ((string * const) * thm) list));
   439 
   440 fun stmt_names_of (MLFuns fs) = map fst fs
   441   | stmt_names_of (MLDatas ds) = map fst ds
   442   | stmt_names_of (MLClass (c, _)) = [c]
   443   | stmt_names_of (MLClassinst (i, _)) = [i];
   444 
   445 fun pr_sml_stmt syntax_tyco syntax_const labelled_name reserved_names deresolve is_cons =
   446   let
   447     val pr_label_classrel = translate_string (fn "." => "__" | c => c)
   448       o NameSpace.qualifier;
   449     val pr_label_classparam = NameSpace.base o NameSpace.qualifier;
   450     fun pr_dicts fxy ds =
   451       let
   452         fun pr_dictvar (v, (_, 1)) = first_upper v ^ "_"
   453           | pr_dictvar (v, (i, _)) = first_upper v ^ string_of_int (i+1) ^ "_";
   454         fun pr_proj [] p =
   455               p
   456           | pr_proj [p'] p =
   457               brackets [p', p]
   458           | pr_proj (ps as _ :: _) p =
   459               brackets [Pretty.enum " o" "(" ")" ps, p];
   460         fun pr_dict fxy (DictConst (inst, dss)) =
   461               brackify fxy ((str o deresolve) inst :: map (pr_dicts BR) dss)
   462           | pr_dict fxy (DictVar (classrels, v)) =
   463               pr_proj (map (str o deresolve) classrels) ((str o pr_dictvar) v)
   464       in case ds
   465        of [] => str "()"
   466         | [d] => pr_dict fxy d
   467         | _ :: _ => (Pretty.list "(" ")" o map (pr_dict NOBR)) ds
   468       end;
   469     fun pr_tyvar_dicts vs =
   470       vs
   471       |> map (fn (v, sort) => map_index (fn (i, _) =>
   472            DictVar ([], (v, (i, length sort)))) sort)
   473       |> map (pr_dicts BR);
   474     fun pr_tycoexpr fxy (tyco, tys) =
   475       let
   476         val tyco' = (str o deresolve) tyco
   477       in case map (pr_typ BR) tys
   478        of [] => tyco'
   479         | [p] => Pretty.block [p, Pretty.brk 1, tyco']
   480         | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
   481       end
   482     and pr_typ fxy (tyco `%% tys) = (case syntax_tyco tyco
   483          of NONE => pr_tycoexpr fxy (tyco, tys)
   484           | SOME (i, pr) => pr pr_typ fxy tys)
   485       | pr_typ fxy (ITyVar v) = str ("'" ^ v);
   486     fun pr_term thm pat vars fxy (IConst c) =
   487           pr_app thm pat vars fxy (c, [])
   488       | pr_term thm pat vars fxy (IVar v) =
   489           str (CodeName.lookup_var vars v)
   490       | pr_term thm pat vars fxy (t as t1 `$ t2) =
   491           (case CodeThingol.unfold_const_app t
   492            of SOME c_ts => pr_app thm pat vars fxy c_ts
   493             | NONE =>
   494                 brackify fxy [pr_term thm pat vars NOBR t1, pr_term thm pat vars BR t2])
   495       | pr_term thm pat vars fxy (t as _ `|-> _) =
   496           let
   497             val (binds, t') = CodeThingol.unfold_abs t;
   498             fun pr ((v, pat), ty) =
   499               pr_bind thm NOBR ((SOME v, pat), ty)
   500               #>> (fn p => concat [str "fn", p, str "=>"]);
   501             val (ps, vars') = fold_map pr binds vars;
   502           in brackets (ps @ [pr_term thm pat vars' NOBR t']) end
   503       | pr_term thm pat vars fxy (ICase (cases as (_, t0))) =
   504           (case CodeThingol.unfold_const_app t0
   505            of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
   506                 then pr_case thm vars fxy cases
   507                 else pr_app thm pat vars fxy c_ts
   508             | NONE => pr_case thm vars fxy cases)
   509     and pr_app' thm pat vars (app as ((c, (iss, tys)), ts)) =
   510       if is_cons c then let
   511         val k = length tys
   512       in if k < 2 then 
   513         (str o deresolve) c :: map (pr_term thm pat vars BR) ts
   514       else if k = length ts then
   515         [(str o deresolve) c, Pretty.enum "," "(" ")" (map (pr_term thm pat vars NOBR) ts)]
   516       else [pr_term thm pat vars BR (CodeThingol.eta_expand app k)] end else
   517         (str o deresolve) c
   518           :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts
   519     and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons thm pat vars
   520     and pr_bind' ((NONE, NONE), _) = str "_"
   521       | pr_bind' ((SOME v, NONE), _) = str v
   522       | pr_bind' ((NONE, SOME p), _) = p
   523       | pr_bind' ((SOME v, SOME p), _) = concat [str v, str "as", p]
   524     and pr_bind thm = gen_pr_bind pr_bind' pr_term thm
   525     and pr_case thm vars fxy (cases as ((_, [_]), _)) =
   526           let
   527             val (binds, t') = CodeThingol.unfold_let (ICase cases);
   528             fun pr ((pat, ty), t) vars =
   529               vars
   530               |> pr_bind thm NOBR ((NONE, SOME pat), ty)
   531               |>> (fn p => semicolon [str "val", p, str "=", pr_term thm false vars NOBR t])
   532             val (ps, vars') = fold_map pr binds vars;
   533           in
   534             Pretty.chunks [
   535               [str ("let"), Pretty.fbrk, Pretty.chunks ps] |> Pretty.block,
   536               [str ("in"), Pretty.fbrk, pr_term thm false vars' NOBR t'] |> Pretty.block,
   537               str ("end")
   538             ]
   539           end
   540       | pr_case thm vars fxy (((td, ty), b::bs), _) =
   541           let
   542             fun pr delim (pat, t) =
   543               let
   544                 val (p, vars') = pr_bind thm NOBR ((NONE, SOME pat), ty) vars;
   545               in
   546                 concat [str delim, p, str "=>", pr_term thm false vars' NOBR t]
   547               end;
   548           in
   549             (Pretty.enclose "(" ")" o single o brackify fxy) (
   550               str "case"
   551               :: pr_term thm false vars NOBR td
   552               :: pr "of" b
   553               :: map (pr "|") bs
   554             )
   555           end
   556       | pr_case thm vars fxy ((_, []), _) = str "raise Fail \"empty case\"";
   557     fun pr_stmt (MLFuns (funns as (funn :: funns'))) =
   558           let
   559             val definer =
   560               let
   561                 fun no_args _ (((ts, _), _) :: _) = length ts
   562                   | no_args ty [] = (length o fst o CodeThingol.unfold_fun) ty;
   563                 fun mk 0 [] = "val"
   564                   | mk 0 vs = if (null o filter_out (null o snd)) vs
   565                       then "val" else "fun"
   566                   | mk k _ = "fun";
   567                 fun chk (_, ((vs, ty), eqs)) NONE = SOME (mk (no_args ty eqs) vs)
   568                   | chk (_, ((vs, ty), eqs)) (SOME defi) =
   569                       if defi = mk (no_args ty eqs) vs then SOME defi
   570                       else error ("Mixing simultaneous vals and funs not implemented: "
   571                         ^ commas (map (labelled_name o fst) funns));
   572               in the (fold chk funns NONE) end;
   573             fun pr_funn definer (name, ((vs, ty), [])) =
   574                   let
   575                     val vs_dict = filter_out (null o snd) vs;
   576                     val n = length vs_dict + (length o fst o CodeThingol.unfold_fun) ty;
   577                     val exc_str =
   578                       (ML_Syntax.print_string o NameSpace.base o NameSpace.qualifier) name;
   579                   in
   580                     concat (
   581                       str definer
   582                       :: (str o deresolve) name
   583                       :: map str (replicate n "_")
   584                       @ str "="
   585                       :: str "raise"
   586                       :: str "(Fail"
   587                       @@ str (exc_str ^ ")")
   588                     )
   589                   end
   590               | pr_funn definer (name, ((vs, ty), eqs as eq :: eqs')) =
   591                   let
   592                     val vs_dict = filter_out (null o snd) vs;
   593                     val shift = if null eqs' then I else
   594                       map (Pretty.block o single o Pretty.block o single);
   595                     fun pr_eq definer ((ts, t), thm) =
   596                       let
   597                         val consts = map_filter
   598                           (fn c => if (is_some o syntax_const) c
   599                             then NONE else (SOME o NameSpace.base o deresolve) c)
   600                             ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);
   601                         val vars = reserved_names
   602                           |> CodeName.intro_vars consts
   603                           |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)
   604                                (insert (op =)) ts []);
   605                       in
   606                         concat (
   607                           [str definer, (str o deresolve) name]
   608                           @ (if null ts andalso null vs_dict
   609                              then [str ":", pr_typ NOBR ty]
   610                              else
   611                                pr_tyvar_dicts vs_dict
   612                                @ map (pr_term thm true vars BR) ts)
   613                        @ [str "=", pr_term thm false vars NOBR t]
   614                         )
   615                       end
   616                   in
   617                     (Pretty.block o Pretty.fbreaks o shift) (
   618                       pr_eq definer eq
   619                       :: map (pr_eq "|") eqs'
   620                     )
   621                   end;
   622             val (ps, p) = split_last (pr_funn definer funn :: map (pr_funn "and") funns');
   623           in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end
   624      | pr_stmt (MLDatas (datas as (data :: datas'))) =
   625           let
   626             fun pr_co (co, []) =
   627                   str (deresolve co)
   628               | pr_co (co, tys) =
   629                   concat [
   630                     str (deresolve co),
   631                     str "of",
   632                     Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys)
   633                   ];
   634             fun pr_data definer (tyco, (vs, [])) =
   635                   concat (
   636                     str definer
   637                     :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
   638                     :: str "="
   639                     @@ str "EMPTY__" 
   640                   )
   641               | pr_data definer (tyco, (vs, cos)) =
   642                   concat (
   643                     str definer
   644                     :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
   645                     :: str "="
   646                     :: separate (str "|") (map pr_co cos)
   647                   );
   648             val (ps, p) = split_last
   649               (pr_data "datatype" data :: map (pr_data "and") datas');
   650           in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end
   651      | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
   652           let
   653             val w = first_upper v ^ "_";
   654             fun pr_superclass_field (class, classrel) =
   655               (concat o map str) [
   656                 pr_label_classrel classrel, ":", "'" ^ v, deresolve class
   657               ];
   658             fun pr_classparam_field (classparam, ty) =
   659               concat [
   660                 (str o pr_label_classparam) classparam, str ":", pr_typ NOBR ty
   661               ];
   662             fun pr_classparam_proj (classparam, _) =
   663               semicolon [
   664                 str "fun",
   665                 (str o deresolve) classparam,
   666                 Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolve class)],
   667                 str "=",
   668                 str ("#" ^ pr_label_classparam classparam),
   669                 str w
   670               ];
   671             fun pr_superclass_proj (_, classrel) =
   672               semicolon [
   673                 str "fun",
   674                 (str o deresolve) classrel,
   675                 Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolve class)],
   676                 str "=",
   677                 str ("#" ^ pr_label_classrel classrel),
   678                 str w
   679               ];
   680           in
   681             Pretty.chunks (
   682               concat [
   683                 str ("type '" ^ v),
   684                 (str o deresolve) class,
   685                 str "=",
   686                 Pretty.enum "," "{" "};" (
   687                   map pr_superclass_field superclasses @ map pr_classparam_field classparams
   688                 )
   689               ]
   690               :: map pr_superclass_proj superclasses
   691               @ map pr_classparam_proj classparams
   692             )
   693           end
   694      | pr_stmt (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =
   695           let
   696             fun pr_superclass (_, (classrel, dss)) =
   697               concat [
   698                 (str o pr_label_classrel) classrel,
   699                 str "=",
   700                 pr_dicts NOBR [DictConst dss]
   701               ];
   702             fun pr_classparam ((classparam, c_inst), thm) =
   703               concat [
   704                 (str o pr_label_classparam) classparam,
   705                 str "=",
   706                 pr_app thm false reserved_names NOBR (c_inst, [])
   707               ];
   708           in
   709             semicolon ([
   710               str (if null arity then "val" else "fun"),
   711               (str o deresolve) inst ] @
   712               pr_tyvar_dicts arity @ [
   713               str "=",
   714               Pretty.enum "," "{" "}"
   715                 (map pr_superclass superarities @ map pr_classparam classparam_insts),
   716               str ":",
   717               pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
   718             ])
   719           end;
   720   in pr_stmt end;
   721 
   722 fun pr_sml_module name content =
   723   Pretty.chunks (
   724     str ("structure " ^ name ^ " = ")
   725     :: str "struct"
   726     :: str ""
   727     :: content
   728     @ str ""
   729     @@ str ("end; (*struct " ^ name ^ "*)")
   730   );
   731 
   732 fun pr_ocaml_stmt syntax_tyco syntax_const labelled_name reserved_names deresolve is_cons =
   733   let
   734     fun pr_dicts fxy ds =
   735       let
   736         fun pr_dictvar (v, (_, 1)) = "_" ^ first_upper v
   737           | pr_dictvar (v, (i, _)) = "_" ^ first_upper v ^ string_of_int (i+1);
   738         fun pr_proj ps p =
   739           fold_rev (fn p2 => fn p1 => Pretty.block [p1, str ".", str p2]) ps p
   740         fun pr_dict fxy (DictConst (inst, dss)) =
   741               brackify fxy ((str o deresolve) inst :: map (pr_dicts BR) dss)
   742           | pr_dict fxy (DictVar (classrels, v)) =
   743               pr_proj (map deresolve classrels) ((str o pr_dictvar) v)
   744       in case ds
   745        of [] => str "()"
   746         | [d] => pr_dict fxy d
   747         | _ :: _ => (Pretty.list "(" ")" o map (pr_dict NOBR)) ds
   748       end;
   749     fun pr_tyvar_dicts vs =
   750       vs
   751       |> map (fn (v, sort) => map_index (fn (i, _) =>
   752            DictVar ([], (v, (i, length sort)))) sort)
   753       |> map (pr_dicts BR);
   754     fun pr_tycoexpr fxy (tyco, tys) =
   755       let
   756         val tyco' = (str o deresolve) tyco
   757       in case map (pr_typ BR) tys
   758        of [] => tyco'
   759         | [p] => Pretty.block [p, Pretty.brk 1, tyco']
   760         | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
   761       end
   762     and pr_typ fxy (tyco `%% tys) = (case syntax_tyco tyco
   763          of NONE => pr_tycoexpr fxy (tyco, tys)
   764           | SOME (i, pr) => pr pr_typ fxy tys)
   765       | pr_typ fxy (ITyVar v) = str ("'" ^ v);
   766     fun pr_term thm pat vars fxy (IConst c) =
   767           pr_app thm pat vars fxy (c, [])
   768       | pr_term thm pat vars fxy (IVar v) =
   769           str (CodeName.lookup_var vars v)
   770       | pr_term thm pat vars fxy (t as t1 `$ t2) =
   771           (case CodeThingol.unfold_const_app t
   772            of SOME c_ts => pr_app thm pat vars fxy c_ts
   773             | NONE =>
   774                 brackify fxy [pr_term thm pat vars NOBR t1, pr_term thm pat vars BR t2])
   775       | pr_term thm pat vars fxy (t as _ `|-> _) =
   776           let
   777             val (binds, t') = CodeThingol.unfold_abs t;
   778             fun pr ((v, pat), ty) = pr_bind thm BR ((SOME v, pat), ty);
   779             val (ps, vars') = fold_map pr binds vars;
   780           in brackets (str "fun" :: ps @ str "->" @@ pr_term thm pat vars' NOBR t') end
   781       | pr_term thm pat vars fxy (ICase (cases as (_, t0))) = (case CodeThingol.unfold_const_app t0
   782            of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
   783                 then pr_case thm vars fxy cases
   784                 else pr_app thm pat vars fxy c_ts
   785             | NONE => pr_case thm vars fxy cases)
   786     and pr_app' thm pat vars (app as ((c, (iss, tys)), ts)) =
   787       if is_cons c then
   788         if length tys = length ts
   789         then case ts
   790          of [] => [(str o deresolve) c]
   791           | [t] => [(str o deresolve) c, pr_term thm pat vars BR t]
   792           | _ => [(str o deresolve) c, Pretty.enum "," "(" ")"
   793                     (map (pr_term thm pat vars NOBR) ts)]
   794         else [pr_term thm pat vars BR (CodeThingol.eta_expand app (length tys))]
   795       else (str o deresolve) c
   796         :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts)
   797     and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons thm pat vars
   798     and pr_bind' ((NONE, NONE), _) = str "_"
   799       | pr_bind' ((SOME v, NONE), _) = str v
   800       | pr_bind' ((NONE, SOME p), _) = p
   801       | pr_bind' ((SOME v, SOME p), _) = brackets [p, str "as", str v]
   802     and pr_bind thm = gen_pr_bind pr_bind' pr_term thm
   803     and pr_case thm vars fxy (cases as ((_, [_]), _)) =
   804           let
   805             val (binds, t') = CodeThingol.unfold_let (ICase cases);
   806             fun pr ((pat, ty), t) vars =
   807               vars
   808               |> pr_bind thm NOBR ((NONE, SOME pat), ty)
   809               |>> (fn p => concat
   810                   [str "let", p, str "=", pr_term thm false vars NOBR t, str "in"])
   811             val (ps, vars') = fold_map pr binds vars;
   812           in Pretty.chunks (ps @| pr_term thm false vars' NOBR t') end
   813       | pr_case thm vars fxy (((td, ty), b::bs), _) =
   814           let
   815             fun pr delim (pat, t) =
   816               let
   817                 val (p, vars') = pr_bind thm NOBR ((NONE, SOME pat), ty) vars;
   818               in concat [str delim, p, str "->", pr_term thm false vars' NOBR t] end;
   819           in
   820             (Pretty.enclose "(" ")" o single o brackify fxy) (
   821               str "match"
   822               :: pr_term thm false vars NOBR td
   823               :: pr "with" b
   824               :: map (pr "|") bs
   825             )
   826           end
   827       | pr_case thm vars fxy ((_, []), _) = str "failwith \"empty case\"";
   828     fun fish_params vars eqs =
   829       let
   830         fun fish_param _ (w as SOME _) = w
   831           | fish_param (IVar v) NONE = SOME v
   832           | fish_param _ NONE = NONE;
   833         fun fillup_param _ (_, SOME v) = v
   834           | fillup_param x (i, NONE) = x ^ string_of_int i;
   835         val fished1 = fold (map2 fish_param) eqs (replicate (length (hd eqs)) NONE);
   836         val x = Name.variant (map_filter I fished1) "x";
   837         val fished2 = map_index (fillup_param x) fished1;
   838         val (fished3, _) = Name.variants fished2 Name.context;
   839         val vars' = CodeName.intro_vars fished3 vars;
   840       in map (CodeName.lookup_var vars') fished3 end;
   841     fun pr_stmt (MLFuns (funns as funn :: funns')) =
   842           let
   843             fun pr_eq ((ts, t), thm) =
   844               let
   845                 val consts = map_filter
   846                   (fn c => if (is_some o syntax_const) c
   847                     then NONE else (SOME o NameSpace.base o deresolve) c)
   848                     ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);
   849                 val vars = reserved_names
   850                   |> CodeName.intro_vars consts
   851                   |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)
   852                       (insert (op =)) ts []);
   853               in concat [
   854                 (Pretty.block o Pretty.commas) (map (pr_term thm true vars NOBR) ts),
   855                 str "->",
   856                 pr_term thm false vars NOBR t
   857               ] end;
   858             fun pr_eqs name ty [] =
   859                   let
   860                     val n = (length o fst o CodeThingol.unfold_fun) ty;
   861                     val exc_str =
   862                       (ML_Syntax.print_string o NameSpace.base o NameSpace.qualifier) name;
   863                   in
   864                     concat (
   865                       map str (replicate n "_")
   866                       @ str "="
   867                       :: str "failwith"
   868                       @@ str exc_str
   869                     )
   870                   end
   871               | pr_eqs _ _ [((ts, t), thm)] =
   872                   let
   873                     val consts = map_filter
   874                       (fn c => if (is_some o syntax_const) c
   875                         then NONE else (SOME o NameSpace.base o deresolve) c)
   876                         ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);
   877                     val vars = reserved_names
   878                       |> CodeName.intro_vars consts
   879                       |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)
   880                           (insert (op =)) ts []);
   881                   in
   882                     concat (
   883                       map (pr_term thm true vars BR) ts
   884                       @ str "="
   885                       @@ pr_term thm false vars NOBR t
   886                     )
   887                   end
   888               | pr_eqs _ _ (eqs as (eq as (([_], _), _)) :: eqs') =
   889                   Pretty.block (
   890                     str "="
   891                     :: Pretty.brk 1
   892                     :: str "function"
   893                     :: Pretty.brk 1
   894                     :: pr_eq eq
   895                     :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
   896                           o single o pr_eq) eqs'
   897                   )
   898               | pr_eqs _ _ (eqs as eq :: eqs') =
   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)
   904                           (insert (op =)) (map (snd o fst) eqs) []);
   905                     val vars = reserved_names
   906                       |> CodeName.intro_vars consts;
   907                     val dummy_parms = (map str o fish_params vars o map (fst o fst)) eqs;
   908                   in
   909                     Pretty.block (
   910                       Pretty.breaks dummy_parms
   911                       @ Pretty.brk 1
   912                       :: str "="
   913                       :: Pretty.brk 1
   914                       :: str "match"
   915                       :: Pretty.brk 1
   916                       :: (Pretty.block o Pretty.commas) dummy_parms
   917                       :: Pretty.brk 1
   918                       :: str "with"
   919                       :: Pretty.brk 1
   920                       :: pr_eq eq
   921                       :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
   922                            o single o pr_eq) eqs'
   923                     )
   924                   end;
   925             fun pr_funn definer (name, ((vs, ty), eqs)) =
   926               concat (
   927                 str definer
   928                 :: (str o deresolve) name
   929                 :: pr_tyvar_dicts (filter_out (null o snd) vs)
   930                 @| pr_eqs name ty eqs
   931               );
   932             val (ps, p) = split_last
   933               (pr_funn "let rec" funn :: map (pr_funn "and") funns');
   934           in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end
   935      | pr_stmt (MLDatas (datas as (data :: datas'))) =
   936           let
   937             fun pr_co (co, []) =
   938                   str (deresolve co)
   939               | pr_co (co, tys) =
   940                   concat [
   941                     str (deresolve co),
   942                     str "of",
   943                     Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys)
   944                   ];
   945             fun pr_data definer (tyco, (vs, [])) =
   946                   concat (
   947                     str definer
   948                     :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
   949                     :: str "="
   950                     @@ str "EMPTY_"
   951                   )
   952               | pr_data definer (tyco, (vs, cos)) =
   953                   concat (
   954                     str definer
   955                     :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
   956                     :: str "="
   957                     :: separate (str "|") (map pr_co cos)
   958                   );
   959             val (ps, p) = split_last
   960               (pr_data "type" data :: map (pr_data "and") datas');
   961           in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end
   962      | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
   963           let
   964             val w = "_" ^ first_upper v;
   965             fun pr_superclass_field (class, classrel) =
   966               (concat o map str) [
   967                 deresolve classrel, ":", "'" ^ v, deresolve class
   968               ];
   969             fun pr_classparam_field (classparam, ty) =
   970               concat [
   971                 (str o deresolve) classparam, str ":", pr_typ NOBR ty
   972               ];
   973             fun pr_classparam_proj (classparam, _) =
   974               concat [
   975                 str "let",
   976                 (str o deresolve) classparam,
   977                 str w,
   978                 str "=",
   979                 str (w ^ "." ^ deresolve classparam ^ ";;")
   980               ];
   981           in Pretty.chunks (
   982             concat [
   983               str ("type '" ^ v),
   984               (str o deresolve) class,
   985               str "=",
   986               enum_default "();;" ";" "{" "};;" (
   987                 map pr_superclass_field superclasses
   988                 @ map pr_classparam_field classparams
   989               )
   990             ]
   991             :: map pr_classparam_proj classparams
   992           ) end
   993      | pr_stmt (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =
   994           let
   995             fun pr_superclass (_, (classrel, dss)) =
   996               concat [
   997                 (str o deresolve) classrel,
   998                 str "=",
   999                 pr_dicts NOBR [DictConst dss]
  1000               ];
  1001             fun pr_classparam_inst ((classparam, c_inst), thm) =
  1002               concat [
  1003                 (str o deresolve) classparam,
  1004                 str "=",
  1005                 pr_app thm false reserved_names NOBR (c_inst, [])
  1006               ];
  1007           in
  1008             concat (
  1009               str "let"
  1010               :: (str o deresolve) inst
  1011               :: pr_tyvar_dicts arity
  1012               @ str "="
  1013               @@ (Pretty.enclose "(" ");;" o Pretty.breaks) [
  1014                 enum_default "()" ";" "{" "}" (map pr_superclass superarities
  1015                   @ map pr_classparam_inst classparam_insts),
  1016                 str ":",
  1017                 pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
  1018               ]
  1019             )
  1020           end;
  1021   in pr_stmt end;
  1022 
  1023 fun pr_ocaml_module name content =
  1024   Pretty.chunks (
  1025     str ("module " ^ name ^ " = ")
  1026     :: str "struct"
  1027     :: str ""
  1028     :: content
  1029     @ str ""
  1030     @@ str ("end;; (*struct " ^ name ^ "*)")
  1031   );
  1032 
  1033 local
  1034 
  1035 datatype ml_node =
  1036     Dummy of string
  1037   | Stmt of string * ml_stmt
  1038   | Module of string * ((Name.context * Name.context) * ml_node Graph.T);
  1039 
  1040 in
  1041 
  1042 fun ml_node_of_program labelled_name module_name reserved_names raw_module_alias program =
  1043   let
  1044     val module_alias = if is_some module_name then K module_name else raw_module_alias;
  1045     val reserved_names = Name.make_context reserved_names;
  1046     val empty_module = ((reserved_names, reserved_names), Graph.empty);
  1047     fun map_node [] f = f
  1048       | map_node (m::ms) f =
  1049           Graph.default_node (m, Module (m, empty_module))
  1050           #> Graph.map_node m (fn (Module (module_name, (nsp, nodes))) =>
  1051                Module (module_name, (nsp, map_node ms f nodes)));
  1052     fun map_nsp_yield [] f (nsp, nodes) =
  1053           let
  1054             val (x, nsp') = f nsp
  1055           in (x, (nsp', nodes)) end
  1056       | map_nsp_yield (m::ms) f (nsp, nodes) =
  1057           let
  1058             val (x, nodes') =
  1059               nodes
  1060               |> Graph.default_node (m, Module (m, empty_module))
  1061               |> Graph.map_node_yield m (fn Module (d_module_name, nsp_nodes) => 
  1062                   let
  1063                     val (x, nsp_nodes') = map_nsp_yield ms f nsp_nodes
  1064                   in (x, Module (d_module_name, nsp_nodes')) end)
  1065           in (x, (nsp, nodes')) end;
  1066     fun map_nsp_fun_yield f (nsp_fun, nsp_typ) =
  1067       let
  1068         val (x, nsp_fun') = f nsp_fun
  1069       in (x, (nsp_fun', nsp_typ)) end;
  1070     fun map_nsp_typ_yield f (nsp_fun, nsp_typ) =
  1071       let
  1072         val (x, nsp_typ') = f nsp_typ
  1073       in (x, (nsp_fun, nsp_typ')) end;
  1074     val mk_name_module = mk_name_module reserved_names NONE module_alias program;
  1075     fun mk_name_stmt upper name nsp =
  1076       let
  1077         val (_, base) = dest_name name;
  1078         val base' = if upper then first_upper base else base;
  1079         val ([base''], nsp') = Name.variants [base'] nsp;
  1080       in (base'', nsp') end;
  1081     fun add_funs stmts =
  1082       fold_map
  1083         (fn (name, CodeThingol.Fun stmt) =>
  1084               map_nsp_fun_yield (mk_name_stmt false name) #>>
  1085                 rpair (name, stmt)
  1086           | (name, _) =>
  1087               error ("Function block containing illegal statement: " ^ labelled_name name)
  1088         ) stmts
  1089       #>> (split_list #> apsnd MLFuns);
  1090     fun add_datatypes stmts =
  1091       fold_map
  1092         (fn (name, CodeThingol.Datatype stmt) =>
  1093               map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt))
  1094           | (name, CodeThingol.Datatypecons _) =>
  1095               map_nsp_fun_yield (mk_name_stmt true name) #>> rpair NONE
  1096           | (name, _) =>
  1097               error ("Datatype block containing illegal statement: " ^ labelled_name name)
  1098         ) stmts
  1099       #>> (split_list #> apsnd (map_filter I
  1100         #> (fn [] => error ("Datatype block without data statement: "
  1101                   ^ (commas o map (labelled_name o fst)) stmts)
  1102              | stmts => MLDatas stmts)));
  1103     fun add_class stmts =
  1104       fold_map
  1105         (fn (name, CodeThingol.Class info) =>
  1106               map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, info))
  1107           | (name, CodeThingol.Classrel _) =>
  1108               map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
  1109           | (name, CodeThingol.Classparam _) =>
  1110               map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
  1111           | (name, _) =>
  1112               error ("Class block containing illegal statement: " ^ labelled_name name)
  1113         ) stmts
  1114       #>> (split_list #> apsnd (map_filter I
  1115         #> (fn [] => error ("Class block without class statement: "
  1116                   ^ (commas o map (labelled_name o fst)) stmts)
  1117              | [stmt] => MLClass stmt)));
  1118     fun add_inst [(name, CodeThingol.Classinst stmt)] =
  1119       map_nsp_fun_yield (mk_name_stmt false name)
  1120       #>> (fn base => ([base], MLClassinst (name, stmt)));
  1121     fun add_stmts ((stmts as (_, CodeThingol.Fun _)::_)) =
  1122           add_funs stmts
  1123       | add_stmts ((stmts as (_, CodeThingol.Datatypecons _)::_)) =
  1124           add_datatypes stmts
  1125       | add_stmts ((stmts as (_, CodeThingol.Datatype _)::_)) =
  1126           add_datatypes stmts
  1127       | add_stmts ((stmts as (_, CodeThingol.Class _)::_)) =
  1128           add_class stmts
  1129       | add_stmts ((stmts as (_, CodeThingol.Classrel _)::_)) =
  1130           add_class stmts
  1131       | add_stmts ((stmts as (_, CodeThingol.Classparam _)::_)) =
  1132           add_class stmts
  1133       | add_stmts ((stmts as [(_, CodeThingol.Classinst _)])) =
  1134           add_inst stmts
  1135       | add_stmts stmts = error ("Illegal mutual dependencies: " ^
  1136           (commas o map (labelled_name o fst)) stmts);
  1137     fun add_stmts' stmts nsp_nodes =
  1138       let
  1139         val names as (name :: names') = map fst stmts;
  1140         val deps =
  1141           []
  1142           |> fold (fold (insert (op =)) o Graph.imm_succs program) names
  1143           |> subtract (op =) names;
  1144         val (module_names, _) = (split_list o map dest_name) names;
  1145         val module_name = (the_single o distinct (op =) o map mk_name_module) module_names
  1146           handle Empty =>
  1147             error ("Different namespace prefixes for mutual dependencies:\n"
  1148               ^ commas (map labelled_name names)
  1149               ^ "\n"
  1150               ^ commas module_names);
  1151         val module_name_path = NameSpace.explode module_name;
  1152         fun add_dep name name' =
  1153           let
  1154             val module_name' = (mk_name_module o fst o dest_name) name';
  1155           in if module_name = module_name' then
  1156             map_node module_name_path (Graph.add_edge (name, name'))
  1157           else let
  1158             val (common, (diff1::_, diff2::_)) = chop_prefix (op =)
  1159               (module_name_path, NameSpace.explode module_name');
  1160           in
  1161             map_node common
  1162               (fn node => Graph.add_edge_acyclic (diff1, diff2) node
  1163                 handle Graph.CYCLES _ => error ("Dependency "
  1164                   ^ quote name ^ " -> " ^ quote name'
  1165                   ^ " would result in module dependency cycle"))
  1166           end end;
  1167       in
  1168         nsp_nodes
  1169         |> map_nsp_yield module_name_path (add_stmts stmts)
  1170         |-> (fn (base' :: bases', stmt') =>
  1171            apsnd (map_node module_name_path (Graph.new_node (name, (Stmt (base', stmt')))
  1172               #> fold2 (fn name' => fn base' =>
  1173                    Graph.new_node (name', (Dummy base'))) names' bases')))
  1174         |> apsnd (fold (fn name => fold (add_dep name) deps) names)
  1175         |> apsnd (fold_product (curry (map_node module_name_path o Graph.add_edge)) names names)
  1176       end;
  1177     val (_, nodes) = empty_module
  1178       |> fold add_stmts' (map (AList.make (Graph.get_node program))
  1179           (rev (Graph.strong_conn program)));
  1180     fun deresolver prefix name = 
  1181       let
  1182         val module_name = (fst o dest_name) name;
  1183         val module_name' = (NameSpace.explode o mk_name_module) module_name;
  1184         val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name');
  1185         val stmt_name =
  1186           nodes
  1187           |> fold (fn name => fn node => case Graph.get_node node name
  1188               of Module (_, (_, node)) => node) module_name'
  1189           |> (fn node => case Graph.get_node node name of Stmt (stmt_name, _) => stmt_name
  1190                | Dummy stmt_name => stmt_name);
  1191       in
  1192         NameSpace.implode (remainder @ [stmt_name])
  1193       end handle Graph.UNDEF _ =>
  1194         error ("Unknown statement name: " ^ labelled_name name);
  1195   in (deresolver, nodes) end;
  1196 
  1197 fun serialize_ml compile pr_module pr_stmt projection raw_module_name labelled_name reserved_names includes raw_module_alias
  1198   _ syntax_tyco syntax_const program cs destination =
  1199   let
  1200     val is_cons = CodeThingol.is_cons program;
  1201     val stmt_names = stmt_names_of_destination destination;
  1202     val module_name = if null stmt_names then raw_module_name else SOME "Code";
  1203     val (deresolver, nodes) = ml_node_of_program labelled_name module_name
  1204       reserved_names raw_module_alias program;
  1205     val reserved_names = CodeName.make_vars reserved_names;
  1206     fun pr_node prefix (Dummy _) =
  1207           NONE
  1208       | pr_node prefix (Stmt (_, stmt)) = if null stmt_names orelse
  1209           (not o null o filter (member (op =) stmt_names) o stmt_names_of) stmt then SOME
  1210             (pr_stmt syntax_tyco syntax_const labelled_name reserved_names
  1211               (deresolver prefix) is_cons stmt)
  1212           else NONE
  1213       | pr_node prefix (Module (module_name, (_, nodes))) =
  1214           let
  1215             val ps = separate (str "")
  1216               ((map_filter (pr_node (prefix @ [module_name]) o Graph.get_node nodes)
  1217                 o rev o flat o Graph.strong_conn) nodes)
  1218           in SOME (case destination of String _ => Pretty.chunks ps
  1219            | _ => pr_module module_name ps)
  1220           end;
  1221     val cs' = map_filter (try (deresolver (if is_some module_name then the_list module_name else [])))
  1222       cs;
  1223     val p = Pretty.chunks (separate (str "") (map snd includes @ (map_filter
  1224       (pr_node [] o Graph.get_node nodes) o rev o flat o Graph.strong_conn) nodes));
  1225     fun output Compile = K NONE o compile o code_of_pretty
  1226       | output Export = K NONE o code_writeln
  1227       | output (File file) = K NONE o File.write file o code_of_pretty
  1228       | output (String _) = SOME o code_of_pretty;
  1229   in projection (output destination p) cs' end;
  1230 
  1231 end; (*local*)
  1232 
  1233 fun isar_seri_sml module_name =
  1234   parse_args (Scan.succeed ())
  1235   #> (fn () => serialize_ml (use_text (1, "generated code") Output.ml_output false)
  1236       pr_sml_module pr_sml_stmt K module_name);
  1237 
  1238 fun isar_seri_ocaml module_name =
  1239   parse_args (Scan.succeed ())
  1240   #> (fn () => serialize_ml (fn _ => error "OCaml: no internal compilation")
  1241       pr_ocaml_module pr_ocaml_stmt K module_name);
  1242 
  1243 
  1244 (** Haskell serializer **)
  1245 
  1246 fun pr_haskell_bind pr_term =
  1247   let
  1248     fun pr_bind ((NONE, NONE), _) = str "_"
  1249       | pr_bind ((SOME v, NONE), _) = str v
  1250       | pr_bind ((NONE, SOME p), _) = p
  1251       | pr_bind ((SOME v, SOME p), _) = brackets [str v, str "@", p];
  1252   in gen_pr_bind pr_bind pr_term end;
  1253 
  1254 fun pr_haskell_stmt syntax_class syntax_tyco syntax_const labelled_name
  1255     init_syms deresolve is_cons contr_classparam_typs deriving_show =
  1256   let
  1257     val deresolve_base = NameSpace.base o deresolve;
  1258     fun class_name class = case syntax_class class
  1259      of NONE => deresolve class
  1260       | SOME (class, _) => class;
  1261     fun classparam_name class classparam = case syntax_class class
  1262      of NONE => deresolve_base classparam
  1263       | SOME (_, classparam_syntax) => case classparam_syntax classparam
  1264          of NONE => (snd o dest_name) classparam
  1265           | SOME classparam => classparam;
  1266     fun pr_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs
  1267      of [] => []
  1268       | classbinds => Pretty.enum "," "(" ")" (
  1269           map (fn (v, class) =>
  1270             str (class_name class ^ " " ^ CodeName.lookup_var tyvars v)) classbinds)
  1271           @@ str " => ";
  1272     fun pr_typforall tyvars vs = case map fst vs
  1273      of [] => []
  1274       | vnames => str "forall " :: Pretty.breaks
  1275           (map (str o CodeName.lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
  1276     fun pr_tycoexpr tyvars fxy (tyco, tys) =
  1277       brackify fxy (str tyco :: map (pr_typ tyvars BR) tys)
  1278     and pr_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco
  1279          of NONE => pr_tycoexpr tyvars fxy (deresolve tyco, tys)
  1280           | SOME (i, pr) => pr (pr_typ tyvars) fxy tys)
  1281       | pr_typ tyvars fxy (ITyVar v) = (str o CodeName.lookup_var tyvars) v;
  1282     fun pr_typdecl tyvars (vs, tycoexpr) =
  1283       Pretty.block (pr_typcontext tyvars vs @| pr_tycoexpr tyvars NOBR tycoexpr);
  1284     fun pr_typscheme tyvars (vs, ty) =
  1285       Pretty.block (pr_typforall tyvars vs @ pr_typcontext tyvars vs @| pr_typ tyvars NOBR ty);
  1286     fun pr_term tyvars thm pat vars fxy (IConst c) =
  1287           pr_app tyvars thm pat vars fxy (c, [])
  1288       | pr_term tyvars thm pat vars fxy (t as (t1 `$ t2)) =
  1289           (case CodeThingol.unfold_const_app t
  1290            of SOME app => pr_app tyvars thm pat vars fxy app
  1291             | _ =>
  1292                 brackify fxy [
  1293                   pr_term tyvars thm pat vars NOBR t1,
  1294                   pr_term tyvars thm pat vars BR t2
  1295                 ])
  1296       | pr_term tyvars thm pat vars fxy (IVar v) =
  1297           (str o CodeName.lookup_var vars) v
  1298       | pr_term tyvars thm pat vars fxy (t as _ `|-> _) =
  1299           let
  1300             val (binds, t') = CodeThingol.unfold_abs t;
  1301             fun pr ((v, pat), ty) = pr_bind tyvars thm BR ((SOME v, pat), ty);
  1302             val (ps, vars') = fold_map pr binds vars;
  1303           in brackets (str "\\" :: ps @ str "->" @@ pr_term tyvars thm pat vars' NOBR t') end
  1304       | pr_term tyvars thm pat vars fxy (ICase (cases as (_, t0))) =
  1305           (case CodeThingol.unfold_const_app t0
  1306            of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
  1307                 then pr_case tyvars thm vars fxy cases
  1308                 else pr_app tyvars thm pat vars fxy c_ts
  1309             | NONE => pr_case tyvars thm vars fxy cases)
  1310     and pr_app' tyvars thm pat vars ((c, (_, tys)), ts) = case contr_classparam_typs c
  1311      of [] => (str o deresolve) c :: map (pr_term tyvars thm pat vars BR) ts
  1312       | fingerprint => let
  1313           val ts_fingerprint = ts ~~ curry Library.take (length ts) fingerprint;
  1314           val needs_annotation = forall (fn (_, NONE) => true | (t, SOME _) =>
  1315             (not o CodeThingol.locally_monomorphic) t) ts_fingerprint;
  1316           fun pr_term_anno (t, NONE) _ = pr_term tyvars thm pat vars BR t
  1317             | pr_term_anno (t, SOME _) ty =
  1318                 brackets [pr_term tyvars thm pat vars NOBR t, str "::", pr_typ tyvars NOBR ty];
  1319         in
  1320           if needs_annotation then
  1321             (str o deresolve) c :: map2 pr_term_anno ts_fingerprint (curry Library.take (length ts) tys)
  1322           else (str o deresolve) c :: map (pr_term tyvars thm pat vars BR) ts
  1323         end
  1324     and pr_app tyvars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const is_cons
  1325     and pr_bind tyvars = pr_haskell_bind (pr_term tyvars)
  1326     and pr_case tyvars thm vars fxy (cases as ((_, [_]), _)) =
  1327           let
  1328             val (binds, t) = CodeThingol.unfold_let (ICase cases);
  1329             fun pr ((pat, ty), t) vars =
  1330               vars
  1331               |> pr_bind tyvars thm BR ((NONE, SOME pat), ty)
  1332               |>> (fn p => semicolon [p, str "=", pr_term tyvars thm false vars NOBR t])
  1333             val (ps, vars') = fold_map pr binds vars;
  1334           in
  1335             Pretty.block_enclose (
  1336               str "let {",
  1337               concat [str "}", str "in", pr_term tyvars thm false vars' NOBR t]
  1338             ) ps
  1339           end
  1340       | pr_case tyvars thm vars fxy (((td, ty), bs as _ :: _), _) =
  1341           let
  1342             fun pr (pat, t) =
  1343               let
  1344                 val (p, vars') = pr_bind tyvars thm NOBR ((NONE, SOME pat), ty) vars;
  1345               in semicolon [p, str "->", pr_term tyvars thm false vars' NOBR t] end;
  1346           in
  1347             Pretty.block_enclose (
  1348               concat [str "(case", pr_term tyvars thm false vars NOBR td, str "of", str "{"],
  1349               str "})"
  1350             ) (map pr bs)
  1351           end
  1352       | pr_case tyvars thm vars fxy ((_, []), _) = str "error \"empty case\"";
  1353     fun pr_stmt (name, CodeThingol.Fun ((vs, ty), [])) =
  1354           let
  1355             val tyvars = CodeName.intro_vars (map fst vs) init_syms;
  1356             val n = (length o fst o CodeThingol.unfold_fun) ty;
  1357           in
  1358             Pretty.chunks [
  1359               Pretty.block [
  1360                 (str o suffix " ::" o deresolve_base) name,
  1361                 Pretty.brk 1,
  1362                 pr_typscheme tyvars (vs, ty),
  1363                 str ";"
  1364               ],
  1365               concat (
  1366                 (str o deresolve_base) name
  1367                 :: map str (replicate n "_")
  1368                 @ str "="
  1369                 :: str "error"
  1370                 @@ (str o (fn s => s ^ ";") o ML_Syntax.print_string
  1371                     o NameSpace.base o NameSpace.qualifier) name
  1372               )
  1373             ]
  1374           end
  1375       | pr_stmt (name, CodeThingol.Fun ((vs, ty), eqs)) =
  1376           let
  1377             val tyvars = CodeName.intro_vars (map fst vs) init_syms;
  1378             fun pr_eq ((ts, t), thm) =
  1379               let
  1380                 val consts = map_filter
  1381                   (fn c => if (is_some o syntax_const) c
  1382                     then NONE else (SOME o NameSpace.base o deresolve) c)
  1383                     ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);
  1384                 val vars = init_syms
  1385                   |> CodeName.intro_vars consts
  1386                   |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)
  1387                        (insert (op =)) ts []);
  1388               in
  1389                 semicolon (
  1390                   (str o deresolve_base) name
  1391                   :: map (pr_term tyvars thm true vars BR) ts
  1392                   @ str "="
  1393                   @@ pr_term tyvars thm false vars NOBR t
  1394                 )
  1395               end;
  1396           in
  1397             Pretty.chunks (
  1398               Pretty.block [
  1399                 (str o suffix " ::" o deresolve_base) name,
  1400                 Pretty.brk 1,
  1401                 pr_typscheme tyvars (vs, ty),
  1402                 str ";"
  1403               ]
  1404               :: map pr_eq eqs
  1405             )
  1406           end
  1407       | pr_stmt (name, CodeThingol.Datatype (vs, [])) =
  1408           let
  1409             val tyvars = CodeName.intro_vars (map fst vs) init_syms;
  1410           in
  1411             semicolon [
  1412               str "data",
  1413               pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
  1414             ]
  1415           end
  1416       | pr_stmt (name, CodeThingol.Datatype (vs, [(co, [ty])])) =
  1417           let
  1418             val tyvars = CodeName.intro_vars (map fst vs) init_syms;
  1419           in
  1420             semicolon (
  1421               str "newtype"
  1422               :: pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
  1423               :: str "="
  1424               :: (str o deresolve_base) co
  1425               :: pr_typ tyvars BR ty
  1426               :: (if deriving_show name then [str "deriving (Read, Show)"] else [])
  1427             )
  1428           end
  1429       | pr_stmt (name, CodeThingol.Datatype (vs, co :: cos)) =
  1430           let
  1431             val tyvars = CodeName.intro_vars (map fst vs) init_syms;
  1432             fun pr_co (co, tys) =
  1433               concat (
  1434                 (str o deresolve_base) co
  1435                 :: map (pr_typ tyvars BR) tys
  1436               )
  1437           in
  1438             semicolon (
  1439               str "data"
  1440               :: pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
  1441               :: str "="
  1442               :: pr_co co
  1443               :: map ((fn p => Pretty.block [str "| ", p]) o pr_co) cos
  1444               @ (if deriving_show name then [str "deriving (Read, Show)"] else [])
  1445             )
  1446           end
  1447       | pr_stmt (name, CodeThingol.Class (v, (superclasses, classparams))) =
  1448           let
  1449             val tyvars = CodeName.intro_vars [v] init_syms;
  1450             fun pr_classparam (classparam, ty) =
  1451               semicolon [
  1452                 (str o classparam_name name) classparam,
  1453                 str "::",
  1454                 pr_typ tyvars NOBR ty
  1455               ]
  1456           in
  1457             Pretty.block_enclose (
  1458               Pretty.block [
  1459                 str "class ",
  1460                 Pretty.block (pr_typcontext tyvars [(v, map fst superclasses)]),
  1461                 str (deresolve_base name ^ " " ^ CodeName.lookup_var tyvars v),
  1462                 str " where {"
  1463               ],
  1464               str "};"
  1465             ) (map pr_classparam classparams)
  1466           end
  1467       | pr_stmt (_, CodeThingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =
  1468           let
  1469             val tyvars = CodeName.intro_vars (map fst vs) init_syms;
  1470             fun pr_instdef ((classparam, c_inst), thm) =
  1471               semicolon [
  1472                 (str o classparam_name class) classparam,
  1473                 str "=",
  1474                 pr_app tyvars thm false init_syms NOBR (c_inst, [])
  1475               ];
  1476           in
  1477             Pretty.block_enclose (
  1478               Pretty.block [
  1479                 str "instance ",
  1480                 Pretty.block (pr_typcontext tyvars vs),
  1481                 str (class_name class ^ " "),
  1482                 pr_typ tyvars BR (tyco `%% map (ITyVar o fst) vs),
  1483                 str " where {"
  1484               ],
  1485               str "};"
  1486             ) (map pr_instdef classparam_insts)
  1487           end;
  1488   in pr_stmt end;
  1489 
  1490 fun pretty_haskell_monad c_bind =
  1491   let
  1492     fun pretty pr thm pat vars fxy [(t, _)] =
  1493       let
  1494         val pr_bind = pr_haskell_bind (K (K pr)) thm;
  1495         fun pr_monad (NONE, t) vars =
  1496               (semicolon [pr vars NOBR t], vars)
  1497           | pr_monad (SOME (bind, true), t) vars = vars
  1498               |> pr_bind NOBR bind
  1499               |>> (fn p => semicolon [p, str "<-", pr vars NOBR t])
  1500           | pr_monad (SOME (bind, false), t) vars = vars
  1501               |> pr_bind NOBR bind
  1502               |>> (fn p => semicolon [str "let", p, str "=", pr vars NOBR t]);
  1503         val (binds, t) = implode_monad c_bind t;
  1504         val (ps, vars') = fold_map pr_monad binds vars;
  1505         fun brack p = if fixity BR fxy then Pretty.block [str "(", p, str ")"] else p;
  1506       in (brack o Pretty.block_enclose (str "do {", str "}")) (ps @| pr vars' NOBR t) end;
  1507   in (1, pretty) end;
  1508 
  1509 fun haskell_program_of_program labelled_name module_name module_prefix reserved_names raw_module_alias program =
  1510   let
  1511     val module_alias = if is_some module_name then K module_name else raw_module_alias;
  1512     val reserved_names = Name.make_context reserved_names;
  1513     val mk_name_module = mk_name_module reserved_names module_prefix module_alias program;
  1514     fun add_stmt (name, (stmt, deps)) =
  1515       let
  1516         val (module_name, base) = dest_name name;
  1517         val module_name' = mk_name_module module_name;
  1518         val mk_name_stmt = yield_singleton Name.variants;
  1519         fun add_fun upper (nsp_fun, nsp_typ) =
  1520           let
  1521             val (base', nsp_fun') =
  1522               mk_name_stmt (if upper then first_upper base else base) nsp_fun
  1523           in (base', (nsp_fun', nsp_typ)) end;
  1524         fun add_typ (nsp_fun, nsp_typ) =
  1525           let
  1526             val (base', nsp_typ') = mk_name_stmt (first_upper base) nsp_typ
  1527           in (base', (nsp_fun, nsp_typ')) end;
  1528         val add_name = case stmt
  1529          of CodeThingol.Fun _ => add_fun false
  1530           | CodeThingol.Datatype _ => add_typ
  1531           | CodeThingol.Datatypecons _ => add_fun true
  1532           | CodeThingol.Class _ => add_typ
  1533           | CodeThingol.Classrel _ => pair base
  1534           | CodeThingol.Classparam _ => add_fun false
  1535           | CodeThingol.Classinst _ => pair base;
  1536         fun add_stmt' base' = case stmt
  1537          of CodeThingol.Datatypecons _ =>
  1538               cons (name, (NameSpace.append module_name' base', NONE))
  1539           | CodeThingol.Classrel _ => I
  1540           | CodeThingol.Classparam _ =>
  1541               cons (name, (NameSpace.append module_name' base', NONE))
  1542           | _ => cons (name, (NameSpace.append module_name' base', SOME stmt));
  1543       in
  1544         Symtab.map_default (module_name', ([], ([], (reserved_names, reserved_names))))
  1545               (apfst (fold (insert (op = : string * string -> bool)) deps))
  1546         #> `(fn program => add_name ((snd o snd o the o Symtab.lookup program) module_name'))
  1547         #-> (fn (base', names) =>
  1548               (Symtab.map_entry module_name' o apsnd) (fn (stmts, _) =>
  1549               (add_stmt' base' stmts, names)))
  1550       end;
  1551     val hs_program = fold add_stmt (AList.make (fn name =>
  1552       (Graph.get_node program name, Graph.imm_succs program name))
  1553       (Graph.strong_conn program |> flat)) Symtab.empty;
  1554     fun deresolver name =
  1555       (fst o the o AList.lookup (op =) ((fst o snd o the
  1556         o Symtab.lookup hs_program) ((mk_name_module o fst o dest_name) name))) name
  1557         handle Option => error ("Unknown statement name: " ^ labelled_name name);
  1558   in (deresolver, hs_program) end;
  1559 
  1560 fun serialize_haskell module_prefix raw_module_name string_classes labelled_name
  1561     reserved_names includes raw_module_alias
  1562     syntax_class syntax_tyco syntax_const program cs destination =
  1563   let
  1564     val stmt_names = stmt_names_of_destination destination;
  1565     val module_name = if null stmt_names then raw_module_name else SOME "Code";
  1566     val (deresolver, hs_program) = haskell_program_of_program labelled_name
  1567       module_name module_prefix reserved_names raw_module_alias program;
  1568     val is_cons = CodeThingol.is_cons program;
  1569     val contr_classparam_typs = CodeThingol.contr_classparam_typs program;
  1570     fun deriving_show tyco =
  1571       let
  1572         fun deriv _ "fun" = false
  1573           | deriv tycos tyco = member (op =) tycos tyco orelse
  1574               case try (Graph.get_node program) tyco
  1575                 of SOME (CodeThingol.Datatype (_, cs)) => forall (deriv' (tyco :: tycos))
  1576                     (maps snd cs)
  1577                  | NONE => true
  1578         and deriv' tycos (tyco `%% tys) = deriv tycos tyco
  1579               andalso forall (deriv' tycos) tys
  1580           | deriv' _ (ITyVar _) = true
  1581       in deriv [] tyco end;
  1582     val reserved_names = CodeName.make_vars reserved_names;
  1583     fun pr_stmt qualified = pr_haskell_stmt syntax_class syntax_tyco
  1584       syntax_const labelled_name reserved_names
  1585       (if qualified then deresolver else NameSpace.base o deresolver)
  1586       is_cons contr_classparam_typs
  1587       (if string_classes then deriving_show else K false);
  1588     fun pr_module name content =
  1589       (name, Pretty.chunks [
  1590         str ("module " ^ name ^ " where {"),
  1591         str "",
  1592         content,
  1593         str "",
  1594         str "}"
  1595       ]);
  1596     fun serialize_module1 (module_name', (deps, (stmts, _))) =
  1597       let
  1598         val stmt_names = map fst stmts;
  1599         val deps' = subtract (op =) stmt_names deps
  1600           |> distinct (op =)
  1601           |> map_filter (try deresolver);
  1602         val qualified = is_none module_name andalso
  1603           map deresolver stmt_names @ deps'
  1604           |> map NameSpace.base
  1605           |> has_duplicates (op =);
  1606         val imports = deps'
  1607           |> map NameSpace.qualifier
  1608           |> distinct (op =);
  1609         fun pr_import_include (name, _) = str ("import " ^ name ^ ";");
  1610         val pr_import_module = str o (if qualified
  1611           then prefix "import qualified "
  1612           else prefix "import ") o suffix ";";
  1613         val content = Pretty.chunks (
  1614             map pr_import_include includes
  1615             @ map pr_import_module imports
  1616             @ str ""
  1617             :: separate (str "") (map_filter
  1618               (fn (name, (_, SOME stmt)) => SOME (pr_stmt qualified (name, stmt))
  1619                 | (_, (_, NONE)) => NONE) stmts)
  1620           )
  1621       in pr_module module_name' content end;
  1622     fun serialize_module2 (_, (_, (stmts, _))) = Pretty.chunks (
  1623       separate (str "") (map_filter
  1624         (fn (name, (_, SOME stmt)) => if null stmt_names
  1625               orelse member (op =) stmt_names name
  1626               then SOME (pr_stmt false (name, stmt))
  1627               else NONE
  1628           | (_, (_, NONE)) => NONE) stmts));
  1629     val serialize_module = case destination of String _ => pair "" o serialize_module2
  1630       | _ => serialize_module1;
  1631     fun write_module destination (modlname, content) =
  1632       let
  1633         val filename = case modlname
  1634          of "" => Path.explode "Main.hs"
  1635           | _ => (Path.ext "hs" o Path.explode o implode o separate "/"
  1636                 o NameSpace.explode) modlname;
  1637         val pathname = Path.append destination filename;
  1638         val _ = File.mkdir (Path.dir pathname);
  1639       in File.write pathname (code_of_pretty content) end
  1640     fun output Compile = error ("Haskell: no internal compilation")
  1641       | output Export = K NONE o map (code_writeln o snd)
  1642       | output (File destination) = K NONE o map (write_module destination)
  1643       | output (String _) = SOME o cat_lines o map (code_of_pretty o snd);
  1644   in
  1645     output destination (map (uncurry pr_module) includes
  1646       @ map serialize_module (Symtab.dest hs_program))
  1647   end;
  1648 
  1649 fun isar_seri_haskell module =
  1650   parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name)
  1651     -- Scan.optional (Args.$$$ "string_classes" >> K true) false
  1652     >> (fn (module_prefix, string_classes) =>
  1653       serialize_haskell module_prefix module string_classes));
  1654 
  1655 
  1656 (** optional pretty serialization **)
  1657 
  1658 local
  1659 
  1660 fun ocaml_char c =
  1661   let
  1662     fun chr i =
  1663       let
  1664         val xs = string_of_int i;
  1665         val ys = replicate_string (3 - length (explode xs)) "0";
  1666       in "\\" ^ ys ^ xs end;
  1667     val i = ord c;
  1668     val s = if i < 32 orelse i = 34 orelse i = 39 orelse i = 92 orelse i > 126
  1669       then chr i else c
  1670   in s end;
  1671 
  1672 fun haskell_char c =
  1673   let
  1674     val s = ML_Syntax.print_char c;
  1675   in if s = "'" then "\\'" else s end;
  1676 
  1677 val pretty : (string * {
  1678     pretty_char: string -> string,
  1679     pretty_string: string -> string,
  1680     pretty_numeral: bool -> int -> string,
  1681     pretty_list: Pretty.T list -> Pretty.T,
  1682     infix_cons: int * string
  1683   }) list = [
  1684   ("SML", { pretty_char = prefix "#" o quote o ML_Syntax.print_char,
  1685       pretty_string = quote o translate_string ML_Syntax.print_char,
  1686       pretty_numeral = fn unbounded => fn k =>
  1687         if unbounded then "(" ^ string_of_int k ^ " : IntInf.int)"
  1688         else string_of_int k,
  1689       pretty_list = Pretty.enum "," "[" "]",
  1690       infix_cons = (7, "::")}),
  1691   ("OCaml", { pretty_char = enclose "'" "'" o ocaml_char,
  1692       pretty_string = quote o translate_string ocaml_char,
  1693       pretty_numeral = fn unbounded => fn k => if k >= 0 then
  1694             if unbounded then
  1695               "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
  1696             else string_of_int k
  1697           else
  1698             if unbounded then
  1699               "(Big_int.big_int_of_int " ^ (enclose "(" ")" o prefix "-"
  1700                 o string_of_int o op ~) k ^ ")"
  1701             else (enclose "(" ")" o prefix "-" o string_of_int o op ~) k,
  1702       pretty_list = Pretty.enum ";" "[" "]",
  1703       infix_cons = (6, "::")}),
  1704   ("Haskell", { pretty_char = enclose "'" "'" o haskell_char,
  1705       pretty_string = quote o translate_string haskell_char,
  1706       pretty_numeral = fn unbounded => fn k => if k >= 0 then string_of_int k
  1707           else enclose "(" ")" (signed_string_of_int k),
  1708       pretty_list = Pretty.enum "," "[" "]",
  1709       infix_cons = (5, ":")})
  1710 ];
  1711 
  1712 in
  1713 
  1714 fun pr_pretty target = case AList.lookup (op =) pretty target
  1715  of SOME x => x
  1716   | NONE => error ("Unknown code target language: " ^ quote target);
  1717 
  1718 fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
  1719   brackify_infix (target_fxy, R) fxy [
  1720     pr (INFX (target_fxy, X)) t1,
  1721     str target_cons,
  1722     pr (INFX (target_fxy, R)) t2
  1723   ];
  1724 
  1725 fun pretty_list c_nil c_cons target =
  1726   let
  1727     val pretty_ops = pr_pretty target;
  1728     val mk_list = #pretty_list pretty_ops;
  1729     fun pretty pr thm pat vars fxy [(t1, _), (t2, _)] =
  1730       case Option.map (cons t1) (implode_list c_nil c_cons t2)
  1731        of SOME ts => mk_list (map (pr vars NOBR) ts)
  1732         | NONE => default_list (#infix_cons pretty_ops) (pr vars) fxy t1 t2;
  1733   in (2, pretty) end;
  1734 
  1735 fun pretty_list_string c_nil c_cons c_char c_nibbles target =
  1736   let
  1737     val pretty_ops = pr_pretty target;
  1738     val mk_list = #pretty_list pretty_ops;
  1739     val mk_char = #pretty_char pretty_ops;
  1740     val mk_string = #pretty_string pretty_ops;
  1741     fun pretty pr thm pat vars fxy [(t1, _), (t2, _)] =
  1742       case Option.map (cons t1) (implode_list c_nil c_cons t2)
  1743        of SOME ts => (case implode_string c_char c_nibbles mk_char mk_string ts
  1744            of SOME p => p
  1745             | NONE => mk_list (map (pr vars NOBR) ts))
  1746         | NONE => default_list (#infix_cons pretty_ops) (pr vars) fxy t1 t2;
  1747   in (2, pretty) end;
  1748 
  1749 fun pretty_char c_char c_nibbles target =
  1750   let
  1751     val mk_char = #pretty_char (pr_pretty target);
  1752     fun pretty _ thm _ _ _ [(t1, _), (t2, _)] =
  1753       case decode_char c_nibbles (t1, t2)
  1754        of SOME c => (str o mk_char) c
  1755         | NONE => nerror thm "Illegal character expression";
  1756   in (2, pretty) end;
  1757 
  1758 fun pretty_numeral unbounded negative c_pls c_min c_bit0 c_bit1 target =
  1759   let
  1760     val mk_numeral = #pretty_numeral (pr_pretty target);
  1761     fun pretty _ thm _ _ _ [(t, _)] =
  1762       (str o mk_numeral unbounded o implode_numeral thm negative c_pls c_min c_bit0 c_bit1) t;
  1763   in (1, pretty) end;
  1764 
  1765 fun pretty_message c_char c_nibbles c_nil c_cons target =
  1766   let
  1767     val pretty_ops = pr_pretty target;
  1768     val mk_char = #pretty_char pretty_ops;
  1769     val mk_string = #pretty_string pretty_ops;
  1770     fun pretty _ thm _ _ _ [(t, _)] =
  1771       case implode_list c_nil c_cons t
  1772        of SOME ts => (case implode_string c_char c_nibbles mk_char mk_string ts
  1773            of SOME p => p
  1774             | NONE => nerror thm "Illegal message expression")
  1775         | NONE => nerror thm "Illegal message expression";
  1776   in (1, pretty) end;
  1777 
  1778 fun pretty_imperative_monad_bind bind' return' unit' =
  1779   let
  1780     val dummy_name = "";
  1781     val dummy_type = ITyVar dummy_name;
  1782     val dummy_case_term = IVar dummy_name;
  1783     (*assumption: dummy values are not relevant for serialization*)
  1784     val unitt = IConst (unit', ([], []));
  1785     fun dest_abs ((v, ty) `|-> t, _) = ((v, ty), t)
  1786       | dest_abs (t, ty) =
  1787           let
  1788             val vs = CodeThingol.fold_varnames cons t [];
  1789             val v = Name.variant vs "x";
  1790             val ty' = (hd o fst o CodeThingol.unfold_fun) ty;
  1791           in ((v, ty'), t `$ IVar v) end;
  1792     fun force (t as IConst (c, _) `$ t') = if c = return'
  1793           then t' else t `$ unitt
  1794       | force t = t `$ unitt;
  1795     fun tr_bind' [(t1, _), (t2, ty2)] =
  1796       let
  1797         val ((v, ty), t) = dest_abs (t2, ty2);
  1798       in ICase (((force t1, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end
  1799     and tr_bind'' t = case CodeThingol.unfold_app t
  1800          of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if c = bind'
  1801               then tr_bind' [(x1, ty1), (x2, ty2)]
  1802               else force t
  1803           | _ => force t;
  1804     fun tr_bind ts = (dummy_name, dummy_type)
  1805       `|-> ICase (((IVar dummy_name, dummy_type), [(unitt, tr_bind' ts)]), dummy_case_term);
  1806     fun pretty pr thm pat vars fxy ts = pr vars fxy (tr_bind ts);
  1807   in (2, pretty) end;
  1808 
  1809 end; (*local*)
  1810 
  1811 
  1812 (** serializer use cases **)
  1813 
  1814 (* evaluation *)
  1815 
  1816 fun code_antiq_serializer module [] = serialize_ml (K ()) (K Pretty.chunks) pr_sml_stmt
  1817   (fn SOME s => fn cs => SOME ("let\n" ^ s ^ "\nin fn () => " ^ enclose "(" ")" (commas cs) ^ " end"))
  1818   (SOME "Isabelle_Eval");
  1819 
  1820 fun sml_code_of thy program cs = mount_serializer thy (SOME code_antiq_serializer) target_SML NONE [] program cs (String [])
  1821   |> the;
  1822 
  1823 fun eval eval'' term_of reff thy ct args =
  1824   let
  1825     val _ = if null (term_frees (term_of ct)) then () else error ("Term "
  1826       ^ quote (Syntax.string_of_term_global thy (term_of ct))
  1827       ^ " to be evaluated contains free variables");
  1828     fun eval' program ((vs, ty), t) deps =
  1829       let
  1830         val _ = if CodeThingol.contains_dictvar t then
  1831           error "Term to be evaluated constains free dictionaries" else ();
  1832         val program' = program
  1833           |> Graph.new_node (CodeName.value_name, CodeThingol.Fun (([], ty), [(([], t), Drule.dummy_thm)]))
  1834           |> fold (curry Graph.add_edge CodeName.value_name) deps;
  1835         val value_code = sml_code_of thy program' [CodeName.value_name] ;
  1836         val sml_code = space_implode " " (value_code :: "()" :: map (enclose "(" ")") args);
  1837       in ML_Context.evaluate Output.ml_output false reff sml_code end;
  1838   in eval'' thy (fn t => (t, eval')) ct end;
  1839 
  1840 fun eval_conv reff = eval CodeThingol.eval_conv Thm.term_of reff;
  1841 fun eval_term reff = eval CodeThingol.eval_term I reff;
  1842 
  1843 
  1844 (* instrumentalization by antiquotation *)
  1845 
  1846 val ml_code_antiq = (Scan.state >> Context.theory_of) -- Scan.repeat1 Args.term >> (fn (thy, ts) =>
  1847   let
  1848     val cs = map (CodeUnit.check_const thy) ts;
  1849     val (cs', program) = CodeThingol.consts_program thy cs;
  1850   in sml_code_of thy program cs' ^ " ()" end);
  1851 
  1852 
  1853 (* code presentation *)
  1854 
  1855 fun code_of thy target module_name cs stmt_names =
  1856   let
  1857     val (cs', program) = CodeThingol.consts_program thy cs;
  1858   in
  1859     string stmt_names (serialize thy target (SOME module_name) [] program cs')
  1860   end;
  1861 
  1862 
  1863 (* code generation *)
  1864 
  1865 fun read_const_exprs thy cs =
  1866   let
  1867     val (cs1, cs2) = CodeName.read_const_exprs thy cs;
  1868     val (cs3, program) = CodeThingol.consts_program thy cs2;
  1869     val cs4 = CodeThingol.transitivly_non_empty_funs program (abort_allowed thy);
  1870     val cs5 = map_filter
  1871       (fn (c, c') => if member (op =) cs4 c' then SOME c else NONE) (cs2 ~~ cs3);
  1872   in fold (insert (op =)) cs5 cs1 end;
  1873 
  1874 fun cached_program thy = 
  1875   let
  1876     val program = CodeThingol.cached_program thy;
  1877   in (CodeThingol.transitivly_non_empty_funs program (abort_allowed thy), program) end
  1878 
  1879 fun export_code thy cs seris =
  1880   let
  1881     val (cs', program) = if null cs then cached_program thy
  1882       else CodeThingol.consts_program thy cs;
  1883     fun mk_seri_dest dest = case dest
  1884      of NONE => compile
  1885       | SOME "-" => export
  1886       | SOME f => file (Path.explode f)
  1887     val _ = map (fn (((target, module), dest), args) =>
  1888       (mk_seri_dest dest (serialize thy target module args program cs'))) seris;
  1889   in () end;
  1890 
  1891 fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs) seris;
  1892 
  1893 
  1894 (** serializer data **)
  1895 
  1896 (* infix syntax *)
  1897 
  1898 datatype 'a mixfix =
  1899     Arg of fixity
  1900   | Pretty of Pretty.T;
  1901 
  1902 fun mk_mixfix prep_arg (fixity_this, mfx) =
  1903   let
  1904     fun is_arg (Arg _) = true
  1905       | is_arg _ = false;
  1906     val i = (length o filter is_arg) mfx;
  1907     fun fillin _ [] [] =
  1908           []
  1909       | fillin pr (Arg fxy :: mfx) (a :: args) =
  1910           (pr fxy o prep_arg) a :: fillin pr mfx args
  1911       | fillin pr (Pretty p :: mfx) args =
  1912           p :: fillin pr mfx args;
  1913   in
  1914     (i, fn pr => fn fixity_ctxt => fn args =>
  1915       gen_brackify (fixity fixity_this fixity_ctxt) (fillin pr mfx args))
  1916   end;
  1917 
  1918 fun parse_infix prep_arg (x, i) s =
  1919   let
  1920     val l = case x of L => INFX (i, L) | _ => INFX (i, X);
  1921     val r = case x of R => INFX (i, R) | _ => INFX (i, X);
  1922   in
  1923     mk_mixfix prep_arg (INFX (i, x),
  1924       [Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r])
  1925   end;
  1926 
  1927 
  1928 (* data access *)
  1929 
  1930 local
  1931 
  1932 fun cert_class thy class =
  1933   let
  1934     val _ = AxClass.get_info thy class;
  1935   in class end;
  1936 
  1937 fun read_class thy = cert_class thy o Sign.intern_class thy;
  1938 
  1939 fun cert_tyco thy tyco =
  1940   let
  1941     val _ = if Sign.declared_tyname thy tyco then ()
  1942       else error ("No such type constructor: " ^ quote tyco);
  1943   in tyco end;
  1944 
  1945 fun read_tyco thy = cert_tyco thy o Sign.intern_type thy;
  1946 
  1947 fun gen_add_syntax_class prep_class prep_const target raw_class raw_syn thy =
  1948   let
  1949     val class = prep_class thy raw_class;
  1950     val class' = CodeName.class thy class;
  1951     fun mk_classparam c = case AxClass.class_of_param thy c
  1952      of SOME class'' => if class = class'' then CodeName.const thy c
  1953           else error ("Not a class operation for class " ^ quote class ^ ": " ^ quote c)
  1954       | NONE => error ("Not a class operation: " ^ quote c);
  1955     fun mk_syntax_params raw_params = AList.lookup (op =)
  1956       ((map o apfst) (mk_classparam o prep_const thy) raw_params);
  1957   in case raw_syn
  1958    of SOME (syntax, raw_params) =>
  1959       thy
  1960       |> (map_name_syntax target o apfst o apfst)
  1961            (Symtab.update (class', (syntax, mk_syntax_params raw_params)))
  1962     | NONE =>
  1963       thy
  1964       |> (map_name_syntax target o apfst o apfst)
  1965            (Symtab.delete_safe class')
  1966   end;
  1967 
  1968 fun gen_add_syntax_inst prep_class prep_tyco target (raw_tyco, raw_class) add_del thy =
  1969   let
  1970     val inst = CodeName.instance thy (prep_class thy raw_class, prep_tyco thy raw_tyco);
  1971   in if add_del then
  1972     thy
  1973     |> (map_name_syntax target o apfst o apsnd)
  1974         (Symtab.update (inst, ()))
  1975   else
  1976     thy
  1977     |> (map_name_syntax target o apfst o apsnd)
  1978         (Symtab.delete_safe inst)
  1979   end;
  1980 
  1981 fun gen_add_syntax_tyco prep_tyco target raw_tyco raw_syn thy =
  1982   let
  1983     val tyco = prep_tyco thy raw_tyco;
  1984     val tyco' = if tyco = "fun" then "fun" else CodeName.tyco thy tyco;
  1985     fun check_args (syntax as (n, _)) = if n <> Sign.arity_number thy tyco
  1986       then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
  1987       else syntax
  1988   in case raw_syn
  1989    of SOME syntax =>
  1990       thy
  1991       |> (map_name_syntax target o apsnd o apfst)
  1992            (Symtab.update (tyco', check_args syntax))
  1993    | NONE =>
  1994       thy
  1995       |> (map_name_syntax target o apsnd o apfst)
  1996            (Symtab.delete_safe tyco')
  1997   end;
  1998 
  1999 fun simple_const_syntax x = (Option.map o apsnd)
  2000   (fn pretty => fn pr => fn thm => fn pat => fn vars => pretty (pr vars)) x;
  2001 
  2002 fun gen_add_syntax_const prep_const target raw_c raw_syn thy =
  2003   let
  2004     val c = prep_const thy raw_c;
  2005     val c' = CodeName.const thy c;
  2006     fun check_args (syntax as (n, _)) = if n > CodeUnit.no_args thy c
  2007       then error ("Too many arguments in syntax for constant " ^ quote c)
  2008       else syntax;
  2009   in case raw_syn
  2010    of SOME syntax =>
  2011       thy
  2012       |> (map_name_syntax target o apsnd o apsnd)
  2013            (Symtab.update (c', check_args syntax))
  2014    | NONE =>
  2015       thy
  2016       |> (map_name_syntax target o apsnd o apsnd)
  2017            (Symtab.delete_safe c')
  2018   end;
  2019 
  2020 fun add_reserved target =
  2021   let
  2022     fun add sym syms = if member (op =) syms sym
  2023       then error ("Reserved symbol " ^ quote sym ^ " already declared")
  2024       else insert (op =) sym syms
  2025   in map_reserved target o add end;
  2026 
  2027 fun add_include target =
  2028   let
  2029     fun add (name, SOME content) incls =
  2030           let
  2031             val _ = if Symtab.defined incls name
  2032               then warning ("Overwriting existing include " ^ name)
  2033               else ();
  2034           in Symtab.update (name, str content) incls end
  2035       | add (name, NONE) incls =
  2036           Symtab.delete name incls;
  2037   in map_includes target o add end;
  2038 
  2039 fun add_module_alias target =
  2040   map_module_alias target o Symtab.update o apsnd CodeName.check_modulename;
  2041 
  2042 fun add_monad target raw_c_run raw_c_bind raw_c_return_unit thy =
  2043   let
  2044     val c_run = CodeUnit.read_const thy raw_c_run;
  2045     val c_bind = CodeUnit.read_const thy raw_c_bind;
  2046     val c_bind' = CodeName.const thy c_bind;
  2047     val c_return_unit' = (Option.map o pairself)
  2048       (CodeName.const thy o CodeUnit.read_const thy) raw_c_return_unit;
  2049     val is_haskell = target = target_Haskell;
  2050     val _ = if is_haskell andalso is_some c_return_unit'
  2051       then error ("No unit entry may be given for Haskell monad")
  2052       else ();
  2053     val _ = if not is_haskell andalso is_none c_return_unit'
  2054       then error ("Unit entry must be given for SML/OCaml monad")
  2055       else ();
  2056   in if target = target_Haskell then
  2057     thy
  2058     |> gen_add_syntax_const (K I) target_Haskell c_run
  2059           (SOME (pretty_haskell_monad c_bind'))
  2060     |> gen_add_syntax_const (K I) target_Haskell c_bind
  2061           (simple_const_syntax (SOME (parse_infix fst (L, 1) ">>=")))
  2062   else
  2063     thy
  2064     |> gen_add_syntax_const (K I) target c_bind
  2065           (SOME (pretty_imperative_monad_bind c_bind'
  2066             ((fst o the) c_return_unit') ((snd o the) c_return_unit')))
  2067   end;
  2068 
  2069 fun gen_allow_abort prep_cs raw_c thy =
  2070   let
  2071     val c = prep_cs thy raw_c;
  2072     val c' = CodeName.const thy c;
  2073   in thy |> (CodeTargetData.map o apsnd) (insert (op =) c') end;
  2074 
  2075 fun zip_list (x::xs) f g =
  2076   f
  2077   #-> (fn y =>
  2078     fold_map (fn x => g |-- f >> pair x) xs
  2079     #-> (fn xys => pair ((x, y) :: xys)));
  2080 
  2081 
  2082 (* concrete syntax *)
  2083 
  2084 structure P = OuterParse
  2085 and K = OuterKeyword
  2086 
  2087 fun parse_multi_syntax parse_thing parse_syntax =
  2088   P.and_list1 parse_thing
  2089   #-> (fn things => Scan.repeat1 (P.$$$ "(" |-- P.name --
  2090         (zip_list things parse_syntax (P.$$$ "and")) --| P.$$$ ")"));
  2091 
  2092 val (infixK, infixlK, infixrK) = ("infix", "infixl", "infixr");
  2093 
  2094 fun parse_mixfix prep_arg s =
  2095   let
  2096     val sym_any = Scan.one Symbol.is_regular;
  2097     val parse = Scan.optional ($$ "!" >> K true) false -- Scan.repeat (
  2098          ($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR))
  2099       || ($$ "_" >> K (Arg BR))
  2100       || ($$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length))
  2101       || (Scan.repeat1
  2102            (   $$ "'" |-- sym_any
  2103             || Scan.unless ($$ "_" || $$ "/" || $$ "(" |-- $$ "_" |-- $$ ")")
  2104                  sym_any) >> (Pretty o str o implode)));
  2105   in case Scan.finite Symbol.stopper parse (Symbol.explode s)
  2106    of ((_, p as [_]), []) => mk_mixfix prep_arg (NOBR, p)
  2107     | ((b, p as _ :: _ :: _), []) => mk_mixfix prep_arg (if b then NOBR else BR, p)
  2108     | _ => Scan.!!
  2109         (the_default ("malformed mixfix annotation: " ^ quote s) o snd) Scan.fail ()
  2110   end;
  2111 
  2112 fun parse_syntax prep_arg xs =
  2113   Scan.option ((
  2114       ((P.$$$ infixK  >> K X)
  2115         || (P.$$$ infixlK >> K L)
  2116         || (P.$$$ infixrK >> K R))
  2117         -- P.nat >> parse_infix prep_arg
  2118       || Scan.succeed (parse_mixfix prep_arg))
  2119       -- P.string
  2120       >> (fn (parse, s) => parse s)) xs;
  2121 
  2122 in
  2123 
  2124 val parse_syntax = parse_syntax;
  2125 
  2126 val add_syntax_class = gen_add_syntax_class cert_class (K I);
  2127 val add_syntax_inst = gen_add_syntax_inst cert_class cert_tyco;
  2128 val add_syntax_tyco = gen_add_syntax_tyco cert_tyco;
  2129 val add_syntax_const = gen_add_syntax_const (K I);
  2130 val allow_abort = gen_allow_abort (K I);
  2131 
  2132 val add_syntax_class_cmd = gen_add_syntax_class read_class CodeUnit.read_const;
  2133 val add_syntax_inst_cmd = gen_add_syntax_inst read_class read_tyco;
  2134 val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco;
  2135 val add_syntax_const_cmd = gen_add_syntax_const CodeUnit.read_const;
  2136 val allow_abort_cmd = gen_allow_abort CodeUnit.read_const;
  2137 
  2138 fun add_syntax_tycoP target tyco = parse_syntax I >> add_syntax_tyco_cmd target tyco;
  2139 fun add_syntax_constP target c = parse_syntax fst >> (add_syntax_const_cmd target c o simple_const_syntax);
  2140 
  2141 fun add_undefined target undef target_undefined thy =
  2142   let
  2143     fun pr _ _ _ _ _ _ = str target_undefined;
  2144   in
  2145     thy
  2146     |> add_syntax_const target undef (SOME (~1, pr))
  2147   end;
  2148 
  2149 fun add_pretty_list target nill cons thy =
  2150   let
  2151     val nil' = CodeName.const thy nill;
  2152     val cons' = CodeName.const thy cons;
  2153     val pr = pretty_list nil' cons' target;
  2154   in
  2155     thy
  2156     |> add_syntax_const target cons (SOME pr)
  2157   end;
  2158 
  2159 fun add_pretty_list_string target nill cons charr nibbles thy =
  2160   let
  2161     val nil' = CodeName.const thy nill;
  2162     val cons' = CodeName.const thy cons;
  2163     val charr' = CodeName.const thy charr;
  2164     val nibbles' = map (CodeName.const thy) nibbles;
  2165     val pr = pretty_list_string nil' cons' charr' nibbles' target;
  2166   in
  2167     thy
  2168     |> add_syntax_const target cons (SOME pr)
  2169   end;
  2170 
  2171 fun add_pretty_char target charr nibbles thy =
  2172   let
  2173     val charr' = CodeName.const thy charr;
  2174     val nibbles' = map (CodeName.const thy) nibbles;
  2175     val pr = pretty_char charr' nibbles' target;
  2176   in
  2177     thy
  2178     |> add_syntax_const target charr (SOME pr)
  2179   end;
  2180 
  2181 fun add_pretty_numeral target unbounded negative number_of pls min bit0 bit1 thy =
  2182   let
  2183     val pls' = CodeName.const thy pls;
  2184     val min' = CodeName.const thy min;
  2185     val bit0' = CodeName.const thy bit0;
  2186     val bit1' = CodeName.const thy bit1;
  2187     val pr = pretty_numeral unbounded negative pls' min' bit0' bit1' target;
  2188   in
  2189     thy
  2190     |> add_syntax_const target number_of (SOME pr)
  2191   end;
  2192 
  2193 fun add_pretty_message target charr nibbles nill cons str thy =
  2194   let
  2195     val charr' = CodeName.const thy charr;
  2196     val nibbles' = map (CodeName.const thy) nibbles;
  2197     val nil' = CodeName.const thy nill;
  2198     val cons' = CodeName.const thy cons;
  2199     val pr = pretty_message charr' nibbles' nil' cons' target;
  2200   in
  2201     thy
  2202     |> add_syntax_const target str (SOME pr)
  2203   end;
  2204 
  2205 
  2206 
  2207 (** Isar setup **)
  2208 
  2209 val (inK, module_nameK, fileK) = ("in", "module_name", "file");
  2210 
  2211 fun code_exprP cmd =
  2212   (Scan.repeat P.term
  2213   -- Scan.repeat (P.$$$ inK |-- P.name
  2214      -- Scan.option (P.$$$ module_nameK |-- P.name)
  2215      -- Scan.option (P.$$$ fileK |-- P.name)
  2216      -- Scan.optional (P.$$$ "(" |-- P.arguments --| P.$$$ ")") []
  2217   ) >> (fn (raw_cs, seris) => cmd raw_cs seris));
  2218 
  2219 val _ = List.app OuterKeyword.keyword [infixK, infixlK, infixrK, inK, module_nameK, fileK];
  2220 
  2221 val _ =
  2222   OuterSyntax.command "code_class" "define code syntax for class" K.thy_decl (
  2223     parse_multi_syntax P.xname
  2224       (Scan.option (P.string -- Scan.optional (P.$$$ "where" |-- Scan.repeat1
  2225         (P.term --| (P.$$$ "\<equiv>" || P.$$$ "==") -- P.string)) []))
  2226     >> (Toplevel.theory oo fold) (fn (target, syns) =>
  2227           fold (fn (raw_class, syn) => add_syntax_class_cmd target raw_class syn) syns)
  2228   );
  2229 
  2230 val _ =
  2231   OuterSyntax.command "code_instance" "define code syntax for instance" K.thy_decl (
  2232     parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname)
  2233       ((P.minus >> K true) || Scan.succeed false)
  2234     >> (Toplevel.theory oo fold) (fn (target, syns) =>
  2235           fold (fn (raw_inst, add_del) => add_syntax_inst_cmd target raw_inst add_del) syns)
  2236   );
  2237 
  2238 val _ =
  2239   OuterSyntax.command "code_type" "define code syntax for type constructor" K.thy_decl (
  2240     parse_multi_syntax P.xname (parse_syntax I)
  2241     >> (Toplevel.theory oo fold) (fn (target, syns) =>
  2242           fold (fn (raw_tyco, syn) => add_syntax_tyco_cmd target raw_tyco syn) syns)
  2243   );
  2244 
  2245 val _ =
  2246   OuterSyntax.command "code_const" "define code syntax for constant" K.thy_decl (
  2247     parse_multi_syntax P.term (parse_syntax fst)
  2248     >> (Toplevel.theory oo fold) (fn (target, syns) =>
  2249           fold (fn (raw_const, syn) => add_syntax_const_cmd target raw_const (simple_const_syntax syn)) syns)
  2250   );
  2251 
  2252 val _ =
  2253   OuterSyntax.command "code_monad" "define code syntax for monads" K.thy_decl (
  2254     P.term -- P.term -- ((P.term -- P.term >> SOME) -- Scan.repeat1 P.name
  2255       || Scan.succeed NONE -- Scan.repeat1 P.name)
  2256     >> (fn ((raw_run, raw_bind), (raw_unit_return, targets)) => Toplevel.theory 
  2257           (fold (fn target => add_monad target raw_run raw_bind raw_unit_return) targets))
  2258   );
  2259 
  2260 val _ =
  2261   OuterSyntax.command "code_reserved" "declare words as reserved for target language" K.thy_decl (
  2262     P.name -- Scan.repeat1 P.name
  2263     >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds)
  2264   );
  2265 
  2266 val _ =
  2267   OuterSyntax.command "code_include" "declare piece of code to be included in generated code" K.thy_decl (
  2268     P.name -- P.name -- (P.text >> (fn "-" => NONE | s => SOME s))
  2269     >> (fn ((target, name), content) => (Toplevel.theory o add_include target)
  2270       (name, content))
  2271   );
  2272 
  2273 val _ =
  2274   OuterSyntax.command "code_modulename" "alias module to other name" K.thy_decl (
  2275     P.name -- Scan.repeat1 (P.name -- P.name)
  2276     >> (fn (target, modlnames) => (Toplevel.theory o fold (add_module_alias target)) modlnames)
  2277   );
  2278 
  2279 val _ =
  2280   OuterSyntax.command "code_abort" "permit constant to be implemented as program abort" K.thy_decl (
  2281     Scan.repeat1 P.term >> (Toplevel.theory o fold allow_abort_cmd)
  2282   );
  2283 
  2284 val _ =
  2285   OuterSyntax.command "export_code" "generate executable code for constants"
  2286     K.diag (P.!!! (code_exprP export_code_cmd) >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
  2287 
  2288 fun shell_command thyname cmd = Toplevel.program (fn _ =>
  2289   (use_thy thyname; case Scan.read OuterLex.stopper (P.!!! (code_exprP export_code_cmd)) ((filter OuterLex.is_proper o OuterSyntax.scan) cmd)
  2290    of SOME f => (writeln "Now generating code..."; f (theory thyname))
  2291     | NONE => error ("Bad directive " ^ quote cmd)))
  2292   handle TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
  2293 
  2294 val _ = ML_Antiquote.value "code" ml_code_antiq;
  2295 
  2296 
  2297 (* serializer setup, including serializer defaults *)
  2298 
  2299 val setup =
  2300   add_target (target_SML, isar_seri_sml)
  2301   #> add_target (target_OCaml, isar_seri_ocaml)
  2302   #> add_target (target_Haskell, isar_seri_haskell)
  2303   #> add_syntax_tyco "SML" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
  2304       brackify_infix (1, R) fxy [
  2305         pr_typ (INFX (1, X)) ty1,
  2306         str "->",
  2307         pr_typ (INFX (1, R)) ty2
  2308       ]))
  2309   #> add_syntax_tyco "OCaml" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
  2310       brackify_infix (1, R) fxy [
  2311         pr_typ (INFX (1, X)) ty1,
  2312         str "->",
  2313         pr_typ (INFX (1, R)) ty2
  2314       ]))
  2315   #> add_syntax_tyco "Haskell" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
  2316       brackify_infix (1, R) fxy [
  2317         pr_typ (INFX (1, X)) ty1,
  2318         str "->",
  2319         pr_typ (INFX (1, R)) ty2
  2320       ]))
  2321   #> fold (add_reserved "SML") ML_Syntax.reserved_names
  2322   #> fold (add_reserved "SML")
  2323       ["o" (*dictionary projections use it already*), "Fail", "div", "mod" (*standard infixes*)]
  2324   #> fold (add_reserved "OCaml") [
  2325       "and", "as", "assert", "begin", "class",
  2326       "constraint", "do", "done", "downto", "else", "end", "exception",
  2327       "external", "false", "for", "fun", "function", "functor", "if",
  2328       "in", "include", "inherit", "initializer", "lazy", "let", "match", "method",
  2329       "module", "mutable", "new", "object", "of", "open", "or", "private", "rec",
  2330       "sig", "struct", "then", "to", "true", "try", "type", "val",
  2331       "virtual", "when", "while", "with"
  2332     ]
  2333   #> fold (add_reserved "OCaml") ["failwith", "mod"]
  2334   #> fold (add_reserved "Haskell") [
  2335       "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
  2336       "import", "default", "forall", "let", "in", "class", "qualified", "data",
  2337       "newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
  2338     ]
  2339   #> fold (add_reserved "Haskell") [
  2340       "Prelude", "Main", "Bool", "Maybe", "Either", "Ordering", "Char", "String", "Int",
  2341       "Integer", "Float", "Double", "Rational", "IO", "Eq", "Ord", "Enum", "Bounded",
  2342       "Num", "Real", "Integral", "Fractional", "Floating", "RealFloat", "Monad", "Functor",
  2343       "AlreadyExists", "ArithException", "ArrayException", "AssertionFailed", "AsyncException",
  2344       "BlockedOnDeadMVar", "Deadlock", "Denormal", "DivideByZero", "DotNetException", "DynException",
  2345       "Dynamic", "EOF", "EQ", "EmptyRec", "ErrorCall", "ExitException", "ExitFailure",
  2346       "ExitSuccess", "False", "GT", "HeapOverflow",
  2347       "IOError", "IOException", "IllegalOperation",
  2348       "IndexOutOfBounds", "Just", "Key", "LT", "Left", "LossOfPrecision", "NoMethodError",
  2349       "NoSuchThing", "NonTermination", "Nothing", "Obj", "OtherError", "Overflow",
  2350       "PatternMatchFail", "PermissionDenied", "ProtocolError", "RecConError", "RecSelError",
  2351       "RecUpdError", "ResourceBusy", "ResourceExhausted", "Right", "StackOverflow",
  2352       "ThreadKilled", "True", "TyCon", "TypeRep", "UndefinedElement", "Underflow",
  2353       "UnsupportedOperation", "UserError", "abs", "absReal", "acos", "acosh", "all",
  2354       "and", "any", "appendFile", "asTypeOf", "asciiTab", "asin", "asinh", "atan",
  2355       "atan2", "atanh", "basicIORun", "blockIO", "boundedEnumFrom", "boundedEnumFromThen",
  2356       "boundedEnumFromThenTo", "boundedEnumFromTo", "boundedPred", "boundedSucc", "break",
  2357       "catch", "catchException", "ceiling", "compare", "concat", "concatMap", "const",
  2358       "cos", "cosh", "curry", "cycle", "decodeFloat", "denominator", "div", "divMod",
  2359       "doubleToRatio", "doubleToRational", "drop", "dropWhile", "either", "elem",
  2360       "emptyRec", "encodeFloat", "enumFrom", "enumFromThen", "enumFromThenTo",
  2361       "enumFromTo", "error", "even", "exp", "exponent", "fail", "filter", "flip",
  2362       "floatDigits", "floatProperFraction", "floatRadix", "floatRange", "floatToRational",
  2363       "floor", "fmap", "foldl", "foldl'", "foldl1", "foldr", "foldr1", "fromDouble",
  2364       "fromEnum", "fromEnum_0", "fromInt", "fromInteger", "fromIntegral", "fromObj",
  2365       "fromRational", "fst", "gcd", "getChar", "getContents", "getLine", "head",
  2366       "id", "inRange", "index", "init", "intToRatio", "interact", "ioError", "isAlpha",
  2367       "isAlphaNum", "isDenormalized", "isDigit", "isHexDigit", "isIEEE", "isInfinite",
  2368       "isLower", "isNaN", "isNegativeZero", "isOctDigit", "isSpace", "isUpper", "iterate", "iterate'",
  2369       "last", "lcm", "length", "lex", "lexDigits", "lexLitChar", "lexmatch", "lines", "log",
  2370       "logBase", "lookup", "loop", "map", "mapM", "mapM_", "max", "maxBound", "maximum",
  2371       "maybe", "min", "minBound", "minimum", "mod", "negate", "nonnull", "not", "notElem",
  2372       "null", "numerator", "numericEnumFrom", "numericEnumFromThen", "numericEnumFromThenTo",
  2373       "numericEnumFromTo", "odd", "or", "otherwise", "pi", "pred", 
  2374       "print", "product", "properFraction", "protectEsc", "putChar", "putStr", "putStrLn",
  2375       "quot", "quotRem", "range", "rangeSize", "rationalToDouble", "rationalToFloat",
  2376       "rationalToRealFloat", "read", "readDec", "readField", "readFieldName", "readFile",
  2377       "readFloat", "readHex", "readIO", "readInt", "readList", "readLitChar", "readLn",
  2378       "readOct", "readParen", "readSigned", "reads", "readsPrec", "realFloatToRational",
  2379       "realToFrac", "recip", "reduce", "rem", "repeat", "replicate", "return", "reverse",
  2380       "round", "scaleFloat", "scanl", "scanl1", "scanr", "scanr1", "seq", "sequence",
  2381       "sequence_", "show", "showChar", "showException", "showField", "showList",
  2382       "showLitChar", "showParen", "showString", "shows", "showsPrec", "significand",
  2383       "signum", "signumReal", "sin", "sinh", "snd", "span", "splitAt", "sqrt", "subtract",
  2384       "succ", "sum", "tail", "take", "takeWhile", "takeWhile1", "tan", "tanh", "threadToIOResult",
  2385       "throw", "toEnum", "toInt", "toInteger", "toObj", "toRational", "truncate", "uncurry",
  2386       "undefined", "unlines", "unsafeCoerce", "unsafeIndex", "unsafeRangeSize", "until", "unwords",
  2387       "unzip", "unzip3", "userError", "words", "writeFile", "zip", "zip3", "zipWith", "zipWith3"
  2388     ] (*due to weird handling of ':', we can't do anything else than to import *all* prelude symbols*);
  2389 
  2390 end; (*local*)
  2391 
  2392 end; (*struct*)