# HG changeset patch
# User haftmann
# Date 1283253335 -7200
# Node ID ec2a8efd8990cea6162b2f089ef4e3701cf48704
# Parent  15f8cffdbf5d30e0823d7fff7abb8859a6a23dd0
Code_Printer.tuplify

diff -r 15f8cffdbf5d -r ec2a8efd8990 src/Tools/Code/code_eval.ML
--- a/src/Tools/Code/code_eval.ML	Tue Aug 31 13:08:58 2010 +0200
+++ b/src/Tools/Code/code_eval.ML	Tue Aug 31 13:15:35 2010 +0200
@@ -150,7 +150,7 @@
   let
     val k = Code.args_number thy const;
     fun pr pr' fxy ts = Code_Printer.brackify fxy
-      (const' :: the_list (Code_ML.print_tuple pr' Code_Printer.BR (map fst ts)));
+      (const' :: the_list (Code_Printer.tuplify pr' Code_Printer.BR (map fst ts)));
   in
     thy
     |> Code_Target.add_syntax_const target const (SOME (Code_Printer.simple_const_syntax (k, pr)))
diff -r 15f8cffdbf5d -r ec2a8efd8990 src/Tools/Code/code_ml.ML
--- 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
diff -r 15f8cffdbf5d -r ec2a8efd8990 src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Tue Aug 31 13:08:58 2010 +0200
+++ b/src/Tools/Code/code_printer.ML	Tue Aug 31 13:15:35 2010 +0200
@@ -68,6 +68,8 @@
   val brackify_infix: int * lrx -> fixity -> Pretty.T * Pretty.T * Pretty.T -> Pretty.T
   val brackify_block: fixity -> Pretty.T -> Pretty.T list -> Pretty.T -> Pretty.T
   val applify: string -> string -> ('a -> Pretty.T) -> fixity -> Pretty.T -> 'a list -> Pretty.T
+  val tuplify: (fixity -> 'a -> Pretty.T) -> fixity -> 'a list -> Pretty.T option
+
 
   type tyco_syntax
   type simple_const_syntax
@@ -244,6 +246,10 @@
       (if (fixity BR fxy_ctxt) then enclose "(" ")" else Pretty.block)
         (p @@ enum "," opn cls (map f ps));
 
+fun tuplify _ _ [] = NONE
+  | tuplify print fxy [x] = SOME (print fxy x)
+  | tuplify print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs));
+
 
 (* generic syntax *)
 
diff -r 15f8cffdbf5d -r ec2a8efd8990 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Tue Aug 31 13:08:58 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Tue Aug 31 13:15:35 2010 +0200
@@ -171,8 +171,8 @@
               else aux_params vars1 (map (fst o fst) eqs);
             val vars2 = intro_vars params vars1;
             val (tys', ty') = Code_Thingol.unfold_fun_n (length params) ty;
-            fun print_tuple [p] = p
-              | print_tuple ps = enum "," "(" ")" ps;
+            fun tuplify [p] = p
+              | tuplify ps = enum "," "(" ")" ps;
             fun print_rhs vars' ((_, t), (some_thm, _)) =
               print_term tyvars false some_thm vars' NOBR t;
             fun print_clause (eq as ((ts, _), (some_thm, _))) =
@@ -181,7 +181,7 @@
                   (insert (op =)) ts []) vars1;
               in
                 concat [str "case",
-                  print_tuple (map (print_term tyvars true some_thm vars' NOBR) ts),
+                  tuplify (map (print_term tyvars true some_thm vars' NOBR) ts),
                   str "=>", print_rhs vars' eq]
               end;
             val head = print_defhead tyvars vars2 name vs params tys' ty';
@@ -189,7 +189,7 @@
             concat [head, print_rhs vars2 (hd eqs)]
           else
             Pretty.block_enclose
-              (concat [head, print_tuple (map (str o lookup_var vars2) params),
+              (concat [head, tuplify (map (str o lookup_var vars2) params),
                 str "match", str "{"], str "}")
               (map print_clause eqs)
           end;