src/Tools/code/code_target.ML
author haftmann
Thu Oct 25 13:52:05 2007 +0200 (2007-10-25)
changeset 25191 e1146aa1e3e3
parent 25147 85463aff6dbe
child 25204 36cf92f63a44
permissions -rw-r--r--
tuned
     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 (map_node modl_explode o Graph.add_edge) (product 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 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_typparms tyvars vs =
  1144       case maps (fn (v, sort) => map (pair v) sort) vs
  1145        of [] => str ""
  1146         | xs => Pretty.block [
  1147             Pretty.enum "," "(" ")" (
  1148               map (fn (v, class) => str
  1149                 (class_name class ^ " " ^ CodeName.lookup_var tyvars v)) xs
  1150             ),
  1151             str " => "
  1152           ];
  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_typscheme_expr tyvars (vs, tycoexpr) =
  1168       Pretty.block (pr_typparms tyvars vs @@ pr_tycoexpr tyvars NOBR tycoexpr);
  1169     fun pr_typscheme tyvars (vs, ty) =
  1170       Pretty.block (pr_typparms tyvars vs @@ pr_typ tyvars NOBR ty);
  1171     fun pr_term lhs vars fxy (IConst c) =
  1172           pr_app lhs vars fxy (c, [])
  1173       | pr_term lhs vars fxy (t as (t1 `$ t2)) =
  1174           (case CodeThingol.unfold_const_app t
  1175            of SOME app => pr_app lhs vars fxy app
  1176             | _ =>
  1177                 brackify fxy [
  1178                   pr_term lhs vars NOBR t1,
  1179                   pr_term lhs vars BR t2
  1180                 ])
  1181       | pr_term lhs vars fxy (IVar v) =
  1182           (str o CodeName.lookup_var vars) v
  1183       | pr_term lhs vars fxy (t as _ `|-> _) =
  1184           let
  1185             val (binds, t') = CodeThingol.unfold_abs t;
  1186             fun pr ((v, pat), ty) = pr_bind BR ((SOME v, pat), ty);
  1187             val (ps, vars') = fold_map pr binds vars;
  1188           in brackets (str "\\" :: ps @ str "->" @@ pr_term lhs vars' NOBR t') end
  1189       | pr_term 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 vars fxy cases
  1193                 else pr_app lhs vars fxy c_ts
  1194             | NONE => pr_case vars fxy cases)
  1195     and pr_app' lhs vars ((c, _), ts) =
  1196       (str o deresolv) c :: map (pr_term lhs vars BR) ts
  1197     and pr_app lhs vars = gen_pr_app pr_app' pr_term const_syntax
  1198       labelled_name is_cons lhs vars
  1199     and pr_bind fxy = pr_bind_haskell pr_term fxy
  1200     and pr_case vars fxy (cases as ((_, [_]), _)) =
  1201           let
  1202             val (binds, t) = CodeThingol.unfold_let (ICase cases);
  1203             fun pr ((pat, ty), t) vars =
  1204               vars
  1205               |> pr_bind BR ((NONE, SOME pat), ty)
  1206               |>> (fn p => semicolon [p, str "=", pr_term false vars NOBR t])
  1207             val (ps, vars') = fold_map pr binds vars;
  1208           in
  1209             Pretty.block_enclose (
  1210               str "let {",
  1211               concat [str "}", str "in", pr_term false vars' NOBR t]
  1212             ) ps
  1213           end
  1214       | pr_case vars fxy (((td, ty), bs as _ :: _), _) =
  1215           let
  1216             fun pr (pat, t) =
  1217               let
  1218                 val (p, vars') = pr_bind NOBR ((NONE, SOME pat), ty) vars;
  1219               in semicolon [p, str "->", pr_term false vars' NOBR t] end;
  1220           in
  1221             Pretty.block_enclose (
  1222               concat [str "(case", pr_term false vars NOBR td, str "of", str "{"],
  1223               str "})"
  1224             ) (map pr bs)
  1225           end
  1226       | pr_case vars fxy ((_, []), _) = str "error \"empty case\"";
  1227     fun pr_def (name, CodeThingol.Fun ((vs, ty), [])) =
  1228           let
  1229             val tyvars = CodeName.intro_vars (map fst vs) init_syms;
  1230             val n = (length o fst o CodeThingol.unfold_fun) ty;
  1231           in
  1232             Pretty.chunks [
  1233               Pretty.block [
  1234                 (str o suffix " ::" o deresolv_here) name,
  1235                 Pretty.brk 1,
  1236                 pr_typscheme tyvars (vs, ty),
  1237                 str ";"
  1238               ],
  1239               concat (
  1240                 (str o deresolv_here) name
  1241                 :: map str (replicate n "_")
  1242                 @ str "="
  1243                 :: str "error"
  1244                 @@ (str o (fn s => s ^ ";") o ML_Syntax.print_string
  1245                     o NameSpace.base o NameSpace.qualifier) name
  1246               )
  1247             ]
  1248           end
  1249       | pr_def (name, CodeThingol.Fun ((vs, ty), eqs)) =
  1250           let
  1251             val tyvars = CodeName.intro_vars (map fst vs) init_syms;
  1252             fun pr_eq ((ts, t), _) =
  1253               let
  1254                 val consts = map_filter
  1255                   (fn c => if (is_some o const_syntax) c
  1256                     then NONE else (SOME o NameSpace.base o deresolv) c)
  1257                     ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);
  1258                 val vars = init_syms
  1259                   |> CodeName.intro_vars consts
  1260                   |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)
  1261                        (insert (op =)) ts []);
  1262               in
  1263                 semicolon (
  1264                   (str o deresolv_here) name
  1265                   :: map (pr_term true vars BR) ts
  1266                   @ str "="
  1267                   @@ pr_term false vars NOBR t
  1268                 )
  1269               end;
  1270           in
  1271             Pretty.chunks (
  1272               Pretty.block [
  1273                 (str o suffix " ::" o deresolv_here) name,
  1274                 Pretty.brk 1,
  1275                 pr_typscheme tyvars (vs, ty),
  1276                 str ";"
  1277               ]
  1278               :: map pr_eq eqs
  1279             )
  1280           end
  1281       | pr_def (name, CodeThingol.Datatype (vs, [])) =
  1282           let
  1283             val tyvars = CodeName.intro_vars (map fst vs) init_syms;
  1284           in
  1285             semicolon [
  1286               str "data",
  1287               pr_typscheme_expr tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs))
  1288             ]
  1289           end
  1290       | pr_def (name, CodeThingol.Datatype (vs, [(co, [ty])])) =
  1291           let
  1292             val tyvars = CodeName.intro_vars (map fst vs) init_syms;
  1293           in
  1294             semicolon (
  1295               str "newtype"
  1296               :: pr_typscheme_expr tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs))
  1297               :: str "="
  1298               :: (str o deresolv_here) co
  1299               :: pr_typ tyvars BR ty
  1300               :: (if deriving_show name then [str "deriving (Read, Show)"] else [])
  1301             )
  1302           end
  1303       | pr_def (name, CodeThingol.Datatype (vs, co :: cos)) =
  1304           let
  1305             val tyvars = CodeName.intro_vars (map fst vs) init_syms;
  1306             fun pr_co (co, tys) =
  1307               concat (
  1308                 (str o deresolv_here) co
  1309                 :: map (pr_typ tyvars BR) tys
  1310               )
  1311           in
  1312             semicolon (
  1313               str "data"
  1314               :: pr_typscheme_expr tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs))
  1315               :: str "="
  1316               :: pr_co co
  1317               :: map ((fn p => Pretty.block [str "| ", p]) o pr_co) cos
  1318               @ (if deriving_show name then [str "deriving (Read, Show)"] else [])
  1319             )
  1320           end
  1321       | pr_def (name, CodeThingol.Class (v, (superclasses, classparams))) =
  1322           let
  1323             val tyvars = CodeName.intro_vars [v] init_syms;
  1324             fun pr_classparam (classparam, ty) =
  1325               semicolon [
  1326                 (str o classparam_name name) classparam,
  1327                 str "::",
  1328                 pr_typ tyvars NOBR ty
  1329               ]
  1330           in
  1331             Pretty.block_enclose (
  1332               Pretty.block [
  1333                 str "class ",
  1334                 pr_typparms tyvars [(v, map fst superclasses)],
  1335                 str (deresolv_here name ^ " " ^ CodeName.lookup_var tyvars v),
  1336                 str " where {"
  1337               ],
  1338               str "};"
  1339             ) (map pr_classparam classparams)
  1340           end
  1341       | pr_def (_, CodeThingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =
  1342           let
  1343             val tyvars = CodeName.intro_vars (map fst vs) init_syms;
  1344             fun pr_instdef ((classparam, c_inst), _) =
  1345               semicolon [
  1346                 (str o classparam_name class) classparam,
  1347                 str "=",
  1348                 pr_app false init_syms NOBR (c_inst, [])
  1349               ];
  1350           in
  1351             Pretty.block_enclose (
  1352               Pretty.block [
  1353                 str "instance ",
  1354                 pr_typparms tyvars vs,
  1355                 str (class_name class ^ " "),
  1356                 pr_typ tyvars BR (tyco `%% map (ITyVar o fst) vs),
  1357                 str " where {"
  1358               ],
  1359               str "};"
  1360             ) (map pr_instdef classparam_insts)
  1361           end;
  1362   in pr_def def end;
  1363 
  1364 fun pretty_haskell_monad c_bind =
  1365   let
  1366     fun pretty pr vars fxy [(t, _)] =
  1367       let
  1368         val pr_bind = pr_bind_haskell (K pr);
  1369         fun pr_monad (NONE, t) vars =
  1370               (semicolon [pr vars NOBR t], vars)
  1371           | pr_monad (SOME (bind, true), t) vars = vars
  1372               |> pr_bind NOBR bind
  1373               |>> (fn p => semicolon [p, str "<-", pr vars NOBR t])
  1374           | pr_monad (SOME (bind, false), t) vars = vars
  1375               |> pr_bind NOBR bind
  1376               |>> (fn p => semicolon [str "let", p, str "=", pr vars NOBR t]);
  1377         val (binds, t) = implode_monad c_bind t;
  1378         val (ps, vars') = fold_map pr_monad binds vars;
  1379         fun brack p = if eval_fxy BR fxy then Pretty.block [str "(", p, str ")"] else p;
  1380       in (brack o Pretty.block_enclose (str "do {", str "}")) (ps @| pr vars' NOBR t) end;
  1381   in (1, pretty) end;
  1382 
  1383 end; (*local*)
  1384 
  1385 fun seri_haskell module_prefix module destination string_classes labelled_name
  1386     reserved_syms includes raw_module_alias
  1387     class_syntax tyco_syntax const_syntax code =
  1388   let
  1389     val _ = Option.map File.check destination;
  1390     val is_cons = CodeThingol.is_cons code;
  1391     val module_alias = if is_some module then K module else raw_module_alias;
  1392     val init_names = Name.make_context reserved_syms;
  1393     val name_modl = mk_modl_name_tab init_names module_prefix module_alias code;
  1394     fun add_def (name, (def, deps)) =
  1395       let
  1396         val (modl, base) = dest_name name;
  1397         val name_def = yield_singleton Name.variants;
  1398         fun add_fun upper (nsp_fun, nsp_typ) =
  1399           let
  1400             val (base', nsp_fun') =
  1401               name_def (if upper then first_upper base else base) nsp_fun
  1402           in (base', (nsp_fun', nsp_typ)) end;
  1403         fun add_typ (nsp_fun, nsp_typ) =
  1404           let
  1405             val (base', nsp_typ') = name_def (first_upper base) nsp_typ
  1406           in (base', (nsp_fun, nsp_typ')) end;
  1407         val add_name =
  1408           case def
  1409            of CodeThingol.Bot => pair base
  1410             | CodeThingol.Fun _ => add_fun false
  1411             | CodeThingol.Datatype _ => add_typ
  1412             | CodeThingol.Datatypecons _ => add_fun true
  1413             | CodeThingol.Class _ => add_typ
  1414             | CodeThingol.Classrel _ => pair base
  1415             | CodeThingol.Classparam _ => add_fun false
  1416             | CodeThingol.Classinst _ => pair base;
  1417         val modlname' = name_modl modl;
  1418         fun add_def base' =
  1419           case def
  1420            of CodeThingol.Bot => I
  1421             | CodeThingol.Datatypecons _ =>
  1422                 cons (name, ((NameSpace.append modlname' base', base'), NONE))
  1423             | CodeThingol.Classrel _ => I
  1424             | CodeThingol.Classparam _ =>
  1425                 cons (name, ((NameSpace.append modlname' base', base'), NONE))
  1426             | _ => cons (name, ((NameSpace.append modlname' base', base'), SOME def));
  1427       in
  1428         Symtab.map_default (modlname', ([], ([], (init_names, init_names))))
  1429               (apfst (fold (insert (op = : string * string -> bool)) deps))
  1430         #> `(fn code => add_name ((snd o snd o the o Symtab.lookup code) modlname'))
  1431         #-> (fn (base', names) =>
  1432               (Symtab.map_entry modlname' o apsnd) (fn (defs, _) =>
  1433               (add_def base' defs, names)))
  1434       end;
  1435     val code' =
  1436       fold add_def (AList.make (fn name =>
  1437         (Graph.get_node code name, Graph.imm_succs code name))
  1438         (Graph.strong_conn code |> flat)) Symtab.empty;
  1439     val init_syms = CodeName.make_vars reserved_syms;
  1440     fun deresolv name =
  1441       (fst o fst o the o AList.lookup (op =) ((fst o snd o the
  1442         o Symtab.lookup code') ((name_modl o fst o dest_name) name))) name
  1443         handle Option => error ("Unknown definition name: " ^ labelled_name name);
  1444     fun deresolv_here name =
  1445       (snd o fst o the o AList.lookup (op =) ((fst o snd o the
  1446         o Symtab.lookup code') ((name_modl o fst o dest_name) name))) name
  1447         handle Option => error ("Unknown definition name: " ^ labelled_name name);
  1448     fun deriving_show tyco =
  1449       let
  1450         fun deriv _ "fun" = false
  1451           | deriv tycos tyco = member (op =) tycos tyco orelse
  1452               case the_default CodeThingol.Bot (try (Graph.get_node code) tyco)
  1453                of CodeThingol.Bot => true
  1454                 | CodeThingol.Datatype (_, cs) => forall (deriv' (tyco :: tycos))
  1455                     (maps snd cs)
  1456         and deriv' tycos (tyco `%% tys) = deriv tycos tyco
  1457               andalso forall (deriv' tycos) tys
  1458           | deriv' _ (ITyVar _) = true
  1459       in deriv [] tyco end;
  1460     fun seri_def qualified = pr_haskell class_syntax tyco_syntax
  1461       const_syntax labelled_name init_syms
  1462       deresolv_here (if qualified then deresolv else deresolv_here) is_cons
  1463       (if string_classes then deriving_show else K false);
  1464     fun write_modulefile (SOME destination) modlname =
  1465           let
  1466             val filename = case modlname
  1467              of "" => Path.explode "Main.hs"
  1468               | _ => (Path.ext "hs" o Path.explode o implode o separate "/"
  1469                     o NameSpace.explode) modlname;
  1470             val pathname = Path.append destination filename;
  1471             val _ = File.mkdir (Path.dir pathname);
  1472           in File.write pathname end
  1473       | write_modulefile NONE _ = PrintMode.setmp [] writeln;
  1474     fun write_module destination (modulename, content) =
  1475       Pretty.chunks [
  1476         str ("module " ^ modulename ^ " where {"),
  1477         str "",
  1478         content,
  1479         str "",
  1480         str "}"
  1481       ]
  1482       |> code_output
  1483       |> write_modulefile destination modulename;
  1484     fun seri_module (modlname', (imports, (defs, _))) =
  1485       let
  1486         val imports' =
  1487           imports
  1488           |> map (name_modl o fst o dest_name)
  1489           |> distinct (op =)
  1490           |> remove (op =) modlname';
  1491         val qualified =
  1492           imports @ map fst defs
  1493           |> distinct (op =)
  1494           |> map_filter (try deresolv)
  1495           |> map NameSpace.base
  1496           |> has_duplicates (op =);
  1497         val mk_import = str o (if qualified
  1498           then prefix "import qualified "
  1499           else prefix "import ") o suffix ";";
  1500         fun import_include (name, _) = str ("import " ^ name ^ ";");
  1501         val content = Pretty.chunks (
  1502             map mk_import imports'
  1503             @ map import_include includes
  1504             @ str ""
  1505             :: separate (str "") (map_filter
  1506               (fn (name, (_, SOME def)) => SOME (seri_def qualified (name, def))
  1507                 | (_, (_, NONE)) => NONE) defs)
  1508           )
  1509       in
  1510         write_module destination (modlname', content)
  1511       end;
  1512   in (
  1513     map (write_module destination) includes;
  1514     Symtab.fold (fn modl => fn () => seri_module modl) code' ()
  1515   ) end;
  1516 
  1517 fun isar_seri_haskell module file =
  1518   let
  1519     val destination = case file
  1520      of NONE => error ("Haskell: no internal compilation")
  1521       | SOME "-" => NONE
  1522       | SOME file => SOME (Path.explode file)
  1523   in
  1524     parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name)
  1525       -- Scan.optional (Args.$$$ "string_classes" >> K true) false
  1526       >> (fn (module_prefix, string_classes) =>
  1527         seri_haskell module_prefix module destination string_classes))
  1528   end;
  1529 
  1530 
  1531 (** diagnosis serializer **)
  1532 
  1533 fun seri_diagnosis labelled_name _ _ _ _ _ _ code =
  1534   let
  1535     val init_names = CodeName.make_vars [];
  1536     fun pr_fun "fun" = SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
  1537           brackify_infix (1, R) fxy [
  1538             pr_typ (INFX (1, X)) ty1,
  1539             str "->",
  1540             pr_typ (INFX (1, R)) ty2
  1541           ])
  1542       | pr_fun _ = NONE
  1543     val pr = pr_haskell (K NONE) pr_fun (K NONE) labelled_name init_names
  1544       I I (K false) (K false);
  1545   in
  1546     []
  1547     |> Graph.fold (fn (name, (def, _)) =>
  1548           case try pr (name, def) of SOME p => cons p | NONE => I) code
  1549     |> Pretty.chunks2
  1550     |> code_output
  1551     |> PrintMode.setmp [] writeln
  1552   end;
  1553 
  1554 
  1555 
  1556 (** theory data **)
  1557 
  1558 datatype syntax_expr = SyntaxExpr of {
  1559   class: (string * (string -> string option)) Symtab.table,
  1560   inst: unit Symtab.table,
  1561   tyco: typ_syntax Symtab.table,
  1562   const: term_syntax Symtab.table
  1563 };
  1564 
  1565 fun mk_syntax_expr ((class, inst), (tyco, const)) =
  1566   SyntaxExpr { class = class, inst = inst, tyco = tyco, const = const };
  1567 fun map_syntax_expr f (SyntaxExpr { class, inst, tyco, const }) =
  1568   mk_syntax_expr (f ((class, inst), (tyco, const)));
  1569 fun merge_syntax_expr (SyntaxExpr { class = class1, inst = inst1, tyco = tyco1, const = const1 },
  1570     SyntaxExpr { class = class2, inst = inst2, tyco = tyco2, const = const2 }) =
  1571   mk_syntax_expr (
  1572     (Symtab.join (K snd) (class1, class2),
  1573        Symtab.join (K snd) (inst1, inst2)),
  1574     (Symtab.join (K snd) (tyco1, tyco2),
  1575        Symtab.join (K snd) (const1, const2))
  1576   );
  1577 
  1578 type serializer =
  1579   string option
  1580   -> string option
  1581   -> Args.T list
  1582   -> (string -> string)
  1583   -> string list
  1584   -> (string * Pretty.T) list
  1585   -> (string -> string option)
  1586   -> (string -> class_syntax option)
  1587   -> (string -> typ_syntax option)
  1588   -> (string -> term_syntax option)
  1589   -> CodeThingol.code -> unit;
  1590 
  1591 datatype target = Target of {
  1592   serial: serial,
  1593   serializer: serializer,
  1594   reserved: string list,
  1595   includes: Pretty.T Symtab.table,
  1596   syntax_expr: syntax_expr,
  1597   module_alias: string Symtab.table
  1598 };
  1599 
  1600 fun mk_target ((serial, serializer), ((reserved, includes), (syntax_expr, module_alias))) =
  1601   Target { serial = serial, serializer = serializer, reserved = reserved, 
  1602     includes = includes, syntax_expr = syntax_expr, module_alias = module_alias };
  1603 fun map_target f ( Target { serial, serializer, reserved, includes, syntax_expr, module_alias } ) =
  1604   mk_target (f ((serial, serializer), ((reserved, includes), (syntax_expr, module_alias))));
  1605 fun merge_target target (Target { serial = serial1, serializer = serializer,
  1606   reserved = reserved1, includes = includes1,
  1607   syntax_expr = syntax_expr1, module_alias = module_alias1 },
  1608     Target { serial = serial2, serializer = _,
  1609       reserved = reserved2, includes = includes2,
  1610       syntax_expr = syntax_expr2, module_alias = module_alias2 }) =
  1611   if serial1 = serial2 then
  1612     mk_target ((serial1, serializer),
  1613       ((merge (op =) (reserved1, reserved2), Symtab.merge (op =) (includes1, includes2)),
  1614         (merge_syntax_expr (syntax_expr1, syntax_expr2),
  1615           Symtab.join (K snd) (module_alias1, module_alias2))
  1616     ))
  1617   else
  1618     error ("Incompatible serializers: " ^ quote target);
  1619 
  1620 structure CodeTargetData = TheoryDataFun
  1621 (
  1622   type T = target Symtab.table * string list;
  1623   val empty = (Symtab.empty, []);
  1624   val copy = I;
  1625   val extend = I;
  1626   fun merge _ ((target1, exc1) : T, (target2, exc2)) =
  1627     (Symtab.join merge_target (target1, target2), Library.merge (op =) (exc1, exc2));
  1628 );
  1629 
  1630 val target_SML = "SML";
  1631 val target_OCaml = "OCaml";
  1632 val target_Haskell = "Haskell";
  1633 val target_diag = "diag";
  1634 
  1635 fun the_serializer (Target { serializer, ... }) = serializer;
  1636 fun the_reserved (Target { reserved, ... }) = reserved;
  1637 fun the_includes (Target { includes, ... }) = includes;
  1638 fun the_syntax_expr (Target { syntax_expr = SyntaxExpr x, ... }) = x;
  1639 fun the_module_alias (Target { module_alias , ... }) = module_alias;
  1640 
  1641 fun assert_serializer thy target =
  1642   case Symtab.lookup (fst (CodeTargetData.get thy)) target
  1643    of SOME data => target
  1644     | NONE => error ("Unknown code target language: " ^ quote target);
  1645 
  1646 fun add_serializer (target, seri) thy =
  1647   let
  1648     val _ = case Symtab.lookup (fst (CodeTargetData.get thy)) target
  1649      of SOME _ => warning ("overwriting existing serializer " ^ quote target)
  1650       | NONE => ();
  1651   in
  1652     thy
  1653     |> (CodeTargetData.map o apfst oo Symtab.map_default)
  1654           (target, mk_target ((serial (), seri), (([], Symtab.empty),
  1655             (mk_syntax_expr ((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)),
  1656               Symtab.empty))))
  1657           ((map_target o apfst o apsnd o K) seri)
  1658   end;
  1659 
  1660 fun map_seri_data target f thy =
  1661   let
  1662     val _ = assert_serializer thy target;
  1663   in
  1664     thy
  1665     |> (CodeTargetData.map o apfst o Symtab.map_entry target o map_target) f
  1666   end;
  1667 
  1668 fun map_adaptions target =
  1669   map_seri_data target o apsnd o apfst;
  1670 fun map_syntax_exprs target =
  1671   map_seri_data target o apsnd o apsnd o apfst o map_syntax_expr;
  1672 fun map_module_alias target =
  1673   map_seri_data target o apsnd o apsnd o apsnd;
  1674 
  1675 fun get_serializer thy target permissive module file args
  1676     = fn cs =>
  1677   let
  1678     val (seris, exc) = CodeTargetData.get thy;
  1679     val data = case Symtab.lookup seris target
  1680      of SOME data => data
  1681       | NONE => error ("Unknown code target language: " ^ quote target);
  1682     val seri = the_serializer data;
  1683     val reserved = the_reserved data;
  1684     val includes = Symtab.dest (the_includes data);
  1685     val alias = the_module_alias data;
  1686     val { class, inst, tyco, const } = the_syntax_expr data;
  1687     val project = if target = target_diag then I
  1688       else CodeThingol.project_code permissive
  1689         (Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const) cs;
  1690     fun check_empty_funs code = case (filter_out (member (op =) exc)
  1691         (CodeThingol.empty_funs code))
  1692      of [] => code
  1693       | names => error ("No defining equations for "
  1694           ^ commas (map (CodeName.labelled_name thy) names));
  1695   in
  1696     project
  1697     #> check_empty_funs
  1698     #> seri module file args (CodeName.labelled_name thy) reserved includes
  1699         (Symtab.lookup alias) (Symtab.lookup class) (Symtab.lookup tyco) (Symtab.lookup const)
  1700   end;
  1701 
  1702 fun eval_invoke thy (ref_name, reff) code (t, ty) args =
  1703   let
  1704     val _ = if CodeThingol.contains_dictvar t then
  1705       error "Term to be evaluated constains free dictionaries" else ();
  1706     val val_args = space_implode " "
  1707       (NameSpace.qualifier CodeName.value_name :: map (enclose "(" ")") args);
  1708     val seri = get_serializer thy "SML" false (SOME "Isabelle_Eval") NONE [];
  1709     val code' = CodeThingol.add_value_stmt (t, ty) code;
  1710     val label = "evaluation in SML";
  1711     fun eval () = (seri (SOME [CodeName.value_name]) code';
  1712       evaluate (ref_name, reff) label Output.ml_output (!eval_verbose) val_args);
  1713   in NAMED_CRITICAL label eval end;
  1714 
  1715 
  1716 
  1717 (** optional pretty serialization **)
  1718 
  1719 local
  1720 
  1721 val pretty : (string * {
  1722     pretty_char: string -> string,
  1723     pretty_string: string -> string,
  1724     pretty_numeral: bool -> int -> string,
  1725     pretty_list: Pretty.T list -> Pretty.T,
  1726     infix_cons: int * string
  1727   }) list = [
  1728   ("SML", { pretty_char = prefix "#" o quote o ML_Syntax.print_char,
  1729       pretty_string = ML_Syntax.print_string,
  1730       pretty_numeral = fn unbounded => fn k =>
  1731         if unbounded then "(" ^ string_of_int k ^ " : IntInf.int)"
  1732         else string_of_int k,
  1733       pretty_list = Pretty.enum "," "[" "]",
  1734       infix_cons = (7, "::")}),
  1735   ("OCaml", { pretty_char = fn c => enclose "'" "'"
  1736         (let val i = ord c
  1737           in if i < 32 orelse i = 39 orelse i = 92
  1738             then prefix "\\" (string_of_int i)
  1739             else c
  1740           end),
  1741       pretty_string = ML_Syntax.print_string,
  1742       pretty_numeral = fn unbounded => fn k => if k >= 0 then
  1743             if unbounded then
  1744               "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
  1745             else string_of_int k
  1746           else
  1747             if unbounded then
  1748               "(Big_int.big_int_of_int " ^ (enclose "(" ")" o prefix "-"
  1749                 o string_of_int o op ~) k ^ ")"
  1750             else (enclose "(" ")" o prefix "-" o string_of_int o op ~) k,
  1751       pretty_list = Pretty.enum ";" "[" "]",
  1752       infix_cons = (6, "::")}),
  1753   ("Haskell", { pretty_char = fn c => enclose "'" "'"
  1754         (let val i = ord c
  1755           in if i < 32 orelse i = 39 orelse i = 92
  1756             then Library.prefix "\\" (string_of_int i)
  1757             else c
  1758           end),
  1759       pretty_string = ML_Syntax.print_string,
  1760       pretty_numeral = fn unbounded => fn k => if k >= 0 then string_of_int k
  1761           else enclose "(" ")" (signed_string_of_int k),
  1762       pretty_list = Pretty.enum "," "[" "]",
  1763       infix_cons = (5, ":")})
  1764 ];
  1765 
  1766 in
  1767 
  1768 fun pr_pretty target = case AList.lookup (op =) pretty target
  1769  of SOME x => x
  1770   | NONE => error ("Unknown code target language: " ^ quote target);
  1771 
  1772 fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
  1773   brackify_infix (target_fxy, R) fxy [
  1774     pr (INFX (target_fxy, X)) t1,
  1775     str target_cons,
  1776     pr (INFX (target_fxy, R)) t2
  1777   ];
  1778 
  1779 fun pretty_list c_nil c_cons target =
  1780   let
  1781     val pretty_ops = pr_pretty target;
  1782     val mk_list = #pretty_list pretty_ops;
  1783     fun pretty pr vars fxy [(t1, _), (t2, _)] =
  1784       case Option.map (cons t1) (implode_list c_nil c_cons t2)
  1785        of SOME ts => mk_list (map (pr vars NOBR) ts)
  1786         | NONE => default_list (#infix_cons pretty_ops) (pr vars) fxy t1 t2;
  1787   in (2, pretty) end;
  1788 
  1789 fun pretty_list_string c_nil c_cons c_char c_nibbles target =
  1790   let
  1791     val pretty_ops = pr_pretty target;
  1792     val mk_list = #pretty_list pretty_ops;
  1793     val mk_char = #pretty_char pretty_ops;
  1794     val mk_string = #pretty_string pretty_ops;
  1795     fun pretty pr vars fxy [(t1, _), (t2, _)] =
  1796       case Option.map (cons t1) (implode_list c_nil c_cons t2)
  1797        of SOME ts => case implode_string c_char c_nibbles mk_char mk_string ts
  1798            of SOME p => p
  1799             | NONE => 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_char c_char c_nibbles target =
  1804   let
  1805     val mk_char = #pretty_char (pr_pretty target);
  1806     fun pretty _ _ _ [(t1, _), (t2, _)] =
  1807       case decode_char c_nibbles (t1, t2)
  1808        of SOME c => (str o mk_char) c
  1809         | NONE => error "Illegal character expression";
  1810   in (2, pretty) end;
  1811 
  1812 fun pretty_numeral unbounded c_bit0 c_bit1 c_pls c_min c_bit target =
  1813   let
  1814     val mk_numeral = #pretty_numeral (pr_pretty target);
  1815     fun pretty _ _ _ [(t, _)] =
  1816       case implode_numeral c_bit0 c_bit1 c_pls c_min c_bit t
  1817        of SOME k => (str o mk_numeral unbounded) k
  1818         | NONE => error "Illegal numeral expression";
  1819   in (1, pretty) end;
  1820 
  1821 fun pretty_message c_char c_nibbles c_nil c_cons target =
  1822   let
  1823     val pretty_ops = pr_pretty target;
  1824     val mk_char = #pretty_char pretty_ops;
  1825     val mk_string = #pretty_string pretty_ops;
  1826     fun pretty pr vars fxy [(t, _)] =
  1827       case implode_list c_nil c_cons t
  1828        of SOME ts => (case implode_string c_char c_nibbles mk_char mk_string ts
  1829            of SOME p => p
  1830             | NONE => error "Illegal message expression")
  1831         | NONE => error "Illegal message expression";
  1832   in (1, pretty) end;
  1833 
  1834 fun pretty_imperative_monad_bind bind' =
  1835   let
  1836     fun dest_abs ((v, ty) `|-> t, _) = ((v, ty), t)
  1837       | dest_abs (t, ty) =
  1838           let
  1839             val vs = CodeThingol.fold_varnames cons t [];
  1840             val v = Name.variant vs "x";
  1841             val ty' = (hd o fst o CodeThingol.unfold_fun) ty;
  1842           in ((v, ty'), t `$ IVar v) end;
  1843     fun tr_bind [(t1, _), (t2, ty2)] =
  1844       let
  1845         val ((v, ty), t) = dest_abs (t2, ty2);
  1846       in ICase (((t1, ty), [(IVar v, tr_bind' t)]), IVar "") end
  1847     and tr_bind' (t as _ `$ _) = (case CodeThingol.unfold_app t
  1848          of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if c = bind'
  1849               then tr_bind [(x1, ty1), (x2, ty2)]
  1850               else t
  1851           | _ => t)
  1852       | tr_bind' t = t;
  1853     fun pretty pr vars fxy ts = pr vars fxy (tr_bind ts);
  1854   in (2, pretty) end;
  1855 
  1856 fun no_bindings x = (Option.map o apsnd)
  1857   (fn pretty => fn pr => fn vars => pretty (pr vars)) x;
  1858 
  1859 end; (*local*)
  1860 
  1861 (** ML and Isar interface **)
  1862 
  1863 local
  1864 
  1865 fun cert_class thy class =
  1866   let
  1867     val _ = AxClass.get_info thy class;
  1868   in class end;
  1869 
  1870 fun read_class thy raw_class =
  1871   let
  1872     val class = Sign.intern_class thy raw_class;
  1873     val _ = AxClass.get_info thy class;
  1874   in class end;
  1875 
  1876 fun cert_tyco thy tyco =
  1877   let
  1878     val _ = if Sign.declared_tyname thy tyco then ()
  1879       else error ("No such type constructor: " ^ quote tyco);
  1880   in tyco end;
  1881 
  1882 fun read_tyco thy raw_tyco =
  1883   let
  1884     val tyco = Sign.intern_type thy raw_tyco;
  1885     val _ = if Sign.declared_tyname thy tyco then ()
  1886       else error ("No such type constructor: " ^ quote raw_tyco);
  1887   in tyco end;
  1888 
  1889 fun gen_add_syntax_class prep_class prep_const target raw_class raw_syn thy =
  1890   let
  1891     val class = prep_class thy raw_class;
  1892     val class' = CodeName.class thy class;
  1893     fun mk_classparam c = case AxClass.class_of_param thy c
  1894      of SOME class'' => if class = class'' then CodeName.const thy c
  1895           else error ("Not a class operation for class " ^ quote class ^ ": " ^ quote c)
  1896       | NONE => error ("Not a class operation: " ^ quote c);
  1897     fun mk_syntax_params raw_params = AList.lookup (op =)
  1898       ((map o apfst) (mk_classparam o prep_const thy) raw_params);
  1899   in case raw_syn
  1900    of SOME (syntax, raw_params) =>
  1901       thy
  1902       |> (map_syntax_exprs target o apfst o apfst)
  1903            (Symtab.update (class', (syntax, mk_syntax_params raw_params)))
  1904     | NONE =>
  1905       thy
  1906       |> (map_syntax_exprs target o apfst o apfst)
  1907            (Symtab.delete_safe class')
  1908   end;
  1909 
  1910 fun gen_add_syntax_inst prep_class prep_tyco target (raw_tyco, raw_class) add_del thy =
  1911   let
  1912     val inst = CodeName.instance thy (prep_class thy raw_class, prep_tyco thy raw_tyco);
  1913   in if add_del then
  1914     thy
  1915     |> (map_syntax_exprs target o apfst o apsnd)
  1916         (Symtab.update (inst, ()))
  1917   else
  1918     thy
  1919     |> (map_syntax_exprs target o apfst o apsnd)
  1920         (Symtab.delete_safe inst)
  1921   end;
  1922 
  1923 fun gen_add_syntax_tyco prep_tyco target raw_tyco raw_syn thy =
  1924   let
  1925     val tyco = prep_tyco thy raw_tyco;
  1926     val tyco' = if tyco = "fun" then "fun" else CodeName.tyco thy tyco;
  1927     fun check_args (syntax as (n, _)) = if n <> Sign.arity_number thy tyco
  1928       then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
  1929       else syntax
  1930   in case raw_syn
  1931    of SOME syntax =>
  1932       thy
  1933       |> (map_syntax_exprs target o apsnd o apfst)
  1934            (Symtab.update (tyco', check_args syntax))
  1935    | NONE =>
  1936       thy
  1937       |> (map_syntax_exprs target o apsnd o apfst)
  1938            (Symtab.delete_safe tyco')
  1939   end;
  1940 
  1941 fun gen_add_syntax_const prep_const target raw_c raw_syn thy =
  1942   let
  1943     val c = prep_const thy raw_c;
  1944     val c' = CodeName.const thy c;
  1945     fun check_args (syntax as (n, _)) = if n > CodeUnit.no_args thy c
  1946       then error ("Too many arguments in syntax for constant " ^ quote c)
  1947       else syntax;
  1948   in case raw_syn
  1949    of SOME syntax =>
  1950       thy
  1951       |> (map_syntax_exprs target o apsnd o apsnd)
  1952            (Symtab.update (c', check_args syntax))
  1953    | NONE =>
  1954       thy
  1955       |> (map_syntax_exprs target o apsnd o apsnd)
  1956            (Symtab.delete_safe c')
  1957   end;
  1958 
  1959 fun add_reserved target =
  1960   let
  1961     fun add sym syms = if member (op =) syms sym
  1962       then error ("Reserved symbol " ^ quote sym ^ " already declared")
  1963       else insert (op =) sym syms
  1964   in map_adaptions target o apfst o add end;
  1965 
  1966 fun add_include target =
  1967   let
  1968     fun add (name, SOME content) incls =
  1969           let
  1970             val _ = if Symtab.defined incls name
  1971               then warning ("Overwriting existing include " ^ name)
  1972               else ();
  1973           in Symtab.update (name, str content) incls end
  1974       | add (name, NONE) incls =
  1975           Symtab.delete name incls;
  1976   in map_adaptions target o apsnd o add end;
  1977 
  1978 fun add_modl_alias target =
  1979   map_module_alias target o Symtab.update o apsnd CodeName.check_modulename;
  1980 
  1981 fun add_monad target c_run c_bind thy =
  1982   let
  1983     val c_run' = CodeUnit.read_const thy c_run;
  1984     val c_bind' = CodeUnit.read_const thy c_bind;
  1985     val c_bind'' = CodeName.const thy c_bind';
  1986   in if target = target_Haskell then
  1987     thy
  1988     |> gen_add_syntax_const (K I) target_Haskell c_run'
  1989           (SOME (pretty_haskell_monad c_bind''))
  1990     |> gen_add_syntax_const (K I) target_Haskell c_bind'
  1991           (no_bindings (SOME (parse_infix fst (L, 1) ">>=")))
  1992   else
  1993     thy
  1994     |> gen_add_syntax_const (K I) target c_bind'
  1995           (SOME (pretty_imperative_monad_bind c_bind''))
  1996   end;
  1997 
  1998 fun gen_allow_exception prep_cs raw_c thy =
  1999   let
  2000     val c = prep_cs thy raw_c;
  2001     val c' = CodeName.const thy c;
  2002   in thy |> (CodeTargetData.map o apsnd) (insert (op =) c') end;
  2003 
  2004 fun zip_list (x::xs) f g =
  2005   f
  2006   #-> (fn y =>
  2007     fold_map (fn x => g |-- f >> pair x) xs
  2008     #-> (fn xys => pair ((x, y) :: xys)));
  2009 
  2010 structure P = OuterParse
  2011 and K = OuterKeyword
  2012 
  2013 fun parse_multi_syntax parse_thing parse_syntax =
  2014   P.and_list1 parse_thing
  2015   #-> (fn things => Scan.repeat1 (P.$$$ "(" |-- P.name --
  2016         (zip_list things parse_syntax (P.$$$ "and")) --| P.$$$ ")"));
  2017 
  2018 val (infixK, infixlK, infixrK) = ("infix", "infixl", "infixr");
  2019 
  2020 fun parse_syntax prep_arg xs =
  2021   Scan.option ((
  2022       ((P.$$$ infixK  >> K X)
  2023         || (P.$$$ infixlK >> K L)
  2024         || (P.$$$ infixrK >> K R))
  2025         -- P.nat >> parse_infix prep_arg
  2026       || Scan.succeed (parse_mixfix prep_arg))
  2027       -- P.string
  2028       >> (fn (parse, s) => parse s)) xs;
  2029 
  2030 in
  2031 
  2032 val parse_syntax = parse_syntax;
  2033 
  2034 val add_syntax_class = gen_add_syntax_class cert_class (K I);
  2035 val add_syntax_inst = gen_add_syntax_inst cert_class cert_tyco;
  2036 val add_syntax_tyco = gen_add_syntax_tyco cert_tyco;
  2037 val add_syntax_const = gen_add_syntax_const (K I);
  2038 val allow_exception = gen_allow_exception (K I);
  2039 
  2040 val add_syntax_class_cmd = gen_add_syntax_class read_class CodeUnit.read_const;
  2041 val add_syntax_inst_cmd = gen_add_syntax_inst read_class read_tyco;
  2042 val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco;
  2043 val add_syntax_const_cmd = gen_add_syntax_const CodeUnit.read_const;
  2044 val allow_exception_cmd = gen_allow_exception CodeUnit.read_const;
  2045 
  2046 fun add_syntax_tycoP target tyco = parse_syntax I >> add_syntax_tyco_cmd target tyco;
  2047 fun add_syntax_constP target c = parse_syntax fst >> (add_syntax_const_cmd target c o no_bindings);
  2048 
  2049 fun add_undefined target undef target_undefined thy =
  2050   let
  2051     fun pr _ _ _ _ = str target_undefined;
  2052   in
  2053     thy
  2054     |> add_syntax_const target undef (SOME (~1, pr))
  2055   end;
  2056 
  2057 fun add_pretty_list target nill cons thy =
  2058   let
  2059     val nil' = CodeName.const thy nill;
  2060     val cons' = CodeName.const thy cons;
  2061     val pr = pretty_list nil' cons' target;
  2062   in
  2063     thy
  2064     |> add_syntax_const target cons (SOME pr)
  2065   end;
  2066 
  2067 fun add_pretty_list_string target nill cons charr nibbles thy =
  2068   let
  2069     val nil' = CodeName.const thy nill;
  2070     val cons' = CodeName.const thy cons;
  2071     val charr' = CodeName.const thy charr;
  2072     val nibbles' = map (CodeName.const thy) nibbles;
  2073     val pr = pretty_list_string nil' cons' charr' nibbles' target;
  2074   in
  2075     thy
  2076     |> add_syntax_const target cons (SOME pr)
  2077   end;
  2078 
  2079 fun add_pretty_char target charr nibbles thy =
  2080   let
  2081     val charr' = CodeName.const thy charr;
  2082     val nibbles' = map (CodeName.const thy) nibbles;
  2083     val pr = pretty_char charr' nibbles' target;
  2084   in
  2085     thy
  2086     |> add_syntax_const target charr (SOME pr)
  2087   end;
  2088 
  2089 fun add_pretty_numeral target unbounded number_of b0 b1 pls min bit thy =
  2090   let
  2091     val b0' = CodeName.const thy b0;
  2092     val b1' = CodeName.const thy b1;
  2093     val pls' = CodeName.const thy pls;
  2094     val min' = CodeName.const thy min;
  2095     val bit' = CodeName.const thy bit;
  2096     val pr = pretty_numeral unbounded b0' b1' pls' min' bit' target;
  2097   in
  2098     thy
  2099     |> add_syntax_const target number_of (SOME pr)
  2100   end;
  2101 
  2102 fun add_pretty_message target charr nibbles nill cons str thy =
  2103   let
  2104     val charr' = CodeName.const thy charr;
  2105     val nibbles' = map (CodeName.const thy) nibbles;
  2106     val nil' = CodeName.const thy nill;
  2107     val cons' = CodeName.const thy cons;
  2108     val pr = pretty_message charr' nibbles' nil' cons' target;
  2109   in
  2110     thy
  2111     |> add_syntax_const target str (SOME pr)
  2112   end;
  2113 
  2114 
  2115 val _ = OuterSyntax.keywords [infixK, infixlK, infixrK];
  2116 
  2117 val _ =
  2118   OuterSyntax.command "code_class" "define code syntax for class" K.thy_decl (
  2119     parse_multi_syntax P.xname
  2120       (Scan.option (P.string -- Scan.optional (P.$$$ "where" |-- Scan.repeat1
  2121         (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.string)) []))
  2122     >> (Toplevel.theory oo fold) (fn (target, syns) =>
  2123           fold (fn (raw_class, syn) => add_syntax_class_cmd target raw_class syn) syns)
  2124   );
  2125 
  2126 val _ =
  2127   OuterSyntax.command "code_instance" "define code syntax for instance" K.thy_decl (
  2128     parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname)
  2129       ((P.minus >> K true) || Scan.succeed false)
  2130     >> (Toplevel.theory oo fold) (fn (target, syns) =>
  2131           fold (fn (raw_inst, add_del) => add_syntax_inst_cmd target raw_inst add_del) syns)
  2132   );
  2133 
  2134 val _ =
  2135   OuterSyntax.command "code_type" "define code syntax for type constructor" K.thy_decl (
  2136     parse_multi_syntax P.xname (parse_syntax I)
  2137     >> (Toplevel.theory oo fold) (fn (target, syns) =>
  2138           fold (fn (raw_tyco, syn) => add_syntax_tyco_cmd target raw_tyco syn) syns)
  2139   );
  2140 
  2141 val _ =
  2142   OuterSyntax.command "code_const" "define code syntax for constant" K.thy_decl (
  2143     parse_multi_syntax P.term (parse_syntax fst)
  2144     >> (Toplevel.theory oo fold) (fn (target, syns) =>
  2145           fold (fn (raw_const, syn) => add_syntax_const_cmd target raw_const (no_bindings syn)) syns)
  2146   );
  2147 
  2148 val _ =
  2149   OuterSyntax.command "code_monad" "define code syntax for monads" K.thy_decl (
  2150     P.term -- P.term -- Scan.repeat1 P.name
  2151     >> (fn ((raw_run, raw_bind), targets) => Toplevel.theory 
  2152           (fold (fn target => add_monad target raw_run raw_bind) targets))
  2153   );
  2154 
  2155 val _ =
  2156   OuterSyntax.command "code_reserved" "declare words as reserved for target language" K.thy_decl (
  2157     P.name -- Scan.repeat1 P.name
  2158     >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds)
  2159   );
  2160 
  2161 val _ =
  2162   OuterSyntax.command "code_include" "declare piece of code to be included in generated code" K.thy_decl (
  2163     P.name -- P.name -- (P.text >> (fn "-" => NONE | s => SOME s))
  2164     >> (fn ((target, name), content) => (Toplevel.theory o add_include target)
  2165       (name, content))
  2166   );
  2167 
  2168 val _ =
  2169   OuterSyntax.command "code_modulename" "alias module to other name" K.thy_decl (
  2170     P.name -- Scan.repeat1 (P.name -- P.name)
  2171     >> (fn (target, modlnames) => (Toplevel.theory o fold (add_modl_alias target)) modlnames)
  2172   );
  2173 
  2174 val _ =
  2175   OuterSyntax.command "code_exception" "permit exceptions for constant" K.thy_decl (
  2176     Scan.repeat1 P.term >> (Toplevel.theory o fold allow_exception_cmd)
  2177   );
  2178 
  2179 
  2180 (*including serializer defaults*)
  2181 val setup =
  2182   add_serializer (target_SML, isar_seri_sml)
  2183   #> add_serializer (target_OCaml, isar_seri_ocaml)
  2184   #> add_serializer (target_Haskell, isar_seri_haskell)
  2185   #> add_serializer (target_diag, fn _ => fn _=> fn _ => seri_diagnosis)
  2186   #> add_syntax_tyco "SML" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
  2187       (gen_brackify (case fxy of NOBR => false | _ => eval_fxy (INFX (1, R)) fxy) o Pretty.breaks) [
  2188         pr_typ (INFX (1, X)) ty1,
  2189         str "->",
  2190         pr_typ (INFX (1, R)) ty2
  2191       ]))
  2192   #> add_syntax_tyco "OCaml" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
  2193       (gen_brackify (case fxy of NOBR => false | _ => eval_fxy (INFX (1, R)) fxy) o Pretty.breaks) [
  2194         pr_typ (INFX (1, X)) ty1,
  2195         str "->",
  2196         pr_typ (INFX (1, R)) ty2
  2197       ]))
  2198   #> add_syntax_tyco "Haskell" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
  2199       brackify_infix (1, R) fxy [
  2200         pr_typ (INFX (1, X)) ty1,
  2201         str "->",
  2202         pr_typ (INFX (1, R)) ty2
  2203       ]))
  2204   #> fold (add_reserved "SML") ML_Syntax.reserved_names
  2205   #> fold (add_reserved "SML")
  2206       ["o" (*dictionary projections use it already*), "Fail", "div", "mod" (*standard infixes*)]
  2207   #> fold (add_reserved "OCaml") [
  2208       "and", "as", "assert", "begin", "class",
  2209       "constraint", "do", "done", "downto", "else", "end", "exception",
  2210       "external", "false", "for", "fun", "function", "functor", "if",
  2211       "in", "include", "inherit", "initializer", "lazy", "let", "match", "method",
  2212       "module", "mutable", "new", "object", "of", "open", "or", "private", "rec",
  2213       "sig", "struct", "then", "to", "true", "try", "type", "val",
  2214       "virtual", "when", "while", "with"
  2215     ]
  2216   #> fold (add_reserved "OCaml") ["failwith", "mod"]
  2217   #> fold (add_reserved "Haskell") [
  2218       "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
  2219       "import", "default", "forall", "let", "in", "class", "qualified", "data",
  2220       "newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
  2221     ]
  2222   #> fold (add_reserved "Haskell") [
  2223       "Prelude", "Main", "Bool", "Maybe", "Either", "Ordering", "Char", "String", "Int",
  2224       "Integer", "Float", "Double", "Rational", "IO", "Eq", "Ord", "Enum", "Bounded",
  2225       "Num", "Real", "Integral", "Fractional", "Floating", "RealFloat", "Monad", "Functor",
  2226       "AlreadyExists", "ArithException", "ArrayException", "AssertionFailed", "AsyncException",
  2227       "BlockedOnDeadMVar", "Deadlock", "Denormal", "DivideByZero", "DotNetException", "DynException",
  2228       "Dynamic", "EOF", "EQ", "EmptyRec", "ErrorCall", "ExitException", "ExitFailure",
  2229       "ExitSuccess", "False", "GT", "HeapOverflow",
  2230       "IOError", "IOException", "IllegalOperation",
  2231       "IndexOutOfBounds", "Just", "Key", "LT", "Left", "LossOfPrecision", "NoMethodError",
  2232       "NoSuchThing", "NonTermination", "Nothing", "Obj", "OtherError", "Overflow",
  2233       "PatternMatchFail", "PermissionDenied", "ProtocolError", "RecConError", "RecSelError",
  2234       "RecUpdError", "ResourceBusy", "ResourceExhausted", "Right", "StackOverflow",
  2235       "ThreadKilled", "True", "TyCon", "TypeRep", "UndefinedElement", "Underflow",
  2236       "UnsupportedOperation", "UserError", "abs", "absReal", "acos", "acosh", "all",
  2237       "and", "any", "appendFile", "asTypeOf", "asciiTab", "asin", "asinh", "atan",
  2238       "atan2", "atanh", "basicIORun", "blockIO", "boundedEnumFrom", "boundedEnumFromThen",
  2239       "boundedEnumFromThenTo", "boundedEnumFromTo", "boundedPred", "boundedSucc", "break",
  2240       "catch", "catchException", "ceiling", "compare", "concat", "concatMap", "const",
  2241       "cos", "cosh", "curry", "cycle", "decodeFloat", "denominator", "div", "divMod",
  2242       "doubleToRatio", "doubleToRational", "drop", "dropWhile", "either", "elem",
  2243       "emptyRec", "encodeFloat", "enumFrom", "enumFromThen", "enumFromThenTo",
  2244       "enumFromTo", "error", "even", "exp", "exponent", "fail", "filter", "flip",
  2245       "floatDigits", "floatProperFraction", "floatRadix", "floatRange", "floatToRational",
  2246       "floor", "fmap", "foldl", "foldl'", "foldl1", "foldr", "foldr1", "fromDouble",
  2247       "fromEnum", "fromEnum_0", "fromInt", "fromInteger", "fromIntegral", "fromObj",
  2248       "fromRational", "fst", "gcd", "getChar", "getContents", "getLine", "head",
  2249       "id", "inRange", "index", "init", "intToRatio", "interact", "ioError", "isAlpha",
  2250       "isAlphaNum", "isDenormalized", "isDigit", "isHexDigit", "isIEEE", "isInfinite",
  2251       "isLower", "isNaN", "isNegativeZero", "isOctDigit", "isSpace", "isUpper", "iterate", "iterate'",
  2252       "last", "lcm", "length", "lex", "lexDigits", "lexLitChar", "lexmatch", "lines", "log",
  2253       "logBase", "lookup", "loop", "map", "mapM", "mapM_", "max", "maxBound", "maximum",
  2254       "maybe", "min", "minBound", "minimum", "mod", "negate", "nonnull", "not", "notElem",
  2255       "null", "numerator", "numericEnumFrom", "numericEnumFromThen", "numericEnumFromThenTo",
  2256       "numericEnumFromTo", "odd", "or", "otherwise", "pi", "pred", 
  2257       "print", "product", "properFraction", "protectEsc", "putChar", "putStr", "putStrLn",
  2258       "quot", "quotRem", "range", "rangeSize", "rationalToDouble", "rationalToFloat",
  2259       "rationalToRealFloat", "read", "readDec", "readField", "readFieldName", "readFile",
  2260       "readFloat", "readHex", "readIO", "readInt", "readList", "readLitChar", "readLn",
  2261       "readOct", "readParen", "readSigned", "reads", "readsPrec", "realFloatToRational",
  2262       "realToFrac", "recip", "reduce", "rem", "repeat", "replicate", "return", "reverse",
  2263       "round", "scaleFloat", "scanl", "scanl1", "scanr", "scanr1", "seq", "sequence",
  2264       "sequence_", "show", "showChar", "showException", "showField", "showList",
  2265       "showLitChar", "showParen", "showString", "shows", "showsPrec", "significand",
  2266       "signum", "signumReal", "sin", "sinh", "snd", "span", "splitAt", "sqrt", "subtract",
  2267       "succ", "sum", "tail", "take", "takeWhile", "takeWhile1", "tan", "tanh", "threadToIOResult",
  2268       "throw", "toEnum", "toInt", "toInteger", "toObj", "toRational", "truncate", "uncurry",
  2269       "undefined", "unlines", "unsafeCoerce", "unsafeIndex", "unsafeRangeSize", "until", "unwords",
  2270       "unzip", "unzip3", "userError", "words", "writeFile", "zip", "zip3", "zipWith", "zipWith3"
  2271     ] (*due to weird handling of ':', we can't do anything else than to import *all* prelude symbols*);
  2272 
  2273 end; (*local*)
  2274 
  2275 end; (*struct*)