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