src/Tools/Code/code_ml.ML
author haftmann
Mon Jun 07 13:42:38 2010 +0200 (2010-06-07)
changeset 37384 5aba26803073
parent 37242 97097e589715
child 37437 4202e11ae7dc
permissions -rw-r--r--
more consistent naming aroud type classes and instances
     1 (*  Title:      Tools/code/code_ml.ML
     2     Author:     Florian Haftmann, TU Muenchen
     3 
     4 Serializer for SML and OCaml.
     5 *)
     6 
     7 signature CODE_ML =
     8 sig
     9   val target_SML: string
    10   val evaluation_code_of: theory -> string -> string
    11     -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
    12   val print_tuple: (Code_Printer.fixity -> 'a -> Pretty.T)
    13     -> Code_Printer.fixity -> 'a list -> Pretty.T option
    14   val setup: theory -> theory
    15 end;
    16 
    17 structure Code_ML : CODE_ML =
    18 struct
    19 
    20 open Basic_Code_Thingol;
    21 open Code_Printer;
    22 
    23 infixr 5 @@;
    24 infixr 5 @|;
    25 
    26 
    27 (** generic **)
    28 
    29 val target_SML = "SML";
    30 val target_OCaml = "OCaml";
    31 
    32 datatype ml_binding =
    33     ML_Function of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
    34   | ML_Instance of string * ((class * (string * (vname * sort) list))
    35         * (((class * (string * (string * dict list list))) list * (class * class) list list)
    36       * ((string * const) * (thm * bool)) list));
    37 
    38 datatype ml_stmt =
    39     ML_Exc of string * (typscheme * int)
    40   | ML_Val of ml_binding
    41   | ML_Funs of ml_binding list * string list
    42   | ML_Datas of (string * ((vname * sort) list * (string * itype list) list)) list
    43   | ML_Class of string * (vname * ((class * string) list * (string * itype) list));
    44 
    45 fun stmt_name_of_binding (ML_Function (name, _)) = name
    46   | stmt_name_of_binding (ML_Instance (name, _)) = name;
    47 
    48 fun stmt_names_of (ML_Exc (name, _)) = [name]
    49   | stmt_names_of (ML_Val binding) = [stmt_name_of_binding binding]
    50   | stmt_names_of (ML_Funs (bindings, _)) = map stmt_name_of_binding bindings
    51   | stmt_names_of (ML_Datas ds) = map fst ds
    52   | stmt_names_of (ML_Class (name, _)) = [name];
    53 
    54 fun print_product _ [] = NONE
    55   | print_product print [x] = SOME (print x)
    56   | print_product print xs = (SOME o enum " *" "" "") (map print xs);
    57 
    58 fun print_tuple _ _ [] = NONE
    59   | print_tuple print fxy [x] = SOME (print fxy x)
    60   | print_tuple print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs));
    61 
    62 
    63 (** SML serializer **)
    64 
    65 fun print_sml_stmt labelled_name syntax_tyco syntax_const reserved is_cons deresolve =
    66   let
    67     fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco
    68       | print_tyco_expr fxy (tyco, [ty]) =
    69           concat [print_typ BR ty, (str o deresolve) tyco]
    70       | print_tyco_expr fxy (tyco, tys) =
    71           concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]
    72     and print_typ fxy (tyco `%% tys) = (case syntax_tyco tyco
    73          of NONE => print_tyco_expr fxy (tyco, tys)
    74           | SOME (i, print) => print print_typ fxy tys)
    75       | print_typ fxy (ITyVar v) = str ("'" ^ v);
    76     fun print_dicttyp (class, ty) = print_tyco_expr NOBR (class, [ty]);
    77     fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
    78       (map_filter (fn (v, sort) =>
    79         (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
    80     fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);
    81     fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);
    82     fun print_dict is_pseudo_fun fxy (DictConst (inst, dss)) =
    83           brackify fxy ((str o deresolve) inst ::
    84             (if is_pseudo_fun inst then [str "()"]
    85             else map_filter (print_dicts is_pseudo_fun BR) dss))
    86       | print_dict is_pseudo_fun fxy (DictVar (classrels, (v, (i, k)))) =
    87           let
    88             val v_p = str (if k = 1 then first_upper v ^ "_"
    89               else first_upper v ^ string_of_int (i+1) ^ "_");
    90           in case classrels
    91            of [] => v_p
    92             | [classrel] => brackets [(str o deresolve) classrel, v_p]
    93             | classrels => brackets
    94                 [enum " o" "(" ")" (map (str o deresolve) classrels), v_p]
    95           end
    96     and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun);
    97     val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
    98       (map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort));
    99     fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
   100           print_app is_pseudo_fun some_thm vars fxy (c, [])
   101       | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
   102           str "_"
   103       | print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) =
   104           str (lookup_var vars v)
   105       | print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) =
   106           (case Code_Thingol.unfold_const_app t
   107            of SOME c_ts => print_app is_pseudo_fun some_thm vars fxy c_ts
   108             | NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1,
   109                 print_term is_pseudo_fun some_thm vars BR t2])
   110       | print_term is_pseudo_fun some_thm vars fxy (t as _ `|=> _) =
   111           let
   112             val (binds, t') = Code_Thingol.unfold_pat_abs t;
   113             fun print_abs (pat, ty) =
   114               print_bind is_pseudo_fun some_thm NOBR pat
   115               #>> (fn p => concat [str "fn", p, str "=>"]);
   116             val (ps, vars') = fold_map print_abs binds vars;
   117           in brackets (ps @ [print_term is_pseudo_fun some_thm vars' NOBR t']) end
   118       | print_term is_pseudo_fun some_thm vars fxy (ICase (cases as (_, t0))) =
   119           (case Code_Thingol.unfold_const_app t0
   120            of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
   121                 then print_case is_pseudo_fun some_thm vars fxy cases
   122                 else print_app is_pseudo_fun some_thm vars fxy c_ts
   123             | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
   124     and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), tys)), ts)) =
   125       if is_cons c then
   126         let val k = length tys in
   127           if k < 2 orelse length ts = k
   128           then (str o deresolve) c
   129             :: the_list (print_tuple (print_term is_pseudo_fun some_thm vars) BR ts)
   130           else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
   131         end
   132       else if is_pseudo_fun c
   133         then (str o deresolve) c @@ str "()"
   134       else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss
   135         @ map (print_term is_pseudo_fun some_thm vars BR) ts
   136     and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
   137       (print_term is_pseudo_fun) syntax_const some_thm vars
   138     and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
   139     and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =
   140           let
   141             val (binds, body) = Code_Thingol.unfold_let (ICase cases);
   142             fun print_match ((pat, ty), t) vars =
   143               vars
   144               |> print_bind is_pseudo_fun some_thm NOBR pat
   145               |>> (fn p => semicolon [str "val", p, str "=",
   146                     print_term is_pseudo_fun some_thm vars NOBR t])
   147             val (ps, vars') = fold_map print_match binds vars;
   148           in
   149             Pretty.chunks [
   150               Pretty.block [str "let", Pretty.fbrk, Pretty.chunks ps],
   151               Pretty.block [str "in", Pretty.fbrk, print_term is_pseudo_fun some_thm vars' NOBR body],
   152               str "end"
   153             ]
   154           end
   155       | print_case is_pseudo_fun some_thm vars fxy (((t, ty), clause :: clauses), _) =
   156           let
   157             fun print_select delim (pat, body) =
   158               let
   159                 val (p, vars') = print_bind is_pseudo_fun some_thm NOBR pat vars;
   160               in
   161                 concat [str delim, p, str "=>", print_term is_pseudo_fun some_thm vars' NOBR body]
   162               end;
   163           in
   164             brackets (
   165               str "case"
   166               :: print_term is_pseudo_fun some_thm vars NOBR t
   167               :: print_select "of" clause
   168               :: map (print_select "|") clauses
   169             )
   170           end
   171       | print_case is_pseudo_fun some_thm vars fxy ((_, []), _) =
   172           (concat o map str) ["raise", "Fail", "\"empty case\""];
   173     fun print_val_decl print_typscheme (name, typscheme) = concat
   174       [str "val", str (deresolve name), str ":", print_typscheme typscheme];
   175     fun print_datatype_decl definer (tyco, (vs, cos)) =
   176       let
   177         fun print_co (co, []) = str (deresolve co)
   178           | print_co (co, tys) = concat [str (deresolve co), str "of",
   179               enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
   180       in
   181         concat (
   182           str definer
   183           :: print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs)
   184           :: str "="
   185           :: separate (str "|") (map print_co cos)
   186         )
   187       end;
   188     fun print_def is_pseudo_fun needs_typ definer
   189           (ML_Function (name, (vs_ty as (vs, ty), eq :: eqs))) =
   190           let
   191             fun print_eqn definer ((ts, t), (some_thm, _)) =
   192               let
   193                 val consts = fold Code_Thingol.add_constnames (t :: ts) [];
   194                 val vars = reserved
   195                   |> intro_base_names
   196                        (is_none o syntax_const) deresolve consts
   197                   |> intro_vars ((fold o Code_Thingol.fold_varnames)
   198                        (insert (op =)) ts []);
   199                 val prolog = if needs_typ then
   200                   concat [str definer, (str o deresolve) name, str ":", print_typ NOBR ty]
   201                     else (concat o map str) [definer, deresolve name];
   202               in
   203                 concat (
   204                   prolog
   205                   :: (if is_pseudo_fun name then [str "()"]
   206                       else print_dict_args vs
   207                         @ map (print_term is_pseudo_fun some_thm vars BR) ts)
   208                   @ str "="
   209                   @@ print_term is_pseudo_fun some_thm vars NOBR t
   210                 )
   211               end
   212             val shift = if null eqs then I else
   213               map (Pretty.block o single o Pretty.block o single);
   214           in pair
   215             (print_val_decl print_typscheme (name, vs_ty))
   216             ((Pretty.block o Pretty.fbreaks o shift) (
   217               print_eqn definer eq
   218               :: map (print_eqn "|") eqs
   219             ))
   220           end
   221       | print_def is_pseudo_fun _ definer
   222           (ML_Instance (inst, ((class, (tyco, vs)), ((super_instances, _), classparam_instances)))) =
   223           let
   224             fun print_super_instance (_, (classrel, dss)) =
   225               concat [
   226                 (str o Long_Name.base_name o deresolve) classrel,
   227                 str "=",
   228                 print_dict is_pseudo_fun NOBR (DictConst dss)
   229               ];
   230             fun print_classparam_instance ((classparam, const), (thm, _)) =
   231               concat [
   232                 (str o Long_Name.base_name o deresolve) classparam,
   233                 str "=",
   234                 print_app (K false) (SOME thm) reserved NOBR (const, [])
   235               ];
   236           in pair
   237             (print_val_decl print_dicttypscheme
   238               (inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
   239             (concat (
   240               str definer
   241               :: (str o deresolve) inst
   242               :: (if is_pseudo_fun inst then [str "()"]
   243                   else print_dict_args vs)
   244               @ str "="
   245               :: enum "," "{" "}"
   246                 (map print_super_instance super_instances
   247                   @ map print_classparam_instance classparam_instances)
   248               :: str ":"
   249               @@ print_tyco_expr NOBR (class, [tyco `%% map (ITyVar o fst) vs])
   250             ))
   251           end;
   252     fun print_stmt (ML_Exc (name, (vs_ty, n))) = pair
   253           [print_val_decl print_typscheme (name, vs_ty)]
   254           ((semicolon o map str) (
   255             (if n = 0 then "val" else "fun")
   256             :: deresolve name
   257             :: replicate n "_"
   258             @ "="
   259             :: "raise"
   260             :: "Fail"
   261             @@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name
   262           ))
   263       | print_stmt (ML_Val binding) =
   264           let
   265             val (sig_p, p) = print_def (K false) true "val" binding
   266           in pair
   267             [sig_p]
   268             (semicolon [p])
   269           end
   270       | print_stmt (ML_Funs (binding :: bindings, pseudo_funs)) =
   271           let
   272             val print_def' = print_def (member (op =) pseudo_funs) false;
   273             fun print_pseudo_fun name = concat [
   274                 str "val",
   275                 (str o deresolve) name,
   276                 str "=",
   277                 (str o deresolve) name,
   278                 str "();"
   279               ];
   280             val (sig_ps, (ps, p)) = (apsnd split_last o split_list)
   281               (print_def' "fun" binding :: map (print_def' "and") bindings);
   282             val pseudo_ps = map print_pseudo_fun pseudo_funs;
   283           in pair
   284             sig_ps
   285             (Pretty.chunks (ps @ semicolon [p] :: pseudo_ps))
   286           end
   287      | print_stmt (ML_Datas [(tyco, (vs, []))]) =
   288           let
   289             val ty_p = print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs);
   290           in
   291             pair
   292             [concat [str "type", ty_p]]
   293             (concat [str "datatype", ty_p, str "=", str "EMPTY__"])
   294           end
   295      | print_stmt (ML_Datas (data :: datas)) = 
   296           let
   297             val sig_ps = print_datatype_decl "datatype" data
   298               :: map (print_datatype_decl "and") datas;
   299             val (ps, p) = split_last sig_ps;
   300           in pair
   301             sig_ps
   302             (Pretty.chunks (ps @| semicolon [p]))
   303           end
   304      | print_stmt (ML_Class (class, (v, (super_classes, classparams)))) =
   305           let
   306             fun print_field s p = concat [str s, str ":", p];
   307             fun print_proj s p = semicolon
   308               (map str ["val", s, "=", "#" ^ s, ":"] @| p);
   309             fun print_super_class_decl (super_class, classrel) =
   310               print_val_decl print_dicttypscheme
   311                 (classrel, ([(v, [class])], (super_class, ITyVar v)));
   312             fun print_super_class_field (super_class, classrel) =
   313               print_field (deresolve classrel) (print_dicttyp (super_class, ITyVar v));
   314             fun print_super_class_proj (super_class, classrel) =
   315               print_proj (deresolve classrel)
   316                 (print_dicttypscheme ([(v, [class])], (super_class, ITyVar v)));
   317             fun print_classparam_decl (classparam, ty) =
   318               print_val_decl print_typscheme
   319                 (classparam, ([(v, [class])], ty));
   320             fun print_classparam_field (classparam, ty) =
   321               print_field (deresolve classparam) (print_typ NOBR ty);
   322             fun print_classparam_proj (classparam, ty) =
   323               print_proj (deresolve classparam)
   324                 (print_typscheme ([(v, [class])], ty));
   325           in pair
   326             (concat [str "type", print_dicttyp (class, ITyVar v)]
   327               :: map print_super_class_decl super_classes
   328               @ map print_classparam_decl classparams)
   329             (Pretty.chunks (
   330               concat [
   331                 str ("type '" ^ v),
   332                 (str o deresolve) class,
   333                 str "=",
   334                 enum "," "{" "};" (
   335                   map print_super_class_field super_classes
   336                   @ map print_classparam_field classparams
   337                 )
   338               ]
   339               :: map print_super_class_proj super_classes
   340               @ map print_classparam_proj classparams
   341             ))
   342           end;
   343   in print_stmt end;
   344 
   345 fun print_sml_module name some_decls body = if name = ""
   346   then Pretty.chunks2 body
   347   else Pretty.chunks2 (
   348     Pretty.chunks (
   349       str ("structure " ^ name ^ (if is_some some_decls then " : sig" else " ="))
   350       :: (the_list o Option.map (indent 2 o Pretty.chunks)) some_decls
   351       @| (if is_some some_decls then str "end = struct" else str "struct")
   352     )
   353     :: body
   354     @| str ("end; (*struct " ^ name ^ "*)")
   355   );
   356 
   357 val literals_sml = Literals {
   358   literal_char = prefix "#" o quote o ML_Syntax.print_char,
   359   literal_string = quote o translate_string ML_Syntax.print_char,
   360   literal_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
   361   literal_positive_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
   362   literal_naive_numeral = string_of_int,
   363   literal_list = enum "," "[" "]",
   364   infix_cons = (7, "::")
   365 };
   366 
   367 
   368 (** OCaml serializer **)
   369 
   370 fun print_ocaml_stmt labelled_name syntax_tyco syntax_const reserved is_cons deresolve =
   371   let
   372     fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco
   373       | print_tyco_expr fxy (tyco, [ty]) =
   374           concat [print_typ BR ty, (str o deresolve) tyco]
   375       | print_tyco_expr fxy (tyco, tys) =
   376           concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]
   377     and print_typ fxy (tyco `%% tys) = (case syntax_tyco tyco
   378          of NONE => print_tyco_expr fxy (tyco, tys)
   379           | SOME (i, print) => print print_typ fxy tys)
   380       | print_typ fxy (ITyVar v) = str ("'" ^ v);
   381     fun print_dicttyp (class, ty) = print_tyco_expr NOBR (class, [ty]);
   382     fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
   383       (map_filter (fn (v, sort) =>
   384         (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
   385     fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);
   386     fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);
   387     fun print_dict is_pseudo_fun fxy (DictConst (inst, dss)) =
   388           brackify fxy ((str o deresolve) inst ::
   389             (if is_pseudo_fun inst then [str "()"]
   390             else map_filter (print_dicts is_pseudo_fun BR) dss))
   391       | print_dict is_pseudo_fun fxy (DictVar (classrels, (v, (i, k)))) =
   392           str (if k = 1 then "_" ^ first_upper v
   393             else "_" ^ first_upper v ^ string_of_int (i+1))
   394           |> fold_rev (fn classrel => fn p =>
   395                Pretty.block [p, str ".", (str o deresolve) classrel]) classrels
   396     and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun);
   397     val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
   398       (map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort));
   399     fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
   400           print_app is_pseudo_fun some_thm vars fxy (c, [])
   401       | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
   402           str "_"
   403       | print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) =
   404           str (lookup_var vars v)
   405       | print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) =
   406           (case Code_Thingol.unfold_const_app t
   407            of SOME c_ts => print_app is_pseudo_fun some_thm vars fxy c_ts
   408             | NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1,
   409                 print_term is_pseudo_fun some_thm vars BR t2])
   410       | print_term is_pseudo_fun some_thm vars fxy (t as _ `|=> _) =
   411           let
   412             val (binds, t') = Code_Thingol.unfold_pat_abs t;
   413             val (ps, vars') = fold_map (print_bind is_pseudo_fun some_thm BR o fst) binds vars;
   414           in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun some_thm vars' NOBR t') end
   415       | print_term is_pseudo_fun some_thm vars fxy (ICase (cases as (_, t0))) =
   416           (case Code_Thingol.unfold_const_app t0
   417            of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
   418                 then print_case is_pseudo_fun some_thm vars fxy cases
   419                 else print_app is_pseudo_fun some_thm vars fxy c_ts
   420             | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
   421     and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), tys)), ts)) =
   422       if is_cons c then
   423         let val k = length tys in
   424           if length ts = k
   425           then (str o deresolve) c
   426             :: the_list (print_tuple (print_term is_pseudo_fun some_thm vars) BR ts)
   427           else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
   428         end
   429       else if is_pseudo_fun c
   430         then (str o deresolve) c @@ str "()"
   431       else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss
   432         @ map (print_term is_pseudo_fun some_thm vars BR) ts
   433     and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
   434       (print_term is_pseudo_fun) syntax_const some_thm vars
   435     and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
   436     and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =
   437           let
   438             val (binds, body) = Code_Thingol.unfold_let (ICase cases);
   439             fun print_let ((pat, ty), t) vars =
   440               vars
   441               |> print_bind is_pseudo_fun some_thm NOBR pat
   442               |>> (fn p => concat
   443                   [str "let", p, str "=", print_term is_pseudo_fun some_thm vars NOBR t, str "in"])
   444             val (ps, vars') = fold_map print_let binds vars;
   445           in
   446             brackify_block fxy (Pretty.chunks ps) []
   447               (print_term is_pseudo_fun some_thm vars' NOBR body)
   448           end
   449       | print_case is_pseudo_fun some_thm vars fxy (((t, ty), clause :: clauses), _) =
   450           let
   451             fun print_select delim (pat, body) =
   452               let
   453                 val (p, vars') = print_bind is_pseudo_fun some_thm NOBR pat vars;
   454               in concat [str delim, p, str "->", print_term is_pseudo_fun some_thm vars' NOBR body] end;
   455           in
   456             brackets (
   457               str "match"
   458               :: print_term is_pseudo_fun some_thm vars NOBR t
   459               :: print_select "with" clause
   460               :: map (print_select "|") clauses
   461             )
   462           end
   463       | print_case is_pseudo_fun some_thm vars fxy ((_, []), _) =
   464           (concat o map str) ["failwith", "\"empty case\""];
   465     fun print_val_decl print_typscheme (name, typscheme) = concat
   466       [str "val", str (deresolve name), str ":", print_typscheme typscheme];
   467     fun print_datatype_decl definer (tyco, (vs, cos)) =
   468       let
   469         fun print_co (co, []) = str (deresolve co)
   470           | print_co (co, tys) = concat [str (deresolve co), str "of",
   471               enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
   472       in
   473         concat (
   474           str definer
   475           :: print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs)
   476           :: str "="
   477           :: separate (str "|") (map print_co cos)
   478         )
   479       end;
   480     fun print_def is_pseudo_fun needs_typ definer
   481           (ML_Function (name, (vs_ty as (vs, ty), eqs))) =
   482           let
   483             fun print_eqn ((ts, t), (some_thm, _)) =
   484               let
   485                 val consts = fold Code_Thingol.add_constnames (t :: ts) [];
   486                 val vars = reserved
   487                   |> intro_vars ((fold o Code_Thingol.fold_varnames)
   488                       (insert (op =)) ts []);
   489               in concat [
   490                 (Pretty.block o Pretty.commas)
   491                   (map (print_term is_pseudo_fun some_thm vars NOBR) ts),
   492                 str "->",
   493                 print_term is_pseudo_fun some_thm vars NOBR t
   494               ] end;
   495             fun print_eqns is_pseudo [((ts, t), (some_thm, _))] =
   496                   let
   497                     val consts = fold Code_Thingol.add_constnames (t :: ts) [];
   498                     val vars = reserved
   499                       |> intro_base_names
   500                           (is_none o syntax_const) deresolve consts
   501                       |> intro_vars ((fold o Code_Thingol.fold_varnames)
   502                           (insert (op =)) ts []);
   503                   in
   504                     concat (
   505                       (if is_pseudo then [str "()"]
   506                         else map (print_term is_pseudo_fun some_thm vars BR) ts)
   507                       @ str "="
   508                       @@ print_term is_pseudo_fun some_thm vars NOBR t
   509                     )
   510                   end
   511               | print_eqns _ ((eq as (([_], _), _)) :: eqs) =
   512                   Pretty.block (
   513                     str "="
   514                     :: Pretty.brk 1
   515                     :: str "function"
   516                     :: Pretty.brk 1
   517                     :: print_eqn eq
   518                     :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
   519                           o single o print_eqn) eqs
   520                   )
   521               | print_eqns _ (eqs as eq :: eqs') =
   522                   let
   523                     val consts = fold Code_Thingol.add_constnames (map (snd o fst) eqs) [];
   524                     val vars = reserved
   525                       |> intro_base_names
   526                           (is_none o syntax_const) deresolve consts;
   527                     val dummy_parms = (map str o aux_params vars o map (fst o fst)) eqs;
   528                   in
   529                     Pretty.block (
   530                       Pretty.breaks dummy_parms
   531                       @ Pretty.brk 1
   532                       :: str "="
   533                       :: Pretty.brk 1
   534                       :: str "match"
   535                       :: Pretty.brk 1
   536                       :: (Pretty.block o Pretty.commas) dummy_parms
   537                       :: Pretty.brk 1
   538                       :: str "with"
   539                       :: Pretty.brk 1
   540                       :: print_eqn eq
   541                       :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
   542                            o single o print_eqn) eqs'
   543                     )
   544                   end;
   545             val prolog = if needs_typ then
   546               concat [str definer, (str o deresolve) name, str ":", print_typ NOBR ty]
   547                 else (concat o map str) [definer, deresolve name];
   548           in pair
   549             (print_val_decl print_typscheme (name, vs_ty))
   550             (concat (
   551               prolog
   552               :: print_dict_args vs
   553               @| print_eqns (is_pseudo_fun name) eqs
   554             ))
   555           end
   556       | print_def is_pseudo_fun _ definer
   557             (ML_Instance (inst, ((class, (tyco, vs)), ((super_instances, _), classparam_instances)))) =
   558           let
   559             fun print_super_instance (_, (classrel, dss)) =
   560               concat [
   561                 (str o deresolve) classrel,
   562                 str "=",
   563                 print_dict is_pseudo_fun NOBR (DictConst dss)
   564               ];
   565             fun print_classparam_instance ((classparam, const), (thm, _)) =
   566               concat [
   567                 (str o deresolve) classparam,
   568                 str "=",
   569                 print_app (K false) (SOME thm) reserved NOBR (const, [])
   570               ];
   571           in pair
   572             (print_val_decl print_dicttypscheme
   573               (inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
   574             (concat (
   575               str definer
   576               :: (str o deresolve) inst
   577               :: print_dict_args vs
   578               @ str "="
   579               @@ brackets [
   580                 enum_default "()" ";" "{" "}" (map print_super_instance super_instances
   581                   @ map print_classparam_instance classparam_instances),
   582                 str ":",
   583                 print_tyco_expr NOBR (class, [tyco `%% map (ITyVar o fst) vs])
   584               ]
   585             ))
   586           end;
   587      fun print_stmt (ML_Exc (name, (vs_ty, n))) = pair
   588           [print_val_decl print_typscheme (name, vs_ty)]
   589           ((doublesemicolon o map str) (
   590             "let"
   591             :: deresolve name
   592             :: replicate n "_"
   593             @ "="
   594             :: "failwith"
   595             @@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name
   596           ))
   597       | print_stmt (ML_Val binding) =
   598           let
   599             val (sig_p, p) = print_def (K false) true "let" binding
   600           in pair
   601             [sig_p]
   602             (doublesemicolon [p])
   603           end
   604       | print_stmt (ML_Funs (binding :: bindings, pseudo_funs)) =
   605           let
   606             val print_def' = print_def (member (op =) pseudo_funs) false;
   607             fun print_pseudo_fun name = concat [
   608                 str "let",
   609                 (str o deresolve) name,
   610                 str "=",
   611                 (str o deresolve) name,
   612                 str "();;"
   613               ];
   614             val (sig_ps, (ps, p)) = (apsnd split_last o split_list)
   615               (print_def' "let rec" binding :: map (print_def' "and") bindings);
   616             val pseudo_ps = map print_pseudo_fun pseudo_funs;
   617           in pair
   618             sig_ps
   619             (Pretty.chunks (ps @ doublesemicolon [p] :: pseudo_ps))
   620           end
   621      | print_stmt (ML_Datas [(tyco, (vs, []))]) =
   622           let
   623             val ty_p = print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs);
   624           in
   625             pair
   626             [concat [str "type", ty_p]]
   627             (concat [str "type", ty_p, str "=", str "EMPTY__"])
   628           end
   629      | print_stmt (ML_Datas (data :: datas)) = 
   630           let
   631             val sig_ps = print_datatype_decl "type" data
   632               :: map (print_datatype_decl "and") datas;
   633             val (ps, p) = split_last sig_ps;
   634           in pair
   635             sig_ps
   636             (Pretty.chunks (ps @| doublesemicolon [p]))
   637           end
   638      | print_stmt (ML_Class (class, (v, (super_classes, classparams)))) =
   639           let
   640             fun print_field s p = concat [str s, str ":", p];
   641             fun print_super_class_field (super_class, classrel) =
   642               print_field (deresolve classrel) (print_dicttyp (super_class, ITyVar v));
   643             fun print_classparam_decl (classparam, ty) =
   644               print_val_decl print_typscheme
   645                 (classparam, ([(v, [class])], ty));
   646             fun print_classparam_field (classparam, ty) =
   647               print_field (deresolve classparam) (print_typ NOBR ty);
   648             val w = "_" ^ first_upper v;
   649             fun print_classparam_proj (classparam, _) =
   650               (concat o map str) ["let", deresolve classparam, w, "=",
   651                 w ^ "." ^ deresolve classparam ^ ";;"];
   652             val type_decl_p = concat [
   653                 str ("type '" ^ v),
   654                 (str o deresolve) class,
   655                 str "=",
   656                 enum_default "unit" ";" "{" "}" (
   657                   map print_super_class_field super_classes
   658                   @ map print_classparam_field classparams
   659                 )
   660               ];
   661           in pair
   662             (type_decl_p :: map print_classparam_decl classparams)
   663             (Pretty.chunks (
   664               doublesemicolon [type_decl_p]
   665               :: map print_classparam_proj classparams
   666             ))
   667           end;
   668   in print_stmt end;
   669 
   670 fun print_ocaml_module name some_decls body = if name = ""
   671   then Pretty.chunks2 body
   672   else Pretty.chunks2 (
   673     Pretty.chunks (
   674       str ("module " ^ name ^ (if is_some some_decls then " : sig" else " ="))
   675       :: (the_list o Option.map (indent 2 o Pretty.chunks)) some_decls
   676       @| (if is_some some_decls then str "end = struct" else str "struct")
   677     )
   678     :: body
   679     @| str ("end;; (*struct " ^ name ^ "*)")
   680   );
   681 
   682 val literals_ocaml = let
   683   fun chr i =
   684     let
   685       val xs = string_of_int i;
   686       val ys = replicate_string (3 - length (explode xs)) "0";
   687     in "\\" ^ ys ^ xs end;
   688   fun char_ocaml c =
   689     let
   690       val i = ord c;
   691       val s = if i < 32 orelse i = 34 orelse i = 39 orelse i = 92 orelse i > 126
   692         then chr i else c
   693     in s end;
   694   fun numeral_ocaml k = if k < 0
   695     then "(Big_int.minus_big_int " ^ numeral_ocaml (~ k) ^ ")"
   696     else if k <= 1073741823
   697       then "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
   698       else "(Big_int.big_int_of_string " ^ quote (string_of_int k) ^ ")"
   699 in Literals {
   700   literal_char = Library.enclose "'" "'" o char_ocaml,
   701   literal_string = quote o translate_string char_ocaml,
   702   literal_numeral = numeral_ocaml,
   703   literal_positive_numeral = numeral_ocaml,
   704   literal_naive_numeral = numeral_ocaml,
   705   literal_list = enum ";" "[" "]",
   706   infix_cons = (6, "::")
   707 } end;
   708 
   709 
   710 
   711 (** SML/OCaml generic part **)
   712 
   713 local
   714 
   715 datatype ml_node =
   716     Dummy of string
   717   | Stmt of string * ml_stmt
   718   | Module of string * ((Name.context * Name.context) * ml_node Graph.T);
   719 
   720 in
   721 
   722 fun ml_node_of_program labelled_name module_name reserved raw_module_alias program =
   723   let
   724     val module_alias = if is_some module_name then K module_name else raw_module_alias;
   725     val reserved = Name.make_context reserved;
   726     val empty_module = ((reserved, reserved), Graph.empty);
   727     fun map_node [] f = f
   728       | map_node (m::ms) f =
   729           Graph.default_node (m, Module (m, empty_module))
   730           #> Graph.map_node m (fn (Module (module_name, (nsp, nodes))) =>
   731                Module (module_name, (nsp, map_node ms f nodes)));
   732     fun map_nsp_yield [] f (nsp, nodes) =
   733           let
   734             val (x, nsp') = f nsp
   735           in (x, (nsp', nodes)) end
   736       | map_nsp_yield (m::ms) f (nsp, nodes) =
   737           let
   738             val (x, nodes') =
   739               nodes
   740               |> Graph.default_node (m, Module (m, empty_module))
   741               |> Graph.map_node_yield m (fn Module (d_module_name, nsp_nodes) => 
   742                   let
   743                     val (x, nsp_nodes') = map_nsp_yield ms f nsp_nodes
   744                   in (x, Module (d_module_name, nsp_nodes')) end)
   745           in (x, (nsp, nodes')) end;
   746     fun map_nsp_fun_yield f (nsp_fun, nsp_typ) =
   747       let
   748         val (x, nsp_fun') = f nsp_fun
   749       in (x, (nsp_fun', nsp_typ)) end;
   750     fun map_nsp_typ_yield f (nsp_fun, nsp_typ) =
   751       let
   752         val (x, nsp_typ') = f nsp_typ
   753       in (x, (nsp_fun, nsp_typ')) end;
   754     val mk_name_module = mk_name_module reserved NONE module_alias program;
   755     fun mk_name_stmt upper name nsp =
   756       let
   757         val (_, base) = dest_name name;
   758         val base' = if upper then first_upper base else base;
   759         val ([base''], nsp') = Name.variants [base'] nsp;
   760       in (base'', nsp') end;
   761     fun ml_binding_of_stmt (name, Code_Thingol.Fun (_, (tysm as (vs, ty), raw_eqs))) =
   762           let
   763             val eqs = filter (snd o snd) raw_eqs;
   764             val (eqs', is_value) = if null (filter_out (null o snd) vs) then case eqs
   765                of [(([], t), some_thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty
   766                   then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), some_thm)], NONE)
   767                   else (eqs, SOME (name, member (op =) (Code_Thingol.add_constnames t []) name))
   768                 | _ => (eqs, NONE)
   769               else (eqs, NONE)
   770           in (ML_Function (name, (tysm, eqs')), is_value) end
   771       | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as ((_, (_, vs)), _))) =
   772           (ML_Instance (name, stmt), if forall (null o snd) vs then SOME (name, false) else NONE)
   773       | ml_binding_of_stmt (name, _) =
   774           error ("Binding block containing illegal statement: " ^ labelled_name name)
   775     fun add_fun (name, stmt) =
   776       let
   777         val (binding, some_value_name) = ml_binding_of_stmt (name, stmt);
   778         val ml_stmt = case binding
   779          of ML_Function (name, ((vs, ty), [])) =>
   780               ML_Exc (name, ((vs, ty),
   781                 (length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty))
   782           | _ => case some_value_name
   783              of NONE => ML_Funs ([binding], [])
   784               | SOME (name, true) => ML_Funs ([binding], [name])
   785               | SOME (name, false) => ML_Val binding
   786       in
   787         map_nsp_fun_yield (mk_name_stmt false name)
   788         #>> (fn name' => ([name'], ml_stmt))
   789       end;
   790     fun add_funs stmts =
   791       let
   792         val ml_stmt = ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst);
   793       in
   794         fold_map (fn (name, _) => map_nsp_fun_yield (mk_name_stmt false name)) stmts
   795         #>> rpair ml_stmt
   796       end;
   797     fun add_datatypes stmts =
   798       fold_map
   799         (fn (name, Code_Thingol.Datatype (_, stmt)) =>
   800               map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt))
   801           | (name, Code_Thingol.Datatypecons _) =>
   802               map_nsp_fun_yield (mk_name_stmt true name) #>> rpair NONE
   803           | (name, _) =>
   804               error ("Datatype block containing illegal statement: " ^ labelled_name name)
   805         ) stmts
   806       #>> (split_list #> apsnd (map_filter I
   807         #> (fn [] => error ("Datatype block without data statement: "
   808                   ^ (commas o map (labelled_name o fst)) stmts)
   809              | stmts => ML_Datas stmts)));
   810     fun add_class stmts =
   811       fold_map
   812         (fn (name, Code_Thingol.Class (_, stmt)) =>
   813               map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt))
   814           | (name, Code_Thingol.Classrel _) =>
   815               map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
   816           | (name, Code_Thingol.Classparam _) =>
   817               map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
   818           | (name, _) =>
   819               error ("Class block containing illegal statement: " ^ labelled_name name)
   820         ) stmts
   821       #>> (split_list #> apsnd (map_filter I
   822         #> (fn [] => error ("Class block without class statement: "
   823                   ^ (commas o map (labelled_name o fst)) stmts)
   824              | [stmt] => ML_Class stmt)));
   825     fun add_stmts ([stmt as (name, Code_Thingol.Fun _)]) =
   826           add_fun stmt
   827       | add_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) =
   828           add_funs stmts
   829       | add_stmts ((stmts as (_, Code_Thingol.Datatypecons _)::_)) =
   830           add_datatypes stmts
   831       | add_stmts ((stmts as (_, Code_Thingol.Datatype _)::_)) =
   832           add_datatypes stmts
   833       | add_stmts ((stmts as (_, Code_Thingol.Class _)::_)) =
   834           add_class stmts
   835       | add_stmts ((stmts as (_, Code_Thingol.Classrel _)::_)) =
   836           add_class stmts
   837       | add_stmts ((stmts as (_, Code_Thingol.Classparam _)::_)) =
   838           add_class stmts
   839       | add_stmts ([stmt as (_, Code_Thingol.Classinst _)]) =
   840           add_fun stmt
   841       | add_stmts ((stmts as (_, Code_Thingol.Classinst _)::_)) =
   842           add_funs stmts
   843       | add_stmts stmts = error ("Illegal mutual dependencies: " ^
   844           (commas o map (labelled_name o fst)) stmts);
   845     fun add_stmts' stmts nsp_nodes =
   846       let
   847         val names as (name :: names') = map fst stmts;
   848         val deps =
   849           []
   850           |> fold (fold (insert (op =)) o Graph.imm_succs program) names
   851           |> subtract (op =) names;
   852         val (module_names, _) = (split_list o map dest_name) names;
   853         val module_name = (the_single o distinct (op =) o map mk_name_module) module_names
   854           handle Empty =>
   855             error ("Different namespace prefixes for mutual dependencies:\n"
   856               ^ commas (map labelled_name names)
   857               ^ "\n"
   858               ^ commas module_names);
   859         val module_name_path = Long_Name.explode module_name;
   860         fun add_dep name name' =
   861           let
   862             val module_name' = (mk_name_module o fst o dest_name) name';
   863           in if module_name = module_name' then
   864             map_node module_name_path (Graph.add_edge (name, name'))
   865           else let
   866             val (common, (diff1 :: _, diff2 :: _)) = chop_prefix (op =)
   867               (module_name_path, Long_Name.explode module_name');
   868           in
   869             map_node common
   870               (fn node => Graph.add_edge_acyclic (diff1, diff2) node
   871                 handle Graph.CYCLES _ => error ("Dependency "
   872                   ^ quote name ^ " -> " ^ quote name'
   873                   ^ " would result in module dependency cycle"))
   874           end end;
   875       in
   876         nsp_nodes
   877         |> map_nsp_yield module_name_path (add_stmts stmts)
   878         |-> (fn (base' :: bases', stmt') =>
   879            apsnd (map_node module_name_path (Graph.new_node (name, (Stmt (base', stmt')))
   880               #> fold2 (fn name' => fn base' =>
   881                    Graph.new_node (name', (Dummy base'))) names' bases')))
   882         |> apsnd (fold (fn name => fold (add_dep name) deps) names)
   883         |> apsnd (fold_product (curry (map_node module_name_path o Graph.add_edge)) names names)
   884       end;
   885     val (_, nodes) = empty_module
   886       |> fold add_stmts' (map (AList.make (Graph.get_node program))
   887           (rev (Graph.strong_conn program)));
   888     fun deresolver prefix name = 
   889       let
   890         val module_name = (fst o dest_name) name;
   891         val module_name' = (Long_Name.explode o mk_name_module) module_name;
   892         val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name');
   893         val stmt_name =
   894           nodes
   895           |> fold (fn name => fn node => case Graph.get_node node name
   896               of Module (_, (_, node)) => node) module_name'
   897           |> (fn node => case Graph.get_node node name of Stmt (stmt_name, _) => stmt_name
   898                | Dummy stmt_name => stmt_name);
   899       in
   900         Long_Name.implode (remainder @ [stmt_name])
   901       end handle Graph.UNDEF _ =>
   902         error ("Unknown statement name: " ^ labelled_name name);
   903   in (deresolver, nodes) end;
   904 
   905 fun serialize_ml target compile print_module print_stmt raw_module_name with_signatures labelled_name
   906   reserved includes raw_module_alias _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program stmt_names destination =
   907   let
   908     val is_cons = Code_Thingol.is_cons program;
   909     val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
   910     val is_presentation = not (null presentation_stmt_names);
   911     val module_name = if is_presentation then SOME "Code" else raw_module_name;
   912     val (deresolver, nodes) = ml_node_of_program labelled_name module_name
   913       reserved raw_module_alias program;
   914     val reserved = make_vars reserved;
   915     fun print_node prefix (Dummy _) =
   916           NONE
   917       | print_node prefix (Stmt (_, stmt)) = if is_presentation andalso
   918           (null o filter (member (op =) presentation_stmt_names) o stmt_names_of) stmt
   919           then NONE
   920           else SOME (print_stmt labelled_name syntax_tyco syntax_const reserved is_cons (deresolver prefix) stmt)
   921       | print_node prefix (Module (module_name, (_, nodes))) =
   922           let
   923             val (decls, body) = print_nodes (prefix @ [module_name]) nodes;
   924             val p = if is_presentation then Pretty.chunks2 body
   925               else print_module module_name (if with_signatures then SOME decls else NONE) body;
   926           in SOME ([], p) end
   927     and print_nodes prefix nodes = (map_filter (print_node prefix o Graph.get_node nodes)
   928         o rev o flat o Graph.strong_conn) nodes
   929       |> split_list
   930       |> (fn (decls, body) => (flat decls, body))
   931     val stmt_names' = (map o try)
   932       (deresolver (if is_some module_name then the_list module_name else [])) stmt_names;
   933     val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] nodes));
   934   in
   935     Code_Target.mk_serialization target
   936       (case compile of SOME compile => SOME (compile o code_of_pretty) | NONE => NONE)
   937       (fn NONE => code_writeln | SOME file => File.write file o code_of_pretty)
   938       (rpair stmt_names' o code_of_pretty) p destination
   939   end;
   940 
   941 end; (*local*)
   942 
   943 
   944 (** for instrumentalization **)
   945 
   946 fun evaluation_code_of thy target struct_name =
   947   Code_Target.serialize_custom thy (target, (fn _ => fn [] =>
   948     serialize_ml target (SOME (K ())) print_sml_module print_sml_stmt (SOME struct_name) true, literals_sml));
   949 
   950 
   951 (** Isar setup **)
   952 
   953 fun isar_seri_sml module_name =
   954   Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
   955   >> (fn with_signatures => serialize_ml target_SML
   956       (SOME (use_text ML_Env.local_context (1, "generated code") false))
   957       print_sml_module print_sml_stmt module_name with_signatures));
   958 
   959 fun isar_seri_ocaml module_name =
   960   Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
   961   >> (fn with_signatures => serialize_ml target_OCaml NONE
   962       print_ocaml_module print_ocaml_stmt module_name with_signatures));
   963 
   964 val setup =
   965   Code_Target.add_target (target_SML, (isar_seri_sml, literals_sml))
   966   #> Code_Target.add_target (target_OCaml, (isar_seri_ocaml, literals_ocaml))
   967   #> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   968       brackify_infix (1, R) fxy (
   969         print_typ (INFX (1, X)) ty1,
   970         str "->",
   971         print_typ (INFX (1, R)) ty2
   972       )))
   973   #> Code_Target.add_syntax_tyco target_OCaml "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   974       brackify_infix (1, R) fxy (
   975         print_typ (INFX (1, X)) ty1,
   976         str "->",
   977         print_typ (INFX (1, R)) ty2
   978       )))
   979   #> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names
   980   #> fold (Code_Target.add_reserved target_SML)
   981       ["o" (*dictionary projections use it already*), "Fail", "div", "mod" (*standard infixes*), "IntInf"]
   982   #> fold (Code_Target.add_reserved target_OCaml) [
   983       "and", "as", "assert", "begin", "class",
   984       "constraint", "do", "done", "downto", "else", "end", "exception",
   985       "external", "false", "for", "fun", "function", "functor", "if",
   986       "in", "include", "inherit", "initializer", "lazy", "let", "match", "method",
   987       "module", "mutable", "new", "object", "of", "open", "or", "private", "rec",
   988       "sig", "struct", "then", "to", "true", "try", "type", "val",
   989       "virtual", "when", "while", "with"
   990     ]
   991   #> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod", "Big_int"];
   992 
   993 end; (*struct*)