# HG changeset patch
# User bulwahn
# Date 1258013422 -3600
# Node ID b6bf2dc5aed7407f473b3bb2fce610ae92ac38a0
# Parent  d93a3cb55068b87afe66912f52f57f0e2a7d3928
added interface of user proposals for names of generated constants

diff -r d93a3cb55068 -r b6bf2dc5aed7 src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Thu Nov 12 09:10:16 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Thu Nov 12 09:10:22 2009 +0100
@@ -110,7 +110,10 @@
     fun chk s = member (op =) raw_options s
   in
     Options {
-      expected_modes = Option.map (pair const) modes,
+      expected_modes = Option.map ((pair const) o (map fst)) modes,
+      user_proposals =
+        the_default [] (Option.map (map_filter
+          (fn (m, NONE) => NONE | (m, SOME name) => SOME ((const, m), name))) modes),
       show_steps = chk "show_steps",
       show_intermediate_results = chk "show_intermediate_results",
       show_proof_trace = chk "show_proof_trace",
@@ -198,9 +201,12 @@
 and new_parse_mode3 xs =
   (new_parse_mode2 --| Args.$$$ "=>" -- new_parse_mode3 >> Fun || new_parse_mode2) xs
 
+val mode_and_opt_proposal = new_parse_mode3 --
+  Scan.optional (Args.$$$ "as" |-- P.xname >> SOME) NONE
+
 val opt_modes =
   Scan.optional (P.$$$ "(" |-- Args.$$$ "mode" |-- P.$$$ ":" |--
-    P.enum1 "," new_parse_mode3 --| P.$$$ ")" >> SOME) NONE
+    P.enum1 "," mode_and_opt_proposal --| P.$$$ ")" >> SOME) NONE
 
 (* Parser for options *)
 
diff -r d93a3cb55068 -r b6bf2dc5aed7 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Nov 12 09:10:16 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Nov 12 09:10:22 2009 +0100
@@ -266,6 +266,7 @@
 
 datatype options = Options of {  
   expected_modes : (string * mode' list) option,
+  user_proposals : ((string * mode') * string) list,
   show_steps : bool,
   show_proof_trace : bool,
   show_intermediate_results : bool,
@@ -281,6 +282,9 @@
 };
 
 fun expected_modes (Options opt) = #expected_modes opt
+fun user_proposal (Options opt) name mode = AList.lookup (eq_pair (op =) eq_mode')
+  (#user_proposals opt) (name, mode)
+
 fun show_steps (Options opt) = #show_steps opt
 fun show_intermediate_results (Options opt) = #show_intermediate_results opt
 fun show_proof_trace (Options opt) = #show_proof_trace opt
@@ -296,6 +300,7 @@
 
 val default_options = Options {
   expected_modes = NONE,
+  user_proposals = [],
   show_steps = false,
   show_intermediate_results = false,
   show_proof_trace = false,
diff -r d93a3cb55068 -r b6bf2dc5aed7 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Nov 12 09:10:16 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Nov 12 09:10:22 2009 +0100
@@ -1503,7 +1503,7 @@
   (introthm, elimthm)
 end;
 
-fun create_constname_of_mode thy prefix name mode = 
+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 "_"
@@ -1511,9 +1511,11 @@
         ^ 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 name = the_default system_proposal (user_proposal options name (translate_mode T mode))
   in
-    (Sign.full_bname thy (prefix ^ (Long_Name.base_name name))) ^
-      (if HOmode = "" then "_" else "_for_" ^ HOmode ^ "_yields_") ^ (string_of_mode (snd mode))
+    Sign.full_bname thy name
   end;
 
 fun split_tupleT is T =
@@ -1542,12 +1544,12 @@
     HOLogic.mk_tuple args
   end
 
-fun create_definitions preds (name, modes) thy =
+fun create_definitions options preds (name, modes) thy =
   let
     val compfuns = PredicateCompFuns.compfuns
     val T = AList.lookup (op =) preds name |> the
     fun create_definition (mode as (iss, is)) thy = let
-      val mode_cname = create_constname_of_mode thy "" name mode
+      val mode_cname = create_constname_of_mode options thy "" name T mode
       val mode_cbasename = Long_Name.base_name mode_cname
       val Ts = binder_types T
       val (Ts1, Ts2) = chop (length iss) Ts
@@ -1617,13 +1619,13 @@
     fold create_definition modes thy
   end;
 
-fun define_functions comp_modifiers compfuns preds (name, modes) thy =
+fun define_functions comp_modifiers compfuns options preds (name, modes) thy =
   let
     val T = AList.lookup (op =) preds name |> the
     fun create_definition mode thy =
       let
         val function_name_prefix = Comp_Mod.function_name_prefix comp_modifiers
-        val mode_cname = create_constname_of_mode thy function_name_prefix name mode
+        val mode_cname = create_constname_of_mode options thy function_name_prefix name T mode
         val funT = Comp_Mod.funT_of comp_modifiers compfuns mode T
       in
         thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)]
@@ -2220,7 +2222,7 @@
   {
   compile_preds : theory -> string list -> string list -> (string * typ) list
     -> (moded_clause list) pred_mode_table -> term pred_mode_table,
-  define_functions : (string * typ) list -> string * mode list -> theory -> theory,
+  define_functions : options -> (string * typ) list -> string * mode list -> theory -> theory,
   infer_modes : options -> theory -> (string * mode list) list -> (string * mode list) list
     -> string list -> (string * (term list * indprem list) list) list
     -> moded_clause list pred_mode_table,
@@ -2251,7 +2253,7 @@
     val _ = print_modes options thy modes
       (*val _ = print_moded_clauses thy moded_clauses*)
     val _ = print_step options "Defining executable functions..."
-    val thy' = fold (#define_functions (dest_steps steps) preds) modes thy
+    val thy' = fold (#define_functions (dest_steps steps) options preds) modes thy
       |> Theory.checkpoint
     val _ = print_step options "Compiling equations..."
     val compiled_terms =
@@ -2356,7 +2358,7 @@
 val random_comp_modifiers = Comp_Mod.Comp_Modifiers
   {function_name_of = random_function_name_of,
   set_function_name = set_random_function_name,
-  function_name_prefix = "random",
+  function_name_prefix = "random_",
   funT_of = K random_function_funT_of : (compilation_funs -> mode -> typ -> typ),
   additional_arguments = fn names => [Free (Name.variant names "size", @{typ code_numeral})],
   wrap_compilation = K (K (K (K (K I))))
@@ -2367,7 +2369,7 @@
 val annotated_comp_modifiers = Comp_Mod.Comp_Modifiers
   {function_name_of = annotated_function_name_of,
   set_function_name = set_annotated_function_name,
-  function_name_prefix = "annotated",
+  function_name_prefix = "annotated_",
   funT_of = funT_of : (compilation_funs -> mode -> typ -> typ),
   additional_arguments = K [],
   wrap_compilation =