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