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