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