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