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

(*Is there a unifiable constant?*)

fun uni_mem gctab (c,c_typ) =

  case Symtab.lookup gctab c of

      NONE => false

    | SOME ctyps_list => exists (uni_types c_typ) ctyps_list;

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*)   

fun add_const_typ_table ((c,ctyps), tab) =

  case Symtab.lookup tab c of

      NONE => Symtab.update (c, [ctyps]) tab

    | SOME [] => tab  (*ignore!*)

    | SOME ctyps_list => Symtab.update (c, ctyps ins ctyps_list) tab;

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

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

      add_const_typ_table (const_with_typ thy (c,typ), tab) 

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

      add_const_typ_table (const_with_typ thy (c,typ), tab) 

  | add_term_consts_typs_rm thy (t $ u, tab) =

      add_term_consts_typs_rm thy (t, add_term_consts_typs_rm thy (u, tab))

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

  | add_term_consts_typs_rm thy (_, tab) = tab;

(*The empty list here indicates that the constant is being ignored*)

fun add_standard_const (s,tab) = Symtab.update (s,[]) tab;

val null_const_tab : const_typ list list Symtab.table = 

    foldl add_standard_const Symtab.empty standard_consts;

fun get_goal_consts_typs thy cs = foldl (add_term_consts_typs_rm thy) null_const_tab 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 (uni_mem gctyps) consts_typs

        val rel_weight = consts_typs_weight ctab rel

    in

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

    end;

fun add_consts_with_typs (c,[]) cpairs = cpairs

  | add_consts_with_typs (c, ctyps_list) cpairs =

      foldl (fn (ctyps,cpairs) => (c,ctyps)::cpairs) cpairs ctyps_list;

fun consts_typs_of_term thy t = 

  let val tab = add_term_consts_typs_rm thy (t, null_const_tab)

  in  Symtab.fold add_consts_with_typs tab []  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 

                term_varnames rhs subset term_varnames lhs andalso

                uni_mem gctypes ct 

            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 = List.concat (map #2 newrels)

	          val rel_consts' = foldl add_const_typ_table 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;