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