--- a/src/HOL/Tools/res_atp.ML Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/Tools/res_atp.ML Sat Oct 17 14:43:18 2009 +0200
@@ -1,4 +1,4 @@
-(* Author: Jia Meng, Cambridge University Computer Laboratory, NICTA *)
+(* Author: Jia Meng, Cambridge University Computer Laboratory, NICTA *)
signature RES_ATP =
sig
@@ -156,17 +156,17 @@
fun count_axiom_consts theory_const thy ((thm,_), tab) =
let fun count_const (a, T, tab) =
- let val (c, cts) = const_with_typ thy (a,T)
- in (*Two-dimensional table update. Constant maps to types maps to count.*)
- Symtab.map_default (c, CTtab.empty)
- (CTtab.map_default (cts,0) (fn n => n+1)) tab
- end
+ let val (c, cts) = const_with_typ thy (a,T)
+ in (*Two-dimensional table update. Constant maps to types maps to count.*)
+ Symtab.map_default (c, CTtab.empty)
+ (CTtab.map_default (cts,0) (fn n => n+1)) tab
+ end
fun count_term_consts (Const(a,T), tab) = count_const(a,T,tab)
- | count_term_consts (Free(a,T), tab) = count_const(a,T,tab)
- | count_term_consts (t $ u, tab) =
- count_term_consts (t, count_term_consts (u, tab))
- | count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab)
- | count_term_consts (_, tab) = tab
+ | count_term_consts (Free(a,T), tab) = count_const(a,T,tab)
+ | count_term_consts (t $ u, tab) =
+ count_term_consts (t, count_term_consts (u, tab))
+ | count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab)
+ | count_term_consts (_, tab) = tab
in count_term_consts (const_prop_of theory_const thm, tab) end;
@@ -189,7 +189,7 @@
let val rel = filter (uni_mem gctyps) consts_typs
val rel_weight = List.foldl (add_ct_weight ctab) 0.0 rel
in
- rel_weight / (rel_weight + real (length consts_typs - length rel))
+ rel_weight / (rel_weight + real (length consts_typs - length rel))
end;
(*Multiplies out to a list of pairs: 'a * 'b list -> ('a * 'b) list -> ('a * 'b) list*)
@@ -210,17 +210,17 @@
(*Look for definitions of the form f ?x1 ... ?xn = t, but not reversed.*)
fun defines thy (thm,(name,n)) gctypes =
let val tm = prop_of thm
- fun defs lhs rhs =
+ fun defs lhs rhs =
let val (rator,args) = strip_comb lhs
- val ct = const_with_typ thy (dest_ConstFree rator)
+ val ct = const_with_typ thy (dest_ConstFree rator)
in forall is_Var args andalso uni_mem gctypes ct andalso
Term.add_vars rhs [] subset Term.add_vars lhs []
end
- handle ConstFree => false
+ handle ConstFree => false
in
- case tm of Const ("Trueprop",_) $ (Const("op =",_) $ lhs $ rhs) =>
- defs lhs rhs
- | _ => false
+ case tm of Const ("Trueprop",_) $ (Const("op =",_) $ lhs $ rhs) =>
+ defs lhs rhs
+ | _ => false
end;
type annotd_cls = (thm * (string * int)) * ((string * const_typ list) list);
@@ -238,40 +238,40 @@
val accepted = List.take (cls, max_new)
in
ResAxioms.trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^
- ", exceeds the limit of " ^ Int.toString (max_new)));
+ ", exceeds the limit of " ^ Int.toString (max_new)));
ResAxioms.trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
ResAxioms.trace_msg (fn () => "Actually passed: " ^
space_implode ", " (map (fn (((_,(name,_)),_),_) => name) accepted));
- (map #1 accepted, map #1 (List.drop (cls, max_new)))
+ (map #1 accepted, map #1 (List.drop (cls, max_new)))
end
end;
fun relevant_clauses max_new thy ctab p rel_consts =
let fun relevant ([],_) [] = [] : (thm * (string * int)) list (*Nothing added this iteration*)
- | relevant (newpairs,rejects) [] =
- let val (newrels,more_rejects) = take_best max_new newpairs
- val new_consts = maps #2 newrels
- val rel_consts' = List.foldl add_const_typ_table rel_consts new_consts
- val newp = p + (1.0-p) / convergence
- in
+ | relevant (newpairs,rejects) [] =
+ let val (newrels,more_rejects) = take_best max_new newpairs
+ val new_consts = maps #2 newrels
+ val rel_consts' = List.foldl add_const_typ_table rel_consts new_consts
+ val newp = p + (1.0-p) / convergence
+ in
ResAxioms.trace_msg (fn () => ("relevant this iteration: " ^ Int.toString (length newrels)));
- (map #1 newrels) @
- (relevant_clauses max_new thy ctab newp rel_consts' (more_rejects@rejects))
- end
- | relevant (newrels,rejects) ((ax as (clsthm as (_,(name,n)),consts_typs)) :: axs) =
- let val weight = clause_weight ctab rel_consts consts_typs
- in
- if p <= weight orelse (follow_defs andalso defines thy clsthm rel_consts)
- then (ResAxioms.trace_msg (fn () => (name ^ " clause " ^ Int.toString n ^
- " passes: " ^ Real.toString weight));
- relevant ((ax,weight)::newrels, rejects) axs)
- else relevant (newrels, ax::rejects) axs
- end
+ (map #1 newrels) @
+ (relevant_clauses max_new thy ctab newp rel_consts' (more_rejects@rejects))
+ end
+ | relevant (newrels,rejects) ((ax as (clsthm as (_,(name,n)),consts_typs)) :: axs) =
+ let val weight = clause_weight ctab rel_consts consts_typs
+ in
+ if p <= weight orelse (follow_defs andalso defines thy clsthm rel_consts)
+ then (ResAxioms.trace_msg (fn () => (name ^ " clause " ^ Int.toString n ^
+ " passes: " ^ Real.toString weight));
+ relevant ((ax,weight)::newrels, rejects) axs)
+ else relevant (newrels, ax::rejects) axs
+ end
in ResAxioms.trace_msg (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p));
relevant ([],[])
end;
-
+
fun relevance_filter max_new theory_const thy axioms goals =
if run_relevance_filter andalso pass_mark >= 0.1
then