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