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