# HG changeset patch # User quigley # Date 1118412936 -7200 # Node ID f1275d2a1deed16b48a51e298f4a895747c949af # Parent 94011cf701a4dc3f346a28db675716e61c54c785 All subgoals sent to the watcher at once now. Rules added to parser for Spass proofs. If parsing or translation fails on a proof, the Spass proof is printed out in PG. diff -r 94011cf701a4 -r f1275d2a1dee src/HOL/Tools/ATP/SpassCommunication.ML --- a/src/HOL/Tools/ATP/SpassCommunication.ML Thu Jun 09 23:33:28 2005 +0200 +++ b/src/HOL/Tools/ATP/SpassCommunication.ML Fri Jun 10 16:15:36 2005 +0200 @@ -221,7 +221,8 @@ fun getSpassInput instr = if (isSome (TextIO.canInput(instr, 2))) then let val thisLine = TextIO.inputLine instr - val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_thisLine"))); val _ = TextIO.output (outfile, (thisLine)) + val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_thisLine"))); val _ = TextIO.output (outfile, (thisLine)) + val _ = TextIO.closeOut outfile in @@ -256,7 +257,7 @@ end ) - else if (thisLine = "Proof found but translation failed!") + else if ((substring (thisLine, 0,5)) = "Proof") then ( let val reconstr = thisLine diff -r 94011cf701a4 -r f1275d2a1dee src/HOL/Tools/ATP/recon_parse.ML --- a/src/HOL/Tools/ATP/recon_parse.ML Thu Jun 09 23:33:28 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_parse.ML Fri Jun 10 16:15:36 2005 +0200 @@ -212,6 +212,21 @@ ++ term_num >> (fn (_, (_, (c, (_, e)))) => Para (c, e)) + val super_l = (a (Word "SpL")) ++ (a (Other ":")) + ++ term_num ++ (a (Other ",")) + ++ term_num + >> (fn (_, (_, (c, (_, e)))) => Super_l (c, e)) + + + val super_r = (a (Word "SpR")) ++ (a (Other ":")) + ++ term_num ++ (a (Other ",")) + ++ term_num + >> (fn (_, (_, (c, (_, e)))) => Super_r (c, e)) + + + val aed = (a (Word "AED")) ++ (a (Other ":")) ++ term_num + >> (fn (_, (_, c)) => Obvious ((fst c),(snd c))) + val rewrite = (a (Word "Rew")) ++ (a (Other ":")) ++ term_num ++ (a (Other ",")) ++ term_num @@ -223,10 +238,27 @@ ++ term_num >> (fn (_, (_, (c, (_, e)))) => MRR (c, e)) + val ssi = (a (Word "SSi")) ++ (a (Other ":")) + ++ term_num ++ (a (Other ",")) + ++ term_num + >> (fn (_, (_, (c, (_, e)))) => SortSimp (c, e)) + + val unc = (a (Word "UnC")) ++ (a (Other ":")) + ++ term_num ++ (a (Other ",")) + ++ term_num + >> (fn (_, (_, (c, (_, e)))) => UnitConf (c, e)) + + val obv = (a (Word "Obv")) ++ (a (Other ":")) ++ term_num >> (fn (_, (_, c)) => Obvious ((fst c),(snd c))) - + + val eqres = (a (Word "EqR")) ++ (a (Other ":")) ++ term_num + >> (fn (_, (_, c)) => EqualRes ((fst c),(snd c))) + + val con = (a (Word "Con")) ++ (a (Other ":")) ++ term_num + >> (fn (_, (_, c)) => Condense ((fst c),(snd c))) + (* val hyper = a (Word "hyper") ++ many ((a (Other ",") ++ number) >> snd) @@ -234,7 +266,8 @@ *) (* val method = axiom ||binary || factor || para || hyper*) - val method = axiom || binary || factor || para || rewrite || mrr || obv + val method = axiom || binary || factor || para ||super_l || super_r || rewrite || mrr || obv || aed || ssi || unc|| con + val binary_s = a (Word "binary_s") ++ a (Other ",") ++ term_num >> (fn (_, (_, a)) => Binary_s a) val factor_s = a (Word "factor_s") @@ -316,7 +349,9 @@ || word ++ a (Other "(") ++ arglist ++ a (Other ")") >> (fn ( a, (_,(b,_ ))) => ("~"^" "^(remove_typeinfo a)^" "^b)) - || word >> (fn w => "~"^" "^(remove_typeinfo w))) input + || word ++ a (Other "*") >> (fn (w,b) => "~"^" "^(remove_typeinfo w)) + + || word >> (fn w => "~"^" "^(remove_typeinfo w))) input and nterm input = @@ -338,7 +373,9 @@ || word ++ a (Other "(") ++ arglist ++ a (Other ")") >> (fn (a, (_,(b,_ ))) => ((remove_typeinfo a)^" "^b)) - || word >> (fn w => (remove_typeinfo w)) ) input + || word ++ a (Other "*") >> (fn (w,b) => (remove_typeinfo w)) + || word >> (fn w => (remove_typeinfo w)) + ) input and peqterm input =( diff -r 94011cf701a4 -r f1275d2a1dee src/HOL/Tools/ATP/recon_transfer_proof.ML --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Thu Jun 09 23:33:28 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Fri Jun 10 16:15:36 2005 +0200 @@ -9,7 +9,6 @@ structure Recon_Transfer = struct - open Recon_Parse infixr 8 ++; infixr 7 >>; infixr 6 ||; @@ -210,7 +209,10 @@ end -(* add array and table here, so can retrieve clasimp axioms *) + +(*****************************************************) +(* get names of clasimp axioms used *) +(*****************************************************) fun get_axiom_names proof_steps thms (clause_arr:(ResClause.clause * thm) Array.array) num_of_clauses = let @@ -233,6 +235,33 @@ clasimp_names end + fun get_axiom_names_vamp proof_steps thms (clause_arr:(ResClause.clause * thm) Array.array) num_of_clauses = + let + (* not sure why this is necessary again, but seems to be *) + val _ = (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"]))) + val axioms = get_init_axioms proof_steps + val step_nums = get_step_nums axioms [] + + (***********************************************) + (* here need to add the clauses from clause_arr*) + (***********************************************) + + val (clasimp_names_cls) = get_clasimp_cls clause_arr num_of_clauses step_nums + val clasimp_names = map (#1 o ResClause.clause_info o #1) clasimp_names_cls + + val _ = File.write (File.tmp_path (Path.basic "clasimp_names")) + (concat clasimp_names) + val _ = (print_mode := (["xsymbols", "symbols"] @ ! print_mode)) + in + clasimp_names + end + + + + +(***********************************************) +(* get axioms for reconstruction *) +(***********************************************) fun numclstr (vars, []) str = str | numclstr ( vars, ((num, thm)::rest)) str = let val newstr = str^(string_of_int num)^" "^(string_of_thm thm)^" " @@ -343,18 +372,53 @@ val dummy_tac = PRIMITIVE(fn thm => thm ); -fun spassString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr num_of_clauses = - let val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "thmstringfile"))); val _ = TextIO.output (outfile, (" thmstring is: "^thmstring^"proofstr is: "^proofstr^"goalstr is: "^goalstring^" num of clauses is: "^(string_of_int num_of_clauses))) - val _ = TextIO.closeOut outfile +(*val proofstr = "1242[0:Inp] || -> equal(const_List_Orev(tconst_fun(tconst_List_Olist(U),tconst_List_Olist(U)),const_List_Olist_ONil),const_List_Olist_ONil)**.\ +\1279[0:Inp] || -> equal(const_Nat_Osize(tconst_fun(tconst_List_Olist(U),tconst_nat),const_List_Olist_ONil),const_0)**.\ +\1430[0:Inp] || equal(const_Nat_Osize(tconst_fun(tconst_List_Olist(typ__Ha),tconst_nat),const_List_Orev(tconst_fun(tconst_List_Olist(typ__Ha),tconst_List_Olist(typ__Ha)),const_List_Olist_ONil)),const_Nat_Osize(tconst_fun(tconst_List_Olist(typ__Ha),tconst_nat),const_List_Olist_ONil))** -> .\ +\1453[0:Rew:1279.0,1430.0,1242.0,1430.0,1279.0,1430.0] || equal(const_0,const_0)* -> .\ +\1454[0:Obv:1453.0] || -> .";*) + +fun remove_linebreaks str = let val strlist = explode str + val nonewlines = filter (not_equal "\n") strlist + in + implode nonewlines + end + + +fun subst_for a b [] = "" +| subst_for a b (x::xs) = if (x = a) + then + (b^(subst_for a b xs)) + else + x^(subst_for a b xs) + - (***********************************) - (* parse spass proof into datatype *) - (***********************************) +fun remove_linebreaks str = let val strlist = explode str + in + subst_for "\n" "\t" strlist + end + +fun restore_linebreaks str = let val strlist = explode str + in + subst_for "\t" "\n" strlist + end + + + +fun spassString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr num_of_clauses = + let val outfile = TextIO.openAppend( File.platform_path(File.tmp_path (Path.basic"thmstringfile"))); + val _ = TextIO.output (outfile, ("thmstring is: "^thmstring^"\n proofstr is: "^proofstr^"\n goalstr is: "^goalstring^" \n num of clauses is: "^(string_of_int num_of_clauses))) + + val _ = TextIO.closeOut outfile + + (***********************************) + (* parse spass proof into datatype *) + (***********************************) - val tokens = #1(lex proofstr) - val proof_steps1 = parse tokens - val proof_steps = just_change_space proof_steps1 - val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_parse"))); val _ = TextIO.output (outfile, ("Did parsing on "^proofstr)) + val tokens = #1(lex proofstr) + val proof_steps1 = parse tokens + val proof_steps = just_change_space proof_steps1 + val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_parse"))); val _ = TextIO.output (outfile, ("Did parsing on "^proofstr)) val _ = TextIO.closeOut outfile val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_thmstring_at_parse"))); val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring)) @@ -391,7 +455,7 @@ val _ = TextIO.output (outfile, ("In exception handler")); val _ = TextIO.closeOut outfile in - TextIO.output (toParent,"Proof found but translation failed!" ^"\n"); + TextIO.output (toParent,"Proof found but parsing failed for resolution proof: "^(remove_linebreaks proofstr) ^"\n"); TextIO.flushOut toParent; TextIO.output (toParent, thmstring^"\n"); TextIO.flushOut toParent; @@ -403,6 +467,71 @@ end) +(*fun vampString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr num_of_clauses = + let val outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "thmstringfile"))); val _ = TextIO.output (outfile, (" thmstring is: "^thmstring^"proofstr is: "^proofstr^"goalstr is: "^goalstring^" num of clauses is: "^(string_of_int num_of_clauses))) + val _ = TextIO.closeOut outfile + + (***********************************) + (* parse spass proof into datatype *) + (***********************************) + + val tokens = #1(lex proofstr) + val proof_steps = VampParse.parse tokens + (*val proof_steps = just_change_space proof_steps1*) + val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_parse"))); val _ = TextIO.output (outfile, ("Did parsing on "^proofstr)) + val _ = TextIO.closeOut outfile + + val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_thmstring_at_parse"))); val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring)) + val _ = TextIO.closeOut outfile + (************************************) + (* recreate original subgoal as thm *) + (************************************) + + (* get axioms as correctly numbered clauses w.r.t. the Spass proof *) + (* need to get prems_of thm, then get right one of the prems, relating to whichever*) + (* subgoal this is, and turn it into meta_clauses *) + (* should prob add array and table here, so that we can get axioms*) + (* produced from the clasimpset rather than the problem *) + + val (axiom_names) = get_axiom_names_vamp proof_steps thms clause_arr num_of_clauses + val ax_str = "Rules from clasimpset used in proof found by SPASS: "^(rules_to_string axiom_names "") + val outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "reconstrfile"))); val _ = TextIO.output (outfile, ("reconstring is: "^ax_str^" "^goalstring)) + val _ = TextIO.closeOut outfile + + in + TextIO.output (toParent, ax_str^"\n"); + TextIO.flushOut toParent; + TextIO.output (toParent, "goalstring: "^goalstring^"\n"); + TextIO.flushOut toParent;fdsa + TextIO.output (toParent, "thmstring: "^thmstring^"\n"); + TextIO.flushOut toParent; + + Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); + (* Attempt to prevent several signals from turning up simultaneously *) + Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac + end + handle _ => (let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_handler"))); + + val _ = TextIO.output (outfile, ("In exception handler")); + val _ = TextIO.closeOut outfile + in + TextIO.output (toParent,"Proof found but translation failed for resolution proof: \n"^(remove_linebreaks proofstr) ^"\n"); + TextIO.flushOut toParent; + TextIO.output (toParent, thmstring^"\n"); + TextIO.flushOut toParent; + TextIO.output (toParent, goalstring^"\n"); + TextIO.flushOut toParent; + Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); + (* Attempt to prevent several signals from turning up simultaneously *) + Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac + end) +*) + + + +(* val proofstr = "1582[0:Inp] || -> v_P*.\ + \1583[0:Inp] || v_P* -> .\ + \1584[0:MRR:1583.0,1582.0] || -> ."; *) fun spassString_to_reconString proofstr thmstring goalstring toParent ppid thms clause_arr num_of_clauses = let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "thmstringfile"))); @@ -490,7 +619,7 @@ val _ = TextIO.output (outfile, ("In exception handler")); val _ = TextIO.closeOut outfile in - TextIO.output (toParent,"Proof found but translation failed!" ^"\n"); + TextIO.output (toParent,"Proof found but translation failed for resolution proof: \n"^proofstr ^"\n"); TextIO.flushOut toParent; TextIO.output (toParent, thmstring^"\n"); TextIO.flushOut toParent; @@ -742,12 +871,16 @@ fun have_isar_line (numb,(step, clstrs, thmstrs))="have cl"^(string_of_int numb)^": "^(clause_strs_to_isar clstrs thmstrs)^"\n" - +(*FIX: ask Larry to add and mrr attribute *) fun by_isar_line ((Binary ((a,b), (c,d)))) = "by(rule cl"^ (string_of_int a)^" [binary "^(string_of_int b)^" cl"^ (string_of_int c)^" "^(string_of_int d)^"])\n" +|by_isar_line ((MRR ((a,b), (c,d)))) = + "by(rule cl"^ + (string_of_int a)^" [binary "^(string_of_int b)^" cl"^ + (string_of_int c)^" "^(string_of_int d)^"])\n" | by_isar_line ( (Para ((a,b), (c,d)))) = "by (rule cl"^ (string_of_int a)^" [paramod "^(string_of_int b)^" cl"^ @@ -826,7 +959,8 @@ *) fun apply_res_thm str goalstring = let val tokens = #1 (lex str); - + val _ = File.append (File.tmp_path (Path.basic "applyres")) + ("str is: "^str^" goalstr is: "^goalstring^"\n") val (frees,recon_steps) = parse_step tokens val isar_str = to_isar_proof (frees, recon_steps, goalstring) val foo = TextIO.openOut (File.platform_path(File.tmp_path (Path.basic "foobar"))); @@ -835,6 +969,6 @@ end - - +(* val reconstr = reconstr^"[P%]51Axiom()[~P%]52Axiom[P%][]53MRR((52,0),(51,0))[][]"; +*) end; diff -r 94011cf701a4 -r f1275d2a1dee src/HOL/Tools/ATP/recon_translate_proof.ML --- a/src/HOL/Tools/ATP/recon_translate_proof.ML Thu Jun 09 23:33:28 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_translate_proof.ML Fri Jun 10 16:15:36 2005 +0200 @@ -35,8 +35,15 @@ | MRR of (int * int) * (int * int) | Factor of (int * int * int) (* (clause,lit1, lit2) *) | Para of (int * int) * (int * int) + | Super_l of (int * int) * (int * int) + | Super_r of (int * int) * (int * int) | Rewrite of (int * int) * (int * int) + | SortSimp of (int * int) * (int * int) + | UnitConf of (int * int) * (int * int) | Obvious of (int * int) + | AED of (int*int) + | EqualRes of (int*int) + | Condense of (int*int) (*| Hyper of int list*) | Unusedstep of unit diff -r 94011cf701a4 -r f1275d2a1dee src/HOL/Tools/ATP/res_clasimpset.ML --- a/src/HOL/Tools/ATP/res_clasimpset.ML Thu Jun 09 23:33:28 2005 +0200 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML Fri Jun 10 16:15:36 2005 +0200 @@ -8,6 +8,7 @@ signature RES_CLASIMP = sig val write_out_clasimp :string -> theory -> (ResClause.clause * thm) Array.array * int +val write_out_clasimp_small :string -> theory -> (ResClause.clause * thm) Array.array * int end; structure ResClasimp : RES_CLASIMP = @@ -112,6 +113,53 @@ (clause_arr, num_of_clauses) end; + + + + +(*Write out the claset and simpset rules of the supplied theory. Only include the first 50 rules*) +fun write_out_clasimp_small filename thy = + let val claset_rules = ResAxioms.claset_rules_of_thy thy; + val named_claset = List.filter has_name_pair claset_rules; + val claset_names = map remove_spaces_pair (named_claset) + val claset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_claset []); + + val simpset_rules = ResAxioms.simpset_rules_of_thy thy; + val named_simpset = + map remove_spaces_pair (List.filter has_name_pair simpset_rules) + val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []); + + val cls_thms = (claset_cls_thms@simpset_cls_thms); + val cls_thms_list = List.concat cls_thms; + (* length 1429 *) + (*************************************************) + (* Write out clauses as tptp strings to filename *) + (*************************************************) + val clauses = map #1(cls_thms_list); + val cls_tptp_strs = map ResClause.tptp_clause clauses; + val alllist = pairup cls_thms_list cls_tptp_strs + val whole_list = List.concat (map clause_numbering alllist); + val mini_list = List.take ( whole_list,50) + (*********************************************************) + (* create array and put clausename, number pairs into it *) + (*********************************************************) + val num_of_clauses = 0; + val clause_arr = Array.fromList mini_list; + val num_of_clauses = List.length mini_list; + + (* list of lists of tptp string clauses *) + val stick_clasrls = List.concat cls_tptp_strs; + (* length 1581*) + val out = TextIO.openOut filename; + val _= ResLib.writeln_strs out (List.take (stick_clasrls,50)); + val _= TextIO.flushOut out; + val _= TextIO.closeOut out + in + (clause_arr, num_of_clauses) + end; + + + end; diff -r 94011cf701a4 -r f1275d2a1dee src/HOL/Tools/ATP/watcher.ML --- a/src/HOL/Tools/ATP/watcher.ML Thu Jun 09 23:33:28 2005 +0200 +++ b/src/HOL/Tools/ATP/watcher.ML Fri Jun 10 16:15:36 2005 +0200 @@ -150,60 +150,27 @@ TextIO.flushOut toWatcherStr) (*****************************************************************************************) -(* Send request to Watcher for multiple provers to be called for filenames in arg *) +(* Send request to Watcher for multiple provers to be called for filenames in arg *) +(* need to do the dfg stuff in the watcher, not here! send over the clasimp and stuff files too*) (*****************************************************************************************) + (* need to modify to send over hyps file too *) -fun callResProvers (toWatcherStr, []) = - (sendOutput (toWatcherStr, "End of calls\n"); - TextIO.flushOut toWatcherStr) +fun callResProvers (toWatcherStr, []) = (sendOutput (toWatcherStr, "End of calls\n"); + TextIO.flushOut toWatcherStr) | callResProvers (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings,clasimpfile, axfile, hypsfile,probfile)::args) = - let val dfg_dir = File.tmp_path (Path.basic "dfg"); - (*** need to check here if the directory exists and, if not, create it***) - val _ = File.append (File.tmp_path (Path.basic"thmstring_in_watcher")) - (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n") - (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***) - val probID = ReconOrderClauses.last(explode probfile) - val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID)) - (*** only include problem and clasimp for the moment, not sure how to refer to ***) - - (*** hyps/local axioms just now (*,axfile, hypsfile,*) ***) - val whole_prob_file = system ("cat " ^ clasimpfile ^" "^ probfile ^ " > " ^ File.shell_path wholefile) + let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "tog_comms"))); + val _ = TextIO.output (outfile,(prover^thmstring^goalstring^proverCmd^settings^clasimpfile^hypsfile^probfile) ) + val _ = TextIO.closeOut outfile + in (sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^ + settings^"*"^clasimpfile^"*"^hypsfile^"*"^probfile^"\n")); + goals_being_watched := (!goals_being_watched) + 1; + TextIO.flushOut toWatcherStr; + + callResProvers (toWatcherStr,args)) + end + - val dfg_create = if File.exists dfg_dir - then warning("dfg dir exists") - else File.mkdir dfg_dir; - - val dfg_path = File.platform_path dfg_dir; - (* val exec_tptp2x = - Unix.execute(getenv "TPTP2X_HOME" ^ "/tptp2X", - ["-fdfg", "-d " ^ dfg_path, File.platform_path wholefile]) *) - val tptp_home = getenv "TPTP2X_HOME" ^ "/tptp2X" - - val systemcall = system (tptp_home ^ " -fdfg -d " ^ File.shell_path dfg_dir ^ " " ^ File.shell_path wholefile) - val _ = warning("systemcall is "^ (string_of_int systemcall)) - (*val _ = Posix.Process.wait ()*) - (*val _ =Unix.reap exec_tptp2x*) - val newfile = dfg_path^"/ax_prob"^"_"^(probID)^".dfg" - - in - goals_being_watched := (!goals_being_watched) + 1; - Posix.Process.sleep(Time.fromSeconds 1); - (warning ("probfile is: "^probfile)); - (warning("dfg file is: "^newfile)); - (warning ("wholefile is: "^(File.platform_path wholefile))); - sendOutput (toWatcherStr, - prover ^ "*" ^ thmstring ^ "*" ^ goalstring ^ "*" ^ proverCmd ^ - "*" ^ settings ^ "*" ^ newfile ^ "\n"); - (*sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^"/homes/clq20/IsabelleCVS/isabelle/HOL/Tools/ATP/dfg/mini_p1.dfg"^"\n"));*) - TextIO.flushOut toWatcherStr; - (*Unix.reap exec_tptp2x;*) - if File.exists - (Path.append dfg_dir (Path.basic ("ax_prob"^"_" ^ probID ^ ".dfg"))) - then callResProvers (toWatcherStr, args) - else error ("tptp2X failed: " ^ getenv "TPTP2X_HOME" ^ "/tptp2X" ^ - " -fdfg " ^ File.platform_path wholefile ^ " -d " ^ dfg_path) - end (* fun callResProversStr (toWatcherStr, []) = "End of calls\n" @@ -240,69 +207,155 @@ getSettings rest (settings@[(implode set)]) end -fun separateFields str = - let val (prover, rest) = takeUntil "*" str [] - val prover = implode prover - val (thmstring, rest) = takeUntil "*" rest [] - val thmstring = implode thmstring - val (goalstring, rest) = takeUntil "*" rest [] - val goalstring = implode goalstring - val (proverCmd, rest ) = takeUntil "*" rest [] - val proverCmd = implode proverCmd - - val (settings, rest) = takeUntil "*" rest [] - val settings = getSettings settings [] - val (file, rest) = takeUntil "*" rest [] - val file = implode file - val _ = File.write (File.tmp_path (Path.basic "sep_comms")) - (prover^thmstring^goalstring^proverCmd^file) - in - (prover,thmstring,goalstring, proverCmd, settings, file) - end +fun separateFields str = let val outfile = TextIO.openAppend(*("sep_field")*)(File.platform_path(File.tmp_path (Path.basic "sep_field"))) + val _ = TextIO.output (outfile,("In separateFields, str is: "^(implode str)^"\n\n") ) + val _ = TextIO.closeOut outfile + val (prover, rest) = takeUntil "*" str [] + val prover = implode prover + + val (thmstring, rest) = takeUntil "*" rest [] + val thmstring = implode thmstring + + val (goalstring, rest) = takeUntil "*" rest [] + val goalstring = implode goalstring + + val (proverCmd, rest ) = takeUntil "*" rest [] + val proverCmd = implode proverCmd + + val (settings, rest) = takeUntil "*" rest [] + val settings = getSettings settings [] + + val (clasimpfile, rest ) = takeUntil "*" rest [] + val clasimpfile = implode clasimpfile + + val (hypsfile, rest ) = takeUntil "*" rest [] + val hypsfile = implode hypsfile + + val (file, rest) = takeUntil "*" rest [] + val file = implode file + + val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "sep_comms"))); + val _ = TextIO.output (outfile,("Sep comms are: "^(implode str)^"**"^prover^thmstring^goalstring^proverCmd^clasimpfile^hypsfile^file^"\n\n") ) + val _ = TextIO.closeOut outfile + + in + (prover,thmstring,goalstring, proverCmd, settings, clasimpfile, hypsfile, file) + end + +(***********************************************************************************) +(* do tptp2x and cat to turn clasimpfile, hypsfile and probfile into one .dfg file *) +(***********************************************************************************) + +fun formatCmd (prover,thmstring,goalstring, proverCmd, settings, clasimpfile, hypsfile ,probfile) = + let + val dfg_dir = File.tmp_path (Path.basic "dfg"); + + (*** need to check here if the directory exists and, if not, create it***) + + + (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***) + val probID = List.last(explode probfile) + val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID)) + + (*** only include problem and clasimp for the moment, not sure how to refer to ***) + (*** hyps/local axioms just now ***) + val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*axfile, hypsfile,*)probfile, ">", (File.platform_path wholefile)]) + val dfg_create = + if File.exists dfg_dir + then + ((warning("dfg dir exists"));()) + else + File.mkdir dfg_dir; + val dfg_path = File.platform_path dfg_dir; + + val bar = system ("/usr/groups/theory/tptp/TPTP-v3.0.1/TPTP2X/tptp2X -fdfg "^ + (File.platform_path wholefile)^" -d "^dfg_path) + val newfile = dfg_path^"/ax_prob"^"_"^(probID)^".dfg" + val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic"thmstring_in_watcher"))); + val _ = TextIO.output (outfile, (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^newfile^"\n")) + val _ = TextIO.closeOut outfile + + in + (prover,thmstring,goalstring, proverCmd, settings,newfile) + end; + + +(* remove \n from end of command and put back into tuple format *) + + +(* val cmdStr = "spass*((ALL xa. (~ P x | P xa) & (~ P xa | P x)) & (P xa | (ALL x. P x)) & ((ALL x. ~ P x) | ~ P xb) [.])*(EX x. ALL y. P x = P y) --> (EX x. P x) = (ALL y. P y)*/homes/clq20/bin/SPASS*-DocProof*/local/scratch/clq20/27023/clasimp*/local/scratch/clq20/27023/hyps*/local/scratch/clq20/27023/prob_1\n" *) + +(*FIX: are the two getCmd procs getting confused? Why do I have two anyway? *) fun getCmd cmdStr = let val backList = ((rev(explode cmdStr))) + val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic"cmdStr"))); + val _ = TextIO.output (outfile, (cmdStr)) + val _ = TextIO.closeOut outfile in if (String.isPrefix "\n" (implode backList )) then - separateFields ((rev ((tl backList)))) + ( let + val newCmdStr = (rev(tl backList)) + val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic"backlist"))); + val _ = TextIO.output (outfile, ("about to call sepfields with "^(implode newCmdStr))) + val _ = TextIO.closeOut outfile + val cmdtuple = separateFields newCmdStr + in + formatCmd cmdtuple + end) else - (separateFields (explode cmdStr)) + ( let + val cmdtuple =(separateFields (explode cmdStr)) + in + formatCmd cmdtuple + end) + end fun getProofCmd (a,b,c,d,e,f) = d - + (**************************************************************) (* Get commands from Isabelle *) (**************************************************************) +(* FIX: or perhaps do the tptp2x stuff here - so it's get commands and then format them, before passing them to spass *) fun getCmds (toParentStr,fromParentStr, cmdList) = - let val thisLine = TextIO.inputLine fromParentStr - in - (if (thisLine = "End of calls\n") - then - (cmdList) - else if (thisLine = "Kill children\n") - then - ( TextIO.output (toParentStr,thisLine ); - TextIO.flushOut toParentStr; - (("","","","Kill children",[],"")::cmdList) - ) - else (let val thisCmd = getCmd (thisLine) (* thisCmd = (prover,thmstring,proverCmd, settings, file)*) - in - (*TextIO.output (toParentStr, thisCmd); - TextIO.flushOut toParentStr;*) - getCmds (toParentStr,fromParentStr, (thisCmd::cmdList)) - end - ) - ) - end + let val thisLine = TextIO.inputLine fromParentStr + val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "parent_comms"))); + val _ = TextIO.output (outfile,(thisLine) ) + val _ = TextIO.closeOut outfile + in + (if (thisLine = "End of calls\n") + then + + (cmdList) + + else if (thisLine = "Kill children\n") + then + ( TextIO.output (toParentStr,thisLine ); + TextIO.flushOut toParentStr; + (("","","","Kill children",[],"")::cmdList) + ) + else (let val thisCmd = getCmd (thisLine) + (*********************************************************) + (* thisCmd = (prover,thmstring,proverCmd, settings, file)*) + (* i.e. put back into tuple format *) + (*********************************************************) + in + (*TextIO.output (toParentStr, thisCmd); + TextIO.flushOut toParentStr;*) + getCmds (toParentStr,fromParentStr, (thisCmd::cmdList)) + end + ) + ) + end - + (**************************************************************) (* Get Io-descriptor for polling of an input stream *) (**************************************************************) @@ -388,6 +441,8 @@ if (isSome pd ) then let val pd' = OS.IO.pollIn (valOf pd) val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) + val _ = File.append (File.tmp_path (Path.basic "parent_poll")) + ("In parent_poll\n") in if null pdl then @@ -414,13 +469,15 @@ if (isSome pd ) then let val pd' = OS.IO.pollIn (valOf pd) val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) + val _ = File.append (File.tmp_path (Path.basic "child_poll")) + ("In child_poll\n") in if null pdl then NONE else if (OS.IO.isIn (hd pdl)) then - SOME (getCmd (TextIO.inputLine fromStr)) + SOME ((*getCmd*) (TextIO.inputLine fromStr)) else NONE end @@ -439,13 +496,19 @@ fun checkChildren ([], toParentStr) = [] (*** no children to check ********) (*********************************) | checkChildren ((childProc::otherChildren), toParentStr) = - let val (childInput,childOutput) = cmdstreamsOf childProc + let val _ = File.append (File.tmp_path (Path.basic "child_check")) + ("In check child, length of queue:"^(string_of_int (length (childProc::otherChildren)))^"\n") + val (childInput,childOutput) = cmdstreamsOf childProc val child_handle= cmdchildHandle childProc (* childCmd is the .dfg file that the problem is in *) val childCmd = fst(snd (cmdchildInfo childProc)) + val _ = File.append (File.tmp_path (Path.basic "child_command")) + (childCmd^"\n") (* now get the number of the subgoal from the filename *) val sg_num = int_of_string(ReconOrderClauses.get_nth 5 (rev(explode childCmd))) val childIncoming = pollChildInput childInput + val _ = File.append (File.tmp_path (Path.basic "child_check_polled")) + ("finished polling child \n") val parentID = Posix.ProcEnv.getppid() val prover = cmdProver childProc val thmstring = cmdThm childProc @@ -454,8 +517,8 @@ val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) val _ = warning("subgoals forked to checkChildren: "^prems_string) val goalstring = cmdGoal childProc - val _ = File.write (File.tmp_path (Path.basic "child_comms")) - (prover^thmstring^goalstring^childCmd) + val _ = File.append (File.tmp_path (Path.basic "child_comms")) + (prover^thmstring^goalstring^childCmd^"\n") in if (isSome childIncoming) then @@ -496,8 +559,9 @@ (*** add subgoal id num to this *) fun execCmds [] procList = procList - | execCmds ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList = - if (prover = "spass") + | execCmds ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList = let val _ = File.append (File.tmp_path (Path.basic "pre_exec_child")) ("About to execute command for goal:\n"^goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now())))) + in + if (prover = "spass") then let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file]))) val (instr, outstr)=Unix.streamsOf childhandle @@ -509,12 +573,12 @@ proc_handle = childhandle, instr = instr, outstr = outstr })::procList)) - val _ = File.append (File.tmp_path (Path.basic "exec_child")) ("executing command for goal:"^goalstring^proverCmd^(concat settings)^file) + val _ = File.append (File.tmp_path (Path.basic "exec_child")) ("executing command for goal:\n"^goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now())))) in - execCmds cmds newProcList + Posix.Process.sleep (Time.fromSeconds 1);execCmds cmds newProcList end else - let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file]))) + let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc = (Unix.execute(proverCmd, (settings@[file]))) val (instr, outstr)=Unix.streamsOf childhandle val newProcList = (((CMDPROC{ prover = prover, @@ -525,9 +589,9 @@ instr = instr, outstr = outstr })::procList)) in - execCmds cmds newProcList + Posix.Process.sleep (Time.fromSeconds 1); execCmds cmds newProcList end - + end (****************************************) @@ -587,7 +651,11 @@ let val newProcList = execCmds (valOf cmdsFromIsa) procList val parentID = Posix.ProcEnv.getppid() + val _ = (File.append (File.tmp_path (Path.basic "prekeep_watch")) "Just execed a child\n ") val newProcList' =checkChildren (newProcList, toParentStr) + + val _ = warning("off to keep watching...") + val _ = (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching...\n ") in (*Posix.Process.sleep (Time.fromSeconds 1);*) loop (newProcList') @@ -615,7 +683,8 @@ (******************************) ( let val newProcList = checkChildren ((procList), toParentStr) in - Posix.Process.sleep (Time.fromSeconds 1); + (*Posix.Process.sleep (Time.fromSeconds 1);*) + (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching.2..\n "); loop (newProcList) end @@ -797,11 +866,11 @@ ( goals_being_watched := (!goals_being_watched) -1; Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); - Pretty.writeln(Pretty.str (goalstring^reconstr)); + Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr))); Pretty.writeln(Pretty.str (oct_char "361")); if (!goals_being_watched = 0) then - (let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_comp"))); + (let val outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp"))); val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n")) val _ = TextIO.closeOut outfile in diff -r 94011cf701a4 -r f1275d2a1dee src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Thu Jun 09 23:33:28 2005 +0200 +++ b/src/HOL/Tools/res_atp.ML Fri Jun 10 16:15:36 2005 +0200 @@ -31,12 +31,13 @@ val subgoals = []; val traceflag = ref true; +(* used for debug *) +val debug = ref false; -val debug = ref false; fun debug_tac tac = (warning "testing";tac); - +(* default value is false *) +val full_spass = ref false; val trace_res = ref false; -val full_spass = ref false; val skolem_tac = skolemize_tac; @@ -69,10 +70,13 @@ (**** for Isabelle/ML interface ****) -fun is_proof_char ch = (ch = " ") orelse - ((ord"!" <= ord ch) andalso (ord ch <= ord"~") andalso (ch <> "?")) +fun is_proof_char ch = ((33 <= (ord ch)) andalso ((ord ch ) <= 126) andalso (not ((ord ch ) = 63))) orelse (ch = " ") -fun proofstring x = List.filter (is_proof_char) (explode x); +fun proofstring x = let val exp = explode x + in + List.filter (is_proof_char ) exp + end + (* @@ -130,113 +134,90 @@ val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n) val out = TextIO.openOut(probfile) in - (ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out; - if !trace_res then (warning probfile) else ()) + (ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out; (if !trace_res then (warning probfile) else ())) end; + (*********************************************************************) (* call SPASS with settings and problem file for the current subgoal *) (* should be modified to allow other provers to be called *) (*********************************************************************) +(* now passing in list of skolemized thms and list of sgterms to go with them *) +fun call_resolve_tac (thms: Thm.thm list list) sign (sg_terms: Term.term list) (childin, childout,pid) n = let + val axfile = (File.platform_path axiom_file) + val hypsfile = (File.platform_path hyps_file) + val clasimpfile = (File.platform_path clasimp_file) + val spass_home = getenv "SPASS_HOME" + +fun make_atp_list [] sign n = [] +| make_atp_list ((sko_thm, sg_term)::xs) sign n = +let + val skothmstr = Meson.concat_with_and (map string_of_thm sko_thm) + val thmproofstr = proofstring ( skothmstr) + val no_returns =List.filter not_newline ( thmproofstr) + val thmstr = implode no_returns + val _ = warning ("thmstring in make_atp_lists is: "^thmstr) -fun call_resolve_tac sign thms sg_term (childin, childout,pid) n = - let val thmstring = Meson.concat_with_and (map string_of_thm thms) - val thm_no = length thms - val _ = warning ("number of thms is : "^(string_of_int thm_no)) - val _ = warning ("thmstring in call_res is: "^thmstring) - - val goalstr = Sign.string_of_term sign sg_term - val goalproofstring = proofstring goalstr - val no_returns =List.filter not_newline ( goalproofstring) - val goalstring = implode no_returns - val _ = warning ("goalstring in call_res is: "^goalstring) - - (*val prob_file =File.tmp_path (Path.basic newprobfile); *) - (*val _ =( warning ("calling make_clauses ")) - val clauses = make_clauses thms - val _ =( warning ("called make_clauses "))*) - (*val _ = tptp_inputs clauses prob_file*) - val thmstring = Meson.concat_with_and (map string_of_thm thms) - - val goalstr = Sign.string_of_term sign sg_term - val goalproofstring = proofstring goalstr + val sgstr = Sign.string_of_term sign sg_term + val goalproofstring = proofstring sgstr val no_returns =List.filter not_newline ( goalproofstring) val goalstring = implode no_returns - - val thmproofstring = proofstring ( thmstring) - val no_returns =List.filter not_newline ( thmproofstring) - val thmstr = implode no_returns - + val _ = warning ("goalstring in make_atp_lists is: "^goalstring) + val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n) - val axfile = (File.platform_path axiom_file) - val hypsfile = (File.platform_path hyps_file) - val clasimpfile = (File.platform_path clasimp_file) - val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "hellofile"))) - val _ = TextIO.output(outfile, "prob file path is "^probfile^" thmstring is "^thmstr^" goalstring is "^goalstring); - val _ = TextIO.flushOut outfile; - val _ = TextIO.closeOut outfile - in - (* without paramodulation *) - (warning ("goalstring in call_res_tac is: "^goalstring)); - (warning ("prob file in cal_res_tac is: "^probfile)); - (* Watcher.callResProvers(childout, - [("spass",thmstr,goalstring,*spass_home*, - "-DocProof", - clasimpfile, axfile, hypsfile, probfile)]);*) - if !full_spass - then - (Watcher.callResProvers(childout, - [("spass", thmstr, goalstring (*,spass_home*), - getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell", - "-DocProof%-TimeLimit=60", - clasimpfile, axfile, hypsfile, probfile)])) - else - (Watcher.callResProvers(childout, - [("spass", thmstr, goalstring (*,spass_home*), - getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell", - "-Auto=0%-ISRe%-ISFc%-RTaut%-RFSub%-RBSub%-DocProof%-TimeLimit=60", - clasimpfile, axfile, hypsfile, probfile)])); - - (* with paramodulation *) - (*Watcher.callResProvers(childout, - [("spass",thmstr,goalstring,spass_home, - "-FullRed=0%-ISPm=1%-Split=0%-PObv=0%-DocProof", - prob_path)]); *) - (* Watcher.callResProvers(childout, - [("spass",thmstr,goalstring,spass_home, - "-DocProof", prob_path)]);*) - dummy_tac - end + val _ = (warning ("prob file in cal_res_tac is: "^probfile)) +in + if !full_spass + then + ([("spass", thmstr, goalstring (*,spass_home*), + getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell"(*( getenv "SPASS_HOME")^"/SPASS"*), + "-DocProof%-TimeLimit=60", + clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1))) + else + ([("spass", thmstr, goalstring (*,spass_home*), + getenv "ISABELLE_HOME" ^"/src/HOL/Tools/ATP/spassshell"(* (getenv "SPASS_HOME")^"/SPASS"*), + "-Auto=0%-ISRe%-ISFc%-RTaut%-RFSub%-RBSub%-DocProof%-TimeLimit=60", + clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1))) +end +val thms_goals = ListPair.zip( thms, sg_terms) +val atp_list = make_atp_list thms_goals sign 1 +in + Watcher.callResProvers(childout,atp_list); + warning("Sent commands to watcher!"); + dummy_tac + end +(* + val axfile = (File.platform_path axiom_file) + val hypsfile = (File.platform_path hyps_file) + val clasimpfile = (File.platform_path clasimp_file) + val spass_home = getenv "SPASS_HOME" + val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int 1) + + val (clause_arr, num_of_clauses) = ResClasimp.write_out_clasimp_small (File.platform_path clasimp_file) ; + val (childin,childout,pid) = Watcher.createWatcher(mp, clause_arr, num_of_clauses); +Watcher.callResProvers(childout, [("spass", "thmstring", "goalstr", spass_home, "-DocProof", clasimpfile, axfile, hypsfile,probfile)]); + +Watcher.callResProvers(childout, [("spass", "thmstring", "goalstr", "/homes/clq20/spassshell", "", clasimpfile, axfile, hypsfile,probfile)]); + + +*) (**********************************************************) (* write out the current subgoal as a tptp file, probN, *) (* then call dummy_tac - should be call_res_tac *) (**********************************************************) -fun call_atp_tac_tfrees sign thms n tfrees sg_term (childin, childout,pid) = - ( - warning("in call_atp_tac_tfrees"); - tptp_inputs_tfrees (make_clauses thms) n tfrees; - call_resolve_tac sign thms sg_term (childin, childout, pid) n; - dummy_tac); - -fun atp_tac_tfrees tfrees sg_term (childin, childout,pid) n st = - let val sign = sign_of_thm st - val _ = warning ("in atp_tac_tfrees ") - val _ = warning ("sg_term :" ^ (Sign.string_of_term sign sg_term)) - in - SELECT_GOAL - (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, - METAHYPS(fn negs => (call_atp_tac_tfrees sign negs n tfrees sg_term - (childin, childout,pid) ))]) n st - end; - - -fun isar_atp_g tfrees sg_term (childin, childout, pid) n = - ((warning("in isar_atp_g")); - atp_tac_tfrees tfrees sg_term (childin, childout, pid) n); +fun get_sko_thms tfrees sign sg_terms (childin, childout,pid) thm n sko_thms = + if (equal n 0) then + (call_resolve_tac (rev sko_thms) sign sg_terms (childin, childout, pid) (List.length sg_terms);dummy_tac thm) + else + + ( SELECT_GOAL + (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, + METAHYPS(fn negs => (tptp_inputs_tfrees (make_clauses negs) n tfrees; + get_sko_thms tfrees sign sg_terms (childin, childout, pid) thm (n -1) (negs::sko_thms);dummy_tac))]) n thm ) @@ -246,24 +227,26 @@ (* in proof reconstruction *) (**********************************************) -fun isar_atp_goal' thm k n tfree_lits (childin, childout, pid) = - if (k > n) - then () - else - let val prems = prems_of thm - val sg_term = ReconOrderClauses.get_nth n prems - val thmstring = string_of_thm thm - in - (warning("in isar_atp_goal'")); - (warning("thmstring in isar_atp_goal': "^thmstring)); - isar_atp_g tfree_lits sg_term (childin, childout, pid) k thm; - isar_atp_goal' thm (k+1) n tfree_lits (childin, childout, pid) - end; +fun isar_atp_goal' thm n tfree_lits (childin, childout, pid) = + + (let val prems = prems_of thm + (*val sg_term = get_nth k prems*) + val sign = sign_of_thm thm + val thmstring = string_of_thm thm + in + + (warning("in isar_atp_goal'")); + (warning("thmstring in isar_atp_goal': "^thmstring)); + (* go and call callResProvers with this subgoal *) + (* isar_atp_g tfree_lits sg_term (childin, childout, pid) k thm; *) + (* recursive call to pick up the remaining subgoals *) + (* isar_atp_goal' thm (k+1) n tfree_lits (childin, childout, pid) *) + get_sko_thms tfree_lits sign prems (childin, childout, pid) thm n [] + end); - -fun isar_atp_goal thm n_subgoals tfree_lits (childin, childout, pid) = +(*fun isar_atp_goal thm n_subgoals tfree_lits (childin, childout, pid) = (if (!debug) then warning (string_of_thm thm) - else (isar_atp_goal' thm 1 n_subgoals tfree_lits (childin, childout, pid) )); + else (isar_atp_goal' thm n_subgoals tfree_lits (childin, childout, pid) ));*) (**************************************************) (* convert clauses from "assume" to conjecture. *) @@ -276,8 +259,9 @@ fun isar_atp_aux thms thm n_subgoals (childin, childout, pid) = let val tfree_lits = isar_atp_h thms - in warning("in isar_atp_aux"); - isar_atp_goal thm n_subgoals tfree_lits (childin, childout, pid) + in + (warning("in isar_atp_aux")); + isar_atp_goal' thm n_subgoals tfree_lits (childin, childout, pid) end; (******************************************************************) @@ -287,8 +271,9 @@ (* turns off xsymbol at start of function, restoring it at end *) (******************************************************************) (*FIX changed to clasimp_file *) -fun isar_atp' (ctxt, thms, thm) = - let val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"]))) +fun isar_atp' (ctxt,thms, thm) = + let + val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"]))) val _= (warning ("in isar_atp'")) val prems = prems_of thm val sign = sign_of_thm thm @@ -298,12 +283,11 @@ (* set up variables for writing out the clasimps to a tptp file *) val (clause_arr, num_of_clauses) = - ResClasimp.write_out_clasimp (File.platform_path clasimp_file) + ResClasimp.write_out_clasimp(*_small*) (File.platform_path clasimp_file) (ProofContext.theory_of ctxt) - val _ = warning ("clasimp_file is " ^ File.platform_path clasimp_file) + val _ = (warning ("clasimp_file is this: "^(File.platform_path clasimp_file)) ) (* cq: add write out clasimps to file *) - (* cq:create watcher and pass to isar_atp_aux *) (* tracing *) (*val tenth_ax = fst( Array.sub(clause_arr, 1)) @@ -324,7 +308,7 @@ (warning ("subgoals: "^prems_string)); (warning ("pid: "^ pidstring))); isar_atp_aux thms thm (length prems) (childin, childout, pid) ; - + (warning("turning xsymbol back on!")); print_mode := (["xsymbols", "symbols"] @ ! print_mode) end; @@ -343,6 +327,8 @@ safeEs @ safeIs @ hazEs @ hazIs end; + + fun append_name name [] _ = [] | append_name name (thm::thms) k = (Thm.name_thm ((name ^ "_" ^ (string_of_int k)),thm)) :: (append_name name thms (k+1)); @@ -352,6 +338,7 @@ thms'::(append_names names thmss) end; + fun get_thms_ss [] = [] | get_thms_ss thms = let val names = map Thm.name_of_thm thms @@ -361,6 +348,9 @@ ResLib.flat_noDup thms'' end; + + + in @@ -369,7 +359,7 @@ (* what about clasimpset - it should already be in the ax file - perhaps append to ax file rather than just *) (* write out ? Or keep as a separate file and then cat them all together in the watcher, like we do with the *) (*claset file and prob file*) -(* FIX: update to work with clausify_axiom_pairs now in ResAxioms*) +(* FIX*) (*fun isar_local_thms (delta_cs, delta_ss_thms) = let val thms_cs = get_thms_cs delta_cs val thms_ss = get_thms_ss delta_ss_thms @@ -383,6 +373,8 @@ *) + + (* called in Isar automatically *) fun isar_atp (ctxt,thm) = @@ -398,13 +390,15 @@ (warning ("initial thm in isar_atp: "^thmstring)); (warning ("subgoals in isar_atp: "^prems_string)); (warning ("number of subgoals in isar_atp: "^(string_of_int prem_no))); - ((*isar_local_thms (d_cs,d_ss_thms); *)(warning("about to call isar_atp'")); - isar_atp' (ctxt, prems, thm)) + (*isar_local_thms (d_cs,d_ss_thms);*) + isar_atp' (ctxt,prems, thm) end; end + + end; Proof.atp_hook := ResAtp.isar_atp;