--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Jul 20 22:19:46 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Jul 20 22:19:46 2012 +0200
@@ -85,10 +85,10 @@
| is_rec_def _ = false
fun is_assum assms th = exists (fn ct => prop_of th aconv term_of ct) assms
-fun is_chained chained_ths = member Thm.eq_thm_prop chained_ths
+fun is_chained chained = member Thm.eq_thm_prop chained
-fun scope_of_thm global assms chained_ths th =
- if is_chained chained_ths th then Chained
+fun scope_of_thm global assms chained th =
+ if is_chained chained th then Chained
else if global then Global
else if is_assum assms th then Assum
else Local
@@ -98,20 +98,20 @@
body_type T = @{typ bool}
| _ => false)
-fun status_of_thm css_table name th =
+fun status_of_thm css name th =
(* FIXME: use structured name *)
if (String.isSubstring ".induct" name orelse
String.isSubstring ".inducts" name) andalso
may_be_induction (prop_of th) then
Induction
- else case Termtab.lookup css_table (prop_of th) of
+ else case Termtab.lookup css (prop_of th) of
SOME status => status
| NONE => General
-fun stature_of_thm global assms chained_ths css_table name th =
- (scope_of_thm global assms chained_ths th, status_of_thm css_table name th)
+fun stature_of_thm global assms chained css name th =
+ (scope_of_thm global assms chained th, status_of_thm css name th)
-fun fact_from_ref ctxt reserved chained_ths css_table (xthm as (xref, args)) =
+fun fact_from_ref ctxt reserved chained css (xthm as (xref, args)) =
let
val ths = Attrib.eval_thms ctxt [xthm]
val bracket =
@@ -127,15 +127,12 @@
make_name reserved true
(nth (maps (explode_interval (length ths)) intervals) j) name ^
bracket
- in
- (ths, (0, []))
- |-> fold (fn th => fn (j, rest) =>
- let val name = nth_name j in
- (j + 1, ((name, stature_of_thm false [] chained_ths
- css_table name th), th) :: rest)
- end)
- |> snd
- end
+ fun add_nth th (j, rest) =
+ let val name = nth_name j in
+ (j + 1, ((name, stature_of_thm false [] chained css name th), th)
+ :: rest)
+ end
+ in (0, []) |> fold add_nth ths |> snd end
(* Reject theorems with names like "List.filter.filter_list_def" or
"Accessible_Part.acc.defs", as these are definitions arising from packages. *)
@@ -352,7 +349,7 @@
fun maybe_filter_no_atps ctxt =
not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd)
-fun all_facts ctxt ho_atp reserved add_ths chained_ths css_table =
+fun all_facts ctxt ho_atp reserved add_ths chained css =
let
val thy = Proof_Context.theory_of ctxt
val global_facts = Global_Theory.facts_of thy
@@ -363,7 +360,7 @@
not (Thm.has_name_hint th) andalso
forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
val unnamed_locals =
- union Thm.eq_thm_prop (Facts.props local_facts) chained_ths
+ union Thm.eq_thm_prop (Facts.props local_facts) chained
|> filter is_good_unnamed_local |> map (pair "" o single)
val full_space =
Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
@@ -404,8 +401,8 @@
|> find_first check_thms
|> the_default name0
|> make_name reserved multi j),
- stature_of_thm global assms chained_ths
- css_table name0 th), th)
+ stature_of_thm global assms chained css name0
+ th), th)
in
if multi then (new :: multis, unis)
else (multis, new :: unis)
@@ -420,26 +417,26 @@
|> op @
end
-fun all_facts_of ctxt css_table =
- all_facts ctxt false Symtab.empty [] [] css_table
- |> rev (* try to restore the original order of facts, for MaSh *)
+fun all_facts_of ctxt css =
+ all_facts ctxt false Symtab.empty [] [] css
+ |> rev (* partly restore the original order of facts, for MaSh *)
-fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css_table chained_ths
- hyp_ts concl_t =
+fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css chained hyp_ts
+ concl_t =
if only andalso null add then
[]
else
let
- val chained_ths =
- chained_ths
+ val chained =
+ chained
|> maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th])
in
(if only then
maps (map (fn ((name, stature), th) => ((K name, stature), th))
- o fact_from_ref ctxt reserved chained_ths css_table) add
+ o fact_from_ref ctxt reserved chained css) add
else
let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in
- all_facts ctxt ho_atp reserved add chained_ths css_table
+ all_facts ctxt ho_atp reserved add chained css
|> filter_out (member Thm.eq_thm_prop del o snd)
|> maybe_filter_no_atps ctxt
|> uniquify
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 20 22:19:46 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 20 22:19:46 2012 +0200
@@ -654,7 +654,7 @@
if null new_facts then
if not auto then
"Nothing to learn.\n\nHint: Try " ^ sendback relearn_isarN ^ " or " ^
- sendback relearn_atpN ^ " to learn from scratch."
+ sendback relearn_atpN ^ " to learn from scratch."
else
""
else
@@ -722,13 +722,13 @@
end
end
-fun mash_learn ctxt (params as {provers, ...}) fact_override chained_ths atp =
+fun mash_learn ctxt (params as {provers, ...}) fact_override chained atp =
let
- val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
+ val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
val ctxt = ctxt |> Config.put instantiate_inducts false
val facts =
- nearly_all_facts ctxt false fact_override Symtab.empty css_table
- chained_ths [] @{prop True}
+ nearly_all_facts ctxt false fact_override Symtab.empty css chained []
+ @{prop True}
in
mash_learn_facts ctxt params (hd provers) false atp infinite_timeout facts
|> Output.urgent_message
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Jul 20 22:19:46 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Jul 20 22:19:46 2012 +0200
@@ -325,10 +325,10 @@
val ctxt = Proof.context_of state
val reserved = reserved_isar_keyword_table ()
val chained_ths = #facts (Proof.goal state)
- val css_table = clasimpset_rule_table_of ctxt
+ val css = clasimpset_rule_table_of ctxt
val facts =
refs |> maps (map (apsnd single)
- o fact_from_ref ctxt reserved chained_ths css_table)
+ o fact_from_ref ctxt reserved chained_ths css)
in
case subgoal_count state of
0 => Output.urgent_message "No subgoal!"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Jul 20 22:19:46 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Jul 20 22:19:46 2012 +0200
@@ -183,14 +183,14 @@
val state =
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 {facts = chained, goal, ...} = Proof.goal state
val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i
val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
val reserved = reserved_isar_keyword_table ()
- val css_table = clasimpset_rule_table_of ctxt
+ val css = clasimpset_rule_table_of ctxt
val facts =
- nearly_all_facts ctxt ho_atp fact_override reserved css_table
- chained_ths hyp_ts concl_t
+ nearly_all_facts ctxt ho_atp fact_override reserved css chained hyp_ts
+ concl_t
val _ = () |> not blocking ? kill_provers
val _ = case find_first (not o is_prover_supported ctxt) provers of
SOME name => error ("No such prover: " ^ name ^ ".")