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