src/Tools/Code/code_ml.ML
author haftmann
Mon Jan 04 14:09:56 2010 +0100 (2010-01-04)
changeset 34244 03f8dcab55f3
parent 34178 a78b8d5b91cb
child 34246 5eaff81220a9
permissions -rw-r--r--
code cache without copy; tuned
     1 (*  Title:      Tools/code/code_ml.ML_
     2     Author:     Florian Haftmann, TU Muenchen
     3 
     4 Serializer for SML and OCaml.
     5 *)
     6 
     7 signature CODE_ML =
     8 sig
     9   val target_SML: string
    10   val evaluation_code_of: theory -> string -> string
    11     -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
    12   val setup: theory -> theory
    13 end;
    14 
    15 structure Code_ML : CODE_ML =
    16 struct
    17 
    18 open Basic_Code_Thingol;
    19 open Code_Printer;
    20 
    21 infixr 5 @@;
    22 infixr 5 @|;
    23 
    24 
    25 (** generic **)
    26 
    27 val target_SML = "SML";
    28 val target_OCaml = "OCaml";
    29 
    30 datatype ml_binding =
    31     ML_Function of string * (typscheme * ((iterm list * iterm) * (thm * bool)) list)
    32   | ML_Instance of string * ((class * (string * (vname * sort) list))
    33         * ((class * (string * (string * dict list list))) list
    34       * ((string * const) * (thm * bool)) list));
    35 
    36 datatype ml_stmt =
    37     ML_Exc of string * (typscheme * int)
    38   | ML_Val of ml_binding
    39   | ML_Funs of ml_binding list * string list
    40   | ML_Datas of (string * ((vname * sort) list * (string * itype list) list)) list
    41   | ML_Class of string * (vname * ((class * string) list * (string * itype) list));
    42 
    43 fun stmt_name_of_binding (ML_Function (name, _)) = name
    44   | stmt_name_of_binding (ML_Instance (name, _)) = name;
    45 
    46 fun stmt_names_of (ML_Exc (name, _)) = [name]
    47   | stmt_names_of (ML_Val binding) = [stmt_name_of_binding binding]
    48   | stmt_names_of (ML_Funs (bindings, _)) = map stmt_name_of_binding bindings
    49   | stmt_names_of (ML_Datas ds) = map fst ds
    50   | stmt_names_of (ML_Class (name, _)) = [name];
    51 
    52 fun print_product _ [] = NONE
    53   | print_product print [x] = SOME (print x)
    54   | print_product print xs = (SOME o enum " *" "" "") (map print xs);
    55 
    56 fun print_tuple _ _ [] = NONE
    57   | print_tuple print fxy [x] = SOME (print fxy x)
    58   | print_tuple print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs));
    59 
    60 
    61 (** SML serializer **)
    62 
    63 fun print_sml_stmt labelled_name syntax_tyco syntax_const reserved is_cons deresolve =
    64   let
    65     fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco
    66       | print_tyco_expr fxy (tyco, [ty]) =
    67           concat [print_typ BR ty, (str o deresolve) tyco]
    68       | print_tyco_expr fxy (tyco, tys) =
    69           concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]
    70     and print_typ fxy (tyco `%% tys) = (case syntax_tyco tyco
    71          of NONE => print_tyco_expr fxy (tyco, tys)
    72           | SOME (i, print) => print print_typ fxy tys)
    73       | print_typ fxy (ITyVar v) = str ("'" ^ v);
    74     fun print_dicttyp (class, ty) = print_tyco_expr NOBR (class, [ty]);
    75     fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
    76       (map_filter (fn (v, sort) =>
    77         (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
    78     fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);
    79     fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);
    80     fun print_dict is_pseudo_fun fxy (DictConst (inst, dss)) =
    81           brackify fxy ((str o deresolve) inst ::
    82             (if is_pseudo_fun inst then [str "()"]
    83             else map_filter (print_dicts is_pseudo_fun BR) dss))
    84       | print_dict is_pseudo_fun fxy (DictVar (classrels, (v, (i, k)))) =
    85           let
    86             val v_p = str (if k = 1 then first_upper v ^ "_"
    87               else first_upper v ^ string_of_int (i+1) ^ "_");
    88           in case classrels
    89            of [] => v_p
    90             | [classrel] => brackets [(str o deresolve) classrel, v_p]
    91             | classrels => brackets
    92                 [enum " o" "(" ")" (map (str o deresolve) classrels), v_p]
    93           end
    94     and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun);
    95     val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
    96       (map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort));
    97     fun print_term is_pseudo_fun thm vars fxy (IConst c) =
    98           print_app is_pseudo_fun thm vars fxy (c, [])
    99       | print_term is_pseudo_fun thm vars fxy (IVar NONE) =
   100           str "_"
   101       | print_term is_pseudo_fun thm vars fxy (IVar (SOME v)) =
   102           str (lookup_var vars v)
   103       | print_term is_pseudo_fun thm vars fxy (t as t1 `$ t2) =
   104           (case Code_Thingol.unfold_const_app t
   105            of SOME c_ts => print_app is_pseudo_fun thm vars fxy c_ts
   106             | NONE => brackify fxy [print_term is_pseudo_fun thm vars NOBR t1,
   107                 print_term is_pseudo_fun thm vars BR t2])
   108       | print_term is_pseudo_fun thm vars fxy (t as _ `|=> _) =
   109           let
   110             val (binds, t') = Code_Thingol.unfold_pat_abs t;
   111             fun print_abs (pat, ty) =
   112               print_bind is_pseudo_fun thm NOBR pat
   113               #>> (fn p => concat [str "fn", p, str "=>"]);
   114             val (ps, vars') = fold_map print_abs binds vars;
   115           in brackets (ps @ [print_term is_pseudo_fun thm vars' NOBR t']) end
   116       | print_term is_pseudo_fun thm vars fxy (ICase (cases as (_, t0))) =
   117           (case Code_Thingol.unfold_const_app t0
   118            of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
   119                 then print_case is_pseudo_fun thm vars fxy cases
   120                 else print_app is_pseudo_fun thm vars fxy c_ts
   121             | NONE => print_case is_pseudo_fun thm vars fxy cases)
   122     and print_app_expr is_pseudo_fun thm vars (app as ((c, ((_, iss), tys)), ts)) =
   123       if is_cons c then
   124         let val k = length tys in
   125           if k < 2 orelse length ts = k
   126           then (str o deresolve) c
   127             :: the_list (print_tuple (print_term is_pseudo_fun thm vars) BR ts)
   128           else [print_term is_pseudo_fun thm vars BR (Code_Thingol.eta_expand k app)]
   129         end
   130       else if is_pseudo_fun c
   131         then (str o deresolve) c @@ str "()"
   132       else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss
   133         @ map (print_term is_pseudo_fun thm vars BR) ts
   134     and print_app is_pseudo_fun thm vars = gen_print_app (print_app_expr is_pseudo_fun)
   135       (print_term is_pseudo_fun) syntax_const thm vars
   136     and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
   137     and print_case is_pseudo_fun thm vars fxy (cases as ((_, [_]), _)) =
   138           let
   139             val (binds, body) = Code_Thingol.unfold_let (ICase cases);
   140             fun print_match ((pat, ty), t) vars =
   141               vars
   142               |> print_bind is_pseudo_fun thm NOBR pat
   143               |>> (fn p => semicolon [str "val", p, str "=",
   144                     print_term is_pseudo_fun thm vars NOBR t])
   145             val (ps, vars') = fold_map print_match binds vars;
   146           in
   147             Pretty.chunks [
   148               Pretty.block [str "let", Pretty.fbrk, Pretty.chunks ps],
   149               Pretty.block [str "in", Pretty.fbrk, print_term is_pseudo_fun thm vars' NOBR body],
   150               str "end"
   151             ]
   152           end
   153       | print_case is_pseudo_fun thm vars fxy (((t, ty), clause :: clauses), _) =
   154           let
   155             fun print_select delim (pat, body) =
   156               let
   157                 val (p, vars') = print_bind is_pseudo_fun thm NOBR pat vars;
   158               in
   159                 concat [str delim, p, str "=>", print_term is_pseudo_fun thm vars' NOBR body]
   160               end;
   161           in
   162             brackets (
   163               str "case"
   164               :: print_term is_pseudo_fun thm vars NOBR t
   165               :: print_select "of" clause
   166               :: map (print_select "|") clauses
   167             )
   168           end
   169       | print_case is_pseudo_fun thm vars fxy ((_, []), _) =
   170           (concat o map str) ["raise", "Fail", "\"empty case\""];
   171     fun print_val_decl print_typscheme (name, typscheme) = concat
   172       [str "val", str (deresolve name), str ":", print_typscheme typscheme];
   173     fun print_datatype_decl definer (tyco, (vs, cos)) =
   174       let
   175         fun print_co (co, []) = str (deresolve co)
   176           | print_co (co, tys) = concat [str (deresolve co), str "of",
   177               enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
   178       in
   179         concat (
   180           str definer
   181           :: print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs)
   182           :: str "="
   183           :: separate (str "|") (map print_co cos)
   184         )
   185       end;
   186     fun print_def is_pseudo_fun needs_typ definer
   187           (ML_Function (name, (vs_ty as (vs, ty), eq :: eqs))) =
   188           let
   189             fun print_eqn definer ((ts, t), (thm, _)) =
   190               let
   191                 val consts = fold Code_Thingol.add_constnames (t :: ts) [];
   192                 val vars = reserved
   193                   |> intro_base_names
   194                        (is_none o syntax_const) deresolve consts
   195                   |> intro_vars ((fold o Code_Thingol.fold_varnames)
   196                        (insert (op =)) ts []);
   197                 val prolog = if needs_typ then
   198                   concat [str definer, (str o deresolve) name, str ":", print_typ NOBR ty]
   199                     else (concat o map str) [definer, deresolve name];
   200               in
   201                 concat (
   202                   prolog
   203                   :: (if is_pseudo_fun name then [str "()"]
   204                       else print_dict_args vs
   205                         @ map (print_term is_pseudo_fun thm vars BR) ts)
   206                   @ str "="
   207                   @@ print_term is_pseudo_fun thm vars NOBR t
   208                 )
   209               end
   210             val shift = if null eqs then I else
   211               map (Pretty.block o single o Pretty.block o single);
   212           in pair
   213             (print_val_decl print_typscheme (name, vs_ty))
   214             ((Pretty.block o Pretty.fbreaks o shift) (
   215               print_eqn definer eq
   216               :: map (print_eqn "|") eqs
   217             ))
   218           end
   219       | print_def is_pseudo_fun _ definer
   220           (ML_Instance (inst, ((class, (tyco, vs)), (superinsts, classparams)))) =
   221           let
   222             fun print_superinst (_, (classrel, dss)) =
   223               concat [
   224                 (str o Long_Name.base_name o deresolve) classrel,
   225                 str "=",
   226                 print_dict is_pseudo_fun NOBR (DictConst dss)
   227               ];
   228             fun print_classparam ((classparam, c_inst), (thm, _)) =
   229               concat [
   230                 (str o Long_Name.base_name o deresolve) classparam,
   231                 str "=",
   232                 print_app (K false) thm reserved NOBR (c_inst, [])
   233               ];
   234           in pair
   235             (print_val_decl print_dicttypscheme
   236               (inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
   237             (concat (
   238               str definer
   239               :: (str o deresolve) inst
   240               :: (if is_pseudo_fun inst then [str "()"]
   241                   else print_dict_args vs)
   242               @ str "="
   243               :: enum "," "{" "}"
   244                 (map print_superinst superinsts @ map print_classparam classparams)
   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, (superclasses, 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_superclass_decl (superclass, classrel) =
   307               print_val_decl print_dicttypscheme
   308                 (classrel, ([(v, [class])], (superclass, ITyVar v)));
   309             fun print_superclass_field (superclass, classrel) =
   310               print_field (deresolve classrel) (print_dicttyp (superclass, ITyVar v));
   311             fun print_superclass_proj (superclass, classrel) =
   312               print_proj (deresolve classrel)
   313                 (print_dicttypscheme ([(v, [class])], (superclass, 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_superclass_decl superclasses
   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_superclass_field superclasses
   333                   @ map print_classparam_field classparams
   334                 )
   335               ]
   336               :: map print_superclass_proj superclasses
   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 unbounded => fn k =>
   358     if unbounded then "(" ^ string_of_int k ^ " : IntInf.int)"
   359     else string_of_int k,
   360   literal_list = enum "," "[" "]",
   361   infix_cons = (7, "::")
   362 };
   363 
   364 
   365 (** OCaml serializer **)
   366 
   367 fun print_ocaml_stmt labelled_name syntax_tyco syntax_const 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 syntax_tyco 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 = print_tuple (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 thm vars fxy (IConst c) =
   397           print_app is_pseudo_fun thm vars fxy (c, [])
   398       | print_term is_pseudo_fun thm vars fxy (IVar NONE) =
   399           str "_"
   400       | print_term is_pseudo_fun thm vars fxy (IVar (SOME v)) =
   401           str (lookup_var vars v)
   402       | print_term is_pseudo_fun 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 thm vars fxy c_ts
   405             | NONE => brackify fxy [print_term is_pseudo_fun thm vars NOBR t1,
   406                 print_term is_pseudo_fun thm vars BR t2])
   407       | print_term is_pseudo_fun 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 thm BR o fst) binds vars;
   411           in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun thm vars' NOBR t') end
   412       | print_term is_pseudo_fun 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 (syntax_const c)
   415                 then print_case is_pseudo_fun thm vars fxy cases
   416                 else print_app is_pseudo_fun thm vars fxy c_ts
   417             | NONE => print_case is_pseudo_fun thm vars fxy cases)
   418     and print_app_expr is_pseudo_fun 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 (print_tuple (print_term is_pseudo_fun thm vars) BR ts)
   424           else [print_term is_pseudo_fun 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 thm vars BR) ts
   430     and print_app is_pseudo_fun thm vars = gen_print_app (print_app_expr is_pseudo_fun)
   431       (print_term is_pseudo_fun) syntax_const thm vars
   432     and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
   433     and print_case is_pseudo_fun 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 thm NOBR pat
   439               |>> (fn p => concat
   440                   [str "let", p, str "=", print_term is_pseudo_fun 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 thm vars' NOBR body)
   445           end
   446       | print_case is_pseudo_fun 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 thm NOBR pat vars;
   451               in concat [str delim, p, str "->", print_term is_pseudo_fun thm vars' NOBR body] end;
   452           in
   453             brackets (
   454               str "match"
   455               :: print_term is_pseudo_fun thm vars NOBR t
   456               :: print_select "with" clause
   457               :: map (print_select "|") clauses
   458             )
   459           end
   460       | print_case is_pseudo_fun 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), (thm, _)) =
   481               let
   482                 val consts = fold Code_Thingol.add_constnames (t :: ts) [];
   483                 val vars = reserved
   484                   |> intro_base_names
   485                       (is_none o syntax_const) deresolve consts
   486                   |> intro_vars ((fold o Code_Thingol.fold_varnames)
   487                       (insert (op =)) ts []);
   488               in concat [
   489                 (Pretty.block o Pretty.commas)
   490                   (map (print_term is_pseudo_fun thm vars NOBR) ts),
   491                 str "->",
   492                 print_term is_pseudo_fun thm vars NOBR t
   493               ] end;
   494             fun print_eqns is_pseudo [((ts, t), (thm, _))] =
   495                   let
   496                     val consts = fold Code_Thingol.add_constnames (t :: ts) [];
   497                     val vars = reserved
   498                       |> intro_base_names
   499                           (is_none o syntax_const) deresolve consts
   500                       |> intro_vars ((fold o Code_Thingol.fold_varnames)
   501                           (insert (op =)) ts []);
   502                   in
   503                     concat (
   504                       (if is_pseudo then [str "()"]
   505                         else map (print_term is_pseudo_fun thm vars BR) ts)
   506                       @ str "="
   507                       @@ print_term is_pseudo_fun thm vars NOBR t
   508                     )
   509                   end
   510               | print_eqns _ ((eq as (([_], _), _)) :: eqs) =
   511                   Pretty.block (
   512                     str "="
   513                     :: Pretty.brk 1
   514                     :: str "function"
   515                     :: Pretty.brk 1
   516                     :: print_eqn eq
   517                     :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
   518                           o single o print_eqn) eqs
   519                   )
   520               | print_eqns _ (eqs as eq :: eqs') =
   521                   let
   522                     val consts = fold Code_Thingol.add_constnames (map (snd o fst) eqs) [];
   523                     val vars = reserved
   524                       |> intro_base_names
   525                           (is_none o syntax_const) deresolve consts;
   526                     val dummy_parms = (map str o aux_params vars o map (fst o fst)) eqs;
   527                   in
   528                     Pretty.block (
   529                       Pretty.breaks dummy_parms
   530                       @ Pretty.brk 1
   531                       :: str "="
   532                       :: Pretty.brk 1
   533                       :: str "match"
   534                       :: Pretty.brk 1
   535                       :: (Pretty.block o Pretty.commas) dummy_parms
   536                       :: Pretty.brk 1
   537                       :: str "with"
   538                       :: Pretty.brk 1
   539                       :: print_eqn eq
   540                       :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
   541                            o single o print_eqn) eqs'
   542                     )
   543                   end;
   544             val prolog = if needs_typ then
   545               concat [str definer, (str o deresolve) name, str ":", print_typ NOBR ty]
   546                 else (concat o map str) [definer, deresolve name];
   547           in pair
   548             (print_val_decl print_typscheme (name, vs_ty))
   549             (concat (
   550               prolog
   551               :: print_dict_args vs
   552               @| print_eqns (is_pseudo_fun name) eqs
   553             ))
   554           end
   555       | print_def is_pseudo_fun _ definer (ML_Instance (inst, ((class, (tyco, vs)), (superinsts, classparams)))) =
   556           let
   557             fun print_superinst (_, (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 ((classparam, c_inst), (thm, _)) =
   564               concat [
   565                 (str o deresolve) classparam,
   566                 str "=",
   567                 print_app (K false) thm reserved NOBR (c_inst, [])
   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_superinst superinsts
   579                   @ map print_classparam classparams),
   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, (superclasses, classparams)))) =
   637           let
   638             fun print_field s p = concat [str s, str ":", p];
   639             fun print_superclass_field (superclass, classrel) =
   640               print_field (deresolve classrel) (print_dicttyp (superclass, 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_superclass_field superclasses
   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 bignum_ocaml k = 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 = fn unbounded => fn k => if k >= 0 then
   699       if unbounded then bignum_ocaml k
   700       else string_of_int k
   701     else
   702       if unbounded then "(Big_int.minus_big_int " ^ bignum_ocaml (~ k) ^ ")"
   703       else (Library.enclose "(" ")" o prefix "-" o string_of_int o op ~) k,
   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 module_name reserved raw_module_alias program =
   722   let
   723     val module_alias = if is_some module_name then K module_name else raw_module_alias;
   724     val reserved = Name.make_context reserved;
   725     val empty_module = ((reserved, reserved), Graph.empty);
   726     fun map_node [] f = f
   727       | map_node (m::ms) f =
   728           Graph.default_node (m, Module (m, empty_module))
   729           #> Graph.map_node m (fn (Module (module_name, (nsp, nodes))) =>
   730                Module (module_name, (nsp, map_node ms f nodes)));
   731     fun map_nsp_yield [] f (nsp, nodes) =
   732           let
   733             val (x, nsp') = f nsp
   734           in (x, (nsp', nodes)) end
   735       | map_nsp_yield (m::ms) f (nsp, nodes) =
   736           let
   737             val (x, nodes') =
   738               nodes
   739               |> Graph.default_node (m, Module (m, empty_module))
   740               |> Graph.map_node_yield m (fn Module (d_module_name, nsp_nodes) => 
   741                   let
   742                     val (x, nsp_nodes') = map_nsp_yield ms f nsp_nodes
   743                   in (x, Module (d_module_name, nsp_nodes')) end)
   744           in (x, (nsp, nodes')) end;
   745     fun map_nsp_fun_yield f (nsp_fun, nsp_typ) =
   746       let
   747         val (x, nsp_fun') = f nsp_fun
   748       in (x, (nsp_fun', nsp_typ)) end;
   749     fun map_nsp_typ_yield f (nsp_fun, nsp_typ) =
   750       let
   751         val (x, nsp_typ') = f nsp_typ
   752       in (x, (nsp_fun, nsp_typ')) end;
   753     val mk_name_module = mk_name_module reserved NONE module_alias program;
   754     fun mk_name_stmt upper name nsp =
   755       let
   756         val (_, base) = dest_name name;
   757         val base' = if upper then first_upper base else base;
   758         val ([base''], nsp') = Name.variants [base'] nsp;
   759       in (base'', nsp') end;
   760     fun ml_binding_of_stmt (name, Code_Thingol.Fun (_, (tysm as (vs, ty), raw_eqs))) =
   761           let
   762             val eqs = filter (snd o snd) raw_eqs;
   763             val (eqs', is_value) = if null (filter_out (null o snd) vs) then case eqs
   764                of [(([], t), thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty
   765                   then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), thm)], NONE)
   766                   else (eqs, SOME (name, member (op =) (Code_Thingol.add_constnames t []) name))
   767                 | _ => (eqs, NONE)
   768               else (eqs, NONE)
   769           in (ML_Function (name, (tysm, eqs')), is_value) end
   770       | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as ((_, (_, vs)), _))) =
   771           (ML_Instance (name, stmt), if forall (null o snd) vs then SOME (name, false) else NONE)
   772       | ml_binding_of_stmt (name, _) =
   773           error ("Binding block containing illegal statement: " ^ labelled_name name)
   774     fun add_fun (name, stmt) =
   775       let
   776         val (binding, some_value_name) = ml_binding_of_stmt (name, stmt);
   777         val ml_stmt = case binding
   778          of ML_Function (name, ((vs, ty), [])) =>
   779               ML_Exc (name, ((vs, ty),
   780                 (length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty))
   781           | _ => case some_value_name
   782              of NONE => ML_Funs ([binding], [])
   783               | SOME (name, true) => ML_Funs ([binding], [name])
   784               | SOME (name, false) => ML_Val binding
   785       in
   786         map_nsp_fun_yield (mk_name_stmt false name)
   787         #>> (fn name' => ([name'], ml_stmt))
   788       end;
   789     fun add_funs stmts =
   790       let
   791         val ml_stmt = ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst);
   792       in
   793         fold_map (fn (name, _) => map_nsp_fun_yield (mk_name_stmt false name)) stmts
   794         #>> rpair ml_stmt
   795       end;
   796     fun add_datatypes stmts =
   797       fold_map
   798         (fn (name, Code_Thingol.Datatype (_, stmt)) =>
   799               map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt))
   800           | (name, Code_Thingol.Datatypecons _) =>
   801               map_nsp_fun_yield (mk_name_stmt true name) #>> rpair NONE
   802           | (name, _) =>
   803               error ("Datatype block containing illegal statement: " ^ labelled_name name)
   804         ) stmts
   805       #>> (split_list #> apsnd (map_filter I
   806         #> (fn [] => error ("Datatype block without data statement: "
   807                   ^ (commas o map (labelled_name o fst)) stmts)
   808              | stmts => ML_Datas stmts)));
   809     fun add_class stmts =
   810       fold_map
   811         (fn (name, Code_Thingol.Class (_, stmt)) =>
   812               map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt))
   813           | (name, Code_Thingol.Classrel _) =>
   814               map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
   815           | (name, Code_Thingol.Classparam _) =>
   816               map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
   817           | (name, _) =>
   818               error ("Class block containing illegal statement: " ^ labelled_name name)
   819         ) stmts
   820       #>> (split_list #> apsnd (map_filter I
   821         #> (fn [] => error ("Class block without class statement: "
   822                   ^ (commas o map (labelled_name o fst)) stmts)
   823              | [stmt] => ML_Class stmt)));
   824     fun add_stmts ([stmt as (name, Code_Thingol.Fun _)]) =
   825           add_fun stmt
   826       | add_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) =
   827           add_funs stmts
   828       | add_stmts ((stmts as (_, Code_Thingol.Datatypecons _)::_)) =
   829           add_datatypes stmts
   830       | add_stmts ((stmts as (_, Code_Thingol.Datatype _)::_)) =
   831           add_datatypes stmts
   832       | add_stmts ((stmts as (_, Code_Thingol.Class _)::_)) =
   833           add_class stmts
   834       | add_stmts ((stmts as (_, Code_Thingol.Classrel _)::_)) =
   835           add_class stmts
   836       | add_stmts ((stmts as (_, Code_Thingol.Classparam _)::_)) =
   837           add_class stmts
   838       | add_stmts ([stmt as (_, Code_Thingol.Classinst _)]) =
   839           add_fun stmt
   840       | add_stmts ((stmts as (_, Code_Thingol.Classinst _)::_)) =
   841           add_funs stmts
   842       | add_stmts stmts = error ("Illegal mutual dependencies: " ^
   843           (commas o map (labelled_name o fst)) stmts);
   844     fun add_stmts' stmts nsp_nodes =
   845       let
   846         val names as (name :: names') = map fst stmts;
   847         val deps =
   848           []
   849           |> fold (fold (insert (op =)) o Graph.imm_succs program) names
   850           |> subtract (op =) names;
   851         val (module_names, _) = (split_list o map dest_name) names;
   852         val module_name = (the_single o distinct (op =) o map mk_name_module) module_names
   853           handle Empty =>
   854             error ("Different namespace prefixes for mutual dependencies:\n"
   855               ^ commas (map labelled_name names)
   856               ^ "\n"
   857               ^ commas module_names);
   858         val module_name_path = Long_Name.explode module_name;
   859         fun add_dep name name' =
   860           let
   861             val module_name' = (mk_name_module o fst o dest_name) name';
   862           in if module_name = module_name' then
   863             map_node module_name_path (Graph.add_edge (name, name'))
   864           else let
   865             val (common, (diff1 :: _, diff2 :: _)) = chop_prefix (op =)
   866               (module_name_path, Long_Name.explode module_name');
   867           in
   868             map_node common
   869               (fn node => Graph.add_edge_acyclic (diff1, diff2) node
   870                 handle Graph.CYCLES _ => error ("Dependency "
   871                   ^ quote name ^ " -> " ^ quote name'
   872                   ^ " would result in module dependency cycle"))
   873           end end;
   874       in
   875         nsp_nodes
   876         |> map_nsp_yield module_name_path (add_stmts stmts)
   877         |-> (fn (base' :: bases', stmt') =>
   878            apsnd (map_node module_name_path (Graph.new_node (name, (Stmt (base', stmt')))
   879               #> fold2 (fn name' => fn base' =>
   880                    Graph.new_node (name', (Dummy base'))) names' bases')))
   881         |> apsnd (fold (fn name => fold (add_dep name) deps) names)
   882         |> apsnd (fold_product (curry (map_node module_name_path o Graph.add_edge)) names names)
   883       end;
   884     val (_, nodes) = empty_module
   885       |> fold add_stmts' (map (AList.make (Graph.get_node program))
   886           (rev (Graph.strong_conn program)));
   887     fun deresolver prefix name = 
   888       let
   889         val module_name = (fst o dest_name) name;
   890         val module_name' = (Long_Name.explode o mk_name_module) module_name;
   891         val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name');
   892         val stmt_name =
   893           nodes
   894           |> fold (fn name => fn node => case Graph.get_node node name
   895               of Module (_, (_, node)) => node) module_name'
   896           |> (fn node => case Graph.get_node node name of Stmt (stmt_name, _) => stmt_name
   897                | Dummy stmt_name => stmt_name);
   898       in
   899         Long_Name.implode (remainder @ [stmt_name])
   900       end handle Graph.UNDEF _ =>
   901         error ("Unknown statement name: " ^ labelled_name name);
   902   in (deresolver, nodes) end;
   903 
   904 fun serialize_ml target compile print_module print_stmt raw_module_name with_signatures labelled_name
   905   reserved includes raw_module_alias _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program stmt_names destination =
   906   let
   907     val is_cons = Code_Thingol.is_cons program;
   908     val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
   909     val is_presentation = not (null presentation_stmt_names);
   910     val module_name = if is_presentation then SOME "Code" else raw_module_name;
   911     val (deresolver, nodes) = ml_node_of_program labelled_name module_name
   912       reserved raw_module_alias program;
   913     val reserved = make_vars reserved;
   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_stmt_names) o stmt_names_of) stmt
   918           then NONE
   919           else SOME (print_stmt labelled_name syntax_tyco syntax_const 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 stmt_names' = (map o try)
   931       (deresolver (if is_some module_name then the_list module_name else [])) stmt_names;
   932     val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] nodes));
   933   in
   934     Code_Target.mk_serialization target
   935       (case compile of SOME compile => SOME (compile o code_of_pretty) | NONE => NONE)
   936       (fn NONE => code_writeln | SOME file => File.write file o code_of_pretty)
   937       (rpair stmt_names' o code_of_pretty) p destination
   938   end;
   939 
   940 end; (*local*)
   941 
   942 
   943 (** for instrumentalization **)
   944 
   945 fun evaluation_code_of thy target struct_name =
   946   Code_Target.serialize_custom thy (target, (fn _ => fn [] =>
   947     serialize_ml target (SOME (K ())) print_sml_module print_sml_stmt (SOME struct_name) true, literals_sml));
   948 
   949 
   950 (** Isar setup **)
   951 
   952 fun isar_seri_sml module_name =
   953   Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
   954   >> (fn with_signatures => serialize_ml target_SML
   955       (SOME (use_text ML_Env.local_context (1, "generated code") false))
   956       print_sml_module print_sml_stmt module_name with_signatures));
   957 
   958 fun isar_seri_ocaml module_name =
   959   Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
   960   >> (fn with_signatures => serialize_ml target_OCaml NONE
   961       print_ocaml_module print_ocaml_stmt module_name with_signatures));
   962 
   963 val setup =
   964   Code_Target.add_target (target_SML, (isar_seri_sml, literals_sml))
   965   #> Code_Target.add_target (target_OCaml, (isar_seri_ocaml, literals_ocaml))
   966   #> Code_Target.add_syntax_tyco target_SML "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   #> Code_Target.add_syntax_tyco target_OCaml "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   973       brackify_infix (1, R) fxy [
   974         print_typ (INFX (1, X)) ty1,
   975         str "->",
   976         print_typ (INFX (1, R)) ty2
   977       ]))
   978   #> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names
   979   #> fold (Code_Target.add_reserved target_SML)
   980       ["o" (*dictionary projections use it already*), "Fail", "div", "mod" (*standard infixes*)]
   981   #> fold (Code_Target.add_reserved target_OCaml) [
   982       "and", "as", "assert", "begin", "class",
   983       "constraint", "do", "done", "downto", "else", "end", "exception",
   984       "external", "false", "for", "fun", "function", "functor", "if",
   985       "in", "include", "inherit", "initializer", "lazy", "let", "match", "method",
   986       "module", "mutable", "new", "object", "of", "open", "or", "private", "rec",
   987       "sig", "struct", "then", "to", "true", "try", "type", "val",
   988       "virtual", "when", "while", "with"
   989     ]
   990   #> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod"];
   991 
   992 end; (*struct*)