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