src/Tools/code/code_target.ML
author wenzelm
Tue Sep 18 16:08:00 2007 +0200 (2007-09-18)
changeset 24630 351a308ab58d
parent 24621 97d403d9ab54
child 24634 38db11874724
permissions -rw-r--r--
simplified type int (eliminated IntInf.int, integer);
     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 0
   240           else if c = c_min then SOME ~1
   241           else NONE
   242       | dest_numeral (IConst (c, _) `$ t1 `$ t2) =
   243           if c = c_bit then case (dest_numeral t1, dest_bit t2)
   244            of (SOME n, SOME b) => SOME (2 * n + b)
   245             | _ => NONE
   246           else NONE
   247       | dest_numeral _ = NONE;
   248   in dest_numeral end;
   249 
   250 fun implode_monad c_mbind c_kbind t =
   251   let
   252     fun dest_monad (IConst (c, _) `$ t1 `$ t2) =
   253           if c = c_mbind
   254             then case CodeThingol.split_abs t2
   255              of SOME (((v, pat), ty), t') => SOME ((SOME (((SOME v, pat), ty), true), t1), t')
   256               | NONE => NONE
   257           else if c = c_kbind
   258             then SOME ((NONE, t1), t2)
   259             else NONE
   260       | dest_monad t = case CodeThingol.split_let t
   261            of SOME (((pat, ty), tbind), t') => SOME ((SOME (((NONE, SOME pat), ty), false), tbind), t')
   262             | NONE => NONE;
   263   in CodeThingol.unfoldr dest_monad t end;
   264 
   265 
   266 (** name auxiliary **)
   267 
   268 val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
   269 val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
   270 
   271 val dest_name =
   272   apfst NameSpace.implode o split_last o fst o split_last o NameSpace.explode;
   273 
   274 fun mk_modl_name_tab init_names prefix module_alias code =
   275   let
   276     fun nsp_map f = NameSpace.explode #> map f #> NameSpace.implode;
   277     fun mk_alias name =
   278      case module_alias name
   279       of SOME name' => name'
   280        | NONE => nsp_map (fn name => (the_single o fst)
   281             (Name.variants [name] init_names)) name;
   282     fun mk_prefix name =
   283       case prefix
   284        of SOME prefix => NameSpace.append prefix name
   285         | NONE => name;
   286     val tab =
   287       Symtab.empty
   288       |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))
   289            o fst o dest_name o fst)
   290              code
   291   in fn name => (the o Symtab.lookup tab) name end;
   292 
   293 
   294 
   295 (** SML/OCaml serializer **)
   296 
   297 datatype ml_def =
   298     MLFuns of (string * (typscheme * (iterm list * iterm) list)) list
   299   | MLDatas of (string * ((vname * sort) list * (string * itype list) list)) list
   300   | MLClass of string * ((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 -> 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 "(" ^ string_of_int k ^ " : int)"
  1642         else string_of_int 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 >= 0 then
  1653             if unbounded then
  1654               "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
  1655             else string_of_int k
  1656           else
  1657             if unbounded then
  1658               "(Big_int.big_int_of_int " ^ (enclose "(" ")" o prefix "-"
  1659                 o string_of_int o op ~) k ^ ")"
  1660             else (enclose "(" ")" o prefix "-" o string_of_int 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 >= 0 then string_of_int k
  1671           else enclose "(" ")" (signed_string_of_int k),
  1672       pretty_list = Pretty.enum "," "[" "]",
  1673       infix_cons = (5, ":")})
  1674 ];
  1675 
  1676 in
  1677 
  1678 fun pr_pretty target = case AList.lookup (op =) pretty target
  1679  of SOME x => x
  1680   | NONE => error ("Unknown code target language: " ^ quote target);
  1681 
  1682 fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
  1683   brackify_infix (target_fxy, R) fxy [
  1684     pr (INFX (target_fxy, X)) t1,
  1685     str target_cons,
  1686     pr (INFX (target_fxy, R)) t2
  1687   ];
  1688 
  1689 fun pretty_list c_nil c_cons target =
  1690   let
  1691     val pretty_ops = pr_pretty target;
  1692     val mk_list = #pretty_list pretty_ops;
  1693     fun pretty pr vars fxy [(t1, _), (t2, _)] =
  1694       case Option.map (cons t1) (implode_list c_nil c_cons t2)
  1695        of SOME ts => mk_list (map (pr vars NOBR) ts)
  1696         | NONE => default_list (#infix_cons pretty_ops) (pr vars) fxy t1 t2;
  1697   in (2, pretty) end;
  1698 
  1699 fun pretty_list_string c_nil c_cons c_char c_nibbles target =
  1700   let
  1701     val pretty_ops = pr_pretty target;
  1702     val mk_list = #pretty_list pretty_ops;
  1703     val mk_char = #pretty_char pretty_ops;
  1704     val mk_string = #pretty_string pretty_ops;
  1705     fun pretty pr vars fxy [(t1, _), (t2, _)] =
  1706       case Option.map (cons t1) (implode_list c_nil c_cons t2)
  1707        of SOME ts => case implode_string c_char c_nibbles mk_char mk_string ts
  1708            of SOME p => p
  1709             | NONE => mk_list (map (pr vars NOBR) ts)
  1710         | NONE => default_list (#infix_cons pretty_ops) (pr vars) fxy t1 t2;
  1711   in (2, pretty) end;
  1712 
  1713 fun pretty_char c_char c_nibbles target =
  1714   let
  1715     val mk_char = #pretty_char (pr_pretty target);
  1716     fun pretty _ _ _ [(t1, _), (t2, _)] =
  1717       case decode_char c_nibbles (t1, t2)
  1718        of SOME c => (str o mk_char) c
  1719         | NONE => error "Illegal character expression";
  1720   in (2, pretty) end;
  1721 
  1722 fun pretty_numeral unbounded c_bit0 c_bit1 c_pls c_min c_bit target =
  1723   let
  1724     val mk_numeral = #pretty_numeral (pr_pretty target);
  1725     fun pretty _ _ _ [(t, _)] =
  1726       case implode_numeral c_bit0 c_bit1 c_pls c_min c_bit t
  1727        of SOME k => (str o mk_numeral unbounded) k
  1728         | NONE => error "Illegal numeral expression";
  1729   in (1, pretty) end;
  1730 
  1731 fun pretty_ml_string c_char c_nibbles c_nil c_cons target =
  1732   let
  1733     val pretty_ops = pr_pretty target;
  1734     val mk_char = #pretty_char pretty_ops;
  1735     val mk_string = #pretty_string pretty_ops;
  1736     fun pretty pr vars fxy [(t, _)] =
  1737       case implode_list c_nil c_cons t
  1738        of SOME ts => (case implode_string c_char c_nibbles mk_char mk_string ts
  1739            of SOME p => p
  1740             | NONE => error "Illegal ml_string expression")
  1741         | NONE => error "Illegal ml_string expression";
  1742   in (1, pretty) end;
  1743 
  1744 val pretty_imperative_monad_bind =
  1745   let
  1746     fun pretty (pr : CodeName.var_ctxt -> fixity -> iterm -> Pretty.T)
  1747           vars fxy [(t1, _), ((v, ty) `|-> t2, _)] =
  1748             pr vars fxy (ICase (((t1, ty), ([(IVar v, t2)])), IVar ""))
  1749       | pretty pr vars fxy [(t1, _), (t2, ty2)] =
  1750           let
  1751             (*this code suffers from the lack of a proper concept for bindings*)
  1752             val vs = CodeThingol.fold_varnames cons t2 [];
  1753             val v = Name.variant vs "x";
  1754             val vars' = CodeName.intro_vars [v] vars;
  1755             val var = IVar v;
  1756             val ty = (hd o fst o CodeThingol.unfold_fun) ty2;
  1757           in pr vars' fxy (ICase (((t1, ty), ([(var, t2 `$ var)])), IVar "")) end;
  1758   in (2, pretty) end;
  1759 
  1760 end; (*local*)
  1761 
  1762 (** ML and Isar interface **)
  1763 
  1764 local
  1765 
  1766 fun map_syntax_exprs target =
  1767   map_seri_data target o apsnd o apsnd o apfst o map_syntax_expr;
  1768 fun map_syntax_modls target =
  1769   map_seri_data target o apsnd o apsnd o apsnd o map_syntax_modl;
  1770 fun map_reserveds target =
  1771   map_seri_data target o apsnd o apfst o apsnd;
  1772 
  1773 fun gen_add_syntax_class prep_class prep_const target raw_class raw_syn thy =
  1774   let
  1775     val cls = prep_class thy raw_class;
  1776     val class = CodeName.class thy cls;
  1777     fun mk_classop c = case AxClass.class_of_param thy c
  1778      of SOME class' => if cls = class' then CodeName.const thy c
  1779           else error ("Not a class operation for class " ^ quote class ^ ": " ^ quote c)
  1780       | NONE => error ("Not a class operation: " ^ quote c);
  1781     fun mk_syntax_ops raw_ops = AList.lookup (op =)
  1782       ((map o apfst) (mk_classop o prep_const thy) raw_ops);
  1783   in case raw_syn
  1784    of SOME (syntax, raw_ops) =>
  1785       thy
  1786       |> (map_syntax_exprs target o apfst o apfst)
  1787            (Symtab.update (class, (syntax, mk_syntax_ops raw_ops)))
  1788     | NONE =>
  1789       thy
  1790       |> (map_syntax_exprs target o apfst o apfst)
  1791            (Symtab.delete_safe class)
  1792   end;
  1793 
  1794 fun gen_add_syntax_inst prep_class prep_tyco target (raw_tyco, raw_class) add_del thy =
  1795   let
  1796     val inst = CodeName.instance thy (prep_class thy raw_class, prep_tyco thy raw_tyco);
  1797   in if add_del then
  1798     thy
  1799     |> (map_syntax_exprs target o apfst o apsnd)
  1800         (Symtab.update (inst, ()))
  1801   else
  1802     thy
  1803     |> (map_syntax_exprs target o apfst o apsnd)
  1804         (Symtab.delete_safe inst)
  1805   end;
  1806 
  1807 fun gen_add_syntax_tyco prep_tyco target raw_tyco raw_syn thy =
  1808   let
  1809     val tyco = prep_tyco thy raw_tyco;
  1810     val tyco' = if tyco = "fun" then "fun" else CodeName.tyco thy tyco;
  1811     fun check_args (syntax as (n, _)) = if n <> Sign.arity_number thy tyco
  1812       then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
  1813       else syntax
  1814   in case raw_syn
  1815    of SOME syntax =>
  1816       thy
  1817       |> (map_syntax_exprs target o apsnd o apfst)
  1818            (Symtab.update (tyco', check_args syntax))
  1819    | NONE =>
  1820       thy
  1821       |> (map_syntax_exprs target o apsnd o apfst)
  1822            (Symtab.delete_safe tyco')
  1823   end;
  1824 
  1825 fun gen_add_syntax_const prep_const target raw_c raw_syn thy =
  1826   let
  1827     val c = prep_const thy raw_c;
  1828     val c' = CodeName.const thy c;
  1829     fun check_args (syntax as (n, _)) = if n > CodeUnit.no_args thy c
  1830       then error ("Too many arguments in syntax for constant " ^ quote c)
  1831       else syntax;
  1832   in case raw_syn
  1833    of SOME syntax =>
  1834       thy
  1835       |> (map_syntax_exprs target o apsnd o apsnd)
  1836            (Symtab.update (c', check_args syntax))
  1837    | NONE =>
  1838       thy
  1839       |> (map_syntax_exprs target o apsnd o apsnd)
  1840            (Symtab.delete_safe c')
  1841   end;
  1842 
  1843 fun cert_class thy class =
  1844   let
  1845     val _ = AxClass.get_definition thy class;
  1846   in class end;
  1847 
  1848 fun read_class thy raw_class =
  1849   let
  1850     val class = Sign.intern_class thy raw_class;
  1851     val _ = AxClass.get_definition thy class;
  1852   in class end;
  1853 
  1854 fun cert_tyco thy tyco =
  1855   let
  1856     val _ = if Sign.declared_tyname thy tyco then ()
  1857       else error ("No such type constructor: " ^ quote tyco);
  1858   in tyco end;
  1859 
  1860 fun read_tyco thy raw_tyco =
  1861   let
  1862     val tyco = Sign.intern_type thy raw_tyco;
  1863     val _ = if Sign.declared_tyname thy tyco then ()
  1864       else error ("No such type constructor: " ^ quote raw_tyco);
  1865   in tyco end;
  1866 
  1867 fun no_bindings x = (Option.map o apsnd)
  1868   (fn pretty => fn pr => fn vars => pretty (pr vars)) x;
  1869 
  1870 fun gen_add_haskell_monad prep_const c_run c_mbind c_kbind thy =
  1871   let
  1872     val c_run' = prep_const thy c_run;
  1873     val c_mbind' = prep_const thy c_mbind;
  1874     val c_mbind'' = CodeName.const thy c_mbind';
  1875     val c_kbind' = prep_const thy c_kbind;
  1876     val c_kbind'' = CodeName.const thy c_kbind';
  1877     val pr = pretty_haskell_monad c_mbind'' c_kbind''
  1878   in
  1879     thy
  1880     |> gen_add_syntax_const (K I) target_Haskell c_run' (SOME pr)
  1881     |> gen_add_syntax_const (K I) target_Haskell c_mbind'
  1882           (no_bindings (SOME (parse_infix fst (L, 1) ">>=")))
  1883     |> gen_add_syntax_const (K I) target_Haskell c_kbind'
  1884           (no_bindings (SOME (parse_infix fst (L, 1) ">>")))
  1885   end;
  1886 
  1887 fun add_reserved target =
  1888   let
  1889     fun add sym syms = if member (op =) syms sym
  1890       then error ("Reserved symbol " ^ quote sym ^ " already declared")
  1891       else insert (op =) sym syms
  1892   in map_reserveds target o add end;
  1893 
  1894 fun add_modl_alias target =
  1895   map_syntax_modls target o apfst o Symtab.update o apsnd CodeName.check_modulename;
  1896 
  1897 fun add_modl_prolog target =
  1898   map_syntax_modls target o apsnd o
  1899     (fn (modl, NONE) => Symtab.delete modl | (modl, SOME prolog) =>
  1900       Symtab.update (modl, Pretty.str prolog));
  1901 
  1902 fun zip_list (x::xs) f g =
  1903   f
  1904   #-> (fn y =>
  1905     fold_map (fn x => g |-- f >> pair x) xs
  1906     #-> (fn xys => pair ((x, y) :: xys)));
  1907 
  1908 structure P = OuterParse
  1909 and K = OuterKeyword
  1910 
  1911 fun parse_multi_syntax parse_thing parse_syntax =
  1912   P.and_list1 parse_thing
  1913   #-> (fn things => Scan.repeat1 (P.$$$ "(" |-- P.name --
  1914         (zip_list things parse_syntax (P.$$$ "and")) --| P.$$$ ")"));
  1915 
  1916 val (infixK, infixlK, infixrK) = ("infix", "infixl", "infixr");
  1917 
  1918 fun parse_syntax prep_arg xs =
  1919   Scan.option ((
  1920       ((P.$$$ infixK  >> K X)
  1921         || (P.$$$ infixlK >> K L)
  1922         || (P.$$$ infixrK >> K R))
  1923         -- P.nat >> parse_infix prep_arg
  1924       || Scan.succeed (parse_mixfix prep_arg))
  1925       -- P.string
  1926       >> (fn (parse, s) => parse s)) xs;
  1927 
  1928 val (code_classK, code_instanceK, code_typeK, code_constK, code_monadK,
  1929   code_reservedK, code_modulenameK, code_moduleprologK) =
  1930   ("code_class", "code_instance", "code_type", "code_const", "code_monad",
  1931     "code_reserved", "code_modulename", "code_moduleprolog");
  1932 
  1933 in
  1934 
  1935 val parse_syntax = parse_syntax;
  1936 
  1937 val add_syntax_class = gen_add_syntax_class cert_class (K I);
  1938 val add_syntax_inst = gen_add_syntax_inst cert_class cert_tyco;
  1939 val add_syntax_tyco = gen_add_syntax_tyco cert_tyco;
  1940 val add_syntax_const = gen_add_syntax_const (K I);
  1941 
  1942 val add_syntax_class_cmd = gen_add_syntax_class read_class CodeUnit.read_const;
  1943 val add_syntax_inst_cmd = gen_add_syntax_inst read_class read_tyco;
  1944 val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco;
  1945 val add_syntax_const_cmd = gen_add_syntax_const CodeUnit.read_const;
  1946 
  1947 fun add_syntax_tycoP target tyco = parse_syntax I >> add_syntax_tyco_cmd target tyco;
  1948 fun add_syntax_constP target c = parse_syntax fst >> (add_syntax_const_cmd target c o no_bindings);
  1949 
  1950 fun add_undefined target undef target_undefined thy =
  1951   let
  1952     fun pr _ _ _ _ = str target_undefined;
  1953   in
  1954     thy
  1955     |> add_syntax_const target undef (SOME (~1, pr))
  1956   end;
  1957 
  1958 fun add_pretty_list target nill cons thy =
  1959   let
  1960     val nil' = CodeName.const thy nill;
  1961     val cons' = CodeName.const thy cons;
  1962     val pr = pretty_list nil' cons' target;
  1963   in
  1964     thy
  1965     |> add_syntax_const target cons (SOME pr)
  1966   end;
  1967 
  1968 fun add_pretty_list_string target nill cons charr nibbles thy =
  1969   let
  1970     val nil' = CodeName.const thy nill;
  1971     val cons' = CodeName.const thy cons;
  1972     val charr' = CodeName.const thy charr;
  1973     val nibbles' = map (CodeName.const thy) nibbles;
  1974     val pr = pretty_list_string nil' cons' charr' nibbles' target;
  1975   in
  1976     thy
  1977     |> add_syntax_const target cons (SOME pr)
  1978   end;
  1979 
  1980 fun add_pretty_char target charr nibbles thy =
  1981   let
  1982     val charr' = CodeName.const thy charr;
  1983     val nibbles' = map (CodeName.const thy) nibbles;
  1984     val pr = pretty_char charr' nibbles' target;
  1985   in
  1986     thy
  1987     |> add_syntax_const target charr (SOME pr)
  1988   end;
  1989 
  1990 fun add_pretty_numeral target unbounded number_of b0 b1 pls min bit thy =
  1991   let
  1992     val b0' = CodeName.const thy b0;
  1993     val b1' = CodeName.const thy b1;
  1994     val pls' = CodeName.const thy pls;
  1995     val min' = CodeName.const thy min;
  1996     val bit' = CodeName.const thy bit;
  1997     val pr = pretty_numeral unbounded b0' b1' pls' min' bit' target;
  1998   in
  1999     thy
  2000     |> add_syntax_const target number_of (SOME pr)
  2001   end;
  2002 
  2003 fun add_pretty_ml_string target charr nibbles nill cons str thy =
  2004   let
  2005     val charr' = CodeName.const thy charr;
  2006     val nibbles' = map (CodeName.const thy) nibbles;
  2007     val nil' = CodeName.const thy nill;
  2008     val cons' = CodeName.const thy cons;
  2009     val pr = pretty_ml_string charr' nibbles' nil' cons' target;
  2010   in
  2011     thy
  2012     |> add_syntax_const target str (SOME pr)
  2013   end;
  2014 
  2015 fun add_pretty_imperative_monad_bind target bind thy =
  2016   let
  2017     val pr = pretty_imperative_monad_bind
  2018   in
  2019     thy
  2020     |> add_syntax_const target bind (SOME pr)
  2021   end;
  2022 
  2023 val add_haskell_monad = gen_add_haskell_monad CodeUnit.read_const;
  2024 
  2025 val code_classP =
  2026   OuterSyntax.command code_classK "define code syntax for class" K.thy_decl (
  2027     parse_multi_syntax P.xname
  2028       (Scan.option (P.string -- Scan.optional (P.$$$ "where" |-- Scan.repeat1
  2029         (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.string)) []))
  2030     >> (Toplevel.theory oo fold) (fn (target, syns) =>
  2031           fold (fn (raw_class, syn) => add_syntax_class_cmd target raw_class syn) syns)
  2032   );
  2033 
  2034 val code_instanceP =
  2035   OuterSyntax.command code_instanceK "define code syntax for instance" K.thy_decl (
  2036     parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname)
  2037       ((P.minus >> K true) || Scan.succeed false)
  2038     >> (Toplevel.theory oo fold) (fn (target, syns) =>
  2039           fold (fn (raw_inst, add_del) => add_syntax_inst_cmd target raw_inst add_del) syns)
  2040   );
  2041 
  2042 val code_typeP =
  2043   OuterSyntax.command code_typeK "define code syntax for type constructor" K.thy_decl (
  2044     parse_multi_syntax P.xname (parse_syntax I)
  2045     >> (Toplevel.theory oo fold) (fn (target, syns) =>
  2046           fold (fn (raw_tyco, syn) => add_syntax_tyco_cmd target raw_tyco syn) syns)
  2047   );
  2048 
  2049 val code_constP =
  2050   OuterSyntax.command code_constK "define code syntax for constant" K.thy_decl (
  2051     parse_multi_syntax P.term (parse_syntax fst)
  2052     >> (Toplevel.theory oo fold) (fn (target, syns) =>
  2053           fold (fn (raw_const, syn) => add_syntax_const_cmd target raw_const (no_bindings syn)) syns)
  2054   );
  2055 
  2056 val code_monadP =
  2057   OuterSyntax.command code_monadK "define code syntax for Haskell monads" K.thy_decl (
  2058     P.term -- P.term -- P.term
  2059     >> (fn ((raw_run, raw_mbind), raw_kbind) => Toplevel.theory 
  2060           (add_haskell_monad raw_run raw_mbind raw_kbind))
  2061   );
  2062 
  2063 val code_reservedP =
  2064   OuterSyntax.command code_reservedK "declare words as reserved for target language" K.thy_decl (
  2065     P.name -- Scan.repeat1 P.name
  2066     >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds)
  2067   )
  2068 
  2069 val code_modulenameP =
  2070   OuterSyntax.command code_modulenameK "alias module to other name" K.thy_decl (
  2071     P.name -- Scan.repeat1 (P.name -- P.name)
  2072     >> (fn (target, modlnames) => (Toplevel.theory o fold (add_modl_alias target)) modlnames)
  2073   )
  2074 
  2075 val code_moduleprologP =
  2076   OuterSyntax.command code_moduleprologK "add prolog to module" K.thy_decl (
  2077     P.name -- Scan.repeat1 (P.name -- (P.text >> (fn "-" => NONE | s => SOME s)))
  2078     >> (fn (target, prologs) => (Toplevel.theory o fold (add_modl_prolog target)) prologs)
  2079   )
  2080 
  2081 val _ = OuterSyntax.add_keywords [infixK, infixlK, infixrK];
  2082 
  2083 val _ = OuterSyntax.add_parsers [code_classP, code_instanceP, code_typeP, code_constP,
  2084   code_reservedP, code_modulenameP, code_moduleprologP, code_monadP];
  2085 
  2086 
  2087 (*including serializer defaults*)
  2088 val setup =
  2089   add_serializer (target_SML, isar_seri_sml)
  2090   #> add_serializer (target_OCaml, isar_seri_ocaml)
  2091   #> add_serializer (target_Haskell, isar_seri_haskell)
  2092   #> add_serializer (target_diag, fn _ => fn _ => fn _ => seri_diagnosis)
  2093   #> add_syntax_tyco "SML" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
  2094       (gen_brackify (case fxy of NOBR => false | _ => eval_fxy (INFX (1, R)) fxy) o Pretty.breaks) [
  2095         pr_typ (INFX (1, X)) ty1,
  2096         str "->",
  2097         pr_typ (INFX (1, R)) ty2
  2098       ]))
  2099   #> add_syntax_tyco "OCaml" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
  2100       (gen_brackify (case fxy of NOBR => false | _ => eval_fxy (INFX (1, R)) fxy) o Pretty.breaks) [
  2101         pr_typ (INFX (1, X)) ty1,
  2102         str "->",
  2103         pr_typ (INFX (1, R)) ty2
  2104       ]))
  2105   #> add_syntax_tyco "Haskell" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
  2106       brackify_infix (1, R) fxy [
  2107         pr_typ (INFX (1, X)) ty1,
  2108         str "->",
  2109         pr_typ (INFX (1, R)) ty2
  2110       ]))
  2111   #> fold (add_reserved "SML") ML_Syntax.reserved_names
  2112   #> fold (add_reserved "SML")
  2113       ["o" (*dictionary projections use it already*), "Fail", "div", "mod" (*standard infixes*)]
  2114   #> fold (add_reserved "OCaml") [
  2115       "and", "as", "assert", "begin", "class",
  2116       "constraint", "do", "done", "downto", "else", "end", "exception",
  2117       "external", "false", "for", "fun", "function", "functor", "if",
  2118       "in", "include", "inherit", "initializer", "lazy", "let", "match", "method",
  2119       "module", "mutable", "new", "object", "of", "open", "or", "private", "rec",
  2120       "sig", "struct", "then", "to", "true", "try", "type", "val",
  2121       "virtual", "when", "while", "with"
  2122     ]
  2123   #> fold (add_reserved "OCaml") ["failwith", "mod"]
  2124   #> fold (add_reserved "Haskell") [
  2125       "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
  2126       "import", "default", "forall", "let", "in", "class", "qualified", "data",
  2127       "newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
  2128     ]
  2129   #> fold (add_reserved "Haskell") [
  2130       "Prelude", "Main", "Bool", "Maybe", "Either", "Ordering", "Char", "String", "Int",
  2131       "Integer", "Float", "Double", "Rational", "IO", "Eq", "Ord", "Enum", "Bounded",
  2132       "Num", "Real", "Integral", "Fractional", "Floating", "RealFloat", "Monad", "Functor",
  2133       "AlreadyExists", "ArithException", "ArrayException", "AssertionFailed", "AsyncException",
  2134       "BlockedOnDeadMVar", "Deadlock", "Denormal", "DivideByZero", "DotNetException", "DynException",
  2135       "Dynamic", "EOF", "EQ", "EmptyRec", "ErrorCall", "ExitException", "ExitFailure",
  2136       "ExitSuccess", "False", "GT", "HeapOverflow",
  2137       "IOError", "IOException", "IllegalOperation",
  2138       "IndexOutOfBounds", "Just", "Key", "LT", "Left", "LossOfPrecision", "NoMethodError",
  2139       "NoSuchThing", "NonTermination", "Nothing", "Obj", "OtherError", "Overflow",
  2140       "PatternMatchFail", "PermissionDenied", "ProtocolError", "RecConError", "RecSelError",
  2141       "RecUpdError", "ResourceBusy", "ResourceExhausted", "Right", "StackOverflow",
  2142       "ThreadKilled", "True", "TyCon", "TypeRep", "UndefinedElement", "Underflow",
  2143       "UnsupportedOperation", "UserError", "abs", "absReal", "acos", "acosh", "all",
  2144       "and", "any", "appendFile", "asTypeOf", "asciiTab", "asin", "asinh", "atan",
  2145       "atan2", "atanh", "basicIORun", "blockIO", "boundedEnumFrom", "boundedEnumFromThen",
  2146       "boundedEnumFromThenTo", "boundedEnumFromTo", "boundedPred", "boundedSucc", "break",
  2147       "catch", "catchException", "ceiling", "compare", "concat", "concatMap", "const",
  2148       "cos", "cosh", "curry", "cycle", "decodeFloat", "denominator", "div", "divMod",
  2149       "doubleToRatio", "doubleToRational", "drop", "dropWhile", "either", "elem",
  2150       "emptyRec", "encodeFloat", "enumFrom", "enumFromThen", "enumFromThenTo",
  2151       "enumFromTo", "error", "even", "exp", "exponent", "fail", "filter", "flip",
  2152       "floatDigits", "floatProperFraction", "floatRadix", "floatRange", "floatToRational",
  2153       "floor", "fmap", "foldl", "foldl'", "foldl1", "foldr", "foldr1", "fromDouble",
  2154       "fromEnum", "fromEnum_0", "fromInt", "fromInteger", "fromIntegral", "fromObj",
  2155       "fromRational", "fst", "gcd", "getChar", "getContents", "getLine", "head",
  2156       "id", "inRange", "index", "init", "intToRatio", "interact", "ioError", "isAlpha",
  2157       "isAlphaNum", "isDenormalized", "isDigit", "isHexDigit", "isIEEE", "isInfinite",
  2158       "isLower", "isNaN", "isNegativeZero", "isOctDigit", "isSpace", "isUpper", "iterate", "iterate'",
  2159       "last", "lcm", "length", "lex", "lexDigits", "lexLitChar", "lexmatch", "lines", "log",
  2160       "logBase", "lookup", "loop", "map", "mapM", "mapM_", "max", "maxBound", "maximum",
  2161       "maybe", "min", "minBound", "minimum", "mod", "negate", "nonnull", "not", "notElem",
  2162       "null", "numerator", "numericEnumFrom", "numericEnumFromThen", "numericEnumFromThenTo",
  2163       "numericEnumFromTo", "odd", "or", "otherwise", "pi", "pred", 
  2164       "print", "product", "properFraction", "protectEsc", "putChar", "putStr", "putStrLn",
  2165       "quot", "quotRem", "range", "rangeSize", "rationalToDouble", "rationalToFloat",
  2166       "rationalToRealFloat", "read", "readDec", "readField", "readFieldName", "readFile",
  2167       "readFloat", "readHex", "readIO", "readInt", "readList", "readLitChar", "readLn",
  2168       "readOct", "readParen", "readSigned", "reads", "readsPrec", "realFloatToRational",
  2169       "realToFrac", "recip", "reduce", "rem", "repeat", "replicate", "return", "reverse",
  2170       "round", "scaleFloat", "scanl", "scanl1", "scanr", "scanr1", "seq", "sequence",
  2171       "sequence_", "show", "showChar", "showException", "showField", "showList",
  2172       "showLitChar", "showParen", "showString", "shows", "showsPrec", "significand",
  2173       "signum", "signumReal", "sin", "sinh", "snd", "span", "splitAt", "sqrt", "subtract",
  2174       "succ", "sum", "tail", "take", "takeWhile", "takeWhile1", "tan", "tanh", "threadToIOResult",
  2175       "throw", "toEnum", "toInt", "toInteger", "toObj", "toRational", "truncate", "uncurry",
  2176       "undefined", "unlines", "unsafeCoerce", "unsafeIndex", "unsafeRangeSize", "until", "unwords",
  2177       "unzip", "unzip3", "userError", "words", "writeFile", "zip", "zip3", "zipWith", "zipWith3"
  2178     ] (*due to weird handling of ':', we can't do anything else than to import *all* prelude symbols*);
  2179 
  2180 end; (*local*)
  2181 
  2182 end; (*struct*)