src/Tools/Code/code_ml.ML
author wenzelm
Thu Jun 09 17:51:49 2011 +0200 (2011-06-09)
changeset 43326 47cf4bc789aa
parent 42599 1a82b0400b2a
child 43345 165188299a25
permissions -rw-r--r--
simplified Name.variant -- discontinued builtin fold_map;
     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               :: print_dict_args vs
   579               @ str "="
   580               @@ brackets [
   581                 enum_default "()" ";" "{" "}" (map print_super_instance super_instances
   582                   @ map print_classparam_instance classparam_instances),
   583                 str ":",
   584                 print_tyco_expr NOBR (class, [tyco `%% map (ITyVar o fst) vs])
   585               ]
   586             ))
   587           end;
   588      fun print_stmt (ML_Exc (name, (vs_ty, n))) = pair
   589           [print_val_decl print_typscheme (name, vs_ty)]
   590           ((doublesemicolon o map str) (
   591             "let"
   592             :: deresolve name
   593             :: replicate n "_"
   594             @ "="
   595             :: "failwith"
   596             @@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name
   597           ))
   598       | print_stmt (ML_Val binding) =
   599           let
   600             val (sig_p, p) = print_def (K false) true "let" binding
   601           in pair
   602             [sig_p]
   603             (doublesemicolon [p])
   604           end
   605       | print_stmt (ML_Funs (binding :: bindings, pseudo_funs)) =
   606           let
   607             val print_def' = print_def (member (op =) pseudo_funs) false;
   608             fun print_pseudo_fun name = concat [
   609                 str "let",
   610                 (str o deresolve) name,
   611                 str "=",
   612                 (str o deresolve) name,
   613                 str "();;"
   614               ];
   615             val (sig_ps, (ps, p)) = (apsnd split_last o split_list)
   616               (print_def' "let rec" binding :: map (print_def' "and") bindings);
   617             val pseudo_ps = map print_pseudo_fun pseudo_funs;
   618           in pair
   619             sig_ps
   620             (Pretty.chunks (ps @ doublesemicolon [p] :: pseudo_ps))
   621           end
   622      | print_stmt (ML_Datas [(tyco, (vs, []))]) =
   623           let
   624             val ty_p = print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs);
   625           in
   626             pair
   627             [concat [str "type", ty_p]]
   628             (concat [str "type", ty_p, str "=", str "EMPTY__"])
   629           end
   630      | print_stmt (ML_Datas (data :: datas)) = 
   631           let
   632             val sig_ps = print_datatype_decl "type" data
   633               :: map (print_datatype_decl "and") datas;
   634             val (ps, p) = split_last sig_ps;
   635           in pair
   636             sig_ps
   637             (Pretty.chunks (ps @| doublesemicolon [p]))
   638           end
   639      | print_stmt (ML_Class (class, (v, (super_classes, classparams)))) =
   640           let
   641             fun print_field s p = concat [str s, str ":", p];
   642             fun print_super_class_field (super_class, classrel) =
   643               print_field (deresolve classrel) (print_dicttyp (super_class, ITyVar v));
   644             fun print_classparam_decl (classparam, ty) =
   645               print_val_decl print_typscheme
   646                 (classparam, ([(v, [class])], ty));
   647             fun print_classparam_field (classparam, ty) =
   648               print_field (deresolve classparam) (print_typ NOBR ty);
   649             val w = "_" ^ first_upper v;
   650             fun print_classparam_proj (classparam, _) =
   651               (concat o map str) ["let", deresolve classparam, w, "=",
   652                 w ^ "." ^ deresolve classparam ^ ";;"];
   653             val type_decl_p = concat [
   654                 str ("type '" ^ v),
   655                 (str o deresolve) class,
   656                 str "=",
   657                 enum_default "unit" ";" "{" "}" (
   658                   map print_super_class_field super_classes
   659                   @ map print_classparam_field classparams
   660                 )
   661               ];
   662           in pair
   663             (type_decl_p :: map print_classparam_decl classparams)
   664             (Pretty.chunks (
   665               doublesemicolon [type_decl_p]
   666               :: map print_classparam_proj classparams
   667             ))
   668           end;
   669   in print_stmt end;
   670 
   671 fun print_ocaml_module name some_decls body =
   672   Pretty.chunks2 (
   673     Pretty.chunks (
   674       str ("module " ^ name ^ (if is_some some_decls then " : sig" else " ="))
   675       :: (the_list o Option.map (indent 2 o Pretty.chunks)) some_decls
   676       @| (if is_some some_decls then str "end = struct" else str "struct")
   677     )
   678     :: body
   679     @| str ("end;; (*struct " ^ name ^ "*)")
   680   );
   681 
   682 val literals_ocaml = let
   683   fun chr i =
   684     let
   685       val xs = string_of_int i;
   686       val ys = replicate_string (3 - length (raw_explode xs)) "0";
   687     in "\\" ^ ys ^ xs end;
   688   fun char_ocaml c =
   689     let
   690       val i = ord c;
   691       val s = if i < 32 orelse i = 34 orelse i = 39 orelse i = 92 orelse i > 126
   692         then chr i else c
   693     in s end;
   694   fun numeral_ocaml k = if k < 0
   695     then "(Big_int.minus_big_int " ^ numeral_ocaml (~ k) ^ ")"
   696     else if k <= 1073741823
   697       then "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
   698       else "(Big_int.big_int_of_string " ^ quote (string_of_int k) ^ ")"
   699 in Literals {
   700   literal_char = Library.enclose "'" "'" o char_ocaml,
   701   literal_string = quote o translate_string char_ocaml,
   702   literal_numeral = numeral_ocaml,
   703   literal_positive_numeral = numeral_ocaml,
   704   literal_alternative_numeral = numeral_ocaml,
   705   literal_naive_numeral = numeral_ocaml,
   706   literal_list = enum ";" "[" "]",
   707   infix_cons = (6, "::")
   708 } end;
   709 
   710 
   711 
   712 (** SML/OCaml generic part **)
   713 
   714 fun ml_program_of_program labelled_name reserved module_alias program =
   715   let
   716     fun namify_const upper base (nsp_const, nsp_type) =
   717       let
   718         val (base', nsp_const') =
   719           Name.variant (if upper then first_upper base else base) nsp_const
   720       in (base', (nsp_const', nsp_type)) end;
   721     fun namify_type base (nsp_const, nsp_type) =
   722       let
   723         val (base', nsp_type') = Name.variant base nsp_type
   724       in (base', (nsp_const, nsp_type')) end;
   725     fun namify_stmt (Code_Thingol.Fun _) = namify_const false
   726       | namify_stmt (Code_Thingol.Datatype _) = namify_type
   727       | namify_stmt (Code_Thingol.Datatypecons _) = namify_const true
   728       | namify_stmt (Code_Thingol.Class _) = namify_type
   729       | namify_stmt (Code_Thingol.Classrel _) = namify_const false
   730       | namify_stmt (Code_Thingol.Classparam _) = namify_const false
   731       | namify_stmt (Code_Thingol.Classinst _) = namify_const false;
   732     fun ml_binding_of_stmt (name, Code_Thingol.Fun (_, ((tysm as (vs, ty), raw_eqs), _))) =
   733           let
   734             val eqs = filter (snd o snd) raw_eqs;
   735             val (eqs', some_value_name) = if null (filter_out (null o snd) vs) then case eqs
   736                of [(([], t), some_thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty
   737                   then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), some_thm)], NONE)
   738                   else (eqs, SOME (name, member (op =) (Code_Thingol.add_constnames t []) name))
   739                 | _ => (eqs, NONE)
   740               else (eqs, NONE)
   741           in (ML_Function (name, (tysm, eqs')), some_value_name) end
   742       | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as ((_, (_, vs)), _))) =
   743           (ML_Instance (name, stmt), if forall (null o snd) vs then SOME (name, false) else NONE)
   744       | ml_binding_of_stmt (name, _) =
   745           error ("Binding block containing illegal statement: " ^ labelled_name name)
   746     fun modify_fun (name, stmt) =
   747       let
   748         val (binding, some_value_name) = ml_binding_of_stmt (name, stmt);
   749         val ml_stmt = case binding
   750          of ML_Function (name, ((vs, ty), [])) =>
   751               ML_Exc (name, ((vs, ty),
   752                 (length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty))
   753           | _ => case some_value_name
   754              of NONE => ML_Funs ([binding], [])
   755               | SOME (name, true) => ML_Funs ([binding], [name])
   756               | SOME (name, false) => ML_Val binding
   757       in SOME ml_stmt end;
   758     fun modify_funs stmts = single (SOME
   759       (ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst)))
   760     fun modify_datatypes stmts = single (SOME
   761       (ML_Datas (map_filter
   762         (fn (name, Code_Thingol.Datatype (_, stmt)) => SOME (name, stmt) | _ => NONE) stmts)))
   763     fun modify_class stmts = single (SOME
   764       (ML_Class (the_single (map_filter
   765         (fn (name, Code_Thingol.Class (_, stmt)) => SOME (name, stmt) | _ => NONE) stmts))))
   766     fun modify_stmts ([stmt as (name, stmt' as Code_Thingol.Fun _)]) =
   767           if Code_Thingol.is_case stmt' then [] else [modify_fun stmt]
   768       | modify_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) =
   769           modify_funs (filter_out (Code_Thingol.is_case o snd) stmts)
   770       | modify_stmts ((stmts as (_, Code_Thingol.Datatypecons _)::_)) =
   771           modify_datatypes stmts
   772       | modify_stmts ((stmts as (_, Code_Thingol.Datatype _)::_)) =
   773           modify_datatypes stmts
   774       | modify_stmts ((stmts as (_, Code_Thingol.Class _)::_)) =
   775           modify_class stmts
   776       | modify_stmts ((stmts as (_, Code_Thingol.Classrel _)::_)) =
   777           modify_class stmts
   778       | modify_stmts ((stmts as (_, Code_Thingol.Classparam _)::_)) =
   779           modify_class stmts
   780       | modify_stmts ([stmt as (_, Code_Thingol.Classinst _)]) =
   781           [modify_fun stmt]
   782       | modify_stmts ((stmts as (_, Code_Thingol.Classinst _)::_)) =
   783           modify_funs stmts
   784       | modify_stmts stmts = error ("Illegal mutual dependencies: " ^
   785           (Library.commas o map (labelled_name o fst)) stmts);
   786   in
   787     Code_Namespace.hierarchical_program labelled_name { module_alias = module_alias, reserved = reserved,
   788       empty_nsp = (reserved, reserved), namify_module = pair, namify_stmt = namify_stmt,
   789       cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts } program
   790   end;
   791 
   792 fun serialize_ml target print_ml_module print_ml_stmt with_signatures
   793     { labelled_name, reserved_syms, includes, module_alias,
   794       class_syntax, tyco_syntax, const_syntax } program =
   795   let
   796 
   797     (* build program *)
   798     val { deresolver, hierarchical_program = ml_program } =
   799       ml_program_of_program labelled_name (Name.make_context reserved_syms) module_alias program;
   800 
   801     (* print statements *)
   802     fun print_stmt prefix_fragments (_, stmt) = print_ml_stmt
   803       labelled_name tyco_syntax const_syntax (make_vars reserved_syms)
   804       (Code_Thingol.is_cons program) (deresolver prefix_fragments) stmt
   805       |> apfst SOME;
   806 
   807     (* print modules *)
   808     fun print_module prefix_fragments base _ xs =
   809       let
   810         val (raw_decls, body) = split_list xs;
   811         val decls = if with_signatures then SOME (maps these raw_decls) else NONE 
   812       in (NONE, print_ml_module base decls body) end;
   813 
   814     (* serialization *)
   815     val p = Pretty.chunks2 (map snd includes
   816       @ map snd (Code_Namespace.print_hierarchical {
   817         print_module = print_module, print_stmt = print_stmt,
   818         lift_markup = apsnd } ml_program));
   819     fun write width NONE = writeln o format [] width
   820       | write width (SOME p) = File.write p o format [] width;
   821   in
   822     Code_Target.serialization write (rpair (try (deresolver [])) ooo format) p
   823   end;
   824 
   825 val serializer_sml : Code_Target.serializer =
   826   Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
   827   >> (fn with_signatures => serialize_ml target_SML
   828       print_sml_module print_sml_stmt with_signatures));
   829 
   830 val serializer_ocaml : Code_Target.serializer =
   831   Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
   832   >> (fn with_signatures => serialize_ml target_OCaml
   833       print_ocaml_module print_ocaml_stmt with_signatures));
   834 
   835 
   836 (** Isar setup **)
   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 _ => "\"$ISABELLE_PROCESS\" -r -q -u Pure" } })
   844   #> Code_Target.add_target
   845     (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
   846       check = { env_var = "ISABELLE_OCAML",
   847         make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
   848         make_command = fn _ => "\"$ISABELLE_OCAML\" -w pu nums.cma ROOT.ocaml" } })
   849   #> Code_Target.add_tyco_syntax target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   850       brackify_infix (1, R) fxy (
   851         print_typ (INFX (1, X)) ty1,
   852         str "->",
   853         print_typ (INFX (1, R)) ty2
   854       )))
   855   #> Code_Target.add_tyco_syntax target_OCaml "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   856       brackify_infix (1, R) fxy (
   857         print_typ (INFX (1, X)) ty1,
   858         str "->",
   859         print_typ (INFX (1, R)) ty2
   860       )))
   861   #> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names
   862   #> fold (Code_Target.add_reserved target_SML)
   863       ["ref" (*rebinding is illegal*), "o" (*dictionary projections use it already*),
   864         "Fail", "div", "mod" (*standard infixes*), "IntInf"]
   865   #> fold (Code_Target.add_reserved target_OCaml) [
   866       "and", "as", "assert", "begin", "class",
   867       "constraint", "do", "done", "downto", "else", "end", "exception",
   868       "external", "false", "for", "fun", "function", "functor", "if",
   869       "in", "include", "inherit", "initializer", "lazy", "let", "match", "method",
   870       "module", "mutable", "new", "object", "of", "open", "or", "private", "rec",
   871       "sig", "struct", "then", "to", "true", "try", "type", "val",
   872       "virtual", "when", "while", "with"
   873     ]
   874   #> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod", "Big_int"];
   875 
   876 end; (*struct*)