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