Improvement to classrel clauses: now outputs the minimum needed.
authorpaulson
Fri Nov 10 20:58:48 2006 +0100 (2006-11-10)
changeset 2129033b6bb5d6ab8
parent 21289 920b7b893d9c
child 21291 d59cbb8ce002
Improvement to classrel clauses: now outputs the minimum needed.
Theorem names: trying to minimize the number of multiple theorem names presented
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/res_clause.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Fri Nov 10 19:04:18 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Nov 10 20:58:48 2006 +0100
     1.3 @@ -72,7 +72,7 @@
     1.4  fun set_prover atp = 
     1.5    case String.map Char.toLower atp of
     1.6        "e" => 
     1.7 -          (ReduceAxiomsN.max_new := 80;
     1.8 +          (ReduceAxiomsN.max_new := 100;
     1.9             ReduceAxiomsN.theory_const := false;
    1.10             prover := "E")
    1.11      | "spass" => 
    1.12 @@ -585,11 +585,16 @@
    1.13  fun multi_name a (th, (n,pairs)) = 
    1.14    (n+1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs)
    1.15  
    1.16 -fun multi_names ((a, []), pairs) = pairs
    1.17 -  | multi_names ((a, [th]), pairs) = (a,th)::pairs
    1.18 -  | multi_names ((a, ths), pairs) = #2 (foldl (multi_name a) (1,pairs) ths);
    1.19 +fun add_multi_names ((a, []), pairs) = pairs
    1.20 +  | add_multi_names ((a, [th]), pairs) = (a,th)::pairs
    1.21 +  | add_multi_names ((a, ths), pairs) = #2 (foldl (multi_name a) (1,pairs) ths);
    1.22  
    1.23 -fun name_thm_pairs ctxt = foldl multi_names [] (all_valid_thms ctxt);
    1.24 +fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
    1.25 +
    1.26 +(*The single theorems go BEFORE the multiple ones*)
    1.27 +fun name_thm_pairs ctxt = 
    1.28 +  let val (mults,singles) = List.partition is_multi (all_valid_thms ctxt)
    1.29 +  in  foldl add_multi_names (foldl add_multi_names [] mults) singles  end;
    1.30  
    1.31  fun check_named ("",th) = (warning ("No name for theorem " ^ string_of_thm th); false)
    1.32    | check_named (_,th) = true;
    1.33 @@ -633,6 +638,24 @@
    1.34        in  okthms end
    1.35    else thms;
    1.36  
    1.37 +(***************************************************************)
    1.38 +(* Type Classes Present in the Axiom or Conjecture Clauses     *)
    1.39 +(***************************************************************)
    1.40 +
    1.41 +fun setinsert (x,s) = Symtab.update (x,()) s;
    1.42 +
    1.43 +fun add_classes (sorts, cset) = foldl setinsert cset (List.concat sorts);
    1.44 +
    1.45 +(*Remove this trivial type class*)
    1.46 +fun delete_type cset = Symtab.delete_safe "HOL.type" cset;
    1.47 +
    1.48 +fun tvar_classes_of_terms ts =
    1.49 +  let val sorts_list = map (map #2 o term_tvars) ts
    1.50 +  in  Symtab.keys (delete_type (foldl add_classes Symtab.empty sorts_list))  end;
    1.51 +
    1.52 +fun tfree_classes_of_terms ts =
    1.53 +  let val sorts_list = map (map #2 o term_tfrees) ts
    1.54 +  in  Symtab.keys (delete_type (foldl add_classes Symtab.empty sorts_list))  end;
    1.55  
    1.56  (***************************************************************)
    1.57  (* ATP invocation methods setup                                *)
    1.58 @@ -681,7 +704,12 @@
    1.59  	val axclauses = get_relevant_clauses thy cla_simp_atp_clauses
    1.60  	                            user_cls (map prop_of goal_cls) |> make_unique
    1.61  	val keep_types = if is_fol_logic logic then !fol_keep_types else is_typed_hol ()
    1.62 -	val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else []
    1.63 +        val subs = tfree_classes_of_terms (map prop_of goal_cls)
    1.64 +        and supers = tvar_classes_of_terms (map (prop_of o #1) axclauses)
    1.65 +        (*TFrees in conjecture clauses; TVars in axiom clauses*)
    1.66 +        val classrel_clauses = 
    1.67 +              if keep_types then ResClause.make_classrel_clauses thy subs supers
    1.68 +              else []
    1.69  	val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else []
    1.70          val writer = if dfg then dfg_writer else tptp_writer 
    1.71  	and file = atp_input_file()
    1.72 @@ -800,10 +828,6 @@
    1.73                    axcls_list
    1.74        val keep_types = if is_fol_logic logic then !ResClause.keep_types 
    1.75                         else is_typed_hol ()
    1.76 -      val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy
    1.77 -                             else []
    1.78 -      val _ = Output.debug ("classrel clauses = " ^ 
    1.79 -                            Int.toString (length classrel_clauses))
    1.80        val arity_clauses = if keep_types then ResClause.arity_clause_thy thy 
    1.81                            else []
    1.82        val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
    1.83 @@ -813,6 +837,13 @@
    1.84              let val fname = probfile k
    1.85                  val axcls = make_unique axcls
    1.86                  val ccls = subtract_cls ccls axcls
    1.87 +                val subs = tfree_classes_of_terms (map prop_of ccls)
    1.88 +                and supers = tvar_classes_of_terms (map (prop_of o #1) axcls)
    1.89 +                (*TFrees in conjecture clauses; TVars in axiom clauses*)
    1.90 +                val classrel_clauses = 
    1.91 +                      if keep_types then ResClause.make_classrel_clauses thy subs supers
    1.92 +                      else []
    1.93 +                val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))
    1.94                  val clnames = writer logic ccls fname (axcls,classrel_clauses,arity_clauses) []
    1.95                  val thm_names = Array.fromList clnames
    1.96                  val _ = if !Output.show_debug_msgs 
     2.1 --- a/src/HOL/Tools/res_axioms.ML	Fri Nov 10 19:04:18 2006 +0100
     2.2 +++ b/src/HOL/Tools/res_axioms.ML	Fri Nov 10 20:58:48 2006 +0100
     2.3 @@ -647,7 +647,8 @@
     2.4                         handle THM _ => pairs | ResClause.CLAUSE _ => pairs
     2.5        in  cnf_rules_pairs_aux pairs' ths  end;
     2.6  
     2.7 -val cnf_rules_pairs = cnf_rules_pairs_aux [];
     2.8 +(*The combination of rev and tail recursion preserves the original order*)
     2.9 +fun cnf_rules_pairs l = cnf_rules_pairs_aux [] (rev l);
    2.10  
    2.11  
    2.12  (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****)
     3.1 --- a/src/HOL/Tools/res_clause.ML	Fri Nov 10 19:04:18 2006 +0100
     3.2 +++ b/src/HOL/Tools/res_clause.ML	Fri Nov 10 20:58:48 2006 +0100
     3.3 @@ -23,7 +23,7 @@
     3.4    val arity_clause_thy: theory -> arityClause list 
     3.5    val ascii_of : string -> string
     3.6    val bracket_pack : string list -> string
     3.7 -  val classrel_clauses_thy: theory -> classrelClause list 
     3.8 +  val make_classrel_clauses: theory -> class list -> class list -> classrelClause list 
     3.9    val clause_prefix : string 
    3.10    val clause2tptp : clause -> string * string list
    3.11    val const_prefix : string
    3.12 @@ -529,23 +529,22 @@
    3.13  	 ClassrelClause of {axiom_name: axiom_name,
    3.14  			    subclass: class,
    3.15  			    superclass: class};
    3.16 -
    3.17 -fun make_axiom_classrelClause n subclass superclass =
    3.18 -  ClassrelClause {axiom_name = clrelclause_prefix ^ ascii_of subclass ^ 
    3.19 -                                "_" ^ Int.toString n,
    3.20 -                  subclass = make_type_class subclass, 
    3.21 -                  superclass = make_type_class superclass};
    3.22 + 
    3.23 +(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
    3.24 +fun class_pairs thy subs supers =
    3.25 +  let val class_less = Sorts.class_less(Sign.classes_of thy)
    3.26 +      fun add_super sub (super,pairs) = 
    3.27 +            if class_less (sub,super) then (sub,super)::pairs else pairs
    3.28 +      fun add_supers (sub,pairs) = foldl (add_super sub) pairs supers
    3.29 +  in  foldl add_supers [] subs  end;
    3.30  
    3.31 -fun classrelClauses_of_aux n sub [] = []
    3.32 -  | classrelClauses_of_aux n sub ("HOL.type"::sups) = (*Should be ignored*)
    3.33 -      classrelClauses_of_aux n sub sups
    3.34 -  | classrelClauses_of_aux n sub (sup::sups) =
    3.35 -      make_axiom_classrelClause n sub sup :: classrelClauses_of_aux (n+1) sub sups;
    3.36 +fun make_classrelClause (sub,super) =
    3.37 +  ClassrelClause {axiom_name = clrelclause_prefix ^ ascii_of sub ^ "_" ^ ascii_of super,
    3.38 +                  subclass = make_type_class sub, 
    3.39 +                  superclass = make_type_class super};
    3.40  
    3.41 -fun classrelClauses_of (sub,sups) = classrelClauses_of_aux 0 sub sups;
    3.42 -
    3.43 -val classrel_clauses_thy =
    3.44 -  maps classrelClauses_of o Graph.dest o #classes o Sorts.rep_algebra o Sign.classes_of;
    3.45 +fun make_classrel_clauses thy subs supers =
    3.46 +  map make_classrelClause (class_pairs thy subs supers);
    3.47  
    3.48  
    3.49  (** Isabelle arities **)