# HG changeset patch
# User blanchet
# Date 1306485008 -7200
# Node ID 58150aa44941616ac3bf34134dc94be4c3aacb91
# Parent  cb8d4c2af639c150e5f35ea2bbe4b142aba2b32d
prioritize try and auto try's tools, with fast ones first, with a slight preference for provers vs. counterexample generators

diff -r cb8d4c2af639 -r 58150aa44941 src/HOL/Tools/Nitpick/nitpick_isar.ML
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Fri May 27 10:30:08 2011 +0200
@@ -403,6 +403,6 @@
 
 fun try_nitpick auto = pick_nits [] (if auto then Auto_Try else Try) 1 0
 
-val setup = Try.register_tool (nitpickN, (auto, try_nitpick))
+val setup = Try.register_tool (nitpickN, (50, auto, try_nitpick))
 
 end;
diff -r cb8d4c2af639 -r 58150aa44941 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 27 10:30:08 2011 +0200
@@ -414,6 +414,6 @@
                      (minimize_command [] i) state
   end
 
-val setup = Try.register_tool (sledgehammerN, (auto, try_sledgehammer))
+val setup = Try.register_tool (sledgehammerN, (40, auto, try_sledgehammer))
 
 end;
diff -r cb8d4c2af639 -r 58150aa44941 src/HOL/Tools/try_methods.ML
--- a/src/HOL/Tools/try_methods.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/try_methods.ML	Fri May 27 10:30:08 2011 +0200
@@ -182,6 +182,6 @@
 
 fun try_try_methods auto = do_try_methods auto NONE ([], [], [], [])
 
-val setup = Try.register_tool (try_methodsN, (auto, try_try_methods))
+val setup = Try.register_tool (try_methodsN, (20, auto, try_try_methods))
 
 end;
diff -r cb8d4c2af639 -r 58150aa44941 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/Tools/quickcheck.ML	Fri May 27 10:30:08 2011 +0200
@@ -653,7 +653,7 @@
   end
   |> `(fn (outcome_code, _) => outcome_code = genuineN)
 
-val setup = Try.register_tool (quickcheckN, (auto, try_quickcheck))
+val setup = Try.register_tool (quickcheckN, (30, auto, try_quickcheck))
 
 end;
 
diff -r cb8d4c2af639 -r 58150aa44941 src/Tools/solve_direct.ML
--- a/src/Tools/solve_direct.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/Tools/solve_direct.ML	Fri May 27 10:30:08 2011 +0200
@@ -106,6 +106,6 @@
 
 (* hook *)
 
-val setup = Try.register_tool (solve_directN, (auto, solve_direct));
+val setup = Try.register_tool (solve_directN, (10, auto, solve_direct));
 
 end;
diff -r cb8d4c2af639 -r 58150aa44941 src/Tools/try.ML
--- a/src/Tools/try.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/Tools/try.ML	Fri May 27 10:30:08 2011 +0200
@@ -7,7 +7,7 @@
 signature TRY =
 sig
   type tool =
-    string * (bool Unsynchronized.ref
+    string * (int * bool Unsynchronized.ref
               * (bool -> Proof.state -> bool * (string * Proof.state)))
 
   val tryN : string
@@ -22,7 +22,7 @@
 struct
 
 type tool =
-  string * (bool Unsynchronized.ref
+  string * (int * bool Unsynchronized.ref
             * (bool -> Proof.state -> bool * (string * Proof.state)))
 
 val tryN = "try"
@@ -51,15 +51,16 @@
 
 val get_tools = Data.get
 
-val register_tool = Data.map o AList.update (op =)
+val register_tool = Data.map o Ord_List.insert (int_ord o pairself (#1 o snd))
 
 (* try command *)
 
 fun try_tools state =
   get_tools (Proof.theory_of state)
-  |> tap (fn _ => Output.urgent_message "Trying...")
+  |> tap (fn tools => "Trying " ^ commas_quote (map fst tools) ^ "..."
+                      |> Output.urgent_message)
   |> Par_List.get_some
-         (fn (name, (_, tool)) =>
+         (fn (name, (_, _, tool)) =>
              case try (tool false) state of
                SOME (true, (outcome_code, _)) => SOME (name, outcome_code)
              | _ => NONE)
@@ -74,7 +75,7 @@
 
 fun auto_try state =
   get_tools (Proof.theory_of state)
-  |> map_filter (fn (_, (auto, tool)) => if !auto then SOME tool else NONE)
+  |> map_filter (fn (_, (_, auto, tool)) => if !auto then SOME tool else NONE)
   |> Par_List.get_some (fn tool =>
                            case try (tool true) state of
                              SOME (true, (_, state)) => SOME state