src/Tools/code/code_target.ML
author haftmann
Fri Aug 24 14:14:20 2007 +0200 (2007-08-24)
changeset 24423 ae9cd0e92423
parent 24381 560e8ecdf633
child 24591 6509626eb2c9
permissions -rw-r--r--
overloaded definitions accompanied by explicit constants
     1 (*  Title:      Tools/code/code_target.ML
     2     ID:         $Id$
     3     Author:     Florian Haftmann, TU Muenchen
     4 
     5 Serializer from intermediate language ("Thin-gol")
     6 to target languages (like SML or Haskell).
     7 *)
     8 
     9 signature CODE_TARGET =
    10 sig
    11   include BASIC_CODE_THINGOL;
    12 
    13   val add_syntax_class: string -> class
    14     -> (string * (string * string) list) option -> theory -> theory;
    15   val add_syntax_inst: string -> string * class -> bool -> theory -> theory;
    16   val add_syntax_tycoP: string -> string -> OuterParse.token list
    17     -> (theory -> theory) * OuterParse.token list;
    18   val add_syntax_constP: string -> string -> OuterParse.token list
    19     -> (theory -> theory) * OuterParse.token list;
    20 
    21   val add_undefined: string -> string -> string -> theory -> theory;
    22   val add_pretty_list: string -> string -> string -> theory -> theory;
    23   val add_pretty_list_string: string -> string -> string
    24     -> string -> string list -> theory -> theory;
    25   val add_pretty_char: string -> string -> string list -> theory -> theory
    26   val add_pretty_numeral: string -> bool -> string -> string -> string -> string
    27     -> string -> string -> theory -> theory;
    28   val add_pretty_ml_string: string -> string -> string list -> string
    29     -> string -> string -> theory -> theory;
    30   val add_pretty_imperative_monad_bind: string -> string -> theory -> theory;
    31 
    32   type serializer;
    33   val add_serializer: string * serializer -> theory -> theory;
    34   val get_serializer: theory -> string -> bool -> string option -> string option -> Args.T list
    35     -> (theory -> string -> string) -> string 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 * (typscheme * (iterm list * iterm) list)) 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 (_, ((vs, _), (ts, _) :: _)) NONE = SOME (mk ts vs)
   427                   | chk (_, ((vs, _), (ts, _) :: _)) (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, ((raw_vs, ty), eqs as eq :: eqs')) =
   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 fished1 = fold (map2 fish_parm) eqs (replicate (length (hd eqs)) NONE);
   690                 val x = Name.variant (map_filter I fished1) "x";
   691                 val fished2 = map_index (fillup_parm x) fished1;
   692                 val (fished3, _) = Name.variants fished2 Name.context;
   693                 val vars' = CodeName.intro_vars fished3 vars;
   694               in map (CodeName.lookup_var vars') fished3 end;
   695             fun pr_eq (ts, t) =
   696               let
   697                 val consts = map_filter
   698                   (fn c => if (is_some o const_syntax) c
   699                     then NONE else (SOME o NameSpace.base o deresolv) c)
   700                     ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);
   701                 val vars = init_syms
   702                   |> CodeName.intro_vars consts
   703                   |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)
   704                       (insert (op =)) ts []);
   705               in concat [
   706                 (Pretty.block o Pretty.commas) (map (pr_term true vars NOBR) ts),
   707                 str "->",
   708                 pr_term false vars NOBR t
   709               ] end;
   710             fun pr_eqs [(ts, t)] =
   711                   let
   712                     val consts = map_filter
   713                       (fn c => if (is_some o const_syntax) c
   714                         then NONE else (SOME o NameSpace.base o deresolv) c)
   715                         ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);
   716                     val vars = init_syms
   717                       |> CodeName.intro_vars consts
   718                       |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)
   719                           (insert (op =)) ts []);
   720                   in
   721                     concat (
   722                       map (pr_term true vars BR) ts
   723                       @ str "="
   724                       @@ pr_term false vars NOBR t
   725                     )
   726                   end
   727               | pr_eqs (eqs as (eq as ([_], _)) :: eqs') =
   728                   Pretty.block (
   729                     str "="
   730                     :: Pretty.brk 1
   731                     :: str "function"
   732                     :: Pretty.brk 1
   733                     :: pr_eq eq
   734                     :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1] o single o pr_eq) eqs'
   735                   )
   736               | pr_eqs (eqs as eq :: eqs') =
   737                   let
   738                     val consts = map_filter
   739                       (fn c => if (is_some o const_syntax) c
   740                         then NONE else (SOME o NameSpace.base o deresolv) c)
   741                         ((fold o CodeThingol.fold_constnames) (insert (op =)) (map snd eqs) []);
   742                     val vars = init_syms
   743                       |> CodeName.intro_vars consts;
   744                     val dummy_parms = (map str o fish_parms vars o map fst) eqs;
   745                   in
   746                     Pretty.block (
   747                       Pretty.breaks dummy_parms
   748                       @ Pretty.brk 1
   749                       :: str "="
   750                       :: Pretty.brk 1
   751                       :: str "match"
   752                       :: Pretty.brk 1
   753                       :: (Pretty.block o Pretty.commas) dummy_parms
   754                       :: Pretty.brk 1
   755                       :: str "with"
   756                       :: Pretty.brk 1
   757                       :: pr_eq eq
   758                       :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1] o single o pr_eq) eqs'
   759                     )
   760                   end;
   761             fun pr_funn definer (name, ((vs, ty), eqs)) =
   762               concat (
   763                 str definer
   764                 :: (str o deresolv) name
   765                 :: pr_tyvars (filter_out (null o snd) vs)
   766                 @| pr_eqs eqs
   767               );
   768             val (ps, p) = split_last (pr_funn "let rec" funn :: map (pr_funn "and") funns');
   769           in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end
   770      | pr_def (MLDatas (datas as (data :: datas'))) =
   771           let
   772             fun pr_co (co, []) =
   773                   str (deresolv co)
   774               | pr_co (co, tys) =
   775                   concat [
   776                     str (deresolv co),
   777                     str "of",
   778                     Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys)
   779                   ];
   780             fun pr_data definer (tyco, (vs, [])) =
   781                   concat (
   782                     str definer
   783                     :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
   784                     :: str "="
   785                     @@ str "EMPTY_"
   786                   )
   787               | pr_data definer (tyco, (vs, cos)) =
   788                   concat (
   789                     str definer
   790                     :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
   791                     :: str "="
   792                     :: separate (str "|") (map pr_co cos)
   793                   );
   794             val (ps, p) = split_last (pr_data "type" data :: map (pr_data "and") datas');
   795           in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end
   796      | pr_def (MLClass (class, (superclasses, (v, classops)))) =
   797           let
   798             val w = "_" ^ first_upper v;
   799             fun pr_superclass_field (class, classrel) =
   800               (concat o map str) [
   801                 deresolv classrel, ":", "'" ^ v, deresolv class
   802               ];
   803             fun pr_classop_field (classop, ty) =
   804               concat [
   805                 (str o deresolv) classop, str ":", pr_typ NOBR ty
   806               ];
   807             fun pr_classop_proj (classop, _) =
   808               concat [
   809                 str "let",
   810                 (str o deresolv) classop,
   811                 str w,
   812                 str "=",
   813                 str (w ^ "." ^ deresolv classop ^ ";;")
   814               ];
   815           in Pretty.chunks (
   816             concat [
   817               str ("type '" ^ v),
   818               (str o deresolv) class,
   819               str "=",
   820               Pretty.enum ";" "{" "};;" (
   821                 map pr_superclass_field superclasses @ map pr_classop_field classops
   822               )
   823             ]
   824             :: map pr_classop_proj classops
   825           ) end
   826      | pr_def (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classop_defs)))) =
   827           let
   828             fun pr_superclass (_, (classrel, dss)) =
   829               concat [
   830                 (str o deresolv) classrel,
   831                 str "=",
   832                 pr_dicts NOBR [DictConst dss]
   833               ];
   834             fun pr_classop_def (classop, t) =
   835               let
   836                 val consts = map_filter
   837                   (fn c => if (is_some o const_syntax) c
   838                     then NONE else (SOME o NameSpace.base o deresolv) c)
   839                     (CodeThingol.fold_constnames (insert (op =)) t []);
   840                 val vars = CodeName.intro_vars consts init_syms;
   841               in
   842                 concat [
   843                   (str o deresolv) classop,
   844                   str "=",
   845                   pr_term false vars NOBR t
   846                 ]
   847               end;
   848           in
   849             concat (
   850               str "let"
   851               :: (str o deresolv) inst
   852               :: pr_tyvars arity
   853               @ str "="
   854               @@ (Pretty.enclose "(" ");;" o Pretty.breaks) [
   855                 Pretty.enum ";" "{" "}" (map pr_superclass superarities @ map pr_classop_def classop_defs),
   856                 str ":",
   857                 pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
   858               ]
   859             )
   860           end;
   861   in pr_def ml_def end;
   862 
   863 fun pr_ocaml_modl name content =
   864   Pretty.chunks ([
   865     str ("module " ^ name ^ " = "),
   866     str "struct",
   867     str ""
   868   ] @ content @ [
   869     str "",
   870     str ("end;; (*struct " ^ name ^ "*)")
   871   ]);
   872 
   873 val code_width = ref 80;
   874 fun code_output p = Pretty.setmp_margin (!code_width) Pretty.output p ^ "\n";
   875 
   876 fun seri_ml pr_def pr_modl module output labelled_name reserved_syms raw_module_alias module_prolog
   877   (_ : string -> class_syntax option) tyco_syntax const_syntax code =
   878   let
   879     val module_alias = if is_some module then K module else raw_module_alias;
   880     val is_cons = CodeThingol.is_cons code;
   881     datatype node =
   882         Def of string * ml_def option
   883       | Module of string * ((Name.context * Name.context) * node Graph.T);
   884     val init_names = Name.make_context reserved_syms;
   885     val init_module = ((init_names, init_names), Graph.empty);
   886     fun map_node [] f = f
   887       | map_node (m::ms) f =
   888           Graph.default_node (m, Module (m, init_module))
   889           #> Graph.map_node m (fn (Module (dmodlname, (nsp, nodes))) => Module (dmodlname, (nsp, map_node ms f nodes)));
   890     fun map_nsp_yield [] f (nsp, nodes) =
   891           let
   892             val (x, nsp') = f nsp
   893           in (x, (nsp', nodes)) end
   894       | map_nsp_yield (m::ms) f (nsp, nodes) =
   895           let
   896             val (x, nodes') =
   897               nodes
   898               |> Graph.default_node (m, Module (m, init_module))
   899               |> Graph.map_node_yield m (fn Module (dmodlname, nsp_nodes) => 
   900                   let
   901                     val (x, nsp_nodes') = map_nsp_yield ms f nsp_nodes
   902                   in (x, Module (dmodlname, nsp_nodes')) end)
   903           in (x, (nsp, nodes')) end;
   904     val init_syms = CodeName.make_vars reserved_syms;
   905     val name_modl = mk_modl_name_tab init_names NONE module_alias code;
   906     fun name_def upper name nsp =
   907       let
   908         val (_, base) = dest_name name;
   909         val base' = if upper then first_upper base else base;
   910         val ([base''], nsp') = Name.variants [base'] nsp;
   911       in (base'', nsp') end;
   912     fun map_nsp_fun f (nsp_fun, nsp_typ) =
   913       let
   914         val (x, nsp_fun') = f nsp_fun
   915       in (x, (nsp_fun', nsp_typ)) end;
   916     fun map_nsp_typ f (nsp_fun, nsp_typ) =
   917       let
   918         val (x, nsp_typ') = f nsp_typ
   919       in (x, (nsp_fun, nsp_typ')) end;
   920     fun mk_funs defs =
   921       fold_map
   922         (fn (name, CodeThingol.Fun info) =>
   923               map_nsp_fun (name_def false name) >> (fn base => (base, (name, info)))
   924           | (name, def) => error ("Function block containing illegal definition: " ^ labelled_name name)
   925         ) defs
   926       >> (split_list #> apsnd MLFuns);
   927     fun mk_datatype defs =
   928       fold_map
   929         (fn (name, CodeThingol.Datatype info) =>
   930               map_nsp_typ (name_def false name) >> (fn base => (base, SOME (name, info)))
   931           | (name, CodeThingol.Datatypecons _) =>
   932               map_nsp_fun (name_def true name) >> (fn base => (base, NONE))
   933           | (name, def) => error ("Datatype block containing illegal definition: " ^ labelled_name name)
   934         ) defs
   935       >> (split_list #> apsnd (map_filter I
   936         #> (fn [] => error ("Datatype block without data definition: " ^ (commas o map (labelled_name o fst)) defs)
   937              | infos => MLDatas infos)));
   938     fun mk_class defs =
   939       fold_map
   940         (fn (name, CodeThingol.Class info) =>
   941               map_nsp_typ (name_def false name) >> (fn base => (base, SOME (name, info)))
   942           | (name, CodeThingol.Classrel _) =>
   943               map_nsp_fun (name_def false name) >> (fn base => (base, NONE))
   944           | (name, CodeThingol.Classop _) =>
   945               map_nsp_fun (name_def false name) >> (fn base => (base, NONE))
   946           | (name, def) => error ("Class block containing illegal definition: " ^ labelled_name name)
   947         ) defs
   948       >> (split_list #> apsnd (map_filter I
   949         #> (fn [] => error ("Class block without class definition: " ^ (commas o map (labelled_name o fst)) defs)
   950              | [info] => MLClass info)));
   951     fun mk_inst [(name, CodeThingol.Classinst info)] =
   952       map_nsp_fun (name_def false name)
   953       >> (fn base => ([base], MLClassinst (name, info)));
   954     fun add_group mk defs nsp_nodes =
   955       let
   956         val names as (name :: names') = map fst defs;
   957         val deps =
   958           []
   959           |> fold (fold (insert (op =)) o Graph.imm_succs code) names
   960           |> subtract (op =) names;
   961         val (modls, _) = (split_list o map dest_name) names;
   962         val modl' = (the_single o distinct (op =) o map name_modl) modls
   963           handle Empty =>
   964             error ("Illegal mutual dependencies: " ^ commas (map labelled_name names));
   965         val modl_explode = NameSpace.explode modl';
   966         fun add_dep name name'' =
   967           let
   968             val modl'' = (name_modl o fst o dest_name) name'';
   969           in if modl' = modl'' then
   970             map_node modl_explode
   971               (Graph.add_edge (name, name''))
   972           else let
   973             val (common, (diff1::_, diff2::_)) = chop_prefix (op =)
   974               (modl_explode, NameSpace.explode modl'');
   975           in
   976             map_node common
   977               (fn gr => Graph.add_edge_acyclic (diff1, diff2) gr
   978                 handle Graph.CYCLES _ => error ("Dependency "
   979                   ^ quote name ^ " -> " ^ quote name''
   980                   ^ " would result in module dependency cycle"))
   981           end end;
   982       in
   983         nsp_nodes
   984         |> map_nsp_yield modl_explode (mk defs)
   985         |-> (fn (base' :: bases', def') =>
   986            apsnd (map_node modl_explode (Graph.new_node (name, (Def (base', SOME def')))
   987               #> fold2 (fn name' => fn base' => Graph.new_node (name', (Def (base', NONE)))) names' bases')))
   988         |> apsnd (fold (fn name => fold (add_dep name) deps) names)
   989         |> apsnd (fold (map_node modl_explode o Graph.add_edge) (product names names))
   990       end;
   991     fun group_defs [(_, CodeThingol.Bot)] =
   992           I
   993       | group_defs ((defs as (_, CodeThingol.Fun _)::_)) =
   994           add_group mk_funs defs
   995       | group_defs ((defs as (_, CodeThingol.Datatypecons _)::_)) =
   996           add_group mk_datatype defs
   997       | group_defs ((defs as (_, CodeThingol.Datatype _)::_)) =
   998           add_group mk_datatype defs
   999       | group_defs ((defs as (_, CodeThingol.Class _)::_)) =
  1000           add_group mk_class defs
  1001       | group_defs ((defs as (_, CodeThingol.Classrel _)::_)) =
  1002           add_group mk_class defs
  1003       | group_defs ((defs as (_, CodeThingol.Classop _)::_)) =
  1004           add_group mk_class defs
  1005       | group_defs ((defs as [(_, CodeThingol.Classinst _)])) =
  1006           add_group mk_inst defs
  1007       | group_defs defs = error ("Illegal mutual dependencies: " ^
  1008           (commas o map (labelled_name o fst)) defs)
  1009     val (_, nodes) =
  1010       init_module
  1011       |> fold group_defs (map (AList.make (Graph.get_node code))
  1012           (rev (Graph.strong_conn code)))
  1013     fun deresolver prefix name = 
  1014       let
  1015         val modl = (fst o dest_name) name;
  1016         val modl' = (NameSpace.explode o name_modl) modl;
  1017         val (_, (_, remainder)) = chop_prefix (op =) (prefix, modl');
  1018         val defname' =
  1019           nodes
  1020           |> fold (fn m => fn g => case Graph.get_node g m
  1021               of Module (_, (_, g)) => g) modl'
  1022           |> (fn g => case Graph.get_node g name of Def (defname, _) => defname);
  1023       in
  1024         NameSpace.implode (remainder @ [defname'])
  1025       end handle Graph.UNDEF _ =>
  1026         error ("Unknown definition name: " ^ labelled_name name);
  1027     fun the_prolog modlname = case module_prolog modlname
  1028      of NONE => []
  1029       | SOME p => [p, str ""];
  1030     fun pr_node prefix (Def (_, NONE)) =
  1031           NONE
  1032       | pr_node prefix (Def (_, SOME def)) =
  1033           SOME (pr_def tyco_syntax const_syntax labelled_name init_syms
  1034             (deresolver prefix) is_cons def)
  1035       | pr_node prefix (Module (dmodlname, (_, nodes))) =
  1036           SOME (pr_modl dmodlname (the_prolog (NameSpace.implode (prefix @ [dmodlname]))
  1037             @ separate (str "") ((map_filter (pr_node (prefix @ [dmodlname]) o Graph.get_node nodes)
  1038                 o rev o flat o Graph.strong_conn) nodes)));
  1039     val p = Pretty.chunks (the_prolog "" @ separate (str "") ((map_filter
  1040       (pr_node [] o Graph.get_node nodes) o rev o flat o Graph.strong_conn) nodes))
  1041   in output p end;
  1042 
  1043 val eval_verbose = ref false;
  1044 
  1045 fun isar_seri_sml module file =
  1046   let
  1047     val output = case file
  1048      of NONE => use_text "generated code" Output.ml_output (!eval_verbose) o code_output
  1049       | SOME "-" => writeln o code_output
  1050       | SOME file => File.write (Path.explode file) o code_output;
  1051   in
  1052     parse_args (Scan.succeed ())
  1053     #> (fn () => seri_ml pr_sml pr_sml_modl module output)
  1054   end;
  1055 
  1056 fun isar_seri_ocaml module file =
  1057   let
  1058     val output = case file
  1059      of NONE => error "OCaml: no internal compilation"
  1060       | SOME "-" => writeln o code_output
  1061       | SOME file => File.write (Path.explode file) o code_output;
  1062     fun output_file file = File.write (Path.explode file) o code_output;
  1063     val output_diag = writeln o code_output;
  1064   in
  1065     parse_args (Scan.succeed ())
  1066     #> (fn () => seri_ml pr_ocaml pr_ocaml_modl module output)
  1067   end;
  1068 
  1069 
  1070 (** Haskell serializer **)
  1071 
  1072 local
  1073 
  1074 fun pr_bind' ((NONE, NONE), _) = str "_"
  1075   | pr_bind' ((SOME v, NONE), _) = str v
  1076   | pr_bind' ((NONE, SOME p), _) = p
  1077   | pr_bind' ((SOME v, SOME p), _) = brackets [str v, str "@", p]
  1078 
  1079 val pr_bind_haskell = gen_pr_bind pr_bind';
  1080 
  1081 in
  1082 
  1083 fun pr_haskell class_syntax tyco_syntax const_syntax labelled_name init_syms
  1084     deresolv_here deresolv is_cons deriving_show def =
  1085   let
  1086     fun class_name class = case class_syntax class
  1087      of NONE => deresolv class
  1088       | SOME (class, _) => class;
  1089     fun classop_name class classop = case class_syntax class
  1090      of NONE => deresolv_here classop
  1091       | SOME (_, classop_syntax) => case classop_syntax classop
  1092          of NONE => (snd o dest_name) classop
  1093           | SOME classop => classop
  1094     fun pr_typparms tyvars vs =
  1095       case maps (fn (v, sort) => map (pair v) sort) vs
  1096        of [] => str ""
  1097         | xs => Pretty.block [
  1098             Pretty.enum "," "(" ")" (
  1099               map (fn (v, class) => str
  1100                 (class_name class ^ " " ^ CodeName.lookup_var tyvars v)) xs
  1101             ),
  1102             str " => "
  1103           ];
  1104     fun pr_tycoexpr tyvars fxy (tyco, tys) =
  1105       brackify fxy (str tyco :: map (pr_typ tyvars BR) tys)
  1106     and pr_typ tyvars fxy (tycoexpr as tyco `%% tys) =
  1107           (case tyco_syntax tyco
  1108            of NONE =>
  1109                 pr_tycoexpr tyvars fxy (deresolv tyco, tys)
  1110             | SOME (i, pr) =>
  1111                 if not (i = length tys)
  1112                 then error ("Number of argument mismatch in customary serialization: "
  1113                   ^ (string_of_int o length) tys ^ " given, "
  1114                   ^ string_of_int i ^ " expected")
  1115                 else pr (pr_typ tyvars) fxy tys)
  1116       | pr_typ tyvars fxy (ITyVar v) =
  1117           (str o CodeName.lookup_var tyvars) v;
  1118     fun pr_typscheme_expr tyvars (vs, tycoexpr) =
  1119       Pretty.block (pr_typparms tyvars vs @@ pr_tycoexpr tyvars NOBR tycoexpr);
  1120     fun pr_typscheme tyvars (vs, ty) =
  1121       Pretty.block (pr_typparms tyvars vs @@ pr_typ tyvars NOBR ty);
  1122     fun pr_term lhs vars fxy (IConst c) =
  1123           pr_app lhs vars fxy (c, [])
  1124       | pr_term lhs vars fxy (t as (t1 `$ t2)) =
  1125           (case CodeThingol.unfold_const_app t
  1126            of SOME app => pr_app lhs vars fxy app
  1127             | _ =>
  1128                 brackify fxy [
  1129                   pr_term lhs vars NOBR t1,
  1130                   pr_term lhs vars BR t2
  1131                 ])
  1132       | pr_term lhs vars fxy (IVar v) =
  1133           (str o CodeName.lookup_var vars) v
  1134       | pr_term lhs vars fxy (t as _ `|-> _) =
  1135           let
  1136             val (binds, t') = CodeThingol.unfold_abs t;
  1137             fun pr ((v, pat), ty) = pr_bind BR ((SOME v, pat), ty);
  1138             val (ps, vars') = fold_map pr binds vars;
  1139           in brackets (str "\\" :: ps @ str "->" @@ pr_term lhs vars' NOBR t') end
  1140       | pr_term lhs vars fxy (ICase (cases as (_, t0))) = (case CodeThingol.unfold_const_app t0
  1141            of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
  1142                 then pr_case vars fxy cases
  1143                 else pr_app lhs vars fxy c_ts
  1144             | NONE => pr_case vars fxy cases)
  1145     and pr_app' lhs vars ((c, _), ts) =
  1146       (str o deresolv) c :: map (pr_term lhs vars BR) ts
  1147     and pr_app lhs vars = gen_pr_app pr_app' pr_term const_syntax labelled_name is_cons lhs vars
  1148     and pr_bind fxy = pr_bind_haskell pr_term fxy
  1149     and pr_case vars fxy (cases as ((_, [_]), _)) =
  1150           let
  1151             val (binds, t) = CodeThingol.unfold_let (ICase cases);
  1152             fun pr ((pat, ty), t) vars =
  1153               vars
  1154               |> pr_bind BR ((NONE, SOME pat), ty)
  1155               |>> (fn p => semicolon [p, str "=", pr_term false vars NOBR t])
  1156             val (ps, vars') = fold_map pr binds vars;
  1157           in
  1158             Pretty.block_enclose (
  1159               str "let {",
  1160               concat [str "}", str "in", pr_term false vars' NOBR t]
  1161             ) ps
  1162           end
  1163       | pr_case vars fxy (((td, ty), bs as _ :: _), _) =
  1164           let
  1165             fun pr (pat, t) =
  1166               let
  1167                 val (p, vars') = pr_bind NOBR ((NONE, SOME pat), ty) vars;
  1168               in semicolon [p, str "->", pr_term false vars' NOBR t] end;
  1169           in
  1170             Pretty.block_enclose (
  1171               concat [str "(case", pr_term false vars NOBR td, str "of", str "{"],
  1172               str "})"
  1173             ) (map pr bs)
  1174           end
  1175       | pr_case vars fxy ((_, []), _) = str "error \"empty case\"";
  1176     fun pr_def (name, CodeThingol.Fun ((vs, ty), eqs)) =
  1177           let
  1178             val tyvars = CodeName.intro_vars (map fst vs) init_syms;
  1179             fun pr_eq (ts, t) =
  1180               let
  1181                 val consts = map_filter
  1182                   (fn c => if (is_some o const_syntax) c
  1183                     then NONE else (SOME o NameSpace.base o deresolv) c)
  1184                     ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);
  1185                 val vars = init_syms
  1186                   |> CodeName.intro_vars consts
  1187                   |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)
  1188                        (insert (op =)) ts []);
  1189               in
  1190                 semicolon (
  1191                   (str o deresolv_here) name
  1192                   :: map (pr_term true vars BR) ts
  1193                   @ str "="
  1194                   @@ pr_term false vars NOBR t
  1195                 )
  1196               end;
  1197           in
  1198             Pretty.chunks (
  1199               Pretty.block [
  1200                 (str o suffix " ::" o deresolv_here) name,
  1201                 Pretty.brk 1,
  1202                 pr_typscheme tyvars (vs, ty),
  1203                 str ";"
  1204               ]
  1205               :: map pr_eq eqs
  1206             )
  1207           end
  1208       | pr_def (name, CodeThingol.Datatype (vs, [])) =
  1209           let
  1210             val tyvars = CodeName.intro_vars (map fst vs) init_syms;
  1211           in
  1212             semicolon [
  1213               str "data",
  1214               pr_typscheme_expr tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs))
  1215             ]
  1216           end
  1217       | pr_def (name, CodeThingol.Datatype (vs, [(co, [ty])])) =
  1218           let
  1219             val tyvars = CodeName.intro_vars (map fst vs) init_syms;
  1220           in
  1221             semicolon (
  1222               str "newtype"
  1223               :: pr_typscheme_expr tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs))
  1224               :: str "="
  1225               :: (str o deresolv_here) co
  1226               :: pr_typ tyvars BR ty
  1227               :: (if deriving_show name then [str "deriving (Read, Show)"] else [])
  1228             )
  1229           end
  1230       | pr_def (name, CodeThingol.Datatype (vs, co :: cos)) =
  1231           let
  1232             val tyvars = CodeName.intro_vars (map fst vs) init_syms;
  1233             fun pr_co (co, tys) =
  1234               concat (
  1235                 (str o deresolv_here) co
  1236                 :: map (pr_typ tyvars BR) tys
  1237               )
  1238           in
  1239             semicolon (
  1240               str "data"
  1241               :: pr_typscheme_expr tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs))
  1242               :: str "="
  1243               :: pr_co co
  1244               :: map ((fn p => Pretty.block [str "| ", p]) o pr_co) cos
  1245               @ (if deriving_show name then [str "deriving (Read, Show)"] else [])
  1246             )
  1247           end
  1248       | pr_def (name, CodeThingol.Class (superclasss, (v, classops))) =
  1249           let
  1250             val tyvars = CodeName.intro_vars [v] init_syms;
  1251             fun pr_classop (classop, ty) =
  1252               semicolon [
  1253                 (str o classop_name name) classop,
  1254                 str "::",
  1255                 pr_typ tyvars NOBR ty
  1256               ]
  1257           in
  1258             Pretty.block_enclose (
  1259               Pretty.block [
  1260                 str "class ",
  1261                 pr_typparms tyvars [(v, map fst superclasss)],
  1262                 str (deresolv_here name ^ " " ^ CodeName.lookup_var tyvars v),
  1263                 str " where {"
  1264               ],
  1265               str "};"
  1266             ) (map pr_classop classops)
  1267           end
  1268       | pr_def (_, CodeThingol.Classinst ((class, (tyco, vs)), (_, classop_defs))) =
  1269           let
  1270             val tyvars = CodeName.intro_vars (map fst vs) init_syms;
  1271             fun pr_instdef (classop, t) =
  1272                 let
  1273                   val consts = map_filter
  1274                     (fn c => if (is_some o const_syntax) c
  1275                       then NONE else (SOME o NameSpace.base o deresolv) c)
  1276                       (CodeThingol.fold_constnames (insert (op =)) t []);
  1277                   val vars = init_syms
  1278                     |> CodeName.intro_vars consts;
  1279                 in
  1280                   semicolon [
  1281                     (str o classop_name class) classop,
  1282                     str "=",
  1283                     pr_term false vars NOBR t
  1284                   ]
  1285                 end;
  1286           in
  1287             Pretty.block_enclose (
  1288               Pretty.block [
  1289                 str "instance ",
  1290                 pr_typparms tyvars vs,
  1291                 str (class_name class ^ " "),
  1292                 pr_typ tyvars BR (tyco `%% map (ITyVar o fst) vs),
  1293                 str " where {"
  1294               ],
  1295               str "};"
  1296             ) (map pr_instdef classop_defs)
  1297           end;
  1298   in pr_def def end;
  1299 
  1300 fun pretty_haskell_monad c_mbind c_kbind =
  1301   let
  1302     fun pretty pr vars fxy [(t, _)] =
  1303       let
  1304         val pr_bind = pr_bind_haskell (K pr);
  1305         fun pr_mbind (NONE, t) vars =
  1306               (semicolon [pr vars NOBR t], vars)
  1307           | pr_mbind (SOME (bind, true), t) vars = vars
  1308               |> pr_bind NOBR bind
  1309               |>> (fn p => semicolon [p, str "<-", pr vars NOBR t])
  1310           | pr_mbind (SOME (bind, false), t) vars = vars
  1311               |> pr_bind NOBR bind
  1312               |>> (fn p => semicolon [str "let", p, str "=", pr vars NOBR t]);
  1313         val (binds, t) = implode_monad c_mbind c_kbind t;
  1314         val (ps, vars') = fold_map pr_mbind binds vars;
  1315         fun brack p = if eval_fxy BR fxy then Pretty.block [str "(", p, str ")"] else p;
  1316       in (brack o Pretty.block_enclose (str "do {", str "}")) (ps @| pr vars' NOBR t) end;
  1317   in (1, pretty) end;
  1318 
  1319 end; (*local*)
  1320 
  1321 fun seri_haskell module_prefix module destination string_classes labelled_name
  1322     reserved_syms raw_module_alias module_prolog class_syntax tyco_syntax const_syntax code =
  1323   let
  1324     val _ = Option.map File.check destination;
  1325     val is_cons = CodeThingol.is_cons code;
  1326     val module_alias = if is_some module then K module else raw_module_alias;
  1327     val init_names = Name.make_context reserved_syms;
  1328     val name_modl = mk_modl_name_tab init_names module_prefix module_alias code;
  1329     fun add_def (name, (def, deps)) =
  1330       let
  1331         val (modl, base) = dest_name name;
  1332         fun name_def base = Name.variants [base] #>> the_single;
  1333         fun add_fun upper (nsp_fun, nsp_typ) =
  1334           let
  1335             val (base', nsp_fun') = name_def (if upper then first_upper base else base) nsp_fun
  1336           in (base', (nsp_fun', nsp_typ)) end;
  1337         fun add_typ (nsp_fun, nsp_typ) =
  1338           let
  1339             val (base', nsp_typ') = name_def (first_upper base) nsp_typ
  1340           in (base', (nsp_fun, nsp_typ')) end;
  1341         val add_name =
  1342           case def
  1343            of CodeThingol.Bot => pair base
  1344             | CodeThingol.Fun _ => add_fun false
  1345             | CodeThingol.Datatype _ => add_typ
  1346             | CodeThingol.Datatypecons _ => add_fun true
  1347             | CodeThingol.Class _ => add_typ
  1348             | CodeThingol.Classrel _ => pair base
  1349             | CodeThingol.Classop _ => add_fun false
  1350             | CodeThingol.Classinst _ => pair base;
  1351         val modlname' = name_modl modl;
  1352         fun add_def base' =
  1353           case def
  1354            of CodeThingol.Bot => I
  1355             | CodeThingol.Datatypecons _ =>
  1356                 cons (name, ((NameSpace.append modlname' base', base'), NONE))
  1357             | CodeThingol.Classrel _ => I
  1358             | CodeThingol.Classop _ =>
  1359                 cons (name, ((NameSpace.append modlname' base', base'), NONE))
  1360             | _ => cons (name, ((NameSpace.append modlname' base', base'), SOME def));
  1361       in
  1362         Symtab.map_default (modlname', ([], ([], (init_names, init_names))))
  1363               (apfst (fold (insert (op = : string * string -> bool)) deps))
  1364         #> `(fn code => add_name ((snd o snd o the o Symtab.lookup code) modlname'))
  1365         #-> (fn (base', names) =>
  1366               (Symtab.map_entry modlname' o apsnd) (fn (defs, _) =>
  1367               (add_def base' defs, names)))
  1368       end;
  1369     val code' =
  1370       fold add_def (AList.make (fn name => (Graph.get_node code name, Graph.imm_succs code name))
  1371         (Graph.strong_conn code |> flat)) Symtab.empty;
  1372     val init_syms = CodeName.make_vars reserved_syms;
  1373     fun deresolv name =
  1374       (fst o fst o the o AList.lookup (op =) ((fst o snd o the
  1375         o Symtab.lookup code') ((name_modl o fst o dest_name) name))) name
  1376         handle Option => error ("Unknown definition name: " ^ labelled_name name);
  1377     fun deresolv_here name =
  1378       (snd o fst o the o AList.lookup (op =) ((fst o snd o the
  1379         o Symtab.lookup code') ((name_modl o fst o dest_name) name))) name
  1380         handle Option => error ("Unknown definition name: " ^ labelled_name name);
  1381     fun deriving_show tyco =
  1382       let
  1383         fun deriv _ "fun" = false
  1384           | deriv tycos tyco = member (op =) tycos tyco orelse
  1385               case the_default CodeThingol.Bot (try (Graph.get_node code) tyco)
  1386                of CodeThingol.Bot => true
  1387                 | CodeThingol.Datatype (_, cs) => forall (deriv' (tyco :: tycos))
  1388                     (maps snd cs)
  1389         and deriv' tycos (tyco `%% tys) = deriv tycos tyco
  1390               andalso forall (deriv' tycos) tys
  1391           | deriv' _ (ITyVar _) = true
  1392       in deriv [] tyco end;
  1393     fun seri_def qualified = pr_haskell class_syntax tyco_syntax const_syntax labelled_name init_syms
  1394       deresolv_here (if qualified then deresolv else deresolv_here) is_cons
  1395       (if string_classes then deriving_show else K false);
  1396     fun write_module (SOME destination) modlname =
  1397           let
  1398             val filename = case modlname
  1399              of "" => Path.explode "Main.hs"
  1400               | _ => (Path.ext "hs" o Path.explode o implode o separate "/" o NameSpace.explode) modlname;
  1401             val pathname = Path.append destination filename;
  1402             val _ = File.mkdir (Path.dir pathname);
  1403           in File.write pathname end
  1404       | write_module NONE _ = writeln;
  1405     fun seri_module (modlname', (imports, (defs, _))) =
  1406       let
  1407         val imports' =
  1408           imports
  1409           |> map (name_modl o fst o dest_name)
  1410           |> distinct (op =)
  1411           |> remove (op =) modlname';
  1412         val qualified =
  1413           imports @ map fst defs
  1414           |> map_filter (try deresolv)
  1415           |> map NameSpace.base
  1416           |> has_duplicates (op =);
  1417         val mk_import = str o (if qualified
  1418           then prefix "import qualified "
  1419           else prefix "import ") o suffix ";";
  1420       in
  1421         Pretty.chunks (
  1422           str ("module " ^ modlname' ^ " where {")
  1423           :: str ""
  1424           :: map mk_import imports'
  1425           @ str ""
  1426           :: separate (str "") ((case module_prolog modlname'
  1427              of SOME prolog => [prolog]
  1428               | NONE => [])
  1429           @ map_filter
  1430             (fn (name, (_, SOME def)) => SOME (seri_def qualified (name, def))
  1431               | (_, (_, NONE)) => NONE) defs)
  1432           @ str ""
  1433           @@ str "}"
  1434         )
  1435         |> code_output
  1436         |> write_module destination modlname'
  1437       end;
  1438   in Symtab.fold (fn modl => fn () => seri_module modl) code' () end;
  1439 
  1440 fun isar_seri_haskell module file =
  1441   let
  1442     val destination = case file
  1443      of NONE => error ("Haskell: no internal compilation")
  1444       | SOME "-" => NONE
  1445       | SOME file => SOME (Path.explode file)
  1446   in
  1447     parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name)
  1448       -- Scan.optional (Args.$$$ "string_classes" >> K true) false
  1449       >> (fn (module_prefix, string_classes) =>
  1450         seri_haskell module_prefix module destination string_classes))
  1451   end;
  1452 
  1453 
  1454 (** diagnosis serializer **)
  1455 
  1456 fun seri_diagnosis labelled_name _ _ _ _ _ _ code =
  1457   let
  1458     val init_names = CodeName.make_vars [];
  1459     fun pr_fun "fun" = SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
  1460           brackify_infix (1, R) fxy [
  1461             pr_typ (INFX (1, X)) ty1,
  1462             str "->",
  1463             pr_typ (INFX (1, R)) ty2
  1464           ])
  1465       | pr_fun _ = NONE
  1466     val pr = pr_haskell (K NONE) pr_fun (K NONE) labelled_name init_names I I (K false) (K false);
  1467   in
  1468     []
  1469     |> Graph.fold (fn (name, (def, _)) => case try pr (name, def) of SOME p => cons p | NONE => I) code
  1470     |> Pretty.chunks2
  1471     |> code_output
  1472     |> writeln
  1473   end;
  1474 
  1475 
  1476 
  1477 (** theory data **)
  1478 
  1479 datatype syntax_expr = SyntaxExpr of {
  1480   class: (string * (string -> string option)) Symtab.table,
  1481   inst: unit Symtab.table,
  1482   tyco: typ_syntax Symtab.table,
  1483   const: term_syntax Symtab.table
  1484 };
  1485 
  1486 fun mk_syntax_expr ((class, inst), (tyco, const)) =
  1487   SyntaxExpr { class = class, inst = inst, tyco = tyco, const = const };
  1488 fun map_syntax_expr f (SyntaxExpr { class, inst, tyco, const }) =
  1489   mk_syntax_expr (f ((class, inst), (tyco, const)));
  1490 fun merge_syntax_expr (SyntaxExpr { class = class1, inst = inst1, tyco = tyco1, const = const1 },
  1491     SyntaxExpr { class = class2, inst = inst2, tyco = tyco2, const = const2 }) =
  1492   mk_syntax_expr (
  1493     (Symtab.join (K snd) (class1, class2),
  1494        Symtab.join (K snd) (inst1, inst2)),
  1495     (Symtab.join (K snd) (tyco1, tyco2),
  1496        Symtab.join (K snd) (const1, const2))
  1497   );
  1498 
  1499 datatype syntax_modl = SyntaxModl of {
  1500   alias: string Symtab.table,
  1501   prolog: Pretty.T Symtab.table
  1502 };
  1503 
  1504 fun mk_syntax_modl (alias, prolog) =
  1505   SyntaxModl { alias = alias, prolog = prolog };
  1506 fun map_syntax_modl f (SyntaxModl { alias, prolog }) =
  1507   mk_syntax_modl (f (alias, prolog));
  1508 fun merge_syntax_modl (SyntaxModl { alias = alias1, prolog = prolog1 },
  1509     SyntaxModl { alias = alias2, prolog = prolog2 }) =
  1510   mk_syntax_modl (
  1511     Symtab.join (K snd) (alias1, alias2),
  1512     Symtab.join (K snd) (prolog1, prolog2)
  1513   );
  1514 
  1515 type serializer =
  1516   string option
  1517   -> string option
  1518   -> Args.T list
  1519   -> (string -> string)
  1520   -> string list
  1521   -> (string -> string option)
  1522   -> (string -> Pretty.T option)
  1523   -> (string -> class_syntax option)
  1524   -> (string -> typ_syntax option)
  1525   -> (string -> term_syntax option)
  1526   -> CodeThingol.code -> unit;
  1527 
  1528 datatype target = Target of {
  1529   serial: serial,
  1530   serializer: serializer,
  1531   syntax_expr: syntax_expr,
  1532   syntax_modl: syntax_modl,
  1533   reserved: string list
  1534 };
  1535 
  1536 fun mk_target (serial, ((serializer, reserved), (syntax_expr, syntax_modl))) =
  1537   Target { serial = serial, reserved = reserved, serializer = serializer, syntax_expr = syntax_expr, syntax_modl = syntax_modl };
  1538 fun map_target f ( Target { serial, serializer, reserved, syntax_expr, syntax_modl } ) =
  1539   mk_target (f (serial, ((serializer, reserved), (syntax_expr, syntax_modl))));
  1540 fun merge_target target (Target { serial = serial1, serializer = serializer, reserved = reserved1,
  1541   syntax_expr = syntax_expr1, syntax_modl = syntax_modl1 },
  1542     Target { serial = serial2, serializer = _, reserved = reserved2,
  1543       syntax_expr = syntax_expr2, syntax_modl = syntax_modl2 }) =
  1544   if serial1 = serial2 then
  1545     mk_target (serial1, ((serializer, merge (op =) (reserved1, reserved2)),
  1546       (merge_syntax_expr (syntax_expr1, syntax_expr2),
  1547         merge_syntax_modl (syntax_modl1, syntax_modl2))
  1548     ))
  1549   else
  1550     error ("Incompatible serializers: " ^ quote target);
  1551 
  1552 structure CodeTargetData = TheoryDataFun
  1553 (
  1554   type T = target Symtab.table;
  1555   val empty = Symtab.empty;
  1556   val copy = I;
  1557   val extend = I;
  1558   fun merge _ = Symtab.join merge_target;
  1559 );
  1560 
  1561 fun the_serializer (Target { serializer, ... }) = serializer;
  1562 fun the_reserved (Target { reserved, ... }) = reserved;
  1563 fun the_syntax_expr (Target { syntax_expr = SyntaxExpr x, ... }) = x;
  1564 fun the_syntax_modl (Target { syntax_modl = SyntaxModl x, ... }) = x;
  1565 
  1566 fun assert_serializer thy target =
  1567   case Symtab.lookup (CodeTargetData.get thy) target
  1568    of SOME data => target
  1569     | NONE => error ("Unknown code target language: " ^ quote target);
  1570 
  1571 fun add_serializer (target, seri) thy =
  1572   let
  1573     val _ = case Symtab.lookup (CodeTargetData.get thy) target
  1574      of SOME _ => warning ("overwriting existing serializer " ^ quote target)
  1575       | NONE => ();
  1576   in
  1577     thy
  1578     |> (CodeTargetData.map oo Symtab.map_default)
  1579           (target, mk_target (serial (), ((seri, []),
  1580             (mk_syntax_expr ((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)),
  1581               mk_syntax_modl (Symtab.empty, Symtab.empty)))))
  1582           (map_target (fn (serial, ((_, keywords), syntax)) => (serial, ((seri, keywords), syntax))))
  1583   end;
  1584 
  1585 fun map_seri_data target f thy =
  1586   let
  1587     val _ = assert_serializer thy target;
  1588   in
  1589     thy
  1590     |> (CodeTargetData.map o Symtab.map_entry target o map_target) f
  1591   end;
  1592 
  1593 val target_SML = "SML";
  1594 val target_OCaml = "OCaml";
  1595 val target_Haskell = "Haskell";
  1596 val target_diag = "diag";
  1597 
  1598 fun get_serializer thy target permissive module file args labelled_name = fn cs =>
  1599   let
  1600     val data = case Symtab.lookup (CodeTargetData.get thy) target
  1601      of SOME data => data
  1602       | NONE => error ("Unknown code target language: " ^ quote target);
  1603     val seri = the_serializer data;
  1604     val reserved = the_reserved data;
  1605     val { alias, prolog } = the_syntax_modl data;
  1606     val { class, inst, tyco, const } = the_syntax_expr data;
  1607     val project = if target = target_diag then I
  1608       else CodeThingol.project_code permissive
  1609         (Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const) cs;
  1610     fun check_empty_funs code = case CodeThingol.empty_funs code
  1611      of [] => code
  1612       | names => error ("No defining equations for " ^ commas (map (labelled_name thy) names));
  1613   in
  1614     project
  1615     #> check_empty_funs
  1616     #> seri module file args (labelled_name thy) reserved (Symtab.lookup alias) (Symtab.lookup prolog)
  1617       (Symtab.lookup class) (Symtab.lookup tyco) (Symtab.lookup const)
  1618   end;
  1619 
  1620 fun eval_term thy (ref_name, reff) code (t, ty) args =
  1621   let
  1622     val val_name = "Isabelle_Eval.EVAL.EVAL";
  1623     val val_name' = "Isabelle_Eval.EVAL";
  1624     val val_name'_args = space_implode " " (val_name' :: map (enclose "(" ")") args);
  1625     val seri = get_serializer thy "SML" false (SOME "Isabelle_Eval") NONE [] CodeName.labelled_name;
  1626     fun eval code = (
  1627       reff := NONE;
  1628       seri (SOME [val_name]) code;
  1629       use_text "generated code for evaluation" Output.ml_output (!eval_verbose)
  1630         ("val _ = (" ^ ref_name ^ " := SOME (" ^ val_name'_args ^ "))");
  1631       case !reff
  1632        of NONE => error ("Could not retrieve value of ML reference " ^ quote ref_name
  1633             ^ " (reference probably has been shadowed)")
  1634         | SOME value => value
  1635       );
  1636   in
  1637     code
  1638     |> CodeThingol.add_eval_def (val_name, (t, ty))
  1639     |> eval
  1640   end;
  1641 
  1642 
  1643 
  1644 (** optional pretty serialization **)
  1645 
  1646 local
  1647 
  1648 val pretty : (string * {
  1649     pretty_char: string -> string,
  1650     pretty_string: string -> string,
  1651     pretty_numeral: bool -> IntInf.int -> string,
  1652     pretty_list: Pretty.T list -> Pretty.T,
  1653     infix_cons: int * string
  1654   }) list = [
  1655   ("SML", { pretty_char = prefix "#" o quote o ML_Syntax.print_char,
  1656       pretty_string = ML_Syntax.print_string,
  1657       pretty_numeral = fn unbounded => fn k =>
  1658         if unbounded then "(" ^ IntInf.toString k ^ " : IntInf.int)"
  1659         else IntInf.toString k,
  1660       pretty_list = Pretty.enum "," "[" "]",
  1661       infix_cons = (7, "::")}),
  1662   ("OCaml", { pretty_char = fn c => enclose "'" "'"
  1663         (let val i = ord c
  1664           in if i < 32 orelse i = 39 orelse i = 92
  1665             then prefix "\\" (string_of_int i)
  1666             else c
  1667           end),
  1668       pretty_string = (fn _ => error "OCaml: no pretty strings"),
  1669       pretty_numeral = fn unbounded => fn k => if k >= IntInf.fromInt 0 then
  1670             if unbounded then
  1671               "(Big_int.big_int_of_int " ^ IntInf.toString k ^ ")"
  1672             else IntInf.toString k
  1673           else
  1674             if unbounded then
  1675               "(Big_int.big_int_of_int " ^ (enclose "(" ")" o prefix "-"
  1676                 o IntInf.toString o op ~) k ^ ")"
  1677             else (enclose "(" ")" o prefix "-" o IntInf.toString o op ~) k,
  1678       pretty_list = Pretty.enum ";" "[" "]",
  1679       infix_cons = (6, "::")}),
  1680   ("Haskell", { pretty_char = fn c => enclose "'" "'"
  1681         (let val i = ord c
  1682           in if i < 32 orelse i = 39 orelse i = 92
  1683             then Library.prefix "\\" (string_of_int i)
  1684             else c
  1685           end),
  1686       pretty_string = ML_Syntax.print_string,
  1687       pretty_numeral = fn unbounded => fn k => if k >= IntInf.fromInt 0 then
  1688             IntInf.toString k
  1689           else
  1690             (enclose "(" ")" o Library.prefix "-" o IntInf.toString o IntInf.~) k,
  1691       pretty_list = Pretty.enum "," "[" "]",
  1692       infix_cons = (5, ":")})
  1693 ];
  1694 
  1695 in
  1696 
  1697 fun pr_pretty target = case AList.lookup (op =) pretty target
  1698  of SOME x => x
  1699   | NONE => error ("Unknown code target language: " ^ quote target);
  1700 
  1701 fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
  1702   brackify_infix (target_fxy, R) fxy [
  1703     pr (INFX (target_fxy, X)) t1,
  1704     str target_cons,
  1705     pr (INFX (target_fxy, R)) t2
  1706   ];
  1707 
  1708 fun pretty_list c_nil c_cons target =
  1709   let
  1710     val pretty_ops = pr_pretty target;
  1711     val mk_list = #pretty_list pretty_ops;
  1712     fun pretty pr vars fxy [(t1, _), (t2, _)] =
  1713       case Option.map (cons t1) (implode_list c_nil c_cons t2)
  1714        of SOME ts => mk_list (map (pr vars NOBR) ts)
  1715         | NONE => default_list (#infix_cons pretty_ops) (pr vars) fxy t1 t2;
  1716   in (2, pretty) end;
  1717 
  1718 fun pretty_list_string c_nil c_cons c_char c_nibbles target =
  1719   let
  1720     val pretty_ops = pr_pretty target;
  1721     val mk_list = #pretty_list pretty_ops;
  1722     val mk_char = #pretty_char pretty_ops;
  1723     val mk_string = #pretty_string pretty_ops;
  1724     fun pretty pr vars fxy [(t1, _), (t2, _)] =
  1725       case Option.map (cons t1) (implode_list c_nil c_cons t2)
  1726        of SOME ts => case implode_string c_char c_nibbles mk_char mk_string ts
  1727            of SOME p => p
  1728             | NONE => mk_list (map (pr vars NOBR) ts)
  1729         | NONE => default_list (#infix_cons pretty_ops) (pr vars) fxy t1 t2;
  1730   in (2, pretty) end;
  1731 
  1732 fun pretty_char c_char c_nibbles target =
  1733   let
  1734     val mk_char = #pretty_char (pr_pretty target);
  1735     fun pretty _ _ _ [(t1, _), (t2, _)] =
  1736       case decode_char c_nibbles (t1, t2)
  1737        of SOME c => (str o mk_char) c
  1738         | NONE => error "Illegal character expression";
  1739   in (2, pretty) end;
  1740 
  1741 fun pretty_numeral unbounded c_bit0 c_bit1 c_pls c_min c_bit target =
  1742   let
  1743     val mk_numeral = #pretty_numeral (pr_pretty target);
  1744     fun pretty _ _ _ [(t, _)] =
  1745       case implode_numeral c_bit0 c_bit1 c_pls c_min c_bit t
  1746        of SOME k => (str o mk_numeral unbounded) k
  1747         | NONE => error "Illegal numeral expression";
  1748   in (1, pretty) end;
  1749 
  1750 fun pretty_ml_string c_char c_nibbles c_nil c_cons target =
  1751   let
  1752     val pretty_ops = pr_pretty target;
  1753     val mk_char = #pretty_char pretty_ops;
  1754     val mk_string = #pretty_string pretty_ops;
  1755     fun pretty pr vars fxy [(t, _)] =
  1756       case implode_list c_nil c_cons t
  1757        of SOME ts => (case implode_string c_char c_nibbles mk_char mk_string ts
  1758            of SOME p => p
  1759             | NONE => error "Illegal ml_string expression")
  1760         | NONE => error "Illegal ml_string expression";
  1761   in (1, pretty) end;
  1762 
  1763 val pretty_imperative_monad_bind =
  1764   let
  1765     fun pretty (pr : CodeName.var_ctxt -> fixity -> iterm -> Pretty.T)
  1766           vars fxy [(t1, _), ((v, ty) `|-> t2, _)] =
  1767             pr vars fxy (ICase (((t1, ty), ([(IVar v, t2)])), IVar ""))
  1768       | pretty pr vars fxy [(t1, _), (t2, ty2)] =
  1769           let
  1770             (*this code suffers from the lack of a proper concept for bindings*)
  1771             val vs = CodeThingol.fold_varnames cons t2 [];
  1772             val v = Name.variant vs "x";
  1773             val vars' = CodeName.intro_vars [v] vars;
  1774             val var = IVar v;
  1775             val ty = (hd o fst o CodeThingol.unfold_fun) ty2;
  1776           in pr vars' fxy (ICase (((t1, ty), ([(var, t2 `$ var)])), IVar "")) end;
  1777   in (2, pretty) end;
  1778 
  1779 end; (*local*)
  1780 
  1781 (** ML and Isar interface **)
  1782 
  1783 local
  1784 
  1785 fun map_syntax_exprs target =
  1786   map_seri_data target o apsnd o apsnd o apfst o map_syntax_expr;
  1787 fun map_syntax_modls target =
  1788   map_seri_data target o apsnd o apsnd o apsnd o map_syntax_modl;
  1789 fun map_reserveds target =
  1790   map_seri_data target o apsnd o apfst o apsnd;
  1791 
  1792 fun gen_add_syntax_class prep_class prep_const target raw_class raw_syn thy =
  1793   let
  1794     val cls = prep_class thy raw_class;
  1795     val class = CodeName.class thy cls;
  1796     fun mk_classop c = case AxClass.class_of_param thy c
  1797      of SOME class' => if cls = class' then CodeName.const thy c
  1798           else error ("Not a class operation for class " ^ quote class ^ ": " ^ quote c)
  1799       | NONE => error ("Not a class operation: " ^ quote c);
  1800     fun mk_syntax_ops raw_ops = AList.lookup (op =)
  1801       ((map o apfst) (mk_classop o prep_const thy) raw_ops);
  1802   in case raw_syn
  1803    of SOME (syntax, raw_ops) =>
  1804       thy
  1805       |> (map_syntax_exprs target o apfst o apfst)
  1806            (Symtab.update (class, (syntax, mk_syntax_ops raw_ops)))
  1807     | NONE =>
  1808       thy
  1809       |> (map_syntax_exprs target o apfst o apfst)
  1810            (Symtab.delete_safe class)
  1811   end;
  1812 
  1813 fun gen_add_syntax_inst prep_class prep_tyco target (raw_tyco, raw_class) add_del thy =
  1814   let
  1815     val inst = CodeName.instance thy (prep_class thy raw_class, prep_tyco thy raw_tyco);
  1816   in if add_del then
  1817     thy
  1818     |> (map_syntax_exprs target o apfst o apsnd)
  1819         (Symtab.update (inst, ()))
  1820   else
  1821     thy
  1822     |> (map_syntax_exprs target o apfst o apsnd)
  1823         (Symtab.delete_safe inst)
  1824   end;
  1825 
  1826 fun gen_add_syntax_tyco prep_tyco target raw_tyco raw_syn thy =
  1827   let
  1828     val tyco = prep_tyco thy raw_tyco;
  1829     val tyco' = if tyco = "fun" then "fun" else CodeName.tyco thy tyco;
  1830     fun check_args (syntax as (n, _)) = if n <> Sign.arity_number thy tyco
  1831       then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
  1832       else syntax
  1833   in case raw_syn
  1834    of SOME syntax =>
  1835       thy
  1836       |> (map_syntax_exprs target o apsnd o apfst)
  1837            (Symtab.update (tyco', check_args syntax))
  1838    | NONE =>
  1839       thy
  1840       |> (map_syntax_exprs target o apsnd o apfst)
  1841            (Symtab.delete_safe tyco')
  1842   end;
  1843 
  1844 fun gen_add_syntax_const prep_const target raw_c raw_syn thy =
  1845   let
  1846     val c = prep_const thy raw_c;
  1847     val c' = CodeName.const thy c;
  1848     fun check_args (syntax as (n, _)) = if n > CodeUnit.no_args thy c
  1849       then error ("Too many arguments in syntax for constant " ^ quote c)
  1850       else syntax;
  1851   in case raw_syn
  1852    of SOME syntax =>
  1853       thy
  1854       |> (map_syntax_exprs target o apsnd o apsnd)
  1855            (Symtab.update (c', check_args syntax))
  1856    | NONE =>
  1857       thy
  1858       |> (map_syntax_exprs target o apsnd o apsnd)
  1859            (Symtab.delete_safe c')
  1860   end;
  1861 
  1862 fun cert_class thy class =
  1863   let
  1864     val _ = AxClass.get_definition thy class;
  1865   in class end;
  1866 
  1867 fun read_class thy raw_class =
  1868   let
  1869     val class = Sign.intern_class thy raw_class;
  1870     val _ = AxClass.get_definition thy class;
  1871   in class end;
  1872 
  1873 fun cert_tyco thy tyco =
  1874   let
  1875     val _ = if Sign.declared_tyname thy tyco then ()
  1876       else error ("No such type constructor: " ^ quote tyco);
  1877   in tyco end;
  1878 
  1879 fun read_tyco thy raw_tyco =
  1880   let
  1881     val tyco = Sign.intern_type thy raw_tyco;
  1882     val _ = if Sign.declared_tyname thy tyco then ()
  1883       else error ("No such type constructor: " ^ quote raw_tyco);
  1884   in tyco end;
  1885 
  1886 fun no_bindings x = (Option.map o apsnd)
  1887   (fn pretty => fn pr => fn vars => pretty (pr vars)) x;
  1888 
  1889 fun gen_add_haskell_monad prep_const c_run c_mbind c_kbind thy =
  1890   let
  1891     val c_run' = prep_const thy c_run;
  1892     val c_mbind' = prep_const thy c_mbind;
  1893     val c_mbind'' = CodeName.const thy c_mbind';
  1894     val c_kbind' = prep_const thy c_kbind;
  1895     val c_kbind'' = CodeName.const thy c_kbind';
  1896     val pr = pretty_haskell_monad c_mbind'' c_kbind''
  1897   in
  1898     thy
  1899     |> gen_add_syntax_const (K I) target_Haskell c_run' (SOME pr)
  1900     |> gen_add_syntax_const (K I) target_Haskell c_mbind'
  1901           (no_bindings (SOME (parse_infix fst (L, 1) ">>=")))
  1902     |> gen_add_syntax_const (K I) target_Haskell c_kbind'
  1903           (no_bindings (SOME (parse_infix fst (L, 1) ">>")))
  1904   end;
  1905 
  1906 fun add_reserved target =
  1907   let
  1908     fun add sym syms = if member (op =) syms sym
  1909       then error ("Reserved symbol " ^ quote sym ^ " already declared")
  1910       else insert (op =) sym syms
  1911   in map_reserveds target o add end;
  1912 
  1913 fun add_modl_alias target =
  1914   map_syntax_modls target o apfst o Symtab.update o apsnd CodeName.check_modulename;
  1915 
  1916 fun add_modl_prolog target =
  1917   map_syntax_modls target o apsnd o
  1918     (fn (modl, NONE) => Symtab.delete modl | (modl, SOME prolog) =>
  1919       Symtab.update (modl, Pretty.str prolog));
  1920 
  1921 fun zip_list (x::xs) f g =
  1922   f
  1923   #-> (fn y =>
  1924     fold_map (fn x => g |-- f >> pair x) xs
  1925     #-> (fn xys => pair ((x, y) :: xys)));
  1926 
  1927 structure P = OuterParse
  1928 and K = OuterKeyword
  1929 
  1930 fun parse_multi_syntax parse_thing parse_syntax =
  1931   P.and_list1 parse_thing
  1932   #-> (fn things => Scan.repeat1 (P.$$$ "(" |-- P.name --
  1933         (zip_list things parse_syntax (P.$$$ "and")) --| P.$$$ ")"));
  1934 
  1935 val (infixK, infixlK, infixrK) = ("infix", "infixl", "infixr");
  1936 
  1937 fun parse_syntax prep_arg xs =
  1938   Scan.option ((
  1939       ((P.$$$ infixK  >> K X)
  1940         || (P.$$$ infixlK >> K L)
  1941         || (P.$$$ infixrK >> K R))
  1942         -- P.nat >> parse_infix prep_arg
  1943       || Scan.succeed (parse_mixfix prep_arg))
  1944       -- P.string
  1945       >> (fn (parse, s) => parse s)) xs;
  1946 
  1947 val (code_classK, code_instanceK, code_typeK, code_constK, code_monadK,
  1948   code_reservedK, code_modulenameK, code_moduleprologK) =
  1949   ("code_class", "code_instance", "code_type", "code_const", "code_monad",
  1950     "code_reserved", "code_modulename", "code_moduleprolog");
  1951 
  1952 in
  1953 
  1954 val parse_syntax = parse_syntax;
  1955 
  1956 val add_syntax_class = gen_add_syntax_class cert_class (K I);
  1957 val add_syntax_inst = gen_add_syntax_inst cert_class cert_tyco;
  1958 val add_syntax_tyco = gen_add_syntax_tyco cert_tyco;
  1959 val add_syntax_const = gen_add_syntax_const (K I);
  1960 
  1961 val add_syntax_class_cmd = gen_add_syntax_class read_class CodeUnit.read_const;
  1962 val add_syntax_inst_cmd = gen_add_syntax_inst read_class read_tyco;
  1963 val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco;
  1964 val add_syntax_const_cmd = gen_add_syntax_const CodeUnit.read_const;
  1965 
  1966 fun add_syntax_tycoP target tyco = parse_syntax I >> add_syntax_tyco_cmd target tyco;
  1967 fun add_syntax_constP target c = parse_syntax fst >> (add_syntax_const_cmd target c o no_bindings);
  1968 
  1969 fun add_undefined target undef target_undefined thy =
  1970   let
  1971     fun pr _ _ _ _ = str target_undefined;
  1972   in
  1973     thy
  1974     |> add_syntax_const target undef (SOME (~1, pr))
  1975   end;
  1976 
  1977 fun add_pretty_list target nill cons thy =
  1978   let
  1979     val nil' = CodeName.const thy nill;
  1980     val cons' = CodeName.const thy cons;
  1981     val pr = pretty_list nil' cons' target;
  1982   in
  1983     thy
  1984     |> add_syntax_const target cons (SOME pr)
  1985   end;
  1986 
  1987 fun add_pretty_list_string target nill cons charr nibbles thy =
  1988   let
  1989     val nil' = CodeName.const thy nill;
  1990     val cons' = CodeName.const thy cons;
  1991     val charr' = CodeName.const thy charr;
  1992     val nibbles' = map (CodeName.const thy) nibbles;
  1993     val pr = pretty_list_string nil' cons' charr' nibbles' target;
  1994   in
  1995     thy
  1996     |> add_syntax_const target cons (SOME pr)
  1997   end;
  1998 
  1999 fun add_pretty_char target charr nibbles thy =
  2000   let
  2001     val charr' = CodeName.const thy charr;
  2002     val nibbles' = map (CodeName.const thy) nibbles;
  2003     val pr = pretty_char charr' nibbles' target;
  2004   in
  2005     thy
  2006     |> add_syntax_const target charr (SOME pr)
  2007   end;
  2008 
  2009 fun add_pretty_numeral target unbounded number_of b0 b1 pls min bit thy =
  2010   let
  2011     val b0' = CodeName.const thy b0;
  2012     val b1' = CodeName.const thy b1;
  2013     val pls' = CodeName.const thy pls;
  2014     val min' = CodeName.const thy min;
  2015     val bit' = CodeName.const thy bit;
  2016     val pr = pretty_numeral unbounded b0' b1' pls' min' bit' target;
  2017   in
  2018     thy
  2019     |> add_syntax_const target number_of (SOME pr)
  2020   end;
  2021 
  2022 fun add_pretty_ml_string target charr nibbles nill cons str thy =
  2023   let
  2024     val charr' = CodeName.const thy charr;
  2025     val nibbles' = map (CodeName.const thy) nibbles;
  2026     val nil' = CodeName.const thy nill;
  2027     val cons' = CodeName.const thy cons;
  2028     val pr = pretty_ml_string charr' nibbles' nil' cons' target;
  2029   in
  2030     thy
  2031     |> add_syntax_const target str (SOME pr)
  2032   end;
  2033 
  2034 fun add_pretty_imperative_monad_bind target bind thy =
  2035   let
  2036     val pr = pretty_imperative_monad_bind
  2037   in
  2038     thy
  2039     |> add_syntax_const target bind (SOME pr)
  2040   end;
  2041 
  2042 val add_haskell_monad = gen_add_haskell_monad CodeUnit.read_const;
  2043 
  2044 val code_classP =
  2045   OuterSyntax.command code_classK "define code syntax for class" K.thy_decl (
  2046     parse_multi_syntax P.xname
  2047       (Scan.option (P.string -- Scan.optional (P.$$$ "where" |-- Scan.repeat1
  2048         (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.string)) []))
  2049     >> (Toplevel.theory oo fold) (fn (target, syns) =>
  2050           fold (fn (raw_class, syn) => add_syntax_class_cmd target raw_class syn) syns)
  2051   );
  2052 
  2053 val code_instanceP =
  2054   OuterSyntax.command code_instanceK "define code syntax for instance" K.thy_decl (
  2055     parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname)
  2056       ((P.minus >> K true) || Scan.succeed false)
  2057     >> (Toplevel.theory oo fold) (fn (target, syns) =>
  2058           fold (fn (raw_inst, add_del) => add_syntax_inst_cmd target raw_inst add_del) syns)
  2059   );
  2060 
  2061 val code_typeP =
  2062   OuterSyntax.command code_typeK "define code syntax for type constructor" K.thy_decl (
  2063     parse_multi_syntax P.xname (parse_syntax I)
  2064     >> (Toplevel.theory oo fold) (fn (target, syns) =>
  2065           fold (fn (raw_tyco, syn) => add_syntax_tyco_cmd target raw_tyco syn) syns)
  2066   );
  2067 
  2068 val code_constP =
  2069   OuterSyntax.command code_constK "define code syntax for constant" K.thy_decl (
  2070     parse_multi_syntax P.term (parse_syntax fst)
  2071     >> (Toplevel.theory oo fold) (fn (target, syns) =>
  2072           fold (fn (raw_const, syn) => add_syntax_const_cmd target raw_const (no_bindings syn)) syns)
  2073   );
  2074 
  2075 val code_monadP =
  2076   OuterSyntax.command code_monadK "define code syntax for Haskell monads" K.thy_decl (
  2077     P.term -- P.term -- P.term
  2078     >> (fn ((raw_run, raw_mbind), raw_kbind) => Toplevel.theory 
  2079           (add_haskell_monad raw_run raw_mbind raw_kbind))
  2080   );
  2081 
  2082 val code_reservedP =
  2083   OuterSyntax.command code_reservedK "declare words as reserved for target language" K.thy_decl (
  2084     P.name -- Scan.repeat1 P.name
  2085     >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds)
  2086   )
  2087 
  2088 val code_modulenameP =
  2089   OuterSyntax.command code_modulenameK "alias module to other name" K.thy_decl (
  2090     P.name -- Scan.repeat1 (P.name -- P.name)
  2091     >> (fn (target, modlnames) => (Toplevel.theory o fold (add_modl_alias target)) modlnames)
  2092   )
  2093 
  2094 val code_moduleprologP =
  2095   OuterSyntax.command code_moduleprologK "add prolog to module" K.thy_decl (
  2096     P.name -- Scan.repeat1 (P.name -- (P.text >> (fn "-" => NONE | s => SOME s)))
  2097     >> (fn (target, prologs) => (Toplevel.theory o fold (add_modl_prolog target)) prologs)
  2098   )
  2099 
  2100 val _ = OuterSyntax.add_keywords [infixK, infixlK, infixrK];
  2101 
  2102 val _ = OuterSyntax.add_parsers [code_classP, code_instanceP, code_typeP, code_constP,
  2103   code_reservedP, code_modulenameP, code_moduleprologP, code_monadP];
  2104 
  2105 
  2106 (*including serializer defaults*)
  2107 val setup =
  2108   add_serializer (target_SML, isar_seri_sml)
  2109   #> add_serializer (target_OCaml, isar_seri_ocaml)
  2110   #> add_serializer (target_Haskell, isar_seri_haskell)
  2111   #> add_serializer (target_diag, fn _ => fn _ => fn _ => seri_diagnosis)
  2112   #> add_syntax_tyco "SML" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
  2113       (gen_brackify (case fxy of NOBR => false | _ => eval_fxy (INFX (1, R)) fxy) o Pretty.breaks) [
  2114         pr_typ (INFX (1, X)) ty1,
  2115         str "->",
  2116         pr_typ (INFX (1, R)) ty2
  2117       ]))
  2118   #> add_syntax_tyco "OCaml" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
  2119       (gen_brackify (case fxy of NOBR => false | _ => eval_fxy (INFX (1, R)) fxy) o Pretty.breaks) [
  2120         pr_typ (INFX (1, X)) ty1,
  2121         str "->",
  2122         pr_typ (INFX (1, R)) ty2
  2123       ]))
  2124   #> add_syntax_tyco "Haskell" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
  2125       brackify_infix (1, R) fxy [
  2126         pr_typ (INFX (1, X)) ty1,
  2127         str "->",
  2128         pr_typ (INFX (1, R)) ty2
  2129       ]))
  2130   #> fold (add_reserved "SML") ML_Syntax.reserved_names
  2131   #> fold (add_reserved "SML")
  2132       ["o" (*dictionary projections use it already*), "Fail", "div", "mod" (*standard infixes*)]
  2133   #> fold (add_reserved "OCaml") [
  2134       "and", "as", "assert", "begin", "class",
  2135       "constraint", "do", "done", "downto", "else", "end", "exception",
  2136       "external", "false", "for", "fun", "function", "functor", "if",
  2137       "in", "include", "inherit", "initializer", "lazy", "let", "match", "method",
  2138       "module", "mutable", "new", "object", "of", "open", "or", "private", "rec",
  2139       "sig", "struct", "then", "to", "true", "try", "type", "val",
  2140       "virtual", "when", "while", "with"
  2141     ]
  2142   #> fold (add_reserved "OCaml") ["failwith", "mod"]
  2143   #> fold (add_reserved "Haskell") [
  2144       "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
  2145       "import", "default", "forall", "let", "in", "class", "qualified", "data",
  2146       "newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
  2147     ]
  2148   #> fold (add_reserved "Haskell") [
  2149       "Prelude", "Main", "Bool", "Maybe", "Either", "Ordering", "Char", "String", "Int",
  2150       "Integer", "Float", "Double", "Rational", "IO", "Eq", "Ord", "Enum", "Bounded",
  2151       "Num", "Real", "Integral", "Fractional", "Floating", "RealFloat", "Monad", "Functor",
  2152       "AlreadyExists", "ArithException", "ArrayException", "AssertionFailed", "AsyncException",
  2153       "BlockedOnDeadMVar", "Deadlock", "Denormal", "DivideByZero", "DotNetException", "DynException",
  2154       "Dynamic", "EOF", "EQ", "EmptyRec", "ErrorCall", "ExitException", "ExitFailure",
  2155       "ExitSuccess", "False", "GT", "HeapOverflow",
  2156       "IOError", "IOException", "IllegalOperation",
  2157       "IndexOutOfBounds", "Just", "Key", "LT", "Left", "LossOfPrecision", "NoMethodError",
  2158       "NoSuchThing", "NonTermination", "Nothing", "Obj", "OtherError", "Overflow",
  2159       "PatternMatchFail", "PermissionDenied", "ProtocolError", "RecConError", "RecSelError",
  2160       "RecUpdError", "ResourceBusy", "ResourceExhausted", "Right", "StackOverflow",
  2161       "ThreadKilled", "True", "TyCon", "TypeRep", "UndefinedElement", "Underflow",
  2162       "UnsupportedOperation", "UserError", "abs", "absReal", "acos", "acosh", "all",
  2163       "and", "any", "appendFile", "asTypeOf", "asciiTab", "asin", "asinh", "atan",
  2164       "atan2", "atanh", "basicIORun", "blockIO", "boundedEnumFrom", "boundedEnumFromThen",
  2165       "boundedEnumFromThenTo", "boundedEnumFromTo", "boundedPred", "boundedSucc", "break",
  2166       "catch", "catchException", "ceiling", "compare", "concat", "concatMap", "const",
  2167       "cos", "cosh", "curry", "cycle", "decodeFloat", "denominator", "div", "divMod",
  2168       "doubleToRatio", "doubleToRational", "drop", "dropWhile", "either", "elem",
  2169       "emptyRec", "encodeFloat", "enumFrom", "enumFromThen", "enumFromThenTo",
  2170       "enumFromTo", "error", "even", "exp", "exponent", "fail", "filter", "flip",
  2171       "floatDigits", "floatProperFraction", "floatRadix", "floatRange", "floatToRational",
  2172       "floor", "fmap", "foldl", "foldl'", "foldl1", "foldr", "foldr1", "fromDouble",
  2173       "fromEnum", "fromEnum_0", "fromInt", "fromInteger", "fromIntegral", "fromObj",
  2174       "fromRational", "fst", "gcd", "getChar", "getContents", "getLine", "head",
  2175       "id", "inRange", "index", "init", "intToRatio", "interact", "ioError", "isAlpha",
  2176       "isAlphaNum", "isDenormalized", "isDigit", "isHexDigit", "isIEEE", "isInfinite",
  2177       "isLower", "isNaN", "isNegativeZero", "isOctDigit", "isSpace", "isUpper", "iterate", "iterate'",
  2178       "last", "lcm", "length", "lex", "lexDigits", "lexLitChar", "lexmatch", "lines", "log",
  2179       "logBase", "lookup", "loop", "map", "mapM", "mapM_", "max", "maxBound", "maximum",
  2180       "maybe", "min", "minBound", "minimum", "mod", "negate", "nonnull", "not", "notElem",
  2181       "null", "numerator", "numericEnumFrom", "numericEnumFromThen", "numericEnumFromThenTo",
  2182       "numericEnumFromTo", "odd", "or", "otherwise", "pi", "pred", 
  2183       "print", "product", "properFraction", "protectEsc", "putChar", "putStr", "putStrLn",
  2184       "quot", "quotRem", "range", "rangeSize", "rationalToDouble", "rationalToFloat",
  2185       "rationalToRealFloat", "read", "readDec", "readField", "readFieldName", "readFile",
  2186       "readFloat", "readHex", "readIO", "readInt", "readList", "readLitChar", "readLn",
  2187       "readOct", "readParen", "readSigned", "reads", "readsPrec", "realFloatToRational",
  2188       "realToFrac", "recip", "reduce", "rem", "repeat", "replicate", "return", "reverse",
  2189       "round", "scaleFloat", "scanl", "scanl1", "scanr", "scanr1", "seq", "sequence",
  2190       "sequence_", "show", "showChar", "showException", "showField", "showList",
  2191       "showLitChar", "showParen", "showString", "shows", "showsPrec", "significand",
  2192       "signum", "signumReal", "sin", "sinh", "snd", "span", "splitAt", "sqrt", "subtract",
  2193       "succ", "sum", "tail", "take", "takeWhile", "takeWhile1", "tan", "tanh", "threadToIOResult",
  2194       "throw", "toEnum", "toInt", "toInteger", "toObj", "toRational", "truncate", "uncurry",
  2195       "undefined", "unlines", "unsafeCoerce", "unsafeIndex", "unsafeRangeSize", "until", "unwords",
  2196       "unzip", "unzip3", "userError", "words", "writeFile", "zip", "zip3", "zipWith", "zipWith3"
  2197     ] (*due to weird handling of ':', we can't do anything else than to import *all* prelude symbols*);
  2198 
  2199 end; (*local*)
  2200 
  2201 end; (*struct*)