Fixed the bugs introduced by the last commit! Output is now *identical* to that
authorpaulson
Wed Jul 19 11:55:26 2006 +0200 (2006-07-19)
changeset 201536ff5d35749b0
parent 20152 b6373fe199e1
child 20154 c709a29f1363
Fixed the bugs introduced by the last commit! Output is now *identical* to that
produced by the old version, based on a-lists.
src/HOL/Tools/ATP/reduce_axiomsN.ML
     1.1 --- a/src/HOL/Tools/ATP/reduce_axiomsN.ML	Wed Jul 19 02:35:22 2006 +0200
     1.2 +++ b/src/HOL/Tools/ATP/reduce_axiomsN.ML	Wed Jul 19 11:55:26 2006 +0200
     1.3 @@ -28,35 +28,35 @@
     1.4  (*An abstraction of Isabelle types*)
     1.5  datatype const_typ =  CTVar | CType of string * const_typ list
     1.6  
     1.7 -fun uni_type (CType(con1,args1)) (CType(con2,args2)) = con1=con2 andalso uni_types args1 args2
     1.8 -  | uni_type (CType _) CTVar = true
     1.9 -  | uni_type CTVar CTVar = true
    1.10 -  | uni_type CTVar _ = false
    1.11 -and uni_types [] [] = true
    1.12 -  | uni_types (a1::as1) (a2::as2) = uni_type a1 a2 andalso uni_types as1 as2;
    1.13 +(*Is the second type an instance of the first one?*)
    1.14 +fun match_type (CType(con1,args1)) (CType(con2,args2)) = 
    1.15 +      con1=con2 andalso match_types args1 args2
    1.16 +  | match_type CTVar (CType _) = true
    1.17 +  | match_type CTVar CTVar = true
    1.18 +  | match_type _ CTVar = false
    1.19 +and match_types [] [] = true
    1.20 +  | match_types (a1::as1) (a2::as2) = match_type a1 a2 andalso match_types as1 as2;
    1.21  
    1.22  (*Is there a unifiable constant?*)
    1.23  fun uni_mem gctab (c,c_typ) =
    1.24    case Symtab.lookup gctab c of
    1.25        NONE => false
    1.26 -    | SOME ctyps_list => exists (uni_types c_typ) ctyps_list;
    1.27 +    | SOME ctyps_list => exists (match_types c_typ) ctyps_list;
    1.28    
    1.29 -
    1.30  fun const_typ_of (Type (c,typs)) = CType (c, map const_typ_of typs) 
    1.31    | const_typ_of (TFree _) = CTVar
    1.32    | const_typ_of (TVar _) = CTVar
    1.33  
    1.34 -
    1.35  fun const_with_typ thy (c,typ) = 
    1.36      let val tvars = Sign.const_typargs thy (c,typ)
    1.37      in (c, map const_typ_of tvars) end
    1.38      handle TYPE _ => (c,[]);   (*Variable (locale constant): monomorphic*)   
    1.39  
    1.40 +(*Add a const/type pair to the table, but a [] entry means a standard connective,
    1.41 +  which we ignore.*)
    1.42  fun add_const_typ_table ((c,ctyps), tab) =
    1.43 -  case Symtab.lookup tab c of
    1.44 -      NONE => Symtab.update (c, [ctyps]) tab
    1.45 -    | SOME [] => tab  (*ignore!*)
    1.46 -    | SOME ctyps_list => Symtab.update (c, ctyps ins ctyps_list) tab;
    1.47 +  Symtab.map_default (c, [ctyps]) (fn [] => [] | ctyps_list => ctyps ins ctyps_list) 
    1.48 +    tab;
    1.49  
    1.50  (*Free variables are counted, as well as constants, to handle locales*)
    1.51  fun add_term_consts_typs_rm thy (Const(c, typ), tab) =
    1.52 @@ -99,10 +99,9 @@
    1.53  fun count_axiom_consts thy ((thm,_), tab) = 
    1.54    let fun count_const (a, T, tab) =
    1.55  	let val (c, cts) = const_with_typ thy (a,T)
    1.56 -	    val cttab = Option.getOpt (Symtab.lookup tab c, CTtab.empty)
    1.57 -	    val n = Option.getOpt (CTtab.lookup cttab cts, 0)
    1.58 -	in 
    1.59 -	    Symtab.update (c, CTtab.update (cts, n+1) cttab) tab
    1.60 +	in  (*Two-dimensional table update. Constant maps to types maps to count.*)
    1.61 +	    Symtab.map_default (c, CTtab.empty) 
    1.62 +	                       (CTtab.map_default (cts,0) (fn n => n+1)) tab
    1.63  	end
    1.64        fun count_term_consts (Const(a,T), tab) = count_const(a,T,tab)
    1.65  	| count_term_consts (Free(a,T), tab) = count_const(a,T,tab)
    1.66 @@ -117,7 +116,7 @@
    1.67  
    1.68  fun const_weight ctab (c, cts) =
    1.69    let val pairs = CTtab.dest (Option.valOf (Symtab.lookup ctab c))
    1.70 -      fun add ((cts',m), n) = if uni_types cts cts' then m+n else n
    1.71 +      fun add ((cts',m), n) = if match_types cts cts' then m+n else n
    1.72    in  List.foldl add 0 pairs  end;
    1.73  
    1.74  fun add_ct_weight ctab ((c,T), w) =
    1.75 @@ -136,13 +135,13 @@
    1.76  	rel_weight / (rel_weight + real (length consts_typs - length rel))
    1.77      end;
    1.78      
    1.79 -fun add_consts_with_typs (c,[]) cpairs = cpairs
    1.80 -  | add_consts_with_typs (c, ctyps_list) cpairs =
    1.81 +(*Multiplies out to a list of pairs: 'a * 'b list -> ('a * 'b) list -> ('a * 'b) list*)
    1.82 +fun add_expand_pairs (c, ctyps_list) cpairs =
    1.83        foldl (fn (ctyps,cpairs) => (c,ctyps)::cpairs) cpairs ctyps_list;
    1.84  
    1.85  fun consts_typs_of_term thy t = 
    1.86    let val tab = add_term_consts_typs_rm thy (t, null_const_tab)
    1.87 -  in  Symtab.fold add_consts_with_typs tab []  end;
    1.88 +  in  Symtab.fold add_expand_pairs tab []  end;
    1.89  
    1.90  fun pair_consts_typs_axiom thy (thm,name) =
    1.91      ((thm,name), (consts_typs_of_term thy (prop_of thm)));
    1.92 @@ -158,9 +157,8 @@
    1.93  	fun defs lhs rhs =
    1.94              let val (rator,args) = strip_comb lhs
    1.95  		val ct = const_with_typ thy (dest_ConstFree rator)
    1.96 -            in  forall is_Var args andalso 
    1.97 -                term_varnames rhs subset term_varnames lhs andalso
    1.98 -                uni_mem gctypes ct 
    1.99 +            in  forall is_Var args andalso uni_mem gctypes ct andalso
   1.100 +                term_varnames rhs subset term_varnames lhs
   1.101              end
   1.102  	    handle ConstFree => false
   1.103      in    
   1.104 @@ -180,11 +178,12 @@
   1.105  	      in Output.debug ("found relevant: " ^ Int.toString (length newrels));
   1.106                   newrels @ relevant_clauses thy ctab newp rel_consts' rejects
   1.107  	      end
   1.108 -	| relevant (newrels,rejects) ((ax as (clsthm,consts_typs)) :: axs) =
   1.109 +	| relevant (newrels,rejects) ((ax as (clsthm as (_,(name,n)),consts_typs)) :: axs) =
   1.110  	    let val weight = clause_weight ctab rel_consts consts_typs
   1.111  	    in
   1.112  	      if p <= weight orelse (!follow_defs andalso defines thy clsthm rel_consts)
   1.113 -	      then relevant (ax::newrels, rejects) axs
   1.114 +	      then (Output.debug name; Output.debug "\n";
   1.115 +	            relevant (ax::newrels, rejects) axs)
   1.116  	      else relevant (newrels, ax::rejects) axs
   1.117  	    end
   1.118      in  Output.debug ("relevant_clauses: " ^ Real.toString p);