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.
--- 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
--- 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 =(
--- 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;
--- 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
--- 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;
--- 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
--- 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;