1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Aug 18 18:01:54 2010 +0200
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Aug 18 19:57:12 2010 +0200
1.3 @@ -104,7 +104,8 @@
1.4 introduce a fresh constant to simulate the effect of Skolemization. *)
1.5 fun do_term t =
1.6 case t of
1.7 - Const x => add_const_type_to_table (const_with_typ thy x)
1.8 + Const (@{const_name Let}, _) => I
1.9 + | Const x => add_const_type_to_table (const_with_typ thy x)
1.10 | Free x => add_const_type_to_table (const_with_typ thy x)
1.11 | t1 $ t2 => do_term t1 #> do_term t2
1.12 | Abs (_, _, t) =>
1.13 @@ -297,56 +298,9 @@
1.14 end
1.15 end;
1.16
1.17 -fun relevant_facts ctxt relevance_convergence defs_relevant max_new
1.18 - ({add, del, ...} : relevance_override) const_tab =
1.19 - let
1.20 - val thy = ProofContext.theory_of ctxt
1.21 - val add_thms = maps (ProofContext.get_fact ctxt) add
1.22 - val del_thms = maps (ProofContext.get_fact ctxt) del
1.23 - fun iter threshold rel_const_tab =
1.24 - let
1.25 - fun relevant ([], _) [] = [] (* Nothing added this iteration *)
1.26 - | relevant (newpairs, rejects) [] =
1.27 - let
1.28 - val (newrels, more_rejects) = take_best max_new newpairs
1.29 - val new_consts = maps #2 newrels
1.30 - val rel_const_tab =
1.31 - rel_const_tab |> fold add_const_type_to_table new_consts
1.32 - val threshold =
1.33 - threshold + (1.0 - threshold) / relevance_convergence
1.34 - in
1.35 - trace_msg (fn () => "relevant this iteration: " ^
1.36 - Int.toString (length newrels));
1.37 - map #1 newrels @ iter threshold rel_const_tab
1.38 - (more_rejects @ rejects)
1.39 - end
1.40 - | relevant (newrels, rejects)
1.41 - ((ax as ((name, th), consts_typs)) :: axs) =
1.42 - let
1.43 - val weight =
1.44 - if member Thm.eq_thm add_thms th then 1.0
1.45 - else if member Thm.eq_thm del_thms th then 0.0
1.46 - else formula_weight const_tab rel_const_tab consts_typs
1.47 - in
1.48 - if weight >= threshold orelse
1.49 - (defs_relevant andalso defines thy th rel_const_tab) then
1.50 - (trace_msg (fn () =>
1.51 - name ^ " passes: " ^ Real.toString weight
1.52 - (* ^ " consts: " ^ commas (map fst consts_typs) *));
1.53 - relevant ((ax, weight) :: newrels, rejects) axs)
1.54 - else
1.55 - relevant (newrels, ax :: rejects) axs
1.56 - end
1.57 - in
1.58 - trace_msg (fn () => "relevant_facts, current threshold: " ^
1.59 - Real.toString threshold);
1.60 - relevant ([], [])
1.61 - end
1.62 - in iter end
1.63 -
1.64 fun relevance_filter ctxt relevance_threshold relevance_convergence
1.65 - defs_relevant max_new theory_relevant relevance_override
1.66 - axioms goal_ts =
1.67 + defs_relevant max_new theory_relevant
1.68 + ({add, del, ...} : relevance_override) axioms goal_ts =
1.69 if relevance_threshold > 1.0 then
1.70 []
1.71 else if relevance_threshold < 0.0 then
1.72 @@ -364,12 +318,56 @@
1.73 |> Symtab.dest
1.74 |> filter (curry (op <>) [] o snd)
1.75 |> map fst))
1.76 - val relevant =
1.77 - relevant_facts ctxt relevance_convergence defs_relevant max_new
1.78 - relevance_override const_tab relevance_threshold
1.79 - goal_const_tab
1.80 - (map (pair_consts_typs_axiom theory_relevant thy)
1.81 - axioms)
1.82 + val add_thms = maps (ProofContext.get_fact ctxt) add
1.83 + val del_thms = maps (ProofContext.get_fact ctxt) del
1.84 + fun iter threshold rel_const_tab =
1.85 + let
1.86 + fun relevant ([], rejects) [] =
1.87 + (* Nothing was added this iteration: Add "add:" facts. *)
1.88 + if null add_thms then
1.89 + []
1.90 + else
1.91 + map_filter (fn (p as (name, th), _) =>
1.92 + if member Thm.eq_thm add_thms th then SOME p
1.93 + else NONE) rejects
1.94 + | relevant (newpairs, rejects) [] =
1.95 + let
1.96 + val (newrels, more_rejects) = take_best max_new newpairs
1.97 + val new_consts = maps #2 newrels
1.98 + val rel_const_tab =
1.99 + rel_const_tab |> fold add_const_type_to_table new_consts
1.100 + val threshold =
1.101 + threshold + (1.0 - threshold) / relevance_convergence
1.102 + in
1.103 + trace_msg (fn () => "relevant this iteration: " ^
1.104 + Int.toString (length newrels));
1.105 + map #1 newrels @ iter threshold rel_const_tab
1.106 + (more_rejects @ rejects)
1.107 + end
1.108 + | relevant (newrels, rejects)
1.109 + ((ax as ((name, th), consts_typs)) :: axs) =
1.110 + let
1.111 + val weight =
1.112 + if member Thm.eq_thm del_thms th then 0.0
1.113 + else formula_weight const_tab rel_const_tab consts_typs
1.114 + in
1.115 + if weight >= threshold orelse
1.116 + (defs_relevant andalso defines thy th rel_const_tab) then
1.117 + (trace_msg (fn () =>
1.118 + name ^ " passes: " ^ Real.toString weight
1.119 + (* ^ " consts: " ^ commas (map fst consts_typs) *));
1.120 + relevant ((ax, weight) :: newrels, rejects) axs)
1.121 + else
1.122 + relevant (newrels, ax :: rejects) axs
1.123 + end
1.124 + in
1.125 + trace_msg (fn () => "relevant_facts, current threshold: " ^
1.126 + Real.toString threshold);
1.127 + relevant ([], [])
1.128 + end
1.129 + val relevant = iter relevance_threshold goal_const_tab
1.130 + (map (pair_consts_typs_axiom theory_relevant thy)
1.131 + axioms)
1.132 in
1.133 trace_msg (fn () => "Total relevant: " ^ Int.toString (length relevant));
1.134 relevant
1.135 @@ -559,20 +557,17 @@
1.136 (ctxt, (chained_ths, _)) hyp_ts concl_t =
1.137 let
1.138 val add_thms = maps (ProofContext.get_fact ctxt) add
1.139 - val has_override = not (null add) orelse not (null del)
1.140 val axioms =
1.141 checked_name_thm_pairs (respect_no_atp andalso not only) ctxt
1.142 (map (name_thms_pair_from_ref ctxt chained_ths) add @
1.143 (if only then [] else all_name_thms_pairs ctxt chained_ths))
1.144 - |> not has_override ? make_unique
1.145 |> filter (fn (_, th) => member Thm.eq_thm add_thms th orelse
1.146 not (is_dangerous_term full_types (prop_of th)))
1.147 in
1.148 relevance_filter ctxt relevance_threshold relevance_convergence
1.149 defs_relevant max_new theory_relevant relevance_override
1.150 axioms (concl_t :: hyp_ts)
1.151 - |> has_override ? make_unique
1.152 - |> sort_wrt fst
1.153 + |> make_unique |> sort_wrt fst
1.154 end
1.155
1.156 end;