wneuper/isa: src/Tools/Code/code

     1 (*  Title:      Tools/Code/code_ml.ML

     2     Author:     Florian Haftmann, TU Muenchen

     4 Serializer for SML and OCaml.

     5 *)

     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;

    18 structure Code_ML : CODE_ML =

    19 struct

    21 open Basic_Code_Thingol;

    22 open Code_Printer;

    24 infixr 5 @@;

    25 infixr 5 @|;

    28 (** generic **)

    30 val target_SML = "SML";

    31 val target_OCaml = "OCaml";

    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)));

    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));

    46 fun stmt_name_of_binding (ML_Function (name, _)) = name

    47   | stmt_name_of_binding (ML_Instance (name, _)) = name;

    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];

    55 fun print_product _ [] = NONE

    56   | print_product print [x] = SOME (print x)

    57   | print_product print xs = (SOME o enum " *" "" "") (map print xs);

    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));

    64 (** SML serializer **)

    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;

   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   );

   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 };

   370 (** OCaml serializer **)

   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;

   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   );

   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;

   714 (** SML/OCaml generic part **)

   716 local

   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);

   723 in

   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;

   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.serialization write (fn width => (rpair stmt_names' o string_of_pretty width)) p

   941   end;

   943 end; (*local*)

   946 (** for instrumentalization **)

   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);

   953 (** Isar setup **)

   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));

   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));

   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"];

  1001 end; (*struct*)

author	haftmann
	Mon, 30 Aug 2010 16:33:06 +0200
changeset 39142	c0b857a04758
parent 39141	026526cba0e6
child 39147	15f8cffdbf5d
permissions	-rw-r--r--