--- a/src/HOL/Tools/ATP/AtpCommunication.ML Tue Mar 07 03:59:48 2006 +0100
+++ b/src/HOL/Tools/ATP/AtpCommunication.ML Tue Mar 07 04:01:25 2006 +0100
@@ -12,13 +12,13 @@
val reconstruct : bool ref
val checkEProofFound:
TextIO.instream * TextIO.outstream * Posix.Process.pid *
- string * (ResClause.clause * thm) Array.array -> bool
+ string * string Array.array -> bool
val checkVampProofFound:
TextIO.instream * TextIO.outstream * Posix.Process.pid *
- string * (ResClause.clause * thm) Array.array -> bool
+ string * string Array.array -> bool
val checkSpassProofFound:
TextIO.instream * TextIO.outstream * Posix.Process.pid *
- string * thm * int * (ResClause.clause * thm) Array.array -> bool
+ string * thm * int * string Array.array -> bool
val signal_parent:
TextIO.outstream * Posix.Process.pid * string * string -> unit
end;
@@ -64,7 +64,7 @@
(* and if so, transfer output to the input pipe of the main Isabelle process *)
(*********************************************************************************)
-fun startTransfer (endS, fromChild, toParent, ppid, probfile, clause_arr) =
+fun startTransfer (endS, fromChild, toParent, ppid, probfile, names_arr) =
let fun transferInput currentString =
let val thisLine = TextIO.inputLine fromChild
in
@@ -79,7 +79,7 @@
else Recon_Transfer.e_lemma_list
in
trace ("\nExtracted proof:\n" ^ proofextract);
- lemma_list proofextract probfile toParent ppid clause_arr
+ lemma_list proofextract probfile toParent ppid names_arr
end
else transferInput (currentString^thisLine)
end
@@ -99,25 +99,25 @@
OS.Process.sleep (Time.fromMilliseconds 600));
(*Called from watcher. Returns true if the Vampire process has returned a verdict.*)
-fun checkVampProofFound (fromChild, toParent, ppid, probfile, clause_arr) =
+fun checkVampProofFound (fromChild, toParent, ppid, probfile, names_arr) =
let val thisLine = TextIO.inputLine fromChild
in
trace thisLine;
if thisLine = ""
then (trace "\nNo proof output seen"; false)
else if String.isPrefix start_V8 thisLine
- then startTransfer (end_V8, fromChild, toParent, ppid, probfile, clause_arr)
+ then startTransfer (end_V8, fromChild, toParent, ppid, probfile, names_arr)
else if (String.isPrefix "Satisfiability detected" thisLine) orelse
(String.isPrefix "Refutation not found" thisLine)
then (signal_parent (toParent, ppid, "Failure\n", probfile);
true)
else
- checkVampProofFound (fromChild, toParent, ppid, probfile, clause_arr)
+ checkVampProofFound (fromChild, toParent, ppid, probfile, names_arr)
end
(*Called from watcher. Returns true if the E process has returned a verdict.*)
-fun checkEProofFound (fromChild, toParent, ppid, probfile, clause_arr) =
+fun checkEProofFound (fromChild, toParent, ppid, probfile, names_arr) =
let val thisLine = TextIO.inputLine fromChild
in
trace thisLine;
@@ -125,7 +125,7 @@
then (trace "\nNo proof output seen"; false)
else if String.isPrefix start_E thisLine
then
- startTransfer (end_E, fromChild, toParent, ppid, probfile, clause_arr)
+ startTransfer (end_E, fromChild, toParent, ppid, probfile, names_arr)
else if String.isPrefix "# Problem is satisfiable" thisLine
then (signal_parent (toParent, ppid, "Invalid\n", probfile);
true)
@@ -133,7 +133,7 @@
then (signal_parent (toParent, ppid, "Failure\n", probfile);
true)
else
- checkEProofFound (fromChild, toParent, ppid, probfile, clause_arr)
+ checkEProofFound (fromChild, toParent, ppid, probfile, names_arr)
end
@@ -143,16 +143,16 @@
(* steps as a string to the input pipe of the main Isabelle process *)
(**********************************************************************)
-fun spass_reconstruct_tac proofextract toParent ppid probfile sg_num clause_arr =
+fun spass_reconstruct_tac proofextract toParent ppid probfile sg_num names_arr =
SELECT_GOAL
(EVERY1 [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac,
METAHYPS(fn negs =>
Recon_Transfer.spass_reconstruct proofextract probfile
- toParent ppid negs clause_arr)]) sg_num;
+ toParent ppid negs names_arr)]) sg_num;
fun transferSpassInput (fromChild, toParent, ppid, probfile,
- currentString, thm, sg_num, clause_arr) =
+ currentString, thm, sg_num, names_arr) =
let val thisLine = TextIO.inputLine fromChild
in
trace thisLine;
@@ -166,12 +166,12 @@
trace ("\nextracted spass proof: " ^ proofextract);
if !reconstruct
then (spass_reconstruct_tac proofextract toParent ppid probfile sg_num
- clause_arr thm; ())
+ names_arr thm; ())
else Recon_Transfer.spass_lemma_list proofextract probfile toParent
- ppid clause_arr
+ ppid names_arr
end
else transferSpassInput (fromChild, toParent, ppid, probfile,
- (currentString^thisLine), thm, sg_num, clause_arr)
+ (currentString^thisLine), thm, sg_num, names_arr)
end;
@@ -182,29 +182,29 @@
fun startSpassTransfer (fromChild, toParent, ppid, probfile,
- thm, sg_num,clause_arr) =
+ thm, sg_num,names_arr) =
let val thisLine = TextIO.inputLine fromChild
in
if thisLine = "" then false
else if String.isPrefix "Here is a proof" thisLine then
(trace ("\nabout to transfer SPASS proof:\n");
transferSpassInput (fromChild, toParent, ppid, probfile, thisLine,
- thm, sg_num,clause_arr);
+ thm, sg_num,names_arr);
true) handle EOF => false
- else startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num,clause_arr)
+ else startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num,names_arr)
end
(*Called from watcher. Returns true if the SPASS process has returned a verdict.*)
fun checkSpassProofFound (fromChild, toParent, ppid, probfile,
- thm, sg_num, clause_arr) =
+ thm, sg_num, names_arr) =
let val thisLine = TextIO.inputLine fromChild
in
trace thisLine;
if thisLine = "" then (trace "\nNo proof output seen"; false)
else if thisLine = "SPASS beiseite: Proof found.\n"
then
- startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num, clause_arr)
+ startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num, names_arr)
else if thisLine = "SPASS beiseite: Completion found.\n"
then (signal_parent (toParent, ppid, "Invalid\n", probfile);
true)
@@ -212,7 +212,7 @@
thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n"
then (signal_parent (toParent, ppid, "Failure\n", probfile);
true)
- else checkSpassProofFound (fromChild, toParent, ppid, probfile, thm, sg_num, clause_arr)
+ else checkSpassProofFound (fromChild, toParent, ppid, probfile, thm, sg_num, names_arr)
end
end;
--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Tue Mar 07 03:59:48 2006 +0100
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Tue Mar 07 04:01:25 2006 +0100
@@ -149,17 +149,17 @@
(* retrieve the axioms that were obtained from the clasimpset *)
-fun get_clasimp_cls (clause_arr: (ResClause.clause * thm) array) step_nums =
- let val clasimp_nums = List.filter (is_clasimp_ax (Array.length clause_arr - 1))
+fun get_clasimp_cls (names_arr: string array) step_nums =
+ let val clasimp_nums = List.filter (is_clasimp_ax (Array.length names_arr - 1))
(map subone step_nums)
in
- map (fn x => Array.sub(clause_arr, x)) clasimp_nums
+ map (fn x => Array.sub(names_arr, x)) clasimp_nums
end
(* get names of clasimp axioms used*)
-fun get_axiom_names step_nums clause_arr =
+fun get_axiom_names step_nums names_arr =
sort_distinct string_ord
- (map (ResClause.get_axiomName o #1) (get_clasimp_cls clause_arr step_nums));
+ (get_clasimp_cls names_arr step_nums);
(*String contains multiple lines. We want those of the form
"253[0:Inp] et cetera..."
@@ -171,8 +171,8 @@
val lines = String.tokens (fn c => c = #"\n") proofstr
in List.mapPartial (inputno o toks) lines end
-fun get_axiom_names_spass proofstr clause_arr =
- get_axiom_names (get_spass_linenums proofstr) clause_arr;
+fun get_axiom_names_spass proofstr names_arr =
+ get_axiom_names (get_spass_linenums proofstr) names_arr;
(*String contains multiple lines.
A list consisting of the first number in each line is returned. *)
@@ -183,8 +183,8 @@
val lines = String.tokens (fn c => c = #"\n") proofstr
in List.mapPartial (firstno o numerics) lines end
-fun get_axiom_names_e proofstr clause_arr =
- get_axiom_names (get_linenums proofstr) clause_arr;
+fun get_axiom_names_e proofstr names_arr =
+ get_axiom_names (get_linenums proofstr) names_arr;
(*String contains multiple lines. We want those of the form
"*********** [448, input] ***********".
@@ -196,8 +196,8 @@
val lines = String.tokens (fn c => c = #"\n") proofstr
in List.mapPartial (inputno o toks) lines end
-fun get_axiom_names_vamp proofstr clause_arr =
- get_axiom_names (get_vamp_linenums proofstr) clause_arr;
+fun get_axiom_names_vamp proofstr names_arr =
+ get_axiom_names (get_vamp_linenums proofstr) names_arr;
(***********************************************)
@@ -212,7 +212,7 @@
fun addvars c (a,b) = (a,b,c)
-fun get_axioms_used proof_steps thms clause_arr =
+fun get_axioms_used proof_steps thms names_arr =
let val axioms = (List.filter is_axiom) proof_steps
val step_nums = get_step_nums axioms []
@@ -265,12 +265,12 @@
(*The signal handler in watcher.ML must be able to read the output of this.*)
-fun prover_lemma_list_aux getax proofstr probfile toParent ppid clause_arr =
+fun prover_lemma_list_aux getax proofstr probfile toParent ppid names_arr =
let val _ = trace
("\n\nGetting lemma names. proofstr is " ^ proofstr ^
"\nprobfile is " ^ probfile ^
- " num of clauses is " ^ string_of_int (Array.length clause_arr))
- val axiom_names = getax proofstr clause_arr
+ " num of clauses is " ^ string_of_int (Array.length names_arr))
+ val axiom_names = getax proofstr names_arr
val ax_str = rules_to_string axiom_names
in
trace ("\nDone. Lemma list is " ^ ax_str);
@@ -298,7 +298,7 @@
(**** Full proof reconstruction for SPASS (not really working) ****)
-fun spass_reconstruct proofstr probfile toParent ppid thms clause_arr =
+fun spass_reconstruct proofstr probfile toParent ppid thms names_arr =
let val _ = trace ("\nspass_reconstruct. Proofstr is "^proofstr)
val tokens = #1(lex proofstr)
@@ -315,7 +315,7 @@
(* 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 (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps thms clause_arr
+ val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps thms names_arr
(*val numcls_string = numclstr ( vars, numcls) ""*)
val _ = trace "\ngot axioms"
--- a/src/HOL/Tools/ATP/watcher.ML Tue Mar 07 03:59:48 2006 +0100
+++ b/src/HOL/Tools/ATP/watcher.ML Tue Mar 07 04:01:25 2006 +0100
@@ -23,7 +23,7 @@
(* Start a watcher and set up signal handlers *)
val createWatcher :
- thm * (ResClause.clause * thm) Array.array ->
+ thm * string Array.array ->
TextIO.instream * TextIO.outstream * Posix.Process.pid
val killWatcher : Posix.Process.pid -> unit
val setting_sep : char
@@ -206,7 +206,7 @@
Date.toString(Date.fromTimeLocal(Time.now())))
in execCmds cmds newProcList end
-fun checkChildren (th, clause_arr, toParentStr, children) =
+fun checkChildren (th, names_arr, toParentStr, children) =
let fun check [] = [] (* no children to check *)
| check (child::children) =
let val {prover, file, proc_handle, instr=childIn, ...} : cmdproc =
@@ -220,11 +220,11 @@
let val _ = trace ("\nInput available from child: " ^ file)
val childDone = (case prover of
"vampire" => AtpCommunication.checkVampProofFound
- (childIn, toParentStr, ppid, file, clause_arr)
+ (childIn, toParentStr, ppid, file, names_arr)
| "E" => AtpCommunication.checkEProofFound
- (childIn, toParentStr, ppid, file, clause_arr)
+ (childIn, toParentStr, ppid, file, names_arr)
| "spass" => AtpCommunication.checkSpassProofFound
- (childIn, toParentStr, ppid, file, th, sgno,clause_arr)
+ (childIn, toParentStr, ppid, file, th, sgno,names_arr)
| _ => (trace ("\nBad prover! " ^ prover); true) )
in
if childDone (*child has found a proof and transferred it*)
@@ -240,7 +240,7 @@
end;
-fun setupWatcher (th,clause_arr) =
+fun setupWatcher (th,names_arr) =
let
val p1 = Posix.IO.pipe() (*pipes for communication between parent and watcher*)
val p2 = Posix.IO.pipe()
@@ -277,16 +277,16 @@
if length procList < 40 then (* Execute locally *)
let val _ = trace("\nCommands from parent: " ^
Int.toString(length cmds))
- val newProcList' = checkChildren(th, clause_arr, toParentStr,
+ val newProcList' = checkChildren(th, names_arr, toParentStr,
execCmds cmds procList)
in trace "\nCommands executed"; keepWatching newProcList' end
else (* Execute remotely [FIXME: NOT REALLY] *)
- let val newProcList' = checkChildren (th, clause_arr, toParentStr,
+ let val newProcList' = checkChildren (th, names_arr, toParentStr,
execCmds cmds procList)
in keepWatching newProcList' end
| NONE => (* No new input from Isabelle *)
(trace "\nNothing from parent...";
- keepWatching(checkChildren(th, clause_arr, toParentStr, procList))))
+ keepWatching(checkChildren(th, names_arr, toParentStr, procList))))
handle exn => (*FIXME: exn handler is too general!*)
(trace ("\nkeepWatching exception handler: " ^ Toplevel.exn_message exn);
keepWatching procList);
@@ -344,8 +344,8 @@
fun prems_string_of th = space_implode "\n" (map string_of_cterm (cprems_of th))
-fun createWatcher (th, clause_arr) =
- let val {pid=childpid, instr=childin, outstr=childout} = setupWatcher (th,clause_arr)
+fun createWatcher (th, names_arr) =
+ let val {pid=childpid, instr=childin, outstr=childout} = setupWatcher (th,names_arr)
fun decr_watched() =
(goals_being_watched := !goals_being_watched - 1;
if !goals_being_watched = 0