1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Jul 20 22:19:46 2012 +0200
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Jul 20 22:19:46 2012 +0200
1.3 @@ -85,10 +85,10 @@
1.4 | is_rec_def _ = false
1.5
1.6 fun is_assum assms th = exists (fn ct => prop_of th aconv term_of ct) assms
1.7 -fun is_chained chained_ths = member Thm.eq_thm_prop chained_ths
1.8 +fun is_chained chained = member Thm.eq_thm_prop chained
1.9
1.10 -fun scope_of_thm global assms chained_ths th =
1.11 - if is_chained chained_ths th then Chained
1.12 +fun scope_of_thm global assms chained th =
1.13 + if is_chained chained th then Chained
1.14 else if global then Global
1.15 else if is_assum assms th then Assum
1.16 else Local
1.17 @@ -98,20 +98,20 @@
1.18 body_type T = @{typ bool}
1.19 | _ => false)
1.20
1.21 -fun status_of_thm css_table name th =
1.22 +fun status_of_thm css name th =
1.23 (* FIXME: use structured name *)
1.24 if (String.isSubstring ".induct" name orelse
1.25 String.isSubstring ".inducts" name) andalso
1.26 may_be_induction (prop_of th) then
1.27 Induction
1.28 - else case Termtab.lookup css_table (prop_of th) of
1.29 + else case Termtab.lookup css (prop_of th) of
1.30 SOME status => status
1.31 | NONE => General
1.32
1.33 -fun stature_of_thm global assms chained_ths css_table name th =
1.34 - (scope_of_thm global assms chained_ths th, status_of_thm css_table name th)
1.35 +fun stature_of_thm global assms chained css name th =
1.36 + (scope_of_thm global assms chained th, status_of_thm css name th)
1.37
1.38 -fun fact_from_ref ctxt reserved chained_ths css_table (xthm as (xref, args)) =
1.39 +fun fact_from_ref ctxt reserved chained css (xthm as (xref, args)) =
1.40 let
1.41 val ths = Attrib.eval_thms ctxt [xthm]
1.42 val bracket =
1.43 @@ -127,15 +127,12 @@
1.44 make_name reserved true
1.45 (nth (maps (explode_interval (length ths)) intervals) j) name ^
1.46 bracket
1.47 - in
1.48 - (ths, (0, []))
1.49 - |-> fold (fn th => fn (j, rest) =>
1.50 - let val name = nth_name j in
1.51 - (j + 1, ((name, stature_of_thm false [] chained_ths
1.52 - css_table name th), th) :: rest)
1.53 - end)
1.54 - |> snd
1.55 - end
1.56 + fun add_nth th (j, rest) =
1.57 + let val name = nth_name j in
1.58 + (j + 1, ((name, stature_of_thm false [] chained css name th), th)
1.59 + :: rest)
1.60 + end
1.61 + in (0, []) |> fold add_nth ths |> snd end
1.62
1.63 (* Reject theorems with names like "List.filter.filter_list_def" or
1.64 "Accessible_Part.acc.defs", as these are definitions arising from packages. *)
1.65 @@ -352,7 +349,7 @@
1.66 fun maybe_filter_no_atps ctxt =
1.67 not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd)
1.68
1.69 -fun all_facts ctxt ho_atp reserved add_ths chained_ths css_table =
1.70 +fun all_facts ctxt ho_atp reserved add_ths chained css =
1.71 let
1.72 val thy = Proof_Context.theory_of ctxt
1.73 val global_facts = Global_Theory.facts_of thy
1.74 @@ -363,7 +360,7 @@
1.75 not (Thm.has_name_hint th) andalso
1.76 forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
1.77 val unnamed_locals =
1.78 - union Thm.eq_thm_prop (Facts.props local_facts) chained_ths
1.79 + union Thm.eq_thm_prop (Facts.props local_facts) chained
1.80 |> filter is_good_unnamed_local |> map (pair "" o single)
1.81 val full_space =
1.82 Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
1.83 @@ -404,8 +401,8 @@
1.84 |> find_first check_thms
1.85 |> the_default name0
1.86 |> make_name reserved multi j),
1.87 - stature_of_thm global assms chained_ths
1.88 - css_table name0 th), th)
1.89 + stature_of_thm global assms chained css name0
1.90 + th), th)
1.91 in
1.92 if multi then (new :: multis, unis)
1.93 else (multis, new :: unis)
1.94 @@ -420,26 +417,26 @@
1.95 |> op @
1.96 end
1.97
1.98 -fun all_facts_of ctxt css_table =
1.99 - all_facts ctxt false Symtab.empty [] [] css_table
1.100 - |> rev (* try to restore the original order of facts, for MaSh *)
1.101 +fun all_facts_of ctxt css =
1.102 + all_facts ctxt false Symtab.empty [] [] css
1.103 + |> rev (* partly restore the original order of facts, for MaSh *)
1.104
1.105 -fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css_table chained_ths
1.106 - hyp_ts concl_t =
1.107 +fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css chained hyp_ts
1.108 + concl_t =
1.109 if only andalso null add then
1.110 []
1.111 else
1.112 let
1.113 - val chained_ths =
1.114 - chained_ths
1.115 + val chained =
1.116 + chained
1.117 |> maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th])
1.118 in
1.119 (if only then
1.120 maps (map (fn ((name, stature), th) => ((K name, stature), th))
1.121 - o fact_from_ref ctxt reserved chained_ths css_table) add
1.122 + o fact_from_ref ctxt reserved chained css) add
1.123 else
1.124 let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in
1.125 - all_facts ctxt ho_atp reserved add chained_ths css_table
1.126 + all_facts ctxt ho_atp reserved add chained css
1.127 |> filter_out (member Thm.eq_thm_prop del o snd)
1.128 |> maybe_filter_no_atps ctxt
1.129 |> uniquify
2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 20 22:19:46 2012 +0200
2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 20 22:19:46 2012 +0200
2.3 @@ -654,7 +654,7 @@
2.4 if null new_facts then
2.5 if not auto then
2.6 "Nothing to learn.\n\nHint: Try " ^ sendback relearn_isarN ^ " or " ^
2.7 - sendback relearn_atpN ^ " to learn from scratch."
2.8 + sendback relearn_atpN ^ " to learn from scratch."
2.9 else
2.10 ""
2.11 else
2.12 @@ -722,13 +722,13 @@
2.13 end
2.14 end
2.15
2.16 -fun mash_learn ctxt (params as {provers, ...}) fact_override chained_ths atp =
2.17 +fun mash_learn ctxt (params as {provers, ...}) fact_override chained atp =
2.18 let
2.19 - val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
2.20 + val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
2.21 val ctxt = ctxt |> Config.put instantiate_inducts false
2.22 val facts =
2.23 - nearly_all_facts ctxt false fact_override Symtab.empty css_table
2.24 - chained_ths [] @{prop True}
2.25 + nearly_all_facts ctxt false fact_override Symtab.empty css chained []
2.26 + @{prop True}
2.27 in
2.28 mash_learn_facts ctxt params (hd provers) false atp infinite_timeout facts
2.29 |> Output.urgent_message
3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Jul 20 22:19:46 2012 +0200
3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Jul 20 22:19:46 2012 +0200
3.3 @@ -325,10 +325,10 @@
3.4 val ctxt = Proof.context_of state
3.5 val reserved = reserved_isar_keyword_table ()
3.6 val chained_ths = #facts (Proof.goal state)
3.7 - val css_table = clasimpset_rule_table_of ctxt
3.8 + val css = clasimpset_rule_table_of ctxt
3.9 val facts =
3.10 refs |> maps (map (apsnd single)
3.11 - o fact_from_ref ctxt reserved chained_ths css_table)
3.12 + o fact_from_ref ctxt reserved chained_ths css)
3.13 in
3.14 case subgoal_count state of
3.15 0 => Output.urgent_message "No subgoal!"
4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Jul 20 22:19:46 2012 +0200
4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Jul 20 22:19:46 2012 +0200
4.3 @@ -183,14 +183,14 @@
4.4 val state =
4.5 state |> Proof.map_context (Config.put SMT_Config.verbose debug)
4.6 val ctxt = Proof.context_of state
4.7 - val {facts = chained_ths, goal, ...} = Proof.goal state
4.8 + val {facts = chained, goal, ...} = Proof.goal state
4.9 val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i
4.10 val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
4.11 val reserved = reserved_isar_keyword_table ()
4.12 - val css_table = clasimpset_rule_table_of ctxt
4.13 + val css = clasimpset_rule_table_of ctxt
4.14 val facts =
4.15 - nearly_all_facts ctxt ho_atp fact_override reserved css_table
4.16 - chained_ths hyp_ts concl_t
4.17 + nearly_all_facts ctxt ho_atp fact_override reserved css chained hyp_ts
4.18 + concl_t
4.19 val _ = () |> not blocking ? kill_provers
4.20 val _ = case find_first (not o is_prover_supported ctxt) provers of
4.21 SOME name => error ("No such prover: " ^ name ^ ".")