# HG changeset patch
# User paulson
# Date 1152970010 -7200
# Node ID de3c295000b2ef638846bd05443b0fc7cc832122
# Parent  c89ee2f4efd560b534f2b66764e1b2e7f9672501
Replaced a-lists by tables to improve efficiency

diff -r c89ee2f4efd5 -r de3c295000b2 src/HOL/Tools/ATP/reduce_axiomsN.ML
--- a/src/HOL/Tools/ATP/reduce_axiomsN.ML	Sat Jul 15 13:52:10 2006 +0200
+++ b/src/HOL/Tools/ATP/reduce_axiomsN.ML	Sat Jul 15 15:26:50 2006 +0200
@@ -35,12 +35,12 @@
 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;
+(*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
@@ -52,20 +52,29 @@
     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)) 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 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;
 
-fun consts_typs_of_term thy t = add_term_consts_typs_rm thy t [];
+(*The empty list here indicates that the constant is being ignored*)
+fun add_standard_const (s,tab) = Symtab.update (s,[]) tab;
 
-fun get_goal_consts_typs thy cs = foldl (op union) [] (map (consts_typs_of_term thy) cs)
+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 ****)
@@ -121,12 +130,20 @@
   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
+    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)));
 
@@ -141,8 +158,9 @@
 	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
+            in  forall is_Var args andalso 
+                term_varnames rhs subset term_varnames lhs andalso
+                uni_mem gctypes ct 
             end
 	    handle ConstFree => false
     in    
@@ -150,14 +168,14 @@
 		   defs lhs rhs andalso
 		   (Output.debug ("Definition found: " ^ name ^ "_" ^ Int.toString n); true)
 		 | _ => false
-    end
+    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
+	      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