(* Authors: Jia Meng, NICTA and Lawrence C Paulson, Cambridge University Computer Laboratory

    ID: $Id$

    Filtering strategies *)

 structure ReduceAxiomsN =

 struct

 val pass_mark = ref 0.6;

 val convergence = ref 2.4;   (*Higher numbers allow longer inference chains*)

 val follow_defs = ref true;  (*Follow definitions. Makes problems bigger.*)

 fun log_weight2 (x:real) = 1.0 + 2.0/Math.ln (x+1.0);

 (*The default seems best in practice. A constant function of one ignores

   the constant frequencies.*)

 val weight_fn = ref log_weight2;

 (*Including equality in this list might be expected to stop rules like subset_antisym from

   being chosen, but for some reason filtering works better with them listed.*)

 val standard_consts =

   ["Trueprop","==>","all","Ex","op &","op |","Not","All","op -->",

    "op =","==","True","False"];

 (*** constants with types ***)

 (*An abstraction of Isabelle types*)

 datatype const_typ =  CTVar | CType of string * const_typ list

 fun uni_type (CType(con1,args1)) (CType(con2,args2)) = con1=con2 andalso uni_types args1 args2

   | uni_type (CType _) CTVar = true

   | uni_type CTVar CTVar = true

   | uni_type CTVar _ = false

 and uni_types [] [] = true

   | uni_types (a1::as1) (a2::as2) = uni_type a1 a2 andalso uni_types as1 as2;

 fun uni_constants (c1,ctp1) (c2,ctp2) = (c1=c2) andalso uni_types ctp1 ctp2;

 fun uni_mem _ [] = false

   | uni_mem (c,c_typ) ((c1,c_typ1)::ctyps) =

       uni_constants (c1,c_typ1) (c,c_typ) orelse uni_mem (c,c_typ) ctyps;

 fun const_typ_of (Type (c,typs)) = CType (c, map const_typ_of typs) 

   | const_typ_of (TFree _) = CTVar

   | const_typ_of (TVar _) = CTVar

 fun const_with_typ thy (c,typ) = 

     let val tvars = Sign.const_typargs thy (c,typ)

     in (c, map const_typ_of tvars) end

     handle TYPE _ => (c,[]);   (*Variable (locale constant): monomorphic*)   

 (*Free variables are counted, as well as constants, to handle locales*)

 fun add_term_consts_typs_rm thy (Const(c, typ)) cs =

       if (c mem standard_consts) then cs 

       else const_with_typ thy (c,typ) ins cs   (*suppress multiples*)

   | add_term_consts_typs_rm thy (Free(c, typ)) cs =

       const_with_typ thy (c,typ) ins cs

   | add_term_consts_typs_rm thy (t $ u) cs =

       add_term_consts_typs_rm thy t (add_term_consts_typs_rm thy u cs)

   | add_term_consts_typs_rm thy (Abs(_,_,t)) cs = add_term_consts_typs_rm thy t cs

   | add_term_consts_typs_rm thy _ cs = cs;

 fun consts_typs_of_term thy t = add_term_consts_typs_rm thy t [];

 fun get_goal_consts_typs thy cs = foldl (op union) [] (map (consts_typs_of_term thy) cs)

 (**** Constant / Type Frequencies ****)

 local

 fun cons_nr CTVar = 0

   | cons_nr (CType _) = 1;

 in

 fun const_typ_ord TU =

   case TU of

     (CType (a, Ts), CType (b, Us)) =>

       (case fast_string_ord(a,b) of EQUAL => dict_ord const_typ_ord (Ts,Us) | ord => ord)

   | (T, U) => int_ord (cons_nr T, cons_nr U);

 end;

 structure CTtab = TableFun(type key = const_typ list val ord = dict_ord const_typ_ord);

 fun count_axiom_consts thy ((thm,_), tab) = 

   let fun count_const (a, T, tab) =

 	let val (c, cts) = const_with_typ thy (a,T)

 	    val cttab = Option.getOpt (Symtab.lookup tab c, CTtab.empty)

 	    val n = Option.getOpt (CTtab.lookup cttab cts, 0)

 	in 

 	    Symtab.update (c, CTtab.update (cts, n+1) cttab) 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

   in  count_term_consts (prop_of thm, tab)  end;

 (******** filter clauses ********)

 fun const_weight ctab (c, cts) =

   let val pairs = CTtab.dest (Option.valOf (Symtab.lookup ctab c))

       fun add ((cts',m), n) = if uni_types cts cts' then m+n else n

   in  List.foldl add 0 pairs  end;

 fun add_ct_weight ctab ((c,T), w) =

   w + !weight_fn (real (const_weight ctab (c,T)));

 fun consts_typs_weight ctab =

     List.foldl (add_ct_weight ctab) 0.0;

 (*Relevant constants are weighted according to frequency, 

   but irrelevant constants are simply counted. Otherwise, Skolem functions,

   which are rare, would harm a clause's chances of being picked.*)

 fun clause_weight ctab gctyps consts_typs =

     let val rel = filter (fn s => uni_mem s gctyps) consts_typs

         val rel_weight = consts_typs_weight ctab rel

     in

 	rel_weight / (rel_weight + real (length consts_typs - length rel))

     end;

 fun pair_consts_typs_axiom thy (thm,name) =

     ((thm,name), (consts_typs_of_term thy (prop_of thm)));

 exception ConstFree;

 fun dest_ConstFree (Const aT) = aT

   | dest_ConstFree (Free aT) = aT

   | dest_ConstFree _ = raise ConstFree;

 (*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 =

             let val (rator,args) = strip_comb lhs

 		val ct = const_with_typ thy (dest_ConstFree rator)

             in  forall is_Var args andalso uni_mem ct gctypes andalso

                 term_varnames rhs subset term_varnames lhs

             end

 	    handle ConstFree => false

     in    

 	case tm of Const ("Trueprop",_) $ (Const("op =",_) $ lhs $ rhs) => 

 		   defs lhs rhs andalso

 		   (Output.debug ("Definition found: " ^ name ^ "_" ^ Int.toString n); true)

 		 | _ => false

     end

 fun relevant_clauses thy ctab p rel_consts =

   let fun relevant (newrels,rejects) []  =

 	    if null newrels then [] 

 	    else 

 	      let val new_consts = map #2 newrels

 	          val rel_consts' = foldl (op union) rel_consts new_consts

                   val newp = p + (1.0-p) / !convergence

 	      in Output.debug ("found relevant: " ^ Int.toString (length newrels));

                  newrels @ relevant_clauses thy ctab newp rel_consts' rejects

 	      end

 	| relevant (newrels,rejects) ((ax as (clsthm,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 relevant (ax::newrels, rejects) axs

 	      else relevant (newrels, ax::rejects) axs

 	    end

     in  Output.debug ("relevant_clauses: " ^ Real.toString p);

         relevant ([],[]) end;

 fun relevance_filter_aux thy axioms goals = 

   let val const_tab = List.foldl (count_axiom_consts thy) Symtab.empty axioms

       val goals_consts_typs = get_goal_consts_typs thy goals

       val rels = relevant_clauses thy const_tab (!pass_mark) goals_consts_typs 

                    (map (pair_consts_typs_axiom thy) axioms)

   in

       Output.debug ("Total relevant: " ^ Int.toString (length rels));

       rels

   end;

 fun relevance_filter thy axioms goals =

   if !pass_mark < 0.1 then axioms

   else map #1 (relevance_filter_aux thy axioms goals);

 end;