src/HOL/Tools/res_atp.ML
changeset 21290 33b6bb5d6ab8
parent 21243 afffe1f72143
child 21311 3556301c18cd
equal deleted inserted replaced
21289:920b7b893d9c 21290:33b6bb5d6ab8
    70 val prover = ref "";   
    70 val prover = ref "";   
    71 
    71 
    72 fun set_prover atp = 
    72 fun set_prover atp = 
    73   case String.map Char.toLower atp of
    73   case String.map Char.toLower atp of
    74       "e" => 
    74       "e" => 
    75           (ReduceAxiomsN.max_new := 80;
    75           (ReduceAxiomsN.max_new := 100;
    76            ReduceAxiomsN.theory_const := false;
    76            ReduceAxiomsN.theory_const := false;
    77            prover := "E")
    77            prover := "E")
    78     | "spass" => 
    78     | "spass" => 
    79           (ReduceAxiomsN.max_new := 40;
    79           (ReduceAxiomsN.max_new := 40;
    80            ReduceAxiomsN.theory_const := true;
    80            ReduceAxiomsN.theory_const := true;
   583     (FactIndex.find (ProofContext.fact_index_of ctxt) ([], []));
   583     (FactIndex.find (ProofContext.fact_index_of ctxt) ([], []));
   584 
   584 
   585 fun multi_name a (th, (n,pairs)) = 
   585 fun multi_name a (th, (n,pairs)) = 
   586   (n+1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs)
   586   (n+1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs)
   587 
   587 
   588 fun multi_names ((a, []), pairs) = pairs
   588 fun add_multi_names ((a, []), pairs) = pairs
   589   | multi_names ((a, [th]), pairs) = (a,th)::pairs
   589   | add_multi_names ((a, [th]), pairs) = (a,th)::pairs
   590   | multi_names ((a, ths), pairs) = #2 (foldl (multi_name a) (1,pairs) ths);
   590   | add_multi_names ((a, ths), pairs) = #2 (foldl (multi_name a) (1,pairs) ths);
   591 
   591 
   592 fun name_thm_pairs ctxt = foldl multi_names [] (all_valid_thms ctxt);
   592 fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
       
   593 
       
   594 (*The single theorems go BEFORE the multiple ones*)
       
   595 fun name_thm_pairs ctxt = 
       
   596   let val (mults,singles) = List.partition is_multi (all_valid_thms ctxt)
       
   597   in  foldl add_multi_names (foldl add_multi_names [] mults) singles  end;
   593 
   598 
   594 fun check_named ("",th) = (warning ("No name for theorem " ^ string_of_thm th); false)
   599 fun check_named ("",th) = (warning ("No name for theorem " ^ string_of_thm th); false)
   595   | check_named (_,th) = true;
   600   | check_named (_,th) = true;
   596 
   601 
   597 (* get lemmas from claset, simpset, atpset and extra supplied rules *)
   602 (* get lemmas from claset, simpset, atpset and extra supplied rules *)
   631 	  val okthms = filter ok thms
   636 	  val okthms = filter ok thms
   632           val _ = Output.debug("...and returns " ^ Int.toString (length okthms))
   637           val _ = Output.debug("...and returns " ^ Int.toString (length okthms))
   633       in  okthms end
   638       in  okthms end
   634   else thms;
   639   else thms;
   635 
   640 
       
   641 (***************************************************************)
       
   642 (* Type Classes Present in the Axiom or Conjecture Clauses     *)
       
   643 (***************************************************************)
       
   644 
       
   645 fun setinsert (x,s) = Symtab.update (x,()) s;
       
   646 
       
   647 fun add_classes (sorts, cset) = foldl setinsert cset (List.concat sorts);
       
   648 
       
   649 (*Remove this trivial type class*)
       
   650 fun delete_type cset = Symtab.delete_safe "HOL.type" cset;
       
   651 
       
   652 fun tvar_classes_of_terms ts =
       
   653   let val sorts_list = map (map #2 o term_tvars) ts
       
   654   in  Symtab.keys (delete_type (foldl add_classes Symtab.empty sorts_list))  end;
       
   655 
       
   656 fun tfree_classes_of_terms ts =
       
   657   let val sorts_list = map (map #2 o term_tfrees) ts
       
   658   in  Symtab.keys (delete_type (foldl add_classes Symtab.empty sorts_list))  end;
   636 
   659 
   637 (***************************************************************)
   660 (***************************************************************)
   638 (* ATP invocation methods setup                                *)
   661 (* ATP invocation methods setup                                *)
   639 (***************************************************************)
   662 (***************************************************************)
   640 
   663 
   679 	val user_cls = ResAxioms.cnf_rules_pairs user_rules
   702 	val user_cls = ResAxioms.cnf_rules_pairs user_rules
   680 	val thy = ProofContext.theory_of ctxt
   703 	val thy = ProofContext.theory_of ctxt
   681 	val axclauses = get_relevant_clauses thy cla_simp_atp_clauses
   704 	val axclauses = get_relevant_clauses thy cla_simp_atp_clauses
   682 	                            user_cls (map prop_of goal_cls) |> make_unique
   705 	                            user_cls (map prop_of goal_cls) |> make_unique
   683 	val keep_types = if is_fol_logic logic then !fol_keep_types else is_typed_hol ()
   706 	val keep_types = if is_fol_logic logic then !fol_keep_types else is_typed_hol ()
   684 	val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else []
   707         val subs = tfree_classes_of_terms (map prop_of goal_cls)
       
   708         and supers = tvar_classes_of_terms (map (prop_of o #1) axclauses)
       
   709         (*TFrees in conjecture clauses; TVars in axiom clauses*)
       
   710         val classrel_clauses = 
       
   711               if keep_types then ResClause.make_classrel_clauses thy subs supers
       
   712               else []
   685 	val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else []
   713 	val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else []
   686         val writer = if dfg then dfg_writer else tptp_writer 
   714         val writer = if dfg then dfg_writer else tptp_writer 
   687 	and file = atp_input_file()
   715 	and file = atp_input_file()
   688 	and user_lemmas_names = map #1 user_rules
   716 	and user_lemmas_names = map #1 user_rules
   689     in
   717     in
   798                            goals
   826                            goals
   799       val _ = app (fn axcls => Output.debug ("filtered clauses = " ^ Int.toString(length axcls)))
   827       val _ = app (fn axcls => Output.debug ("filtered clauses = " ^ Int.toString(length axcls)))
   800                   axcls_list
   828                   axcls_list
   801       val keep_types = if is_fol_logic logic then !ResClause.keep_types 
   829       val keep_types = if is_fol_logic logic then !ResClause.keep_types 
   802                        else is_typed_hol ()
   830                        else is_typed_hol ()
   803       val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy
       
   804                              else []
       
   805       val _ = Output.debug ("classrel clauses = " ^ 
       
   806                             Int.toString (length classrel_clauses))
       
   807       val arity_clauses = if keep_types then ResClause.arity_clause_thy thy 
   831       val arity_clauses = if keep_types then ResClause.arity_clause_thy thy 
   808                           else []
   832                           else []
   809       val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
   833       val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
   810       val writer = if !prover = "spass" then dfg_writer else tptp_writer 
   834       val writer = if !prover = "spass" then dfg_writer else tptp_writer 
   811       fun write_all [] [] _ = []
   835       fun write_all [] [] _ = []
   812 	| write_all (ccls::ccls_list) (axcls::axcls_list) k =
   836 	| write_all (ccls::ccls_list) (axcls::axcls_list) k =
   813             let val fname = probfile k
   837             let val fname = probfile k
   814                 val axcls = make_unique axcls
   838                 val axcls = make_unique axcls
   815                 val ccls = subtract_cls ccls axcls
   839                 val ccls = subtract_cls ccls axcls
       
   840                 val subs = tfree_classes_of_terms (map prop_of ccls)
       
   841                 and supers = tvar_classes_of_terms (map (prop_of o #1) axcls)
       
   842                 (*TFrees in conjecture clauses; TVars in axiom clauses*)
       
   843                 val classrel_clauses = 
       
   844                       if keep_types then ResClause.make_classrel_clauses thy subs supers
       
   845                       else []
       
   846                 val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))
   816                 val clnames = writer logic ccls fname (axcls,classrel_clauses,arity_clauses) []
   847                 val clnames = writer logic ccls fname (axcls,classrel_clauses,arity_clauses) []
   817                 val thm_names = Array.fromList clnames
   848                 val thm_names = Array.fromList clnames
   818                 val _ = if !Output.show_debug_msgs 
   849                 val _ = if !Output.show_debug_msgs 
   819                         then trace_array (fname ^ "_thm_names") thm_names else ()
   850                         then trace_array (fname ^ "_thm_names") thm_names else ()
   820             in  (thm_names,fname) :: write_all ccls_list axcls_list (k+1)  end
   851             in  (thm_names,fname) :: write_all ccls_list axcls_list (k+1)  end