src/Tools/Code/code_ml.ML
author haftmann
Sun Feb 23 10:33:43 2014 +0100 (2014-02-23)
changeset 55681 7714287dc044
parent 55679 59244fc1a7ca
child 55682 def6575032df
permissions -rw-r--r--
more fine-grain notion of export
     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 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 first_upper v ^ "_"
    88             else first_upper 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 (binding :: 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") bindings);
   275             val pseudo_ps = map print_pseudo_fun pseudo_funs;
   276           in pair
   277             sig_ps
   278             (Pretty.chunks (ps @ semicolon [p] :: pseudo_ps))
   279           end
   280      | print_stmt _ (ML_Datas [(tyco, (vs, []))]) =
   281           let
   282             val ty_p = print_tyco_expr (Type_Constructor tyco, map ITyVar vs);
   283           in
   284             pair
   285             [concat [str "type", ty_p]]
   286             (semicolon [str "datatype", ty_p, str "=", str "EMPTY__"])
   287           end
   288      | print_stmt export (ML_Datas (data :: datas)) = 
   289           let
   290             val decl_ps = print_datatype_decl "datatype" data
   291               :: map (print_datatype_decl "and") datas;
   292             val (ps, p) = split_last decl_ps;
   293           in pair
   294             (if Code_Namespace.is_public export
   295               then decl_ps
   296               else map (fn (tyco, (vs, _)) =>
   297                 concat [str "type", print_tyco_expr (Type_Constructor tyco, map ITyVar vs)])
   298                 (data :: datas))
   299             (Pretty.chunks (ps @| semicolon [p]))
   300           end
   301      | print_stmt export (ML_Class (class, (v, (classrels, classparams)))) =
   302           let
   303             fun print_field s p = concat [str s, str ":", p];
   304             fun print_proj s p = semicolon
   305               (map str ["val", s, "=", "#" ^ s, ":"] @| p);
   306             fun print_super_class_decl (classrel as (_, super_class)) =
   307               print_val_decl print_dicttypscheme
   308                 (Class_Relation classrel, ([(v, [class])], (super_class, ITyVar v)));
   309             fun print_super_class_field (classrel as (_, super_class)) =
   310               print_field (deresolve_classrel classrel) (print_dicttyp (super_class, ITyVar v));
   311             fun print_super_class_proj (classrel as (_, super_class)) =
   312               print_proj (deresolve_classrel classrel)
   313                 (print_dicttypscheme ([(v, [class])], (super_class, ITyVar v)));
   314             fun print_classparam_decl (classparam, ty) =
   315               print_val_decl print_typscheme
   316                 (Constant classparam, ([(v, [class])], ty));
   317             fun print_classparam_field (classparam, ty) =
   318               print_field (deresolve_const classparam) (print_typ NOBR ty);
   319             fun print_classparam_proj (classparam, ty) =
   320               print_proj (deresolve_const classparam)
   321                 (print_typscheme ([(v, [class])], ty));
   322           in pair
   323             (concat [str "type", print_dicttyp (class, ITyVar v)]
   324               :: (if Code_Namespace.is_public export
   325                  then map print_super_class_decl classrels
   326                    @ map print_classparam_decl classparams
   327                  else []))
   328             (Pretty.chunks (
   329               concat [
   330                 str "type",
   331                 print_dicttyp (class, ITyVar v),
   332                 str "=",
   333                 enum "," "{" "};" (
   334                   map print_super_class_field classrels
   335                   @ map print_classparam_field classparams
   336                 )
   337               ]
   338               :: map print_super_class_proj classrels
   339               @ map print_classparam_proj classparams
   340             ))
   341           end;
   342   in print_stmt end;
   343 
   344 fun print_sml_module name decls body =
   345   Pretty.chunks2 (
   346     Pretty.chunks [
   347       str ("structure " ^ name ^ " : sig"),
   348       (indent 2 o Pretty.chunks) decls,
   349       str "end = struct"
   350     ]
   351     :: body
   352     @| str ("end; (*struct " ^ name ^ "*)")
   353   );
   354 
   355 val literals_sml = Literals {
   356   literal_char = prefix "#" o quote o ML_Syntax.print_char,
   357   literal_string = quote o translate_string ML_Syntax.print_char,
   358   literal_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
   359   literal_list = enum "," "[" "]",
   360   infix_cons = (7, "::")
   361 };
   362 
   363 
   364 (** OCaml serializer **)
   365 
   366 fun print_ocaml_stmt tyco_syntax const_syntax reserved is_constr deresolve =
   367   let
   368     val deresolve_const = deresolve o Constant;
   369     val deresolve_class = deresolve o Type_Class;
   370     val deresolve_classrel = deresolve o Class_Relation;
   371     val deresolve_inst = deresolve o Class_Instance;
   372     fun print_tyco_expr (sym, []) = (str o deresolve) sym
   373       | print_tyco_expr (sym, [ty]) =
   374           concat [print_typ BR ty, (str o deresolve) sym]
   375       | print_tyco_expr (sym, tys) =
   376           concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) sym]
   377     and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
   378          of NONE => print_tyco_expr (Type_Constructor tyco, tys)
   379           | SOME (_, print) => print print_typ fxy tys)
   380       | print_typ fxy (ITyVar v) = str ("'" ^ v);
   381     fun print_dicttyp (class, ty) = print_tyco_expr (Type_Class class, [ty]);
   382     fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
   383       (map_filter (fn (v, sort) =>
   384         (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
   385     fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);
   386     fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);
   387     val print_classrels =
   388       fold_rev (fn classrel => fn p => Pretty.block [p, str ".", (str o deresolve_classrel) classrel])
   389     fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) =
   390       print_plain_dict is_pseudo_fun fxy x
   391       |> print_classrels classrels
   392     and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) =
   393           brackify BR ((str o deresolve_inst) inst ::
   394             (if is_pseudo_fun (Class_Instance inst) then [str "()"]
   395             else map_filter (print_dicts is_pseudo_fun BR) dss))
   396       | print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =
   397           str (if k = 1 then "_" ^ first_upper v
   398             else "_" ^ first_upper v ^ string_of_int (i+1))
   399     and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
   400     val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
   401       (map_index (fn (i, _) => Dict ([], Dict_Var (v, (i, length sort)))) sort));
   402     fun print_term is_pseudo_fun some_thm vars fxy (IConst const) =
   403           print_app is_pseudo_fun some_thm vars fxy (const, [])
   404       | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
   405           str "_"
   406       | print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) =
   407           str (lookup_var vars v)
   408       | print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) =
   409           (case Code_Thingol.unfold_const_app t
   410            of SOME app => print_app is_pseudo_fun some_thm vars fxy app
   411             | NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1,
   412                 print_term is_pseudo_fun some_thm vars BR t2])
   413       | print_term is_pseudo_fun some_thm vars fxy (t as _ `|=> _) =
   414           let
   415             val (binds, t') = Code_Thingol.unfold_pat_abs t;
   416             val (ps, vars') = fold_map (print_bind is_pseudo_fun some_thm BR o fst) binds vars;
   417           in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun some_thm vars' NOBR t') end
   418       | print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) =
   419           (case Code_Thingol.unfold_const_app (#primitive case_expr)
   420            of SOME (app as ({ sym = Constant const, ... }, _)) =>
   421                 if is_none (const_syntax const)
   422                 then print_case is_pseudo_fun some_thm vars fxy case_expr
   423                 else print_app is_pseudo_fun some_thm vars fxy app
   424             | NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
   425     and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts = dss, dom = dom, ... }, ts)) =
   426       if is_constr sym then
   427         let val k = length dom in
   428           if length ts = k
   429           then (str o deresolve) sym
   430             :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
   431           else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
   432         end
   433       else if is_pseudo_fun sym
   434         then (str o deresolve) sym @@ str "()"
   435       else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dss
   436         @ map (print_term is_pseudo_fun some_thm vars BR) ts
   437     and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
   438       (print_term is_pseudo_fun) const_syntax some_thm vars
   439     and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
   440     and print_case is_pseudo_fun some_thm vars fxy { clauses = [], ... } =
   441           (concat o map str) ["failwith", "\"empty case\""]
   442       | print_case is_pseudo_fun some_thm vars fxy (case_expr as { clauses = [_], ... }) =
   443           let
   444             val (binds, body) = Code_Thingol.unfold_let (ICase case_expr);
   445             fun print_let ((pat, _), t) vars =
   446               vars
   447               |> print_bind is_pseudo_fun some_thm NOBR pat
   448               |>> (fn p => concat
   449                   [str "let", p, str "=", print_term is_pseudo_fun some_thm vars NOBR t, str "in"])
   450             val (ps, vars') = fold_map print_let binds vars;
   451           in
   452             brackify_block fxy (Pretty.chunks ps) []
   453               (print_term is_pseudo_fun some_thm vars' NOBR body)
   454           end
   455       | print_case is_pseudo_fun some_thm vars fxy { term = t, typ = ty, clauses = clause :: clauses, ... } =
   456           let
   457             fun print_select delim (pat, body) =
   458               let
   459                 val (p, vars') = print_bind is_pseudo_fun some_thm NOBR pat vars;
   460               in concat [str delim, p, str "->", print_term is_pseudo_fun some_thm vars' NOBR body] end;
   461           in
   462             brackets (
   463               str "match"
   464               :: print_term is_pseudo_fun some_thm vars NOBR t
   465               :: print_select "with" clause
   466               :: map (print_select "|") clauses
   467             )
   468           end;
   469     fun print_val_decl print_typscheme (sym, typscheme) = concat
   470       [str "val", str (deresolve sym), str ":", print_typscheme typscheme];
   471     fun print_datatype_decl definer (tyco, (vs, cos)) =
   472       let
   473         fun print_co ((co, _), []) = str (deresolve_const co)
   474           | print_co ((co, _), tys) = concat [str (deresolve_const co), str "of",
   475               enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
   476       in
   477         concat (
   478           str definer
   479           :: print_tyco_expr (Type_Constructor tyco, map ITyVar vs)
   480           :: str "="
   481           :: separate (str "|") (map print_co cos)
   482         )
   483       end;
   484     fun print_def is_pseudo_fun needs_typ definer
   485           (ML_Function (const, (vs_ty as (vs, ty), eqs))) =
   486           let
   487             fun print_eqn ((ts, t), (some_thm, _)) =
   488               let
   489                 val vars = reserved
   490                   |> intro_base_names_for (is_none o const_syntax)
   491                       deresolve (t :: ts)
   492                   |> intro_vars ((fold o Code_Thingol.fold_varnames)
   493                       (insert (op =)) ts []);
   494               in concat [
   495                 (Pretty.block o commas)
   496                   (map (print_term is_pseudo_fun some_thm vars NOBR) ts),
   497                 str "->",
   498                 print_term is_pseudo_fun some_thm vars NOBR t
   499               ] end;
   500             fun print_eqns is_pseudo [((ts, t), (some_thm, _))] =
   501                   let
   502                     val vars = reserved
   503                       |> intro_base_names_for (is_none o const_syntax)
   504                           deresolve (t :: ts)
   505                       |> intro_vars ((fold o Code_Thingol.fold_varnames)
   506                           (insert (op =)) ts []);
   507                   in
   508                     concat (
   509                       (if is_pseudo then [str "()"]
   510                         else map (print_term is_pseudo_fun some_thm vars BR) ts)
   511                       @ str "="
   512                       @@ print_term is_pseudo_fun some_thm vars NOBR t
   513                     )
   514                   end
   515               | print_eqns _ ((eq as (([_], _), _)) :: eqs) =
   516                   Pretty.block (
   517                     str "="
   518                     :: Pretty.brk 1
   519                     :: str "function"
   520                     :: Pretty.brk 1
   521                     :: print_eqn eq
   522                     :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
   523                           o single o print_eqn) eqs
   524                   )
   525               | print_eqns _ (eqs as eq :: eqs') =
   526                   let
   527                     val vars = reserved
   528                       |> intro_base_names_for (is_none o const_syntax)
   529                            deresolve (map (snd o fst) eqs)
   530                     val dummy_parms = (map str o aux_params vars o map (fst o fst)) eqs;
   531                   in
   532                     Pretty.block (
   533                       Pretty.breaks dummy_parms
   534                       @ Pretty.brk 1
   535                       :: str "="
   536                       :: Pretty.brk 1
   537                       :: str "match"
   538                       :: Pretty.brk 1
   539                       :: (Pretty.block o commas) dummy_parms
   540                       :: Pretty.brk 1
   541                       :: str "with"
   542                       :: Pretty.brk 1
   543                       :: print_eqn eq
   544                       :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
   545                            o single o print_eqn) eqs'
   546                     )
   547                   end;
   548             val prolog = if needs_typ then
   549               concat [str definer, (str o deresolve_const) const, str ":", print_typ NOBR ty]
   550                 else (concat o map str) [definer, deresolve_const const];
   551           in pair
   552             (print_val_decl print_typscheme (Constant const, vs_ty))
   553             (concat (
   554               prolog
   555               :: print_dict_args vs
   556               @| print_eqns (is_pseudo_fun (Constant const)) eqs
   557             ))
   558           end
   559       | print_def is_pseudo_fun _ definer
   560           (ML_Instance (inst as (tyco, class), { vs, superinsts, inst_params, ... })) =
   561           let
   562             fun print_super_instance (super_class, x) =
   563               concat [
   564                 (str o deresolve_classrel) (class, super_class),
   565                 str "=",
   566                 print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const ((tyco, super_class), x)))
   567               ];
   568             fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
   569               concat [
   570                 (str o deresolve_const) classparam,
   571                 str "=",
   572                 print_app (K false) (SOME thm) reserved NOBR (const, [])
   573               ];
   574           in pair
   575             (print_val_decl print_dicttypscheme
   576               (Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
   577             (concat (
   578               str definer
   579               :: (str o deresolve_inst) inst
   580               :: (if is_pseudo_fun (Class_Instance inst) then [str "()"]
   581                   else print_dict_args vs)
   582               @ str "="
   583               @@ brackets [
   584                 enum_default "()" ";" "{" "}" (map print_super_instance superinsts
   585                   @ map print_classparam_instance inst_params),
   586                 str ":",
   587                 print_dicttyp (class, tyco `%% map (ITyVar o fst) vs)
   588               ]
   589             ))
   590           end;
   591      fun print_stmt _ (ML_Exc (const, (vs_ty, n))) = pair
   592           [print_val_decl print_typscheme (Constant const, vs_ty)]
   593           ((doublesemicolon o map str) (
   594             "let"
   595             :: deresolve_const const
   596             :: replicate n "_"
   597             @ "="
   598             :: "failwith"
   599             @@ ML_Syntax.print_string const
   600           ))
   601       | print_stmt _ (ML_Val binding) =
   602           let
   603             val (sig_p, p) = print_def (K false) true "let" binding
   604           in pair
   605             [sig_p]
   606             (doublesemicolon [p])
   607           end
   608       | print_stmt _ (ML_Funs (binding :: bindings, pseudo_funs)) =
   609           let
   610             val print_def' = print_def (member (op =) pseudo_funs) false;
   611             fun print_pseudo_fun sym = concat [
   612                 str "let",
   613                 (str o deresolve) sym,
   614                 str "=",
   615                 (str o deresolve) sym,
   616                 str "();;"
   617               ];
   618             val (sig_ps, (ps, p)) = (apsnd split_last o split_list)
   619               (print_def' "let rec" binding :: map (print_def' "and") bindings);
   620             val pseudo_ps = map print_pseudo_fun pseudo_funs;
   621           in pair
   622             sig_ps
   623             (Pretty.chunks (ps @ doublesemicolon [p] :: pseudo_ps))
   624           end
   625      | print_stmt _ (ML_Datas [(tyco, (vs, []))]) =
   626           let
   627             val ty_p = print_tyco_expr (Type_Constructor tyco, map ITyVar vs);
   628           in
   629             pair
   630             [concat [str "type", ty_p]]
   631             (doublesemicolon [str "type", ty_p, str "=", str "EMPTY__"])
   632           end
   633      | print_stmt export (ML_Datas (data :: datas)) = 
   634           let
   635             val decl_ps = print_datatype_decl "type" data
   636               :: map (print_datatype_decl "and") datas;
   637             val (ps, p) = split_last decl_ps;
   638           in pair
   639             (if Code_Namespace.is_public export
   640               then decl_ps
   641               else map (fn (tyco, (vs, _)) =>
   642                 concat [str "type", print_tyco_expr (Type_Constructor tyco, map ITyVar vs)])
   643                 (data :: datas))
   644             (Pretty.chunks (ps @| doublesemicolon [p]))
   645           end
   646      | print_stmt export (ML_Class (class, (v, (classrels, classparams)))) =
   647           let
   648             fun print_field s p = concat [str s, str ":", p];
   649             fun print_super_class_field (classrel as (_, super_class)) =
   650               print_field (deresolve_classrel classrel) (print_dicttyp (super_class, ITyVar v));
   651             fun print_classparam_decl (classparam, ty) =
   652               print_val_decl print_typscheme
   653                 (Constant classparam, ([(v, [class])], ty));
   654             fun print_classparam_field (classparam, ty) =
   655               print_field (deresolve_const classparam) (print_typ NOBR ty);
   656             val w = "_" ^ first_upper v;
   657             fun print_classparam_proj (classparam, _) =
   658               (concat o map str) ["let", deresolve_const classparam, w, "=",
   659                 w ^ "." ^ deresolve_const classparam ^ ";;"];
   660             val type_decl_p = concat [
   661                 str ("type '" ^ v),
   662                 (str o deresolve_class) class,
   663                 str "=",
   664                 enum_default "unit" ";" "{" "}" (
   665                   map print_super_class_field classrels
   666                   @ map print_classparam_field classparams
   667                 )
   668               ];
   669           in pair
   670             (type_decl_p :: map print_classparam_decl classparams)
   671             (Pretty.chunks (
   672               doublesemicolon [type_decl_p]
   673               :: map print_classparam_proj classparams
   674             ))
   675           end;
   676   in print_stmt end;
   677 
   678 fun print_ocaml_module name decls body =
   679   Pretty.chunks2 (
   680     Pretty.chunks [
   681       str ("module " ^ name ^ " : sig"),
   682       (indent 2 o Pretty.chunks) decls,
   683       str "end = struct"
   684     ]
   685     :: body
   686     @| str ("end;; (*struct " ^ name ^ "*)")
   687   );
   688 
   689 val literals_ocaml = let
   690   fun chr i =
   691     let
   692       val xs = string_of_int i;
   693       val ys = replicate_string (3 - length (raw_explode xs)) "0";
   694     in "\\" ^ ys ^ xs end;
   695   fun char_ocaml c =
   696     let
   697       val i = ord c;
   698       val s = if i < 32 orelse i = 34 orelse i = 39 orelse i = 92 orelse i > 126
   699         then chr i else c
   700     in s end;
   701   fun numeral_ocaml k = if k < 0
   702     then "(Big_int.minus_big_int " ^ numeral_ocaml (~ k) ^ ")"
   703     else if k <= 1073741823
   704       then "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
   705       else "(Big_int.big_int_of_string " ^ quote (string_of_int k) ^ ")"
   706 in Literals {
   707   literal_char = Library.enclose "'" "'" o char_ocaml,
   708   literal_string = quote o translate_string char_ocaml,
   709   literal_numeral = numeral_ocaml,
   710   literal_list = enum ";" "[" "]",
   711   infix_cons = (6, "::")
   712 } end;
   713 
   714 
   715 
   716 (** SML/OCaml generic part **)
   717 
   718 fun ml_program_of_program ctxt module_name reserved identifiers =
   719   let
   720     fun namify_const upper base (nsp_const, nsp_type) =
   721       let
   722         val (base', nsp_const') =
   723           Name.variant (if upper then first_upper base else base) nsp_const
   724       in (base', (nsp_const', nsp_type)) end;
   725     fun namify_type base (nsp_const, nsp_type) =
   726       let
   727         val (base', nsp_type') = Name.variant base nsp_type
   728       in (base', (nsp_const, nsp_type')) end;
   729     fun namify_stmt (Code_Thingol.Fun _) = namify_const false
   730       | namify_stmt (Code_Thingol.Datatype _) = namify_type
   731       | namify_stmt (Code_Thingol.Datatypecons _) = namify_const true
   732       | namify_stmt (Code_Thingol.Class _) = namify_type
   733       | namify_stmt (Code_Thingol.Classrel _) = namify_const false
   734       | namify_stmt (Code_Thingol.Classparam _) = namify_const false
   735       | namify_stmt (Code_Thingol.Classinst _) = namify_const false;
   736     fun ml_binding_of_stmt (sym as Constant const, Code_Thingol.Fun ((tysm as (vs, ty), raw_eqs), _)) =
   737           let
   738             val eqs = filter (snd o snd) raw_eqs;
   739             val (eqs', some_sym) = if null (filter_out (null o snd) vs) then case eqs
   740                of [(([], t), some_thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty
   741                   then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), some_thm)], NONE)
   742                   else (eqs, SOME (sym, member (op =) (Code_Thingol.add_constsyms t []) sym))
   743                 | _ => (eqs, NONE)
   744               else (eqs, NONE)
   745           in (ML_Function (const, (tysm, eqs')), some_sym) end
   746       | ml_binding_of_stmt (sym as Class_Instance inst, Code_Thingol.Classinst (stmt as { vs, ... })) =
   747           (ML_Instance (inst, stmt), if forall (null o snd) vs then SOME (sym, false) else NONE)
   748       | ml_binding_of_stmt (sym, _) =
   749           error ("Binding block containing illegal statement: " ^ 
   750             Code_Symbol.quote ctxt sym)
   751     fun modify_fun (sym, stmt) =
   752       let
   753         val (binding, some_value_sym) = ml_binding_of_stmt (sym, stmt);
   754         val ml_stmt = case binding
   755          of ML_Function (const, ((vs, ty), [])) =>
   756               ML_Exc (const, ((vs, ty),
   757                 (length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty))
   758           | _ => case some_value_sym
   759              of NONE => ML_Funs ([binding], [])
   760               | SOME (sym, true) => ML_Funs ([binding], [sym])
   761               | SOME (sym, false) => ML_Val binding
   762       in SOME ml_stmt end;
   763     fun modify_funs stmts = single (SOME
   764       (ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst)))
   765     fun modify_datatypes stmts = single (SOME
   766       (ML_Datas (map_filter
   767         (fn (Type_Constructor tyco, Code_Thingol.Datatype stmt) => SOME (tyco, stmt) | _ => NONE) stmts)))
   768     fun modify_class stmts = single (SOME
   769       (ML_Class (the_single (map_filter
   770         (fn (Type_Class class, Code_Thingol.Class stmt) => SOME (class, stmt) | _ => NONE) stmts))))
   771     fun modify_stmts ([stmt as (_, stmt' as Code_Thingol.Fun _)]) =
   772           if Code_Thingol.is_case stmt' then [] else [modify_fun stmt]
   773       | modify_stmts ((stmts as (_, Code_Thingol.Fun _) :: _)) =
   774           modify_funs (filter_out (Code_Thingol.is_case o snd) stmts)
   775       | modify_stmts ((stmts as (_, Code_Thingol.Datatypecons _) :: _)) =
   776           modify_datatypes stmts
   777       | modify_stmts ((stmts as (_, Code_Thingol.Datatype _) :: _)) =
   778           modify_datatypes stmts
   779       | modify_stmts ((stmts as (_, Code_Thingol.Class _) :: _)) =
   780           modify_class stmts
   781       | modify_stmts ((stmts as (_, Code_Thingol.Classrel _) :: _)) =
   782           modify_class stmts
   783       | modify_stmts ((stmts as (_, Code_Thingol.Classparam _) :: _)) =
   784           modify_class stmts
   785       | modify_stmts ([stmt as (_, Code_Thingol.Classinst _)]) =
   786           [modify_fun stmt]
   787       | modify_stmts ((stmts as (_, Code_Thingol.Classinst _) :: _)) =
   788           modify_funs stmts
   789       | modify_stmts stmts = error ("Illegal mutual dependencies: " ^
   790           (Library.commas o map (Code_Symbol.quote ctxt o fst)) stmts);
   791   in
   792     Code_Namespace.hierarchical_program ctxt {
   793       module_name = module_name, reserved = reserved, identifiers = identifiers,
   794       empty_nsp = (reserved, reserved), namify_module = pair, namify_stmt = namify_stmt,
   795       cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts }
   796   end;
   797 
   798 fun serialize_ml print_ml_module print_ml_stmt ctxt
   799     { module_name, reserved_syms, identifiers, includes,
   800       class_syntax, tyco_syntax, const_syntax } program =
   801   let
   802 
   803     (* build program *)
   804     val { deresolver, hierarchical_program = ml_program } =
   805       ml_program_of_program ctxt module_name (Name.make_context reserved_syms)
   806         identifiers program;
   807 
   808     (* print statements *)
   809     fun print_stmt prefix_fragments (_, (export, stmt)) = print_ml_stmt
   810       tyco_syntax const_syntax (make_vars reserved_syms)
   811       (Code_Thingol.is_constr program) (deresolver prefix_fragments) export stmt
   812       |> apfst (fn decl => if Code_Namespace.not_private export then SOME decl else NONE);
   813 
   814     (* print modules *)
   815     fun print_module _ base _ xs =
   816       let
   817         val (raw_decls, body) = split_list xs;
   818         val decls = maps these raw_decls
   819       in (NONE, print_ml_module base decls body) end;
   820 
   821     (* serialization *)
   822     val p = Pretty.chunks2 (map snd includes
   823       @ map snd (Code_Namespace.print_hierarchical {
   824         print_module = print_module, print_stmt = print_stmt,
   825         lift_markup = apsnd } ml_program));
   826     fun write width NONE = writeln o format [] width
   827       | write width (SOME p) = File.write p o format [] width;
   828     fun prepare syms width p = ([("", format syms width p)], try (deresolver []));
   829   in
   830     Code_Target.serialization write prepare p
   831   end;
   832 
   833 val serializer_sml : Code_Target.serializer =
   834   Code_Target.parse_args (Scan.succeed ()) #> K (serialize_ml print_sml_module print_sml_stmt);
   835 
   836 val serializer_ocaml : Code_Target.serializer =
   837   Code_Target.parse_args (Scan.succeed ()) #> K (serialize_ml print_ocaml_module print_ocaml_stmt);
   838 
   839 
   840 (** Isar setup **)
   841 
   842 fun fun_syntax print_typ fxy [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 
   849 val setup =
   850   Code_Target.add_target
   851     (target_SML, { serializer = serializer_sml, literals = literals_sml,
   852       check = { env_var = "ISABELLE_PROCESS",
   853         make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
   854         make_command = fn _ =>
   855           "\"$ISABELLE_PROCESS\" -r -q -e 'datatype ref = datatype Unsynchronized.ref; use \"ROOT.ML\" handle _ => exit 1' Pure" } })
   856   #> Code_Target.add_target
   857     (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
   858       check = { env_var = "ISABELLE_OCAML",
   859         make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
   860         make_command = fn _ => "\"$ISABELLE_OCAML\" -w pu nums.cma ROOT.ocaml" } })
   861   #> Code_Target.set_printings (Type_Constructor ("fun",
   862     [(target_SML, SOME (2, fun_syntax)), (target_OCaml, SOME (2, fun_syntax))]))
   863   #> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names
   864   #> fold (Code_Target.add_reserved target_SML)
   865       ["ref" (*rebinding is illegal*), "o" (*dictionary projections use it already*),
   866         "Fail", "div", "mod" (*standard infixes*), "IntInf"]
   867   #> fold (Code_Target.add_reserved target_OCaml) [
   868       "and", "as", "assert", "begin", "class",
   869       "constraint", "do", "done", "downto", "else", "end", "exception",
   870       "external", "false", "for", "fun", "function", "functor", "if",
   871       "in", "include", "inherit", "initializer", "lazy", "let", "match", "method",
   872       "module", "mutable", "new", "object", "of", "open", "or", "private", "rec",
   873       "sig", "struct", "then", "to", "true", "try", "type", "val",
   874       "virtual", "when", "while", "with"
   875     ]
   876   #> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod", "Big_int"];
   877 
   878 end; (*struct*)