# HG changeset patch
# User paulson
# Date 1153302926 -7200
# Node ID 6ff5d35749b0c62e42960246faa69c704e8be01d
# Parent  b6373fe199e13363e473cb518901433c86af5a3f
Fixed the bugs introduced by the last commit! Output is now *identical* to that
produced by the old version, based on a-lists.

diff -r b6373fe199e1 -r 6ff5d35749b0 src/HOL/Tools/ATP/reduce_axiomsN.ML
--- a/src/HOL/Tools/ATP/reduce_axiomsN.ML	Wed Jul 19 02:35:22 2006 +0200
+++ b/src/HOL/Tools/ATP/reduce_axiomsN.ML	Wed Jul 19 11:55:26 2006 +0200
@@ -28,35 +28,35 @@
 (*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 the second type an instance of the first one?*)
+fun match_type (CType(con1,args1)) (CType(con2,args2)) = 
+      con1=con2 andalso match_types args1 args2
+  | match_type CTVar (CType _) = true
+  | match_type CTVar CTVar = true
+  | match_type _ CTVar = false
+and match_types [] [] = true
+  | match_types (a1::as1) (a2::as2) = match_type a1 a2 andalso match_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;
+    | SOME ctyps_list => exists (match_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*)   
 
+(*Add a const/type pair to the table, but a [] entry means a standard connective,
+  which we ignore.*)
 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;
+  Symtab.map_default (c, [ctyps]) (fn [] => [] | ctyps_list => 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) =
@@ -99,10 +99,9 @@
 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
+	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)
@@ -117,7 +116,7 @@
 
 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
+      fun add ((cts',m), n) = if match_types cts cts' then m+n else n
   in  List.foldl add 0 pairs  end;
 
 fun add_ct_weight ctab ((c,T), w) =
@@ -136,13 +135,13 @@
 	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 =
+(*Multiplies out to a list of pairs: 'a * 'b list -> ('a * 'b) list -> ('a * 'b) list*)
+fun add_expand_pairs (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;
+  in  Symtab.fold add_expand_pairs tab []  end;
 
 fun pair_consts_typs_axiom thy (thm,name) =
     ((thm,name), (consts_typs_of_term thy (prop_of thm)));
@@ -158,9 +157,8 @@
 	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 
+            in  forall is_Var args andalso uni_mem gctypes ct andalso
+                term_varnames rhs subset term_varnames lhs
             end
 	    handle ConstFree => false
     in    
@@ -180,11 +178,12 @@
 	      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) =
+	| 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 relevant (ax::newrels, rejects) axs
+	      then (Output.debug name; Output.debug "\n";
+	            relevant (ax::newrels, rejects) axs)
 	      else relevant (newrels, ax::rejects) axs
 	    end
     in  Output.debug ("relevant_clauses: " ^ Real.toString p);