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