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