--- a/src/Tools/Code/code_ml.ML Tue Aug 31 13:08:58 2010 +0200
+++ b/src/Tools/Code/code_ml.ML Tue Aug 31 13:15:35 2010 +0200
@@ -8,8 +8,6 @@
sig
val target_SML: string
val target_OCaml: string
- val print_tuple: (Code_Printer.fixity -> 'a -> Pretty.T)
- -> Code_Printer.fixity -> 'a list -> Pretty.T option
val setup: theory -> theory
end;
@@ -54,9 +52,9 @@
| print_product print [x] = SOME (print x)
| print_product print xs = (SOME o enum " *" "" "") (map print xs);
-fun print_tuple _ _ [] = NONE
- | print_tuple print fxy [x] = SOME (print fxy x)
- | print_tuple print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs));
+fun tuplify _ _ [] = NONE
+ | tuplify print fxy [x] = SOME (print fxy x)
+ | tuplify print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs));
(** SML serializer **)
@@ -92,7 +90,7 @@
| classrels => brackets
[enum " o" "(" ")" (map (str o deresolve) classrels), v_p]
end
- and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun);
+ and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
(map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort));
fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
@@ -125,7 +123,7 @@
let val k = length function_typs in
if k < 2 orelse length ts = k
then (str o deresolve) c
- :: the_list (print_tuple (print_term is_pseudo_fun some_thm vars) BR ts)
+ :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
end
else if is_pseudo_fun c
@@ -393,7 +391,7 @@
else "_" ^ first_upper v ^ string_of_int (i+1))
|> fold_rev (fn classrel => fn p =>
Pretty.block [p, str ".", (str o deresolve) classrel]) classrels
- and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun);
+ and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
(map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort));
fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
@@ -423,7 +421,7 @@
let val k = length tys in
if length ts = k
then (str o deresolve) c
- :: the_list (print_tuple (print_term is_pseudo_fun some_thm vars) BR ts)
+ :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
end
else if is_pseudo_fun c