src/HOL/Tools/res_atp.ML
changeset 21373 18f519614978
parent 21311 3556301c18cd
child 21397 2134b81a0b37
     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