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