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