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