src/Tools/Code/code_ml.ML
author haftmann
Wed Sep 01 08:52:49 2010 +0200 (2010-09-01)
changeset 38966 68853347ba37
parent 38933 bd77e092f67c
child 39028 0dd6c5a0beef
permissions -rw-r--r--
tuned internally and made smlnj happy
     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 =
   343   Pretty.chunks2 (
   344     Pretty.chunks (
   345       str ("structure " ^ name ^ (if is_some some_decls then " : sig" else " ="))
   346       :: (the_list o Option.map (indent 2 o Pretty.chunks)) some_decls
   347       @| (if is_some some_decls then str "end = struct" else str "struct")
   348     )
   349     :: body
   350     @| str ("end; (*struct " ^ name ^ "*)")
   351   );
   352 
   353 val literals_sml = Literals {
   354   literal_char = prefix "#" o quote o ML_Syntax.print_char,
   355   literal_string = quote o translate_string ML_Syntax.print_char,
   356   literal_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
   357   literal_positive_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
   358   literal_alternative_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
   359   literal_naive_numeral = string_of_int,
   360   literal_list = enum "," "[" "]",
   361   infix_cons = (7, "::")
   362 };
   363 
   364 
   365 (** OCaml serializer **)
   366 
   367 fun print_ocaml_stmt labelled_name tyco_syntax const_syntax reserved is_cons deresolve =
   368   let
   369     fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco
   370       | print_tyco_expr fxy (tyco, [ty]) =
   371           concat [print_typ BR ty, (str o deresolve) tyco]
   372       | print_tyco_expr fxy (tyco, tys) =
   373           concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]
   374     and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
   375          of NONE => print_tyco_expr fxy (tyco, tys)
   376           | SOME (i, print) => print print_typ fxy tys)
   377       | print_typ fxy (ITyVar v) = str ("'" ^ v);
   378     fun print_dicttyp (class, ty) = print_tyco_expr NOBR (class, [ty]);
   379     fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
   380       (map_filter (fn (v, sort) =>
   381         (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
   382     fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);
   383     fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);
   384     fun print_dict is_pseudo_fun fxy (DictConst (inst, dss)) =
   385           brackify fxy ((str o deresolve) inst ::
   386             (if is_pseudo_fun inst then [str "()"]
   387             else map_filter (print_dicts is_pseudo_fun BR) dss))
   388       | print_dict is_pseudo_fun fxy (DictVar (classrels, (v, (i, k)))) =
   389           str (if k = 1 then "_" ^ first_upper v
   390             else "_" ^ first_upper v ^ string_of_int (i+1))
   391           |> fold_rev (fn classrel => fn p =>
   392                Pretty.block [p, str ".", (str o deresolve) classrel]) classrels
   393     and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
   394     val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
   395       (map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort));
   396     fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
   397           print_app is_pseudo_fun some_thm vars fxy (c, [])
   398       | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
   399           str "_"
   400       | print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) =
   401           str (lookup_var vars v)
   402       | print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) =
   403           (case Code_Thingol.unfold_const_app t
   404            of SOME c_ts => print_app is_pseudo_fun some_thm vars fxy c_ts
   405             | NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1,
   406                 print_term is_pseudo_fun some_thm vars BR t2])
   407       | print_term is_pseudo_fun some_thm vars fxy (t as _ `|=> _) =
   408           let
   409             val (binds, t') = Code_Thingol.unfold_pat_abs t;
   410             val (ps, vars') = fold_map (print_bind is_pseudo_fun some_thm BR o fst) binds vars;
   411           in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun some_thm vars' NOBR t') end
   412       | print_term is_pseudo_fun some_thm vars fxy (ICase (cases as (_, t0))) =
   413           (case Code_Thingol.unfold_const_app t0
   414            of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
   415                 then print_case is_pseudo_fun some_thm vars fxy cases
   416                 else print_app is_pseudo_fun some_thm vars fxy c_ts
   417             | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
   418     and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), tys)), ts)) =
   419       if is_cons c then
   420         let val k = length tys in
   421           if length ts = k
   422           then (str o deresolve) c
   423             :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
   424           else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
   425         end
   426       else if is_pseudo_fun c
   427         then (str o deresolve) c @@ str "()"
   428       else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss
   429         @ map (print_term is_pseudo_fun some_thm vars BR) ts
   430     and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
   431       (print_term is_pseudo_fun) const_syntax some_thm vars
   432     and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
   433     and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =
   434           let
   435             val (binds, body) = Code_Thingol.unfold_let (ICase cases);
   436             fun print_let ((pat, ty), t) vars =
   437               vars
   438               |> print_bind is_pseudo_fun some_thm NOBR pat
   439               |>> (fn p => concat
   440                   [str "let", p, str "=", print_term is_pseudo_fun some_thm vars NOBR t, str "in"])
   441             val (ps, vars') = fold_map print_let binds vars;
   442           in
   443             brackify_block fxy (Pretty.chunks ps) []
   444               (print_term is_pseudo_fun some_thm vars' NOBR body)
   445           end
   446       | print_case is_pseudo_fun some_thm vars fxy (((t, ty), clause :: clauses), _) =
   447           let
   448             fun print_select delim (pat, body) =
   449               let
   450                 val (p, vars') = print_bind is_pseudo_fun some_thm NOBR pat vars;
   451               in concat [str delim, p, str "->", print_term is_pseudo_fun some_thm vars' NOBR body] end;
   452           in
   453             brackets (
   454               str "match"
   455               :: print_term is_pseudo_fun some_thm vars NOBR t
   456               :: print_select "with" clause
   457               :: map (print_select "|") clauses
   458             )
   459           end
   460       | print_case is_pseudo_fun some_thm vars fxy ((_, []), _) =
   461           (concat o map str) ["failwith", "\"empty case\""];
   462     fun print_val_decl print_typscheme (name, typscheme) = concat
   463       [str "val", str (deresolve name), str ":", print_typscheme typscheme];
   464     fun print_datatype_decl definer (tyco, (vs, cos)) =
   465       let
   466         fun print_co ((co, _), []) = str (deresolve co)
   467           | print_co ((co, _), tys) = concat [str (deresolve co), str "of",
   468               enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
   469       in
   470         concat (
   471           str definer
   472           :: print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs)
   473           :: str "="
   474           :: separate (str "|") (map print_co cos)
   475         )
   476       end;
   477     fun print_def is_pseudo_fun needs_typ definer
   478           (ML_Function (name, (vs_ty as (vs, ty), eqs))) =
   479           let
   480             fun print_eqn ((ts, t), (some_thm, _)) =
   481               let
   482                 val consts = fold Code_Thingol.add_constnames (t :: ts) [];
   483                 val vars = reserved
   484                   |> intro_vars ((fold o Code_Thingol.fold_varnames)
   485                       (insert (op =)) ts []);
   486               in concat [
   487                 (Pretty.block o commas)
   488                   (map (print_term is_pseudo_fun some_thm vars NOBR) ts),
   489                 str "->",
   490                 print_term is_pseudo_fun some_thm vars NOBR t
   491               ] end;
   492             fun print_eqns is_pseudo [((ts, t), (some_thm, _))] =
   493                   let
   494                     val consts = fold Code_Thingol.add_constnames (t :: ts) [];
   495                     val vars = reserved
   496                       |> intro_base_names
   497                           (is_none o const_syntax) deresolve consts
   498                       |> intro_vars ((fold o Code_Thingol.fold_varnames)
   499                           (insert (op =)) ts []);
   500                   in
   501                     concat (
   502                       (if is_pseudo then [str "()"]
   503                         else map (print_term is_pseudo_fun some_thm vars BR) ts)
   504                       @ str "="
   505                       @@ print_term is_pseudo_fun some_thm vars NOBR t
   506                     )
   507                   end
   508               | print_eqns _ ((eq as (([_], _), _)) :: eqs) =
   509                   Pretty.block (
   510                     str "="
   511                     :: Pretty.brk 1
   512                     :: str "function"
   513                     :: Pretty.brk 1
   514                     :: print_eqn eq
   515                     :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
   516                           o single o print_eqn) eqs
   517                   )
   518               | print_eqns _ (eqs as eq :: eqs') =
   519                   let
   520                     val consts = fold Code_Thingol.add_constnames (map (snd o fst) eqs) [];
   521                     val vars = reserved
   522                       |> intro_base_names
   523                           (is_none o const_syntax) deresolve consts;
   524                     val dummy_parms = (map str o aux_params vars o map (fst o fst)) eqs;
   525                   in
   526                     Pretty.block (
   527                       Pretty.breaks dummy_parms
   528                       @ Pretty.brk 1
   529                       :: str "="
   530                       :: Pretty.brk 1
   531                       :: str "match"
   532                       :: Pretty.brk 1
   533                       :: (Pretty.block o commas) dummy_parms
   534                       :: Pretty.brk 1
   535                       :: str "with"
   536                       :: Pretty.brk 1
   537                       :: print_eqn eq
   538                       :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
   539                            o single o print_eqn) eqs'
   540                     )
   541                   end;
   542             val prolog = if needs_typ then
   543               concat [str definer, (str o deresolve) name, str ":", print_typ NOBR ty]
   544                 else (concat o map str) [definer, deresolve name];
   545           in pair
   546             (print_val_decl print_typscheme (name, vs_ty))
   547             (concat (
   548               prolog
   549               :: print_dict_args vs
   550               @| print_eqns (is_pseudo_fun name) eqs
   551             ))
   552           end
   553       | print_def is_pseudo_fun _ definer
   554             (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) =
   555           let
   556             fun print_super_instance (_, (classrel, dss)) =
   557               concat [
   558                 (str o deresolve) classrel,
   559                 str "=",
   560                 print_dict is_pseudo_fun NOBR (DictConst dss)
   561               ];
   562             fun print_classparam_instance ((classparam, const), (thm, _)) =
   563               concat [
   564                 (str o deresolve) classparam,
   565                 str "=",
   566                 print_app (K false) (SOME thm) reserved NOBR (const, [])
   567               ];
   568           in pair
   569             (print_val_decl print_dicttypscheme
   570               (inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
   571             (concat (
   572               str definer
   573               :: (str o deresolve) inst
   574               :: print_dict_args vs
   575               @ str "="
   576               @@ brackets [
   577                 enum_default "()" ";" "{" "}" (map print_super_instance super_instances
   578                   @ map print_classparam_instance classparam_instances),
   579                 str ":",
   580                 print_tyco_expr NOBR (class, [tyco `%% map (ITyVar o fst) vs])
   581               ]
   582             ))
   583           end;
   584      fun print_stmt (ML_Exc (name, (vs_ty, n))) = pair
   585           [print_val_decl print_typscheme (name, vs_ty)]
   586           ((doublesemicolon o map str) (
   587             "let"
   588             :: deresolve name
   589             :: replicate n "_"
   590             @ "="
   591             :: "failwith"
   592             @@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name
   593           ))
   594       | print_stmt (ML_Val binding) =
   595           let
   596             val (sig_p, p) = print_def (K false) true "let" binding
   597           in pair
   598             [sig_p]
   599             (doublesemicolon [p])
   600           end
   601       | print_stmt (ML_Funs (binding :: bindings, pseudo_funs)) =
   602           let
   603             val print_def' = print_def (member (op =) pseudo_funs) false;
   604             fun print_pseudo_fun name = concat [
   605                 str "let",
   606                 (str o deresolve) name,
   607                 str "=",
   608                 (str o deresolve) name,
   609                 str "();;"
   610               ];
   611             val (sig_ps, (ps, p)) = (apsnd split_last o split_list)
   612               (print_def' "let rec" binding :: map (print_def' "and") bindings);
   613             val pseudo_ps = map print_pseudo_fun pseudo_funs;
   614           in pair
   615             sig_ps
   616             (Pretty.chunks (ps @ doublesemicolon [p] :: pseudo_ps))
   617           end
   618      | print_stmt (ML_Datas [(tyco, (vs, []))]) =
   619           let
   620             val ty_p = print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs);
   621           in
   622             pair
   623             [concat [str "type", ty_p]]
   624             (concat [str "type", ty_p, str "=", str "EMPTY__"])
   625           end
   626      | print_stmt (ML_Datas (data :: datas)) = 
   627           let
   628             val sig_ps = print_datatype_decl "type" data
   629               :: map (print_datatype_decl "and") datas;
   630             val (ps, p) = split_last sig_ps;
   631           in pair
   632             sig_ps
   633             (Pretty.chunks (ps @| doublesemicolon [p]))
   634           end
   635      | print_stmt (ML_Class (class, (v, (super_classes, classparams)))) =
   636           let
   637             fun print_field s p = concat [str s, str ":", p];
   638             fun print_super_class_field (super_class, classrel) =
   639               print_field (deresolve classrel) (print_dicttyp (super_class, ITyVar v));
   640             fun print_classparam_decl (classparam, ty) =
   641               print_val_decl print_typscheme
   642                 (classparam, ([(v, [class])], ty));
   643             fun print_classparam_field (classparam, ty) =
   644               print_field (deresolve classparam) (print_typ NOBR ty);
   645             val w = "_" ^ first_upper v;
   646             fun print_classparam_proj (classparam, _) =
   647               (concat o map str) ["let", deresolve classparam, w, "=",
   648                 w ^ "." ^ deresolve classparam ^ ";;"];
   649             val type_decl_p = concat [
   650                 str ("type '" ^ v),
   651                 (str o deresolve) class,
   652                 str "=",
   653                 enum_default "unit" ";" "{" "}" (
   654                   map print_super_class_field super_classes
   655                   @ map print_classparam_field classparams
   656                 )
   657               ];
   658           in pair
   659             (type_decl_p :: map print_classparam_decl classparams)
   660             (Pretty.chunks (
   661               doublesemicolon [type_decl_p]
   662               :: map print_classparam_proj classparams
   663             ))
   664           end;
   665   in print_stmt end;
   666 
   667 fun print_ocaml_module name some_decls body =
   668   Pretty.chunks2 (
   669     Pretty.chunks (
   670       str ("module " ^ name ^ (if is_some some_decls then " : sig" else " ="))
   671       :: (the_list o Option.map (indent 2 o Pretty.chunks)) some_decls
   672       @| (if is_some some_decls then str "end = struct" else str "struct")
   673     )
   674     :: body
   675     @| str ("end;; (*struct " ^ name ^ "*)")
   676   );
   677 
   678 val literals_ocaml = let
   679   fun chr i =
   680     let
   681       val xs = string_of_int i;
   682       val ys = replicate_string (3 - length (explode xs)) "0";
   683     in "\\" ^ ys ^ xs end;
   684   fun char_ocaml c =
   685     let
   686       val i = ord c;
   687       val s = if i < 32 orelse i = 34 orelse i = 39 orelse i = 92 orelse i > 126
   688         then chr i else c
   689     in s end;
   690   fun numeral_ocaml k = if k < 0
   691     then "(Big_int.minus_big_int " ^ numeral_ocaml (~ k) ^ ")"
   692     else if k <= 1073741823
   693       then "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
   694       else "(Big_int.big_int_of_string " ^ quote (string_of_int k) ^ ")"
   695 in Literals {
   696   literal_char = Library.enclose "'" "'" o char_ocaml,
   697   literal_string = quote o translate_string char_ocaml,
   698   literal_numeral = numeral_ocaml,
   699   literal_positive_numeral = numeral_ocaml,
   700   literal_alternative_numeral = numeral_ocaml,
   701   literal_naive_numeral = numeral_ocaml,
   702   literal_list = enum ";" "[" "]",
   703   infix_cons = (6, "::")
   704 } end;
   705 
   706 
   707 
   708 (** SML/OCaml generic part **)
   709 
   710 local
   711 
   712 datatype ml_node =
   713     Dummy of string
   714   | Stmt of string * ml_stmt
   715   | Module of string * ((Name.context * Name.context) * ml_node Graph.T);
   716 
   717 in
   718 
   719 fun ml_node_of_program labelled_name reserved module_alias program =
   720   let
   721     val reserved = Name.make_context reserved;
   722     val empty_module = ((reserved, reserved), Graph.empty);
   723     fun map_node [] f = f
   724       | map_node (m::ms) f =
   725           Graph.default_node (m, Module (m, empty_module))
   726           #> Graph.map_node m (fn (Module (module_name, (nsp, nodes))) =>
   727                Module (module_name, (nsp, map_node ms f nodes)));
   728     fun map_nsp_yield [] f (nsp, nodes) =
   729           let
   730             val (x, nsp') = f nsp
   731           in (x, (nsp', nodes)) end
   732       | map_nsp_yield (m::ms) f (nsp, nodes) =
   733           let
   734             val (x, nodes') =
   735               nodes
   736               |> Graph.default_node (m, Module (m, empty_module))
   737               |> Graph.map_node_yield m (fn Module (d_module_name, nsp_nodes) => 
   738                   let
   739                     val (x, nsp_nodes') = map_nsp_yield ms f nsp_nodes
   740                   in (x, Module (d_module_name, nsp_nodes')) end)
   741           in (x, (nsp, nodes')) end;
   742     fun map_nsp_fun_yield f (nsp_fun, nsp_typ) =
   743       let
   744         val (x, nsp_fun') = f nsp_fun
   745       in (x, (nsp_fun', nsp_typ)) end;
   746     fun map_nsp_typ_yield f (nsp_fun, nsp_typ) =
   747       let
   748         val (x, nsp_typ') = f nsp_typ
   749       in (x, (nsp_fun, nsp_typ')) end;
   750     val mk_name_module = mk_name_module reserved NONE module_alias program;
   751     fun mk_name_stmt upper name nsp =
   752       let
   753         val (_, base) = dest_name name;
   754         val base' = if upper then first_upper base else base;
   755         val ([base''], nsp') = Name.variants [base'] nsp;
   756       in (base'', nsp') end;
   757     fun deps_of names =
   758       []
   759       |> fold (fold (insert (op =)) o Graph.imm_succs program) names
   760       |> subtract (op =) names
   761       |> filter_out (Code_Thingol.is_case o Graph.get_node program);
   762     fun ml_binding_of_stmt (name, Code_Thingol.Fun (_, ((tysm as (vs, ty), raw_eqs), _))) =
   763           let
   764             val eqs = filter (snd o snd) raw_eqs;
   765             val (eqs', is_value) = if null (filter_out (null o snd) vs) then case eqs
   766                of [(([], t), some_thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty
   767                   then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), some_thm)], NONE)
   768                   else (eqs, SOME (name, member (op =) (Code_Thingol.add_constnames t []) name))
   769                 | _ => (eqs, NONE)
   770               else (eqs, NONE)
   771           in (ML_Function (name, (tysm, eqs')), is_value) end
   772       | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as ((_, (_, vs)), _))) =
   773           (ML_Instance (name, stmt), if forall (null o snd) vs then SOME (name, false) else NONE)
   774       | ml_binding_of_stmt (name, _) =
   775           error ("Binding block containing illegal statement: " ^ labelled_name name)
   776     fun add_fun (name, stmt) =
   777       let
   778         val (binding, some_value_name) = ml_binding_of_stmt (name, stmt);
   779         val ml_stmt = case binding
   780          of ML_Function (name, ((vs, ty), [])) =>
   781               ML_Exc (name, ((vs, ty),
   782                 (length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty))
   783           | _ => case some_value_name
   784              of NONE => ML_Funs ([binding], [])
   785               | SOME (name, true) => ML_Funs ([binding], [name])
   786               | SOME (name, false) => ML_Val binding
   787       in
   788         map_nsp_fun_yield (mk_name_stmt false name)
   789         #>> (fn name' => ([name'], ml_stmt))
   790       end;
   791     fun add_funs stmts =
   792       let
   793         val ml_stmt = ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst);
   794       in
   795         fold_map (fn (name, _) => map_nsp_fun_yield (mk_name_stmt false name)) stmts
   796         #>> rpair ml_stmt
   797       end;
   798     fun add_datatypes stmts =
   799       fold_map
   800         (fn (name, Code_Thingol.Datatype (_, stmt)) =>
   801               map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt))
   802           | (name, Code_Thingol.Datatypecons _) =>
   803               map_nsp_fun_yield (mk_name_stmt true name) #>> rpair NONE
   804           | (name, _) =>
   805               error ("Datatype block containing illegal statement: " ^ labelled_name name)
   806         ) stmts
   807       #>> (split_list #> apsnd (map_filter I
   808         #> (fn [] => error ("Datatype block without data statement: "
   809                   ^ (Library.commas o map (labelled_name o fst)) stmts)
   810              | stmts => ML_Datas stmts)));
   811     fun add_class stmts =
   812       fold_map
   813         (fn (name, Code_Thingol.Class (_, stmt)) =>
   814               map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt))
   815           | (name, Code_Thingol.Classrel _) =>
   816               map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
   817           | (name, Code_Thingol.Classparam _) =>
   818               map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
   819           | (name, _) =>
   820               error ("Class block containing illegal statement: " ^ labelled_name name)
   821         ) stmts
   822       #>> (split_list #> apsnd (map_filter I
   823         #> (fn [] => error ("Class block without class statement: "
   824                   ^ (Library.commas o map (labelled_name o fst)) stmts)
   825              | [stmt] => ML_Class stmt)));
   826     fun add_stmts ([stmt as (name, Code_Thingol.Fun _)]) =
   827           add_fun stmt
   828       | add_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) =
   829           add_funs stmts
   830       | add_stmts ((stmts as (_, Code_Thingol.Datatypecons _)::_)) =
   831           add_datatypes stmts
   832       | add_stmts ((stmts as (_, Code_Thingol.Datatype _)::_)) =
   833           add_datatypes stmts
   834       | add_stmts ((stmts as (_, Code_Thingol.Class _)::_)) =
   835           add_class stmts
   836       | add_stmts ((stmts as (_, Code_Thingol.Classrel _)::_)) =
   837           add_class stmts
   838       | add_stmts ((stmts as (_, Code_Thingol.Classparam _)::_)) =
   839           add_class stmts
   840       | add_stmts ([stmt as (_, Code_Thingol.Classinst _)]) =
   841           add_fun stmt
   842       | add_stmts ((stmts as (_, Code_Thingol.Classinst _)::_)) =
   843           add_funs stmts
   844       | add_stmts stmts = error ("Illegal mutual dependencies: " ^
   845           (Library.commas o map (labelled_name o fst)) stmts);
   846     fun add_stmts' stmts nsp_nodes =
   847       let
   848         val names as (name :: names') = map fst stmts;
   849         val deps = deps_of names;
   850         val (module_names, _) = (split_list o map dest_name) names;
   851         val module_name = (the_single o distinct (op =) o map mk_name_module) module_names
   852           handle Empty =>
   853             error ("Different namespace prefixes for mutual dependencies:\n"
   854               ^ Library.commas (map labelled_name names)
   855               ^ "\n"
   856               ^ Library.commas module_names);
   857         val module_name_path = Long_Name.explode module_name;
   858         fun add_dep name name' =
   859           let
   860             val module_name' = (mk_name_module o fst o dest_name) name';
   861           in if module_name = module_name' then
   862             map_node module_name_path (Graph.add_edge (name, name'))
   863           else let
   864             val (common, (diff1 :: _, diff2 :: _)) = chop_prefix (op =)
   865               (module_name_path, Long_Name.explode module_name');
   866           in
   867             map_node common
   868               (fn node => Graph.add_edge_acyclic (diff1, diff2) node
   869                 handle Graph.CYCLES _ => error ("Dependency "
   870                   ^ quote name ^ " -> " ^ quote name'
   871                   ^ " would result in module dependency cycle"))
   872           end end;
   873       in
   874         nsp_nodes
   875         |> map_nsp_yield module_name_path (add_stmts stmts)
   876         |-> (fn (base' :: bases', stmt') =>
   877            apsnd (map_node module_name_path (Graph.new_node (name, (Stmt (base', stmt')))
   878               #> fold2 (fn name' => fn base' =>
   879                    Graph.new_node (name', (Dummy base'))) names' bases')))
   880         |> apsnd (fold (fn name => fold (add_dep name) deps) names)
   881         |> apsnd (fold_product (curry (map_node module_name_path o Graph.add_edge)) names names)
   882       end;
   883     val stmts = map (AList.make (Graph.get_node program)) (rev (Graph.strong_conn program))
   884       |> filter_out (fn [(_, stmt)] => Code_Thingol.is_case stmt | _ => false);
   885     val (_, nodes) = fold add_stmts' stmts empty_module;
   886     fun deresolver prefix name = 
   887       let
   888         val module_name = (fst o dest_name) name;
   889         val module_name' = (Long_Name.explode o mk_name_module) module_name;
   890         val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name');
   891         val stmt_name =
   892           nodes
   893           |> fold (fn name => fn node => case Graph.get_node node name
   894               of Module (_, (_, node)) => node) module_name'
   895           |> (fn node => case Graph.get_node node name of Stmt (stmt_name, _) => stmt_name
   896                | Dummy stmt_name => stmt_name);
   897       in
   898         Long_Name.implode (remainder @ [stmt_name])
   899       end handle Graph.UNDEF _ =>
   900         error ("Unknown statement name: " ^ labelled_name name);
   901   in (deresolver, nodes) end;
   902 
   903 fun serialize_ml target print_module print_stmt with_signatures { labelled_name,
   904   reserved_syms, includes, module_alias, class_syntax, tyco_syntax,
   905   const_syntax, program, names, presentation_names } =
   906   let
   907     val is_cons = Code_Thingol.is_cons program;
   908     val is_presentation = not (null presentation_names);
   909     val (deresolver, nodes) = ml_node_of_program labelled_name
   910       reserved_syms module_alias program;
   911     val reserved = make_vars reserved_syms;
   912     fun print_node prefix (Dummy _) =
   913           NONE
   914       | print_node prefix (Stmt (_, stmt)) = if is_presentation andalso
   915           (null o filter (member (op =) presentation_names) o stmt_names_of) stmt
   916           then NONE
   917           else SOME (print_stmt labelled_name tyco_syntax const_syntax reserved is_cons (deresolver prefix) stmt)
   918       | print_node prefix (Module (module_name, (_, nodes))) =
   919           let
   920             val (decls, body) = print_nodes (prefix @ [module_name]) nodes;
   921             val p = if is_presentation then Pretty.chunks2 body
   922               else print_module module_name (if with_signatures then SOME decls else NONE) body;
   923           in SOME ([], p) end
   924     and print_nodes prefix nodes = (map_filter (print_node prefix o Graph.get_node nodes)
   925         o rev o flat o Graph.strong_conn) nodes
   926       |> split_list
   927       |> (fn (decls, body) => (flat decls, body))
   928     val names' = map (try (deresolver [])) names;
   929     val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] nodes));
   930     fun write width NONE = writeln_pretty width
   931       | write width (SOME p) = File.write p o string_of_pretty width;
   932   in
   933     Code_Target.serialization write (fn width => (rpair names' o string_of_pretty width)) p
   934   end;
   935 
   936 end; (*local*)
   937 
   938 val serializer_sml : Code_Target.serializer =
   939   Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
   940   >> (fn with_signatures => serialize_ml target_SML
   941       print_sml_module print_sml_stmt with_signatures));
   942 
   943 val serializer_ocaml : Code_Target.serializer =
   944   Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
   945   >> (fn with_signatures => serialize_ml target_OCaml
   946       print_ocaml_module print_ocaml_stmt with_signatures));
   947 
   948 
   949 (** Isar setup **)
   950 
   951 val setup =
   952   Code_Target.add_target
   953     (target_SML, { serializer = serializer_sml, literals = literals_sml,
   954       check = { env_var = "ISABELLE_PROCESS", make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
   955         make_command = fn isabelle => fn _ => isabelle ^ " -r -q -u Pure" } })
   956   #> Code_Target.add_target
   957     (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
   958       check = { env_var = "EXEC_OCAML", make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
   959         make_command = fn ocaml => fn _ => ocaml ^ " -w pu nums.cma ROOT.ocaml" } })
   960   #> Code_Target.add_tyco_syntax target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   961       brackify_infix (1, R) fxy (
   962         print_typ (INFX (1, X)) ty1,
   963         str "->",
   964         print_typ (INFX (1, R)) ty2
   965       )))
   966   #> Code_Target.add_tyco_syntax target_OCaml "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   967       brackify_infix (1, R) fxy (
   968         print_typ (INFX (1, X)) ty1,
   969         str "->",
   970         print_typ (INFX (1, R)) ty2
   971       )))
   972   #> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names
   973   #> fold (Code_Target.add_reserved target_SML)
   974       ["ref" (*rebinding is illegal*), "o" (*dictionary projections use it already*),
   975         "Fail", "div", "mod" (*standard infixes*), "IntInf"]
   976   #> fold (Code_Target.add_reserved target_OCaml) [
   977       "and", "as", "assert", "begin", "class",
   978       "constraint", "do", "done", "downto", "else", "end", "exception",
   979       "external", "false", "for", "fun", "function", "functor", "if",
   980       "in", "include", "inherit", "initializer", "lazy", "let", "match", "method",
   981       "module", "mutable", "new", "object", "of", "open", "or", "private", "rec",
   982       "sig", "struct", "then", "to", "true", "try", "type", "val",
   983       "virtual", "when", "while", "with"
   984     ]
   985   #> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod", "Big_int"];
   986 
   987 end; (*struct*)