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