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