src/Tools/Code/code_ml.ML
author wenzelm
Sun Mar 13 19:16:19 2011 +0100 (2011-03-13)
changeset 41952 c7297638599b
parent 41940 a3b68a7a0e15
child 42599 1a82b0400b2a
permissions -rw-r--r--
cleanup of former settings GHC_PATH, EXEC_GHC, EXEC_OCAML, EXEC_SWIPL, EXEC_YAP -- discontinued implicit detection;
determine swipl_version at runtime;
     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_vars ((fold o Code_Thingol.fold_varnames)
   487                       (insert (op =)) ts []);
   488               in concat [
   489                 (Pretty.block o commas)
   490                   (map (print_term is_pseudo_fun some_thm vars NOBR) ts),
   491                 str "->",
   492                 print_term is_pseudo_fun some_thm vars NOBR t
   493               ] end;
   494             fun print_eqns is_pseudo [((ts, t), (some_thm, _))] =
   495                   let
   496                     val consts = fold Code_Thingol.add_constnames (t :: ts) [];
   497                     val vars = reserved
   498                       |> intro_base_names
   499                           (is_none o const_syntax) deresolve consts
   500                       |> intro_vars ((fold o Code_Thingol.fold_varnames)
   501                           (insert (op =)) ts []);
   502                   in
   503                     concat (
   504                       (if is_pseudo then [str "()"]
   505                         else map (print_term is_pseudo_fun some_thm vars BR) ts)
   506                       @ str "="
   507                       @@ print_term is_pseudo_fun some_thm vars NOBR t
   508                     )
   509                   end
   510               | print_eqns _ ((eq as (([_], _), _)) :: eqs) =
   511                   Pretty.block (
   512                     str "="
   513                     :: Pretty.brk 1
   514                     :: str "function"
   515                     :: Pretty.brk 1
   516                     :: print_eqn eq
   517                     :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
   518                           o single o print_eqn) eqs
   519                   )
   520               | print_eqns _ (eqs as eq :: eqs') =
   521                   let
   522                     val consts = fold Code_Thingol.add_constnames (map (snd o fst) eqs) [];
   523                     val vars = reserved
   524                       |> intro_base_names
   525                           (is_none o const_syntax) deresolve consts;
   526                     val dummy_parms = (map str o aux_params vars o map (fst o fst)) eqs;
   527                   in
   528                     Pretty.block (
   529                       Pretty.breaks dummy_parms
   530                       @ Pretty.brk 1
   531                       :: str "="
   532                       :: Pretty.brk 1
   533                       :: str "match"
   534                       :: Pretty.brk 1
   535                       :: (Pretty.block o commas) dummy_parms
   536                       :: Pretty.brk 1
   537                       :: str "with"
   538                       :: Pretty.brk 1
   539                       :: print_eqn eq
   540                       :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
   541                            o single o print_eqn) eqs'
   542                     )
   543                   end;
   544             val prolog = if needs_typ then
   545               concat [str definer, (str o deresolve) name, str ":", print_typ NOBR ty]
   546                 else (concat o map str) [definer, deresolve name];
   547           in pair
   548             (print_val_decl print_typscheme (name, vs_ty))
   549             (concat (
   550               prolog
   551               :: print_dict_args vs
   552               @| print_eqns (is_pseudo_fun name) eqs
   553             ))
   554           end
   555       | print_def is_pseudo_fun _ definer
   556             (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) =
   557           let
   558             fun print_super_instance (_, (classrel, x)) =
   559               concat [
   560                 (str o deresolve) classrel,
   561                 str "=",
   562                 print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const x))
   563               ];
   564             fun print_classparam_instance ((classparam, const), (thm, _)) =
   565               concat [
   566                 (str o deresolve) classparam,
   567                 str "=",
   568                 print_app (K false) (SOME thm) reserved NOBR (const, [])
   569               ];
   570           in pair
   571             (print_val_decl print_dicttypscheme
   572               (inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
   573             (concat (
   574               str definer
   575               :: (str o deresolve) inst
   576               :: print_dict_args vs
   577               @ str "="
   578               @@ brackets [
   579                 enum_default "()" ";" "{" "}" (map print_super_instance super_instances
   580                   @ map print_classparam_instance classparam_instances),
   581                 str ":",
   582                 print_tyco_expr NOBR (class, [tyco `%% map (ITyVar o fst) vs])
   583               ]
   584             ))
   585           end;
   586      fun print_stmt (ML_Exc (name, (vs_ty, n))) = pair
   587           [print_val_decl print_typscheme (name, vs_ty)]
   588           ((doublesemicolon o map str) (
   589             "let"
   590             :: deresolve name
   591             :: replicate n "_"
   592             @ "="
   593             :: "failwith"
   594             @@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name
   595           ))
   596       | print_stmt (ML_Val binding) =
   597           let
   598             val (sig_p, p) = print_def (K false) true "let" binding
   599           in pair
   600             [sig_p]
   601             (doublesemicolon [p])
   602           end
   603       | print_stmt (ML_Funs (binding :: bindings, pseudo_funs)) =
   604           let
   605             val print_def' = print_def (member (op =) pseudo_funs) false;
   606             fun print_pseudo_fun name = concat [
   607                 str "let",
   608                 (str o deresolve) name,
   609                 str "=",
   610                 (str o deresolve) name,
   611                 str "();;"
   612               ];
   613             val (sig_ps, (ps, p)) = (apsnd split_last o split_list)
   614               (print_def' "let rec" binding :: map (print_def' "and") bindings);
   615             val pseudo_ps = map print_pseudo_fun pseudo_funs;
   616           in pair
   617             sig_ps
   618             (Pretty.chunks (ps @ doublesemicolon [p] :: pseudo_ps))
   619           end
   620      | print_stmt (ML_Datas [(tyco, (vs, []))]) =
   621           let
   622             val ty_p = print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs);
   623           in
   624             pair
   625             [concat [str "type", ty_p]]
   626             (concat [str "type", ty_p, str "=", str "EMPTY__"])
   627           end
   628      | print_stmt (ML_Datas (data :: datas)) = 
   629           let
   630             val sig_ps = print_datatype_decl "type" data
   631               :: map (print_datatype_decl "and") datas;
   632             val (ps, p) = split_last sig_ps;
   633           in pair
   634             sig_ps
   635             (Pretty.chunks (ps @| doublesemicolon [p]))
   636           end
   637      | print_stmt (ML_Class (class, (v, (super_classes, classparams)))) =
   638           let
   639             fun print_field s p = concat [str s, str ":", p];
   640             fun print_super_class_field (super_class, classrel) =
   641               print_field (deresolve classrel) (print_dicttyp (super_class, ITyVar v));
   642             fun print_classparam_decl (classparam, ty) =
   643               print_val_decl print_typscheme
   644                 (classparam, ([(v, [class])], ty));
   645             fun print_classparam_field (classparam, ty) =
   646               print_field (deresolve classparam) (print_typ NOBR ty);
   647             val w = "_" ^ first_upper v;
   648             fun print_classparam_proj (classparam, _) =
   649               (concat o map str) ["let", deresolve classparam, w, "=",
   650                 w ^ "." ^ deresolve classparam ^ ";;"];
   651             val type_decl_p = concat [
   652                 str ("type '" ^ v),
   653                 (str o deresolve) class,
   654                 str "=",
   655                 enum_default "unit" ";" "{" "}" (
   656                   map print_super_class_field super_classes
   657                   @ map print_classparam_field classparams
   658                 )
   659               ];
   660           in pair
   661             (type_decl_p :: map print_classparam_decl classparams)
   662             (Pretty.chunks (
   663               doublesemicolon [type_decl_p]
   664               :: map print_classparam_proj classparams
   665             ))
   666           end;
   667   in print_stmt end;
   668 
   669 fun print_ocaml_module name some_decls body =
   670   Pretty.chunks2 (
   671     Pretty.chunks (
   672       str ("module " ^ name ^ (if is_some some_decls then " : sig" else " ="))
   673       :: (the_list o Option.map (indent 2 o Pretty.chunks)) some_decls
   674       @| (if is_some some_decls then str "end = struct" else str "struct")
   675     )
   676     :: body
   677     @| str ("end;; (*struct " ^ name ^ "*)")
   678   );
   679 
   680 val literals_ocaml = let
   681   fun chr i =
   682     let
   683       val xs = string_of_int i;
   684       val ys = replicate_string (3 - length (raw_explode xs)) "0";
   685     in "\\" ^ ys ^ xs end;
   686   fun char_ocaml c =
   687     let
   688       val i = ord c;
   689       val s = if i < 32 orelse i = 34 orelse i = 39 orelse i = 92 orelse i > 126
   690         then chr i else c
   691     in s end;
   692   fun numeral_ocaml k = if k < 0
   693     then "(Big_int.minus_big_int " ^ numeral_ocaml (~ k) ^ ")"
   694     else if k <= 1073741823
   695       then "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
   696       else "(Big_int.big_int_of_string " ^ quote (string_of_int k) ^ ")"
   697 in Literals {
   698   literal_char = Library.enclose "'" "'" o char_ocaml,
   699   literal_string = quote o translate_string char_ocaml,
   700   literal_numeral = numeral_ocaml,
   701   literal_positive_numeral = numeral_ocaml,
   702   literal_alternative_numeral = numeral_ocaml,
   703   literal_naive_numeral = numeral_ocaml,
   704   literal_list = enum ";" "[" "]",
   705   infix_cons = (6, "::")
   706 } end;
   707 
   708 
   709 
   710 (** SML/OCaml generic part **)
   711 
   712 fun ml_program_of_program labelled_name reserved module_alias program =
   713   let
   714     fun namify_const upper base (nsp_const, nsp_type) =
   715       let
   716         val (base', nsp_const') = yield_singleton Name.variants
   717           (if upper then first_upper base else base) nsp_const
   718       in (base', (nsp_const', nsp_type)) end;
   719     fun namify_type base (nsp_const, nsp_type) =
   720       let
   721         val (base', nsp_type') = yield_singleton Name.variants base nsp_type
   722       in (base', (nsp_const, nsp_type')) end;
   723     fun namify_stmt (Code_Thingol.Fun _) = namify_const false
   724       | namify_stmt (Code_Thingol.Datatype _) = namify_type
   725       | namify_stmt (Code_Thingol.Datatypecons _) = namify_const true
   726       | namify_stmt (Code_Thingol.Class _) = namify_type
   727       | namify_stmt (Code_Thingol.Classrel _) = namify_const false
   728       | namify_stmt (Code_Thingol.Classparam _) = namify_const false
   729       | namify_stmt (Code_Thingol.Classinst _) = namify_const false;
   730     fun ml_binding_of_stmt (name, Code_Thingol.Fun (_, ((tysm as (vs, ty), raw_eqs), _))) =
   731           let
   732             val eqs = filter (snd o snd) raw_eqs;
   733             val (eqs', some_value_name) = if null (filter_out (null o snd) vs) then case eqs
   734                of [(([], t), some_thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty
   735                   then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), some_thm)], NONE)
   736                   else (eqs, SOME (name, member (op =) (Code_Thingol.add_constnames t []) name))
   737                 | _ => (eqs, NONE)
   738               else (eqs, NONE)
   739           in (ML_Function (name, (tysm, eqs')), some_value_name) end
   740       | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as ((_, (_, vs)), _))) =
   741           (ML_Instance (name, stmt), if forall (null o snd) vs then SOME (name, false) else NONE)
   742       | ml_binding_of_stmt (name, _) =
   743           error ("Binding block containing illegal statement: " ^ labelled_name name)
   744     fun modify_fun (name, stmt) =
   745       let
   746         val (binding, some_value_name) = ml_binding_of_stmt (name, stmt);
   747         val ml_stmt = case binding
   748          of ML_Function (name, ((vs, ty), [])) =>
   749               ML_Exc (name, ((vs, ty),
   750                 (length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty))
   751           | _ => case some_value_name
   752              of NONE => ML_Funs ([binding], [])
   753               | SOME (name, true) => ML_Funs ([binding], [name])
   754               | SOME (name, false) => ML_Val binding
   755       in SOME ml_stmt end;
   756     fun modify_funs stmts = single (SOME
   757       (ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst)))
   758     fun modify_datatypes stmts = single (SOME
   759       (ML_Datas (map_filter
   760         (fn (name, Code_Thingol.Datatype (_, stmt)) => SOME (name, stmt) | _ => NONE) stmts)))
   761     fun modify_class stmts = single (SOME
   762       (ML_Class (the_single (map_filter
   763         (fn (name, Code_Thingol.Class (_, stmt)) => SOME (name, stmt) | _ => NONE) stmts))))
   764     fun modify_stmts ([stmt as (name, stmt' as Code_Thingol.Fun _)]) =
   765           if Code_Thingol.is_case stmt' then [] else [modify_fun stmt]
   766       | modify_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) =
   767           modify_funs (filter_out (Code_Thingol.is_case o snd) stmts)
   768       | modify_stmts ((stmts as (_, Code_Thingol.Datatypecons _)::_)) =
   769           modify_datatypes stmts
   770       | modify_stmts ((stmts as (_, Code_Thingol.Datatype _)::_)) =
   771           modify_datatypes stmts
   772       | modify_stmts ((stmts as (_, Code_Thingol.Class _)::_)) =
   773           modify_class stmts
   774       | modify_stmts ((stmts as (_, Code_Thingol.Classrel _)::_)) =
   775           modify_class stmts
   776       | modify_stmts ((stmts as (_, Code_Thingol.Classparam _)::_)) =
   777           modify_class stmts
   778       | modify_stmts ([stmt as (_, Code_Thingol.Classinst _)]) =
   779           [modify_fun stmt]
   780       | modify_stmts ((stmts as (_, Code_Thingol.Classinst _)::_)) =
   781           modify_funs stmts
   782       | modify_stmts stmts = error ("Illegal mutual dependencies: " ^
   783           (Library.commas o map (labelled_name o fst)) stmts);
   784   in
   785     Code_Namespace.hierarchical_program labelled_name { module_alias = module_alias, reserved = reserved,
   786       empty_nsp = (reserved, reserved), namify_module = pair, namify_stmt = namify_stmt,
   787       cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts } program
   788   end;
   789 
   790 fun serialize_ml target print_ml_module print_ml_stmt with_signatures
   791     { labelled_name, reserved_syms, includes, module_alias,
   792       class_syntax, tyco_syntax, const_syntax } program =
   793   let
   794 
   795     (* build program *)
   796     val { deresolver, hierarchical_program = ml_program } =
   797       ml_program_of_program labelled_name (Name.make_context reserved_syms) module_alias program;
   798 
   799     (* print statements *)
   800     fun print_stmt prefix_fragments (_, stmt) = print_ml_stmt
   801       labelled_name tyco_syntax const_syntax (make_vars reserved_syms)
   802       (Code_Thingol.is_cons program) (deresolver prefix_fragments) stmt
   803       |> apfst SOME;
   804 
   805     (* print modules *)
   806     fun print_module prefix_fragments base _ xs =
   807       let
   808         val (raw_decls, body) = split_list xs;
   809         val decls = if with_signatures then SOME (maps these raw_decls) else NONE 
   810       in (NONE, print_ml_module base decls body) end;
   811 
   812     (* serialization *)
   813     val p = Pretty.chunks2 (map snd includes
   814       @ map snd (Code_Namespace.print_hierarchical {
   815         print_module = print_module, print_stmt = print_stmt,
   816         lift_markup = apsnd } ml_program));
   817     fun write width NONE = writeln o format [] width
   818       | write width (SOME p) = File.write p o format [] width;
   819   in
   820     Code_Target.serialization write (rpair (try (deresolver [])) ooo format) p
   821   end;
   822 
   823 val serializer_sml : Code_Target.serializer =
   824   Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
   825   >> (fn with_signatures => serialize_ml target_SML
   826       print_sml_module print_sml_stmt with_signatures));
   827 
   828 val serializer_ocaml : Code_Target.serializer =
   829   Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
   830   >> (fn with_signatures => serialize_ml target_OCaml
   831       print_ocaml_module print_ocaml_stmt with_signatures));
   832 
   833 
   834 (** Isar setup **)
   835 
   836 val setup =
   837   Code_Target.add_target
   838     (target_SML, { serializer = serializer_sml, literals = literals_sml,
   839       check = { env_var = "ISABELLE_PROCESS",
   840         make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
   841         make_command = fn _ => "\"$ISABELLE_PROCESS\" -r -q -u Pure" } })
   842   #> Code_Target.add_target
   843     (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
   844       check = { env_var = "ISABELLE_OCAML",
   845         make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
   846         make_command = fn _ => "\"$ISABELLE_OCAML\" -w pu nums.cma ROOT.ocaml" } })
   847   #> Code_Target.add_tyco_syntax target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   848       brackify_infix (1, R) fxy (
   849         print_typ (INFX (1, X)) ty1,
   850         str "->",
   851         print_typ (INFX (1, R)) ty2
   852       )))
   853   #> Code_Target.add_tyco_syntax target_OCaml "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   854       brackify_infix (1, R) fxy (
   855         print_typ (INFX (1, X)) ty1,
   856         str "->",
   857         print_typ (INFX (1, R)) ty2
   858       )))
   859   #> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names
   860   #> fold (Code_Target.add_reserved target_SML)
   861       ["ref" (*rebinding is illegal*), "o" (*dictionary projections use it already*),
   862         "Fail", "div", "mod" (*standard infixes*), "IntInf"]
   863   #> fold (Code_Target.add_reserved target_OCaml) [
   864       "and", "as", "assert", "begin", "class",
   865       "constraint", "do", "done", "downto", "else", "end", "exception",
   866       "external", "false", "for", "fun", "function", "functor", "if",
   867       "in", "include", "inherit", "initializer", "lazy", "let", "match", "method",
   868       "module", "mutable", "new", "object", "of", "open", "or", "private", "rec",
   869       "sig", "struct", "then", "to", "true", "try", "type", "val",
   870       "virtual", "when", "while", "with"
   871     ]
   872   #> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod", "Big_int"];
   873 
   874 end; (*struct*)