Arity clauses are now produced only for types and type classes actually used.
authorpaulson
Wed Nov 15 11:33:59 2006 +0100 (2006-11-15)
changeset 2137318f519614978
parent 21372 4a0a83378669
child 21374 27ae6bc4102a
Arity clauses are now produced only for types and type classes actually used.
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_clause.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Tue Nov 14 22:17:04 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Nov 15 11:33:59 2006 +0100
     1.3 @@ -660,6 +660,18 @@
     1.4    let val sorts_list = map (map #2 o term_tfrees) ts
     1.5    in  Symtab.keys (delete_type (foldl add_classes Symtab.empty sorts_list))  end;
     1.6  
     1.7 +(*fold type constructors*)
     1.8 +fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
     1.9 +  | fold_type_consts f T x = x;
    1.10 +
    1.11 +val add_type_consts_in_type = fold_type_consts setinsert;
    1.12 +
    1.13 +val add_type_consts_in_term = fold_types add_type_consts_in_type;
    1.14 +
    1.15 +fun type_consts_of_terms ts =
    1.16 +  Symtab.keys (fold add_type_consts_in_term ts Symtab.empty);
    1.17 +
    1.18 +
    1.19  (***************************************************************)
    1.20  (* ATP invocation methods setup                                *)
    1.21  (***************************************************************)
    1.22 @@ -708,12 +720,14 @@
    1.23  	                            user_cls (map prop_of goal_cls) |> make_unique
    1.24  	val keep_types = if is_fol_logic logic then !fol_keep_types else is_typed_hol ()
    1.25          val subs = tfree_classes_of_terms (map prop_of goal_cls)
    1.26 -        and supers = tvar_classes_of_terms (map (prop_of o #1) axclauses)
    1.27 +        and axtms = map (prop_of o #1) axclauses
    1.28 +        val supers = tvar_classes_of_terms axtms
    1.29 +        and tycons = type_consts_of_terms axtms
    1.30          (*TFrees in conjecture clauses; TVars in axiom clauses*)
    1.31          val classrel_clauses = 
    1.32                if keep_types then ResClause.make_classrel_clauses thy subs supers
    1.33                else []
    1.34 -	val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else []
    1.35 +	val arity_clauses = if keep_types then ResClause.arity_clause_thy thy tycons supers else []
    1.36          val writer = if dfg then dfg_writer else tptp_writer 
    1.37  	and file = atp_input_file()
    1.38  	and user_lemmas_names = map #1 user_rules
    1.39 @@ -831,9 +845,6 @@
    1.40                    axcls_list
    1.41        val keep_types = if is_fol_logic logic then !ResClause.keep_types 
    1.42                         else is_typed_hol ()
    1.43 -      val arity_clauses = if keep_types then ResClause.arity_clause_thy thy 
    1.44 -                          else []
    1.45 -      val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
    1.46        val writer = if !prover = "spass" then dfg_writer else tptp_writer 
    1.47        fun write_all [] [] _ = []
    1.48  	| write_all (ccls::ccls_list) (axcls::axcls_list) k =
    1.49 @@ -841,12 +852,17 @@
    1.50                  val axcls = make_unique axcls
    1.51                  val ccls = subtract_cls ccls axcls
    1.52                  val subs = tfree_classes_of_terms (map prop_of ccls)
    1.53 -                and supers = tvar_classes_of_terms (map (prop_of o #1) axcls)
    1.54 +                and axtms = map (prop_of o #1) axcls
    1.55 +                val supers = tvar_classes_of_terms axtms
    1.56 +                and tycons = type_consts_of_terms axtms
    1.57                  (*TFrees in conjecture clauses; TVars in axiom clauses*)
    1.58                  val classrel_clauses = 
    1.59                        if keep_types then ResClause.make_classrel_clauses thy subs supers
    1.60                        else []
    1.61                  val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))
    1.62 +                val arity_clauses = if keep_types then ResClause.arity_clause_thy thy tycons supers
    1.63 +                                    else []
    1.64 +                val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
    1.65                  val clnames = writer logic ccls fname (axcls,classrel_clauses,arity_clauses) []
    1.66                  val thm_names = Array.fromList clnames
    1.67                  val _ = if !Output.show_debug_msgs 
     2.1 --- a/src/HOL/Tools/res_clause.ML	Tue Nov 14 22:17:04 2006 +0100
     2.2 +++ b/src/HOL/Tools/res_clause.ML	Wed Nov 15 11:33:59 2006 +0100
     2.3 @@ -490,8 +490,7 @@
     2.4                 | TVarLit of bool * (class * string);
     2.5   
     2.6  datatype arityClause =  
     2.7 -	 ArityClause of {clause_id: clause_id,
     2.8 -	  	         axiom_name: axiom_name,
     2.9 +	 ArityClause of {axiom_name: axiom_name,
    2.10  			 kind: kind,
    2.11  			 conclLit: arLit,
    2.12  			 premLits: arLit list};
    2.13 @@ -509,15 +508,14 @@
    2.14        TConsLit(b, (make_type_class cls, make_fixed_type_const tcons, tvars));
    2.15  
    2.16  (*Arity of type constructor tcon :: (arg1,...,argN)res*)
    2.17 -fun make_axiom_arity_clause (tcons, n, (res,args)) =
    2.18 +fun make_axiom_arity_clause (tcons, axiom_name, (res,args)) =
    2.19     let val nargs = length args
    2.20         val tvars = gen_TVars nargs
    2.21         val tvars_srts = ListPair.zip (tvars,args)
    2.22         val tvars_srts' = union_all(map pack_sort tvars_srts)
    2.23         val false_tvars_srts' = map (pair false) tvars_srts'
    2.24     in
    2.25 -      ArityClause {clause_id = n, kind = Axiom, 
    2.26 -                   axiom_name = lookup_type_const tcons,
    2.27 +      ArityClause {axiom_name = axiom_name, kind = Axiom, 
    2.28                     conclLit = make_TConsLit(true, (res,tcons,tvars)), 
    2.29                     premLits = map make_TVarLit false_tvars_srts'}
    2.30     end;
    2.31 @@ -549,24 +547,34 @@
    2.32  
    2.33  (** Isabelle arities **)
    2.34  
    2.35 -fun arity_clause _ (tcons, []) = []
    2.36 -  | arity_clause n (tcons, ("HOL.type",_)::ars) =  (*ignore*)
    2.37 -      arity_clause n (tcons,ars)
    2.38 -  | arity_clause n (tcons, ar::ars) =
    2.39 -      make_axiom_arity_clause (tcons,n,ar) :: 
    2.40 -      arity_clause (n+1) (tcons,ars);
    2.41 +fun arity_clause _ _ (tcons, []) = []
    2.42 +  | arity_clause seen n (tcons, ("HOL.type",_)::ars) =  (*ignore*)
    2.43 +      arity_clause seen n (tcons,ars)
    2.44 +  | arity_clause seen n (tcons, (ar as (class,_)) :: ars) =
    2.45 +      if class mem_string seen then (*multiple arities for the same tycon, class pair*)
    2.46 +	  make_axiom_arity_clause (tcons, lookup_type_const tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) :: 
    2.47 +	  arity_clause seen (n+1) (tcons,ars)
    2.48 +      else
    2.49 +	  make_axiom_arity_clause (tcons, lookup_type_const tcons ^ "_" ^ class, ar) :: 
    2.50 +	  arity_clause (class::seen) n (tcons,ars)
    2.51  
    2.52  fun multi_arity_clause [] = []
    2.53    | multi_arity_clause ((tcons,ars) :: tc_arlists) =
    2.54 -      (*Reversal ensures that older entries always get the same axiom name*)
    2.55 -      arity_clause 0 (tcons, rev ars)  @  
    2.56 +      arity_clause [] 1 (tcons, ars)  @  
    2.57        multi_arity_clause tc_arlists 
    2.58  
    2.59 -fun arity_clause_thy thy =
    2.60 -  let val arities = thy |> Sign.classes_of
    2.61 -    |> Sorts.rep_algebra |> #arities |> Symtab.dest
    2.62 -    |> map (apsnd (map (fn (c, (_, Ss)) => (c, Ss))));
    2.63 -  in multi_arity_clause (rev arities) end;
    2.64 +(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy.*)
    2.65 +fun type_class_pairs thy tycons classes =
    2.66 +  let val alg = Sign.classes_of thy
    2.67 +      fun domain_sorts (tycon,class) = Sorts.mg_domain alg tycon [class]
    2.68 +      fun add_class tycon (class,pairs) = 
    2.69 +            (class, domain_sorts(tycon,class))::pairs 
    2.70 +            handle Sorts.CLASS_ERROR _ => pairs
    2.71 +      fun try_classes tycon = (tycon, foldl (add_class tycon) [] classes)
    2.72 +  in  map try_classes tycons  end;
    2.73 +
    2.74 +fun arity_clause_thy thy tycons classes =
    2.75 +  multi_arity_clause (type_class_pairs thy tycons classes);
    2.76  
    2.77  
    2.78  (**** Find occurrences of predicates in clauses ****)
    2.79 @@ -594,9 +602,14 @@
    2.80  fun add_classrelClause_preds (ClassrelClause {subclass,superclass,...}, preds) =
    2.81    Symtab.update (subclass,1) (Symtab.update (superclass,1) preds);
    2.82  
    2.83 -fun add_arityClause_preds (ArityClause {conclLit,...}, preds) =
    2.84 -  let val TConsLit(_, (tclass, _, _)) = conclLit
    2.85 -  in  Symtab.update (tclass,1) preds  end;
    2.86 +(*Not sure the TVar case is ever used*)
    2.87 +fun class_of_arityLit (TConsLit(_, (tclass, _, _))) = tclass
    2.88 +  | class_of_arityLit (TVarLit(_, (tclass, _))) = tclass;
    2.89 +
    2.90 +fun add_arityClause_preds (ArityClause {conclLit,premLits,...}, preds) =
    2.91 +  let val classes = map class_of_arityLit (conclLit::premLits)
    2.92 +      fun upd (class,preds) = Symtab.update (class,1) preds
    2.93 +  in  foldl upd preds classes  end;
    2.94  
    2.95  fun preds_of_clauses clauses clsrel_clauses arity_clauses = 
    2.96    Symtab.dest
    2.97 @@ -755,8 +768,8 @@
    2.98  fun dfg_tfree_clause tfree_lit =
    2.99    "clause( %(conjecture)\n" ^ "or( " ^ tfree_lit ^ "),\n" ^ "tfree_tcs" ^ ").\n\n"
   2.100  
   2.101 -fun string_of_arClauseID (ArityClause {clause_id,axiom_name,...}) =
   2.102 -    arclause_prefix ^ ascii_of axiom_name ^ "_" ^ Int.toString clause_id;
   2.103 +fun string_of_arClauseID (ArityClause {axiom_name,...}) =
   2.104 +    arclause_prefix ^ ascii_of axiom_name;
   2.105  
   2.106  fun dfg_of_arLit (TConsLit(pol,(c,t,args))) =
   2.107        dfg_sign pol (c ^ "(" ^ t ^ paren_pack args ^ ")")