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