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