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