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