new names for predicate functions in the predicate compiler
* * *
adopting examples of the predicate compiler

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Nov 12 09:11:16 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Nov 12 09:11:26 2009 +0100
@@ -67,12 +67,30 @@
       | string_of_mode1 Output = "o"
       | string_of_mode1 Bool = "bool"
       | string_of_mode1 mode = "(" ^ (string_of_mode3 mode) ^ ")"
-    and string_of_mode2 (Pair (m1, m2))  = string_of_mode3 m1 ^ " * " ^  string_of_mode2 m2
+    and string_of_mode2 (Pair (m1, m2)) = string_of_mode3 m1 ^ " * " ^  string_of_mode2 m2
       | string_of_mode2 mode = string_of_mode1 mode
     and string_of_mode3 (Fun (m1, m2)) = string_of_mode2 m1 ^ " => " ^ string_of_mode3 m2
       | string_of_mode3 mode = string_of_mode2 mode
   in string_of_mode3 mode' end
 
+fun ascii_string_of_mode' mode' =
+  let
+    fun ascii_string_of_mode' Input = "i"
+      | ascii_string_of_mode' Output = "o"
+      | ascii_string_of_mode' Bool = "b"
+      | ascii_string_of_mode' (Pair (m1, m2)) =
+          "P" ^ ascii_string_of_mode' m1 ^ ascii_string_of_mode'_Pair m2
+      | ascii_string_of_mode' (Fun (m1, m2)) = 
+          "F" ^ ascii_string_of_mode' m1 ^ ascii_string_of_mode'_Fun m2 ^ "B"
+    and ascii_string_of_mode'_Fun (Fun (m1, m2)) =
+          ascii_string_of_mode' m1 ^ (if m2 = Bool then "" else "_" ^ ascii_string_of_mode'_Fun m2)
+      | ascii_string_of_mode'_Fun Bool = "B"
+      | ascii_string_of_mode'_Fun m = ascii_string_of_mode' m
+    and ascii_string_of_mode'_Pair (Pair (m1, m2)) =
+          ascii_string_of_mode' m1 ^ ascii_string_of_mode'_Pair m2
+      | ascii_string_of_mode'_Pair m = ascii_string_of_mode' m
+  in ascii_string_of_mode'_Fun mode' end
+
 fun translate_mode T (iss, is) =
   let
     val Ts = binder_types T

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Nov 12 09:11:16 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Nov 12 09:11:26 2009 +0100
@@ -1504,14 +1504,8 @@
 
 fun create_constname_of_mode options thy prefix name T mode = 
   let
-    fun string_of_mode mode = if null mode then "0"
-      else space_implode "_"
-        (map (fn (i, NONE) => string_of_int i | (i, SOME pis) => string_of_int i ^ "p"
-        ^ space_implode "p" (map string_of_int pis)) mode)
-    val HOmode = space_implode "_and_"
-      (fold (fn NONE => I | SOME mode => cons (string_of_mode mode)) (fst mode) [])
-    val system_proposal = prefix ^ (Long_Name.base_name name) ^
-      (if HOmode = "" then "_" else "_for_" ^ HOmode ^ "_yields_") ^ string_of_mode (snd mode)
+    val system_proposal = prefix ^ (Long_Name.base_name name)
+      ^ "_" ^ ascii_string_of_mode' (translate_mode T mode)
     val name = the_default system_proposal (proposed_names options name (translate_mode T mode))
   in
     Sign.full_bname thy name

--- a/src/HOL/ex/Predicate_Compile_ex.thy	Thu Nov 12 09:11:16 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Thu Nov 12 09:11:26 2009 +0100
@@ -339,7 +339,6 @@
 (*TODO: values with tupled modes*)
 (*values "{xs. tupled_append ([1,2,3], [4,5], xs)}"*)
 
-
 inductive tupled_append'
 where
 "tupled_append' ([], xs, xs)"
@@ -505,9 +504,9 @@
 
 text {* values command needs mode annotation of the parameter succ
 to disambiguate which mode is to be chosen. *} 
-(* TODO: adopt to new mode syntax *)
-values [mode: [1]] 20 "{n. tranclp succ 10 n}"
-values [mode: [2]] 10 "{n. tranclp succ n 10}"
+
+values [mode: i => o => bool] 20 "{n. tranclp succ 10 n}"
+values [mode: o => i => bool] 10 "{n. tranclp succ n 10}"
 values 20 "{(n, m). tranclp succ n m}"
 
 subsection {* IMP *}
@@ -598,8 +597,8 @@
   | "k \<ge> l \<Longrightarrow> divmod_rel (k - l) l q r \<Longrightarrow> divmod_rel k l (Suc q) r"
 
 code_pred divmod_rel ..
-
-value [code] "Predicate.the (divmod_rel_1_2 1705 42)"
+thm divmod_rel.equation
+value [code] "Predicate.the (divmod_rel_i_i_o_o 1705 42)"
 
 subsection {* Minimum *}