src/Tools/Code/code_ml.ML
author haftmann
Thu Sep 02 10:29:48 2010 +0200 (2010-09-02)
changeset 39028 0dd6c5a0beef
parent 38966 68853347ba37
child 39031 b27d6643591c
permissions -rw-r--r--
use code_namespace module for SML and OCaml code
     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 =
   755       (SOME (ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst))
   756         :: replicate (length stmts - 1) NONE)
   757     fun modify_datatypes stmts =
   758       (SOME (ML_Datas (map_filter
   759         (fn (name, Code_Thingol.Datatype (_, stmt)) => SOME (name, stmt) | _ => NONE) stmts))
   760         :: replicate (length stmts - 1) NONE)
   761     fun modify_class stmts =
   762       (SOME (ML_Class (the_single (map_filter
   763         (fn (name, Code_Thingol.Class (_, stmt)) => SOME (name, stmt) | _ => NONE) stmts)))
   764         :: replicate (length stmts - 1) NONE)
   765     fun modify_stmts ([stmt as (name, Code_Thingol.Fun _)]) =
   766           [modify_fun stmt]
   767       | modify_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) =
   768           modify_funs stmts
   769       | modify_stmts ((stmts as (_, Code_Thingol.Datatypecons _)::_)) =
   770           modify_datatypes stmts
   771       | modify_stmts ((stmts as (_, Code_Thingol.Datatype _)::_)) =
   772           modify_datatypes stmts
   773       | modify_stmts ((stmts as (_, Code_Thingol.Class _)::_)) =
   774           modify_class stmts
   775       | modify_stmts ((stmts as (_, Code_Thingol.Classrel _)::_)) =
   776           modify_class stmts
   777       | modify_stmts ((stmts as (_, Code_Thingol.Classparam _)::_)) =
   778           modify_class stmts
   779       | modify_stmts ([stmt as (_, Code_Thingol.Classinst _)]) =
   780           [modify_fun stmt]
   781       | modify_stmts ((stmts as (_, Code_Thingol.Classinst _)::_)) =
   782           modify_funs stmts
   783       | modify_stmts stmts = error ("Illegal mutual dependencies: " ^
   784           (Library.commas o map (labelled_name o fst)) stmts);
   785   in
   786     Code_Namespace.hierarchical_program labelled_name { module_alias = module_alias, reserved = reserved,
   787       empty_nsp = (reserved, reserved), namify_module = pair, namify_stmt = namify_stmt,
   788       cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts } program
   789   end;
   790 
   791 local
   792 
   793 datatype ml_node =
   794     Dummy of string
   795   | Stmt of string * ml_stmt
   796   | Module of string * ((Name.context * Name.context) * ml_node Graph.T);
   797 
   798 in
   799 
   800 fun ml_node_of_program labelled_name reserved module_alias program =
   801   let
   802     val reserved = Name.make_context reserved;
   803     val empty_module = ((reserved, reserved), Graph.empty);
   804     fun map_node [] f = f
   805       | map_node (m::ms) f =
   806           Graph.default_node (m, Module (m, empty_module))
   807           #> Graph.map_node m (fn (Module (module_name, (nsp, nodes))) =>
   808                Module (module_name, (nsp, map_node ms f nodes)));
   809     fun map_nsp_yield [] f (nsp, nodes) =
   810           let
   811             val (x, nsp') = f nsp
   812           in (x, (nsp', nodes)) end
   813       | map_nsp_yield (m::ms) f (nsp, nodes) =
   814           let
   815             val (x, nodes') =
   816               nodes
   817               |> Graph.default_node (m, Module (m, empty_module))
   818               |> Graph.map_node_yield m (fn Module (d_module_name, nsp_nodes) => 
   819                   let
   820                     val (x, nsp_nodes') = map_nsp_yield ms f nsp_nodes
   821                   in (x, Module (d_module_name, nsp_nodes')) end)
   822           in (x, (nsp, nodes')) end;
   823     fun map_nsp_fun_yield f (nsp_fun, nsp_typ) =
   824       let
   825         val (x, nsp_fun') = f nsp_fun
   826       in (x, (nsp_fun', nsp_typ)) end;
   827     fun map_nsp_typ_yield f (nsp_fun, nsp_typ) =
   828       let
   829         val (x, nsp_typ') = f nsp_typ
   830       in (x, (nsp_fun, nsp_typ')) end;
   831     val mk_name_module = mk_name_module reserved NONE module_alias program;
   832     fun mk_name_stmt upper name nsp =
   833       let
   834         val (_, base) = dest_name name;
   835         val base' = if upper then first_upper base else base;
   836         val ([base''], nsp') = Name.variants [base'] nsp;
   837       in (base'', nsp') end;
   838     fun deps_of names =
   839       []
   840       |> fold (fold (insert (op =)) o Graph.imm_succs program) names
   841       |> subtract (op =) names
   842       |> filter_out (Code_Thingol.is_case o Graph.get_node program);
   843     fun ml_binding_of_stmt (name, Code_Thingol.Fun (_, ((tysm as (vs, ty), raw_eqs), _))) =
   844           let
   845             val eqs = filter (snd o snd) raw_eqs;
   846             val (eqs', is_value) = if null (filter_out (null o snd) vs) then case eqs
   847                of [(([], t), some_thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty
   848                   then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), some_thm)], NONE)
   849                   else (eqs, SOME (name, member (op =) (Code_Thingol.add_constnames t []) name))
   850                 | _ => (eqs, NONE)
   851               else (eqs, NONE)
   852           in (ML_Function (name, (tysm, eqs')), is_value) end
   853       | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as ((_, (_, vs)), _))) =
   854           (ML_Instance (name, stmt), if forall (null o snd) vs then SOME (name, false) else NONE)
   855       | ml_binding_of_stmt (name, _) =
   856           error ("Binding block containing illegal statement: " ^ labelled_name name)
   857     fun add_fun (name, stmt) =
   858       let
   859         val (binding, some_value_name) = ml_binding_of_stmt (name, stmt);
   860         val ml_stmt = case binding
   861          of ML_Function (name, ((vs, ty), [])) =>
   862               ML_Exc (name, ((vs, ty),
   863                 (length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty))
   864           | _ => case some_value_name
   865              of NONE => ML_Funs ([binding], [])
   866               | SOME (name, true) => ML_Funs ([binding], [name])
   867               | SOME (name, false) => ML_Val binding
   868       in
   869         map_nsp_fun_yield (mk_name_stmt false name)
   870         #>> (fn name' => ([name'], ml_stmt))
   871       end;
   872     fun add_funs stmts =
   873       let
   874         val ml_stmt = ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst);
   875       in
   876         fold_map (fn (name, _) => map_nsp_fun_yield (mk_name_stmt false name)) stmts
   877         #>> rpair ml_stmt
   878       end;
   879     fun add_datatypes stmts =
   880       fold_map
   881         (fn (name, Code_Thingol.Datatype (_, stmt)) =>
   882               map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt))
   883           | (name, Code_Thingol.Datatypecons _) =>
   884               map_nsp_fun_yield (mk_name_stmt true name) #>> rpair NONE
   885           | (name, _) =>
   886               error ("Datatype block containing illegal statement: " ^ labelled_name name)
   887         ) stmts
   888       #>> (split_list #> apsnd (map_filter I
   889         #> (fn [] => error ("Datatype block without data statement: "
   890                   ^ (Library.commas o map (labelled_name o fst)) stmts)
   891              | stmts => ML_Datas stmts)));
   892     fun add_class stmts =
   893       fold_map
   894         (fn (name, Code_Thingol.Class (_, stmt)) =>
   895               map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt))
   896           | (name, Code_Thingol.Classrel _) =>
   897               map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
   898           | (name, Code_Thingol.Classparam _) =>
   899               map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
   900           | (name, _) =>
   901               error ("Class block containing illegal statement: " ^ labelled_name name)
   902         ) stmts
   903       #>> (split_list #> apsnd (map_filter I
   904         #> (fn [] => error ("Class block without class statement: "
   905                   ^ (Library.commas o map (labelled_name o fst)) stmts)
   906              | [stmt] => ML_Class stmt)));
   907     fun add_stmts ([stmt as (name, Code_Thingol.Fun _)]) =
   908           add_fun stmt
   909       | add_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) =
   910           add_funs stmts
   911       | add_stmts ((stmts as (_, Code_Thingol.Datatypecons _)::_)) =
   912           add_datatypes stmts
   913       | add_stmts ((stmts as (_, Code_Thingol.Datatype _)::_)) =
   914           add_datatypes stmts
   915       | add_stmts ((stmts as (_, Code_Thingol.Class _)::_)) =
   916           add_class stmts
   917       | add_stmts ((stmts as (_, Code_Thingol.Classrel _)::_)) =
   918           add_class stmts
   919       | add_stmts ((stmts as (_, Code_Thingol.Classparam _)::_)) =
   920           add_class stmts
   921       | add_stmts ([stmt as (_, Code_Thingol.Classinst _)]) =
   922           add_fun stmt
   923       | add_stmts ((stmts as (_, Code_Thingol.Classinst _)::_)) =
   924           add_funs stmts
   925       | add_stmts stmts = error ("Illegal mutual dependencies: " ^
   926           (Library.commas o map (labelled_name o fst)) stmts);
   927     fun add_stmts' stmts nsp_nodes =
   928       let
   929         val names as (name :: names') = map fst stmts;
   930         val deps = deps_of names;
   931         val (module_names, _) = (split_list o map dest_name) names;
   932         val module_name = (the_single o distinct (op =) o map mk_name_module) module_names
   933           handle Empty =>
   934             error ("Different namespace prefixes for mutual dependencies:\n"
   935               ^ Library.commas (map labelled_name names)
   936               ^ "\n"
   937               ^ Library.commas module_names);
   938         val module_name_path = Long_Name.explode module_name;
   939         fun add_dep name name' =
   940           let
   941             val module_name' = (mk_name_module o fst o dest_name) name';
   942           in if module_name = module_name' then
   943             map_node module_name_path (Graph.add_edge (name, name'))
   944           else let
   945             val (common, (diff1 :: _, diff2 :: _)) = chop_prefix (op =)
   946               (module_name_path, Long_Name.explode module_name');
   947           in
   948             map_node common
   949               (fn node => Graph.add_edge_acyclic (diff1, diff2) node
   950                 handle Graph.CYCLES _ => error ("Dependency "
   951                   ^ quote name ^ " -> " ^ quote name'
   952                   ^ " would result in module dependency cycle"))
   953           end end;
   954       in
   955         nsp_nodes
   956         |> map_nsp_yield module_name_path (add_stmts stmts)
   957         |-> (fn (base' :: bases', stmt') =>
   958            apsnd (map_node module_name_path (Graph.new_node (name, (Stmt (base', stmt')))
   959               #> fold2 (fn name' => fn base' =>
   960                    Graph.new_node (name', (Dummy base'))) names' bases')))
   961         |> apsnd (fold (fn name => fold (add_dep name) deps) names)
   962         |> apsnd (fold_product (curry (map_node module_name_path o Graph.add_edge)) names names)
   963       end;
   964     val stmts = map (AList.make (Graph.get_node program)) (rev (Graph.strong_conn program))
   965       |> filter_out (fn [(_, stmt)] => Code_Thingol.is_case stmt | _ => false);
   966     val (_, nodes) = fold add_stmts' stmts empty_module;
   967     fun deresolver prefix name = 
   968       let
   969         val module_name = (fst o dest_name) name;
   970         val module_name' = (Long_Name.explode o mk_name_module) module_name;
   971         val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name');
   972         val stmt_name =
   973           nodes
   974           |> fold (fn name => fn node => case Graph.get_node node name
   975               of Module (_, (_, node)) => node) module_name'
   976           |> (fn node => case Graph.get_node node name of Stmt (stmt_name, _) => stmt_name
   977                | Dummy stmt_name => stmt_name);
   978       in
   979         Long_Name.implode (remainder @ [stmt_name])
   980       end handle Graph.UNDEF _ =>
   981         error ("Unknown statement name: " ^ labelled_name name);
   982   in (deresolver, nodes) end;
   983 
   984 fun serialize_ml target print_module print_stmt with_signatures { labelled_name,
   985   reserved_syms, includes, module_alias, class_syntax, tyco_syntax,
   986   const_syntax, program, names, presentation_names } =
   987   let
   988     val is_cons = Code_Thingol.is_cons program;
   989     val is_presentation = not (null presentation_names);
   990     val { deresolver, hierarchical_program = ml_program } =
   991       ml_program_of_program labelled_name (Name.make_context reserved_syms) module_alias program;
   992     fun print_node _ (_, Code_Namespace.Dummy) =
   993           NONE
   994       | print_node prefix_fragments (_, Code_Namespace.Stmt stmt) =
   995           if is_presentation andalso
   996             (null o filter (member (op =) presentation_names) o stmt_names_of) stmt
   997           then NONE
   998           else SOME (print_stmt labelled_name tyco_syntax const_syntax (make_vars reserved_syms)
   999             is_cons (deresolver prefix_fragments) stmt)
  1000       | print_node prefix_fragments (name_fragment, Code_Namespace.Module (_, nodes)) =
  1001           let
  1002             val (decls, body) = print_nodes (prefix_fragments @ [name_fragment]) nodes;
  1003             val p = if is_presentation then Pretty.chunks2 body
  1004               else print_module name_fragment
  1005                 (if with_signatures then SOME decls else NONE) body;
  1006           in SOME ([], p) end
  1007     and print_nodes prefix_fragments nodes = (map_filter
  1008         (fn name => print_node prefix_fragments (name, snd (Graph.get_node nodes name)))
  1009         o rev o flat o Graph.strong_conn) nodes
  1010       |> split_list
  1011       |> (fn (decls, body) => (flat decls, body))
  1012     val names' = map (try (deresolver [])) names;
  1013     val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] ml_program));
  1014     fun write width NONE = writeln_pretty width
  1015       | write width (SOME p) = File.write p o string_of_pretty width;
  1016   in
  1017     Code_Target.serialization write (fn width => (rpair names' o string_of_pretty width)) p
  1018   end;
  1019 
  1020 end; (*local*)
  1021 
  1022 val serializer_sml : Code_Target.serializer =
  1023   Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
  1024   >> (fn with_signatures => serialize_ml target_SML
  1025       print_sml_module print_sml_stmt with_signatures));
  1026 
  1027 val serializer_ocaml : Code_Target.serializer =
  1028   Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
  1029   >> (fn with_signatures => serialize_ml target_OCaml
  1030       print_ocaml_module print_ocaml_stmt with_signatures));
  1031 
  1032 
  1033 (** Isar setup **)
  1034 
  1035 val setup =
  1036   Code_Target.add_target
  1037     (target_SML, { serializer = serializer_sml, literals = literals_sml,
  1038       check = { env_var = "ISABELLE_PROCESS", make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
  1039         make_command = fn isabelle => fn _ => isabelle ^ " -r -q -u Pure" } })
  1040   #> Code_Target.add_target
  1041     (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
  1042       check = { env_var = "EXEC_OCAML", make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
  1043         make_command = fn ocaml => fn _ => ocaml ^ " -w pu nums.cma ROOT.ocaml" } })
  1044   #> Code_Target.add_tyco_syntax target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
  1045       brackify_infix (1, R) fxy (
  1046         print_typ (INFX (1, X)) ty1,
  1047         str "->",
  1048         print_typ (INFX (1, R)) ty2
  1049       )))
  1050   #> Code_Target.add_tyco_syntax target_OCaml "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
  1051       brackify_infix (1, R) fxy (
  1052         print_typ (INFX (1, X)) ty1,
  1053         str "->",
  1054         print_typ (INFX (1, R)) ty2
  1055       )))
  1056   #> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names
  1057   #> fold (Code_Target.add_reserved target_SML)
  1058       ["ref" (*rebinding is illegal*), "o" (*dictionary projections use it already*),
  1059         "Fail", "div", "mod" (*standard infixes*), "IntInf"]
  1060   #> fold (Code_Target.add_reserved target_OCaml) [
  1061       "and", "as", "assert", "begin", "class",
  1062       "constraint", "do", "done", "downto", "else", "end", "exception",
  1063       "external", "false", "for", "fun", "function", "functor", "if",
  1064       "in", "include", "inherit", "initializer", "lazy", "let", "match", "method",
  1065       "module", "mutable", "new", "object", "of", "open", "or", "private", "rec",
  1066       "sig", "struct", "then", "to", "true", "try", "type", "val",
  1067       "virtual", "when", "while", "with"
  1068     ]
  1069   #> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod", "Big_int"];
  1070 
  1071 end; (*struct*)