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