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