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