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