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