merged
authorwenzelm
Fri, 04 Jan 2013 21:24:47 +0100
changeset 50731 72624ff45676
parent 50723 07ecb6716df2 (diff)
parent 50730 883963f45ac9 (current diff)
child 50732 b2e7490a1b3d
merged
NEWS
--- a/NEWS	Fri Jan 04 21:16:08 2013 +0100
+++ b/NEWS	Fri Jan 04 21:24:47 2013 +0100
@@ -143,7 +143,7 @@
     Sledgehammer manual for details.
   - Polished Isar proofs generated with "isar_proofs" option.
   - Rationalized type encodings ("type_enc" option).
-  - Renamed "kill_provers" subcommand to "kill".
+  - Renamed "kill_provers" subcommand to "kill_all".
   - Renamed options:
       isar_proof ~> isar_proofs
       isar_shrink_factor ~> isar_shrink
--- a/src/Doc/Sledgehammer/document/root.tex	Fri Jan 04 21:16:08 2013 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex	Fri Jan 04 21:24:47 2013 +0100
@@ -675,7 +675,7 @@
 currently running automatic provers, including elapsed runtime and remaining
 time until timeout.
 
-\item[\labelitemi] \textbf{\textit{kill}:} Terminates all running
+\item[\labelitemi] \textbf{\textit{kill\_all}:} Terminates all running
 threads (automatic provers and machine learners).
 
 \item[\labelitemi] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote
@@ -711,9 +711,6 @@
 \item[\labelitemi] \textbf{\textit{running\_learners}:} Prints information about
 currently running machine learners, including elapsed runtime and remaining
 time until timeout.
-
-\item[\labelitemi] \textbf{\textit{kill\_learners}:} Terminates all running
-machine learners.
 \end{enum}
 
 Sledgehammer's behavior can be influenced by various \qty{options}, which can be
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Jan 04 21:16:08 2013 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Jan 04 21:24:47 2013 +0100
@@ -451,6 +451,7 @@
 
 fun size_matters_for _ Ts = not (forall
   (fn Type (tyco, []) => is_some (try (unprefix "Enum.finite") tyco) | _ => false) Ts)
+    (*FIXME eliminate dynamic name reference*)
 
 val test_goals =
   Quickcheck_Common.generator_test_goal_terms ("random", (size_matters_for, compile_generator_expr));
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jan 04 21:16:08 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jan 04 21:24:47 2013 +0100
@@ -37,7 +37,7 @@
 val minN = "min"
 val messagesN = "messages"
 val supported_proversN = "supported_provers"
-val killN = "kill"
+val kill_allN = "kill_all"
 val running_proversN = "running_provers"
 val running_learnersN = "running_learners"
 val refresh_tptpN = "refresh_tptp"
@@ -395,7 +395,7 @@
       messages opt_i
     else if subcommand = supported_proversN then
       supported_provers ctxt
-    else if subcommand = killN then
+    else if subcommand = kill_allN then
       (kill_provers (); kill_learners ())
     else if subcommand = running_proversN then
       running_provers ()
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jan 04 21:16:08 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jan 04 21:24:47 2013 +0100
@@ -307,7 +307,7 @@
 
 local
 
-val version = "*** MaSh version 20121227a ***"
+val version = "*** MaSh version 20130104a ***"
 
 exception Too_New of unit
 
@@ -401,29 +401,25 @@
 
 (*** Isabelle helpers ***)
 
-fun parent_of_local_thm th =
-  let
-    val thy = th |> Thm.theory_of_thm
-    val facts = thy |> Global_Theory.facts_of
-    val space = facts |> Facts.space_of
-    fun id_of s = #id (Name_Space.the_entry space s)
-    fun max_id (s', _) (s, id) =
-      let val id' = id_of s' in if id > id' then (s, id) else (s', id') end
-  in ("", ~1) |> Facts.fold_static max_id facts |> fst end
+val local_prefix = "local" ^ Long_Name.separator
 
-val local_prefix = "local" ^ Long_Name.separator
+fun elided_backquote_thm threshold th =
+  elide_string threshold
+    (backquote_thm (Proof_Context.init_global (Thm.theory_of_thm th)) th)
 
 fun nickname_of_thm th =
   if Thm.has_name_hint th then
     let val hint = Thm.get_name_hint th in
-      (* FIXME: There must be a better way to detect local facts. *)
+      (* There must be a better way to detect local facts. *)
       case try (unprefix local_prefix) hint of
         SOME suf =>
-        parent_of_local_thm th ^ Long_Name.separator ^ Long_Name.separator ^ suf
+        Context.theory_name (Thm.theory_of_thm th) ^ Long_Name.separator ^
+        Long_Name.separator ^ suf ^ Long_Name.separator ^
+        elided_backquote_thm 50 th
       | NONE => hint
     end
   else
-    backquote_thm (Proof_Context.init_global (Thm.theory_of_thm th)) th
+    elided_backquote_thm 200 th
 
 fun find_suggested_facts suggs facts =
   let
@@ -486,10 +482,8 @@
 val skos_feature = ("skos", 2.0 (* FUDGE *))
 
 fun theory_ord p =
-  if Theory.eq_thy p then
-    EQUAL
-  else if Theory.subthy p then
-    LESS
+  if Theory.subthy p then
+    if Theory.eq_thy p then EQUAL else LESS
   else if Theory.subthy (swap p) then
     GREATER
   else case int_ord (pairself (length o Theory.ancestors_of) p) of
@@ -1055,7 +1049,7 @@
 
 (* Generate more suggestions than requested, because some might be thrown out
    later for various reasons. *)
-fun generous_max_facts max_facts = max_facts + Int.min (50, max_facts)
+fun generous_max_facts max_facts = max_facts + Int.min (50, max_facts div 2)
 
 (* The threshold should be large enough so that MaSh doesn't kick in for Auto
    Sledgehammer and Try. *)