src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
changeset 37500 7587b6e63454
parent 37498 b426cbdb5a23
child 37501 b5440c78ed3f
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Jun 22 14:48:46 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Jun 22 16:23:29 2010 +0200
     1.3 @@ -5,11 +5,10 @@
     1.4  
     1.5  signature SLEDGEHAMMER_FACT_FILTER =
     1.6  sig
     1.7 +  type cnf_thm = Sledgehammer_Fact_Preprocessor.cnf_thm
     1.8    type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
     1.9    type arity_clause = Sledgehammer_FOL_Clause.arity_clause
    1.10 -  type axiom_name = Sledgehammer_HOL_Clause.axiom_name
    1.11    type hol_clause = Sledgehammer_HOL_Clause.hol_clause
    1.12 -  type hol_clause_id = Sledgehammer_HOL_Clause.hol_clause_id
    1.13  
    1.14    type relevance_override =
    1.15      {add: Facts.ref list,
    1.16 @@ -24,14 +23,12 @@
    1.17    val is_quasi_fol_term : theory -> term -> bool
    1.18    val relevant_facts :
    1.19      bool -> bool -> real -> real -> bool -> int -> bool -> relevance_override
    1.20 -    -> Proof.context * (thm list * 'a) -> thm list
    1.21 -    -> (thm * (string * int)) list
    1.22 +    -> Proof.context * (thm list * 'a) -> thm list -> cnf_thm list
    1.23    val prepare_clauses :
    1.24 -    bool -> thm list -> (thm * (axiom_name * hol_clause_id)) list
    1.25 -    -> (thm * (axiom_name * hol_clause_id)) list -> theory
    1.26 -    -> axiom_name vector
    1.27 -       * (hol_clause list * hol_clause list * hol_clause list *
    1.28 -          hol_clause list * classrel_clause list * arity_clause list)
    1.29 +    bool -> thm list -> cnf_thm list -> cnf_thm list -> theory
    1.30 +    -> string vector
    1.31 +       * (hol_clause list * hol_clause list * hol_clause list
    1.32 +          * hol_clause list * classrel_clause list * arity_clause list)
    1.33  end;
    1.34  
    1.35  structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
    1.36 @@ -234,13 +231,13 @@
    1.37          | _ => false
    1.38      end;
    1.39  
    1.40 -type annotd_cls = (thm * (string * int)) * ((string * const_typ list) list);
    1.41 +type annotated_clause = cnf_thm * ((string * const_typ list) list)
    1.42         
    1.43  (*For a reverse sort, putting the largest values first.*)
    1.44 -fun compare_pairs ((_,w1),(_,w2)) = Real.compare (w2,w1);
    1.45 +fun compare_pairs ((_, w1), (_, w2)) = Real.compare (w2, w1)
    1.46  
    1.47  (*Limit the number of new clauses, to prevent runaway acceptance.*)
    1.48 -fun take_best max_new (newpairs : (annotd_cls*real) list) =
    1.49 +fun take_best max_new (newpairs : (annotated_clause * real) list) =
    1.50    let val nnew = length newpairs
    1.51    in
    1.52      if nnew <= max_new then (map #1 newpairs, [])
    1.53 @@ -252,7 +249,7 @@
    1.54                         ", exceeds the limit of " ^ Int.toString (max_new)));
    1.55          trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
    1.56          trace_msg (fn () => "Actually passed: " ^
    1.57 -          space_implode ", " (map (fn (((_,(name,_)),_),_) => name) accepted));
    1.58 +          space_implode ", " (map (fn (((_,((name,_), _)),_),_) => name) accepted));
    1.59  
    1.60          (map #1 accepted, map #1 (List.drop (cls, max_new)))
    1.61        end
    1.62 @@ -286,7 +283,8 @@
    1.63                    (more_rejects @ rejects)
    1.64              end
    1.65            | relevant (newrels, rejects)
    1.66 -                     ((ax as (clsthm as (thm, (name, n)), consts_typs)) :: axs) =
    1.67 +                     ((ax as (clsthm as (thm, ((name, n), _)), consts_typs)) ::
    1.68 +                      axs) =
    1.69              let
    1.70                val weight = if member Thm.eq_thm add_thms thm then 1.0
    1.71                             else if member Thm.eq_thm del_thms thm then 0.0
    1.72 @@ -309,7 +307,7 @@
    1.73          
    1.74  fun relevance_filter ctxt relevance_threshold relevance_convergence
    1.75                       defs_relevant max_new theory_relevant relevance_override
    1.76 -                     thy axioms goals = 
    1.77 +                     thy (axioms : cnf_thm list) goals = 
    1.78    if relevance_threshold > 0.0 then
    1.79      let
    1.80        val const_tab = List.foldl (count_axiom_consts theory_relevant thy)