normalize indices in chained facts to make sure that backtick facts (which often result in different names) are recognized + changed definition of urgent messages
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri May 27 21:11:44 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Sun May 29 19:40:56 2011 +0200
@@ -189,7 +189,7 @@
let
val ctxt = Proof.context_of state
val reserved = reserved_isar_keyword_table ()
- val chained_ths = #facts (Proof.goal state)
+ val chained_ths = normalize_chained_theorems (#facts (Proof.goal state))
val facts =
refs
|> maps (map (apsnd single) o fact_from_ref ctxt reserved chained_ths)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri May 27 21:11:44 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sun May 29 19:40:56 2011 +0200
@@ -146,7 +146,7 @@
reraise exn
else
(unknownN, "Internal error:\n" ^
- ML_Compiler.exn_message exn ^ "\n"))
+ ML_Compiler.exn_message exn ^ "\n"))
val _ =
(* The "expect" argument is deliberately ignored if the prover is
missing so that the "Metis_Examples" can be processed on any
@@ -183,7 +183,7 @@
end
else
(Async_Manager.launch das_tool birth_time death_time (desc ())
- (apfst (curry (op <>) timeoutN) o go);
+ (apfst (curry (op =) someN) o go);
(unknownN, state))
end
@@ -191,7 +191,8 @@
ctxt |> select_smt_solver name
|> SMT_Config.solver_class_of |> SMT_Utils.string_of_class
-(* Makes backtraces more transparent and might be more efficient as well. *)
+(* Makes backtraces more transparent and might well be more efficient as
+ well. *)
fun smart_par_list_map _ [] = []
| smart_par_list_map f [x] = [f x]
| smart_par_list_map f xs = Par_List.map f xs
@@ -217,6 +218,7 @@
state |> Proof.map_context (Config.put SMT_Config.verbose debug)
val ctxt = Proof.context_of state
val {facts = chained_ths, goal, ...} = Proof.goal state
+ val chained_ths = chained_ths |> normalize_chained_theorems
val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i
val _ = () |> not blocking ? kill_provers
val _ = case find_first (not o is_prover_supported ctxt) provers of
@@ -318,7 +320,7 @@
val launch_ueq_atps =
launch_atps "Unit equational provers" is_unit_equality ueq_atps
fun launch_atps_and_smt_solvers () =
- [launch_full_atps, launch_ueq_atps, launch_smts]
+ [launch_full_atps, launch_smts, launch_ueq_atps]
|> smart_par_list_map (fn f => ignore (f (unknownN, state)))
handle ERROR msg => (print ("Error: " ^ msg); error msg)
fun maybe f (accum as (outcome_code, _)) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri May 27 21:11:44 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sun May 29 19:40:56 2011 +0200
@@ -31,6 +31,7 @@
val subgoal_count : Proof.state -> int
val strip_subgoal :
Proof.context -> thm -> int -> (string * typ) list * term list * term
+ val normalize_chained_theorems : thm list -> thm list
val reserved_isar_keyword_table : unit -> unit Symtab.table
end;
@@ -253,6 +254,8 @@
val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees
in (rev params, hyp_ts, concl_t) end
+val normalize_chained_theorems =
+ maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th])
fun reserved_isar_keyword_table () =
union (op =) (Keyword.dest_keywords ()) (Keyword.dest_commands ())
|> map (rpair ()) |> Symtab.make