# HG changeset patch # User blanchet # Date 1342815586 -7200 # Node ID dd82d190c2af0325279ea8c5b40ff209768e3b9c # Parent 85a7fb65507a292220df4625dced483f6a7dc74d name tuning diff -r 85a7fb65507a -r dd82d190c2af src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- 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 diff -r 85a7fb65507a -r dd82d190c2af src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- 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 diff -r 85a7fb65507a -r dd82d190c2af src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- 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!" diff -r 85a7fb65507a -r dd82d190c2af src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- 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 ^ ".")