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