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