# HG changeset patch # User mengj # Date 1130459239 -7200 # Node ID 6ca14bec7cd591b40de1418caedd35bbb76542b7 # Parent ac059afd6b8625370335528377520e441f47d5ee Added new functions to handle HOL goals and lemmas. Added a funtion to send types and sorts information to ATP: they are clauses written to a separate file. Removed several functions definitions, and combined them with those in other files. diff -r ac059afd6b86 -r 6ca14bec7cd5 src/HOL/Tools/res_atp_setup.ML --- a/src/HOL/Tools/res_atp_setup.ML Fri Oct 28 02:25:57 2005 +0200 +++ b/src/HOL/Tools/res_atp_setup.ML Fri Oct 28 02:27:19 2005 +0200 @@ -11,10 +11,6 @@ val filter_ax = ref false; -fun writeln_strs _ [] = () - | writeln_strs out (s::ss) = (TextIO.output (out, s); TextIO.output (out, "\n"); writeln_strs out ss); - - fun warning_thm thm nm = warning (nm ^ " " ^ (string_of_thm thm)); fun warning_thms_n n thms nm = @@ -36,7 +32,7 @@ val prob_file = File.tmp_path (Path.basic "prob"); val hyps_file = File.tmp_path (Path.basic "hyps"); - +val types_sorts_file = File.tmp_path (Path.basic "typsorts"); (*******************************************************) (* operations on Isabelle theorems: *) @@ -45,14 +41,8 @@ (* CNF *) (*******************************************************) -fun repeat_RS thm1 thm2 = - let val thm1' = thm1 RS thm2 handle THM _ => thm1 - in - if eq_thm(thm1,thm1') then thm1' else (repeat_RS thm1' thm2) - end; - (* a special version of repeat_RS *) -fun repeat_someI_ex thm = repeat_RS thm someI_ex; +fun repeat_someI_ex thm = ResAxioms.repeat_RS thm someI_ex; val include_simpset = ref false; val include_claset = ref false; @@ -101,14 +91,22 @@ (***************** TPTP format *********************************) (* convert each (sub)goal clause (Thm.thm) into one or more TPTP clauses. The additional TPTP clauses are tfree_lits. Write the output TPTP clauses to a problem file *) -fun tptp_form thms n tfrees = - let val clss = ResClause.make_conjecture_clauses (map prop_of thms) - val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss) + +fun mk_conjectures is_fol terms = + if is_fol then + ListPair.unzip (map ResClause.clause2tptp (ResClause.make_conjecture_clauses terms)) + else + ListPair.unzip (map ResHolClause.clause2tptp (ResHolClause.make_conjecture_clauses terms)); + + +fun tptp_form_g is_fol thms n tfrees = + let val terms = map prop_of thms + val (tptp_clss,tfree_litss) = mk_conjectures is_fol terms val tfree_clss = map ResClause.tfree_clause ((ResClause.union_all tfree_litss) \\ tfrees) val probfile = File.platform_path prob_file ^ "_" ^ string_of_int n val out = TextIO.openOut(probfile) in - writeln_strs out (tfree_clss @ tptp_clss); + ResAtp.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out; warning probfile; (* show the location for debugging *) probfile (* return the location *) @@ -116,25 +114,31 @@ end; -fun tptp_hyps [] = ([], []) - | tptp_hyps thms = - let val prems = map (skolemize o make_nnf o ObjectLogic.atomize_thm) thms +val tptp_form = tptp_form_g true; +val tptp_formH = tptp_form_g false; + +fun tptp_hyps_g _ [] = ([], []) + | tptp_hyps_g is_fol thms = + let val mk_nnf = if is_fol then make_nnf else make_nnf1 + val prems = map (skolemize o mk_nnf o ObjectLogic.atomize_thm) thms val prems' = map repeat_someI_ex prems val prems'' = make_clauses prems' val prems''' = ResAxioms.rm_Eps [] prems'' - val clss = ResClause.make_conjecture_clauses prems''' - val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss) + val (tptp_clss,tfree_litss) = mk_conjectures is_fol prems''' val tfree_lits = ResClause.union_all tfree_litss val tfree_clss = map ResClause.tfree_clause tfree_lits val hypsfile = File.platform_path hyps_file val out = TextIO.openOut(hypsfile) in - writeln_strs out (tfree_clss @ tptp_clss); + ResAtp.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out; warning hypsfile; ([hypsfile],tfree_lits) end; +val tptp_hyps = tptp_hyps_g true; +val tptp_hypsH = tptp_hyps_g false; + fun subtract_simpset thy ctxt = let val rules1 = #rules (#1 (rep_ss (simpset_of thy))); @@ -148,33 +152,52 @@ val subtract = map (#2 o #2) oo Net.subtract Tactic.eq_kbrl; in map ResAxioms.pairname (subtract netI1 netI2 @ subtract netE1 netE2) end; + +fun mk_axioms is_fol rules = + if is_fol then + (let val clss = ResClause.union_all(ResAxioms.clausify_rules_pairs rules) + val (clss',names) = ListPair.unzip clss + val (tptpclss,_) = ListPair.unzip(map ResClause.clause2tptp clss') + in tptpclss end) + else + (let val clss = ResClause.union_all(ResAxioms.clausify_rules_pairsH rules) + val (clss',names) = ListPair.unzip clss + val (tptpclss,_) = ListPair.unzip(map ResHolClause.clause2tptp clss') + in tptpclss end) + + local -fun write_rules [] file = [](* no rules, then no need to write anything, thus no clasimp file *) - | write_rules rules file = +fun write_rules_g is_fol [] file = [](* no rules, then no need to write anything, thus no clasimp file *) + | write_rules_g is_fol rules file = let val out = TextIO.openOut(file) - val clss = ResClause.union_all(ResAxioms.clausify_rules_pairs rules) - val (clss',names) = ListPair.unzip clss - val (tptpclss,_) = ListPair.unzip(map ResClause.clause2tptp clss') + val tptpclss = mk_axioms is_fol rules in - writeln_strs out tptpclss; + ResAtp.writeln_strs out tptpclss; TextIO.closeOut out; warning file; [file] end; + +val write_rules = write_rules_g true; +val write_rulesH = write_rules_g false; + in (* TPTP Isabelle theorems *) -fun tptp_cnf_rules (clasetR,simpsetR) = +fun tptp_cnf_rules_g write_rules (clasetR,simpsetR) = let val simpfile = File.platform_path simpset_file val clafile = File.platform_path claset_file in (write_rules clasetR clafile) @ (write_rules simpsetR simpfile) end; +val tptp_cnf_rules = tptp_cnf_rules_g write_rules; +val tptp_cnf_rulesH = tptp_cnf_rules_g write_rulesH; + end -fun tptp_cnf_clasimp ctxt (include_claset,include_simpset) = +fun tptp_cnf_clasimp_g tptp_cnf_rules ctxt (include_claset,include_simpset) = let val local_claR = if include_claset then get_local_claR ctxt else (subtract_claset (ProofContext.theory_of ctxt) ctxt) val local_simpR = if include_simpset then get_local_simpR ctxt else (subtract_simpset (ProofContext.theory_of ctxt) ctxt) @@ -183,36 +206,73 @@ end; +val tptp_cnf_clasimp = tptp_cnf_clasimp_g tptp_cnf_rules; +val tptp_cnf_clasimpH = tptp_cnf_clasimp_g tptp_cnf_rulesH; + + +fun tptp_types_sorts thy = + let val classrel_clauses = ResClause.classrel_clauses_thy thy + val arity_clauses = ResClause.arity_clause_thy thy + val classrel_cls = map ResClause.tptp_classrelClause classrel_clauses + val arity_cls = map ResClause.tptp_arity_clause arity_clauses + fun write_ts () = + let val tsfile = File.platform_path types_sorts_file + val out = TextIO.openOut(tsfile) + in + ResAtp.writeln_strs out (classrel_cls @ arity_cls); + TextIO.closeOut out; + [tsfile] + end + in + if (List.null arity_cls andalso List.null classrel_cls) then [] + else + write_ts () + end; + + + (*FIXME: a function that does not perform any filtering now *) fun find_relevant_ax ctxt = tptp_cnf_clasimp ctxt (true,true); - (***************************************************************) (* setup ATPs as Isabelle methods *) (***************************************************************) -fun atp_meth' tac prems ctxt = +fun atp_meth_g tptp_hyps tptp_cnf_clasimp tac prems ctxt = let val rules = if !filter_ax then find_relevant_ax ctxt else tptp_cnf_clasimp ctxt (!include_claset, !include_simpset) val (hyps,tfrees) = tptp_hyps (ProofContext.prems_of ctxt) - val files = hyps @ rules + val thy = ProofContext.theory_of ctxt + val tsfile = tptp_types_sorts thy + val files = hyps @ rules @ tsfile in Method.METHOD (fn facts => if !debug then (warning_thms_n (length facts) facts "facts";HEADGOAL (tac ctxt files tfrees)) else HEADGOAL (tac ctxt files tfrees)) end; +val atp_meth_f = atp_meth_g tptp_hyps tptp_cnf_clasimp; -fun atp_meth tac prems ctxt = +val atp_meth_h = atp_meth_g tptp_hypsH tptp_cnf_clasimpH; + + +fun atp_meth_G atp_meth tac prems ctxt = let val _ = ResClause.init (ProofContext.theory_of ctxt) in - if not(List.null prems) then (warning_thms_n (length prems) prems "prems!!!"; atp_meth' tac prems ctxt) - else (atp_meth' tac prems ctxt) + if not(List.null prems) then (warning_thms_n (length prems) prems "prems!!!"; atp_meth tac prems ctxt) + else (atp_meth tac prems ctxt) end; -val atp_method = Method.bang_sectioned_args rules_modifiers o atp_meth; + +val atp_meth_H = atp_meth_G atp_meth_h; + +val atp_meth_F = atp_meth_G atp_meth_f; +val atp_method_H = Method.bang_sectioned_args rules_modifiers o atp_meth_H; + +val atp_method_F = Method.bang_sectioned_args rules_modifiers o atp_meth_F; + (*************Remove tmp files********************************)