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