--- a/src/HOL/Tools/ATP/SpassCommunication.ML Thu Sep 15 17:45:17 2005 +0200
+++ b/src/HOL/Tools/ATP/SpassCommunication.ML Thu Sep 15 17:46:00 2005 +0200
@@ -10,9 +10,9 @@
signature SPASS_COMM =
sig
val reconstruct : bool ref
- val getSpassInput : TextIO.instream -> string * string * string
+ val getSpassInput : TextIO.instream -> string * string
val checkSpassProofFound:
- TextIO.instream * TextIO.outstream * Posix.Process.pid * string *
+ TextIO.instream * TextIO.outstream * Posix.Process.pid *
string * string * thm * int * (ResClause.clause * thm) Array.array * int -> bool
end;
@@ -30,7 +30,7 @@
(* steps as a string to the input pipe of the main Isabelle process *)
(**********************************************************************)
-fun reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num
+fun reconstruct_tac proofextract goalstring toParent ppid sg_num
clause_arr num_of_clauses =
let val f = if !reconstruct then Recon_Transfer.spassString_to_reconString
else Recon_Transfer.spassString_to_lemmaString
@@ -38,12 +38,11 @@
SELECT_GOAL
(EVERY1 [rtac ccontr, ResLib.atomize_tac, skolemize_tac,
METAHYPS(fn negs =>
- f proofextract thmstring goalstring
- toParent ppid negs clause_arr num_of_clauses)]) sg_num
+ f proofextract goalstring toParent ppid negs clause_arr num_of_clauses)]) sg_num
end;
-fun transferSpassInput (fromChild, toParent, ppid,thmstring,goalstring,
+fun transferSpassInput (fromChild, toParent, ppid, goalstring,
currentString, thm, sg_num,clause_arr, num_of_clauses) =
let val thisLine = TextIO.inputLine fromChild
in
@@ -55,10 +54,10 @@
let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
in
File.write (File.tmp_path (Path.basic"spass_extracted_prf")) proofextract;
- reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num
+ reconstruct_tac proofextract goalstring toParent ppid sg_num
clause_arr num_of_clauses thm
end
- else transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,
+ else transferSpassInput (fromChild, toParent, ppid, goalstring,
(currentString^thisLine), thm, sg_num, clause_arr,
num_of_clauses)
end;
@@ -70,7 +69,7 @@
(*********************************************************************************)
-fun startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd,
+fun startSpassTransfer (fromChild, toParent, ppid, goalstring,childCmd,
thm, sg_num,clause_arr, num_of_clauses) =
let val thisLine = TextIO.inputLine fromChild
in
@@ -78,15 +77,15 @@
else if String.isPrefix "Here is a proof" thisLine then
(File.append (File.tmp_path (Path.basic "spass_transfer"))
("about to transfer proof, thm is: " ^ string_of_thm thm ^ "\n");
- transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,thisLine,
+ transferSpassInput (fromChild, toParent, ppid, goalstring,thisLine,
thm, sg_num,clause_arr, num_of_clauses);
true) handle EOF => false
- else startSpassTransfer (fromChild, toParent, ppid, thmstring, goalstring,
+ else startSpassTransfer (fromChild, toParent, ppid, goalstring,
childCmd, thm, sg_num,clause_arr, num_of_clauses)
end
-fun checkSpassProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd,
+fun checkSpassProofFound (fromChild, toParent, ppid, goalstring, childCmd,
thm, sg_num, clause_arr, (num_of_clauses:int )) =
let val spass_proof_file = TextIO.openAppend
(File.platform_path(File.tmp_path (Path.basic "spass_proof")))
@@ -101,7 +100,7 @@
else if thisLine = "SPASS beiseite: Proof found.\n"
then
(File.write (File.tmp_path (Path.basic "spass_response")) thisLine;
- startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,
+ startSpassTransfer (fromChild, toParent, ppid, goalstring,
childCmd, thm, sg_num, clause_arr, num_of_clauses))
else if thisLine = "SPASS beiseite: Completion found.\n"
then
@@ -113,7 +112,6 @@
TextIO.closeOut spass_proof_file;
TextIO.output (toParent, thisLine^"\n");
- TextIO.output (toParent, thmstring^"\n");
TextIO.output (toParent, goalstring^"\n");
TextIO.flushOut toParent;
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
@@ -124,7 +122,6 @@
then
(File.write (File.tmp_path (Path.basic "spass_response")) thisLine;
TextIO.output (toParent, thisLine^"\n");
- TextIO.output (toParent, thmstring^"\n");
TextIO.output (toParent, goalstring^"\n");
TextIO.flushOut toParent;
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
@@ -144,7 +141,7 @@
else
(TextIO.output (spass_proof_file, thisLine);
TextIO.flushOut spass_proof_file;
- checkSpassProofFound (fromChild, toParent, ppid, thmstring,goalstring,
+ checkSpassProofFound (fromChild, toParent, ppid, goalstring,
childCmd, thm, sg_num, clause_arr, num_of_clauses))
end
@@ -157,22 +154,20 @@
let val thisLine = TextIO.inputLine instr
val _ = File.write (File.tmp_path (Path.basic "spass_line")) thisLine
in
- if thisLine = "" then ("No output from reconstruction process.\n","","")
+ if thisLine = "" then ("No output from reconstruction process.\n","")
else if String.sub (thisLine, 0) = #"[" orelse
String.isPrefix "SPASS beiseite:" thisLine orelse
String.isPrefix "Rules from" thisLine
then
- let val thmstring = TextIO.inputLine instr
- val goalstring = TextIO.inputLine instr
- in (thisLine, thmstring, goalstring) end
+ let val goalstring = TextIO.inputLine instr
+ in (thisLine, goalstring) end
else if substring (thisLine,0,5) = "Proof" orelse
String.sub (thisLine, 0) = #"%"
then
- let val thmstring = TextIO.inputLine instr
- val goalstring = TextIO.inputLine instr
+ let val goalstring = TextIO.inputLine instr
in
File.write (File.tmp_path (Path.basic "getSpassInput")) thisLine;
- (thisLine, thmstring, goalstring)
+ (thisLine, goalstring)
end
else getSpassInput instr
end
--- a/src/HOL/Tools/ATP/VampCommunication.ML Thu Sep 15 17:45:17 2005 +0200
+++ b/src/HOL/Tools/ATP/VampCommunication.ML Thu Sep 15 17:46:00 2005 +0200
@@ -9,14 +9,14 @@
(***************************************************************************)
signature VAMP_COMM =
sig
- val getEInput : TextIO.instream -> string * string * string
+ val getEInput : TextIO.instream -> string * string
val checkEProofFound:
- TextIO.instream * TextIO.outstream * Posix.Process.pid * string *
+ TextIO.instream * TextIO.outstream * Posix.Process.pid *
string * string * thm * int * (ResClause.clause * thm) Array.array * int -> bool
- val getVampInput : TextIO.instream -> string * string * string
+ val getVampInput : TextIO.instream -> string * string
val checkVampProofFound:
- TextIO.instream * TextIO.outstream * Posix.Process.pid * string *
+ TextIO.instream * TextIO.outstream * Posix.Process.pid *
string * string * thm * int * (ResClause.clause * thm) Array.array * int -> bool
end;
@@ -31,13 +31,13 @@
(* steps as a string to the input pipe of the main Isabelle process *)
(**********************************************************************)
-fun reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num
+fun reconstruct_tac proofextract goalstring toParent ppid sg_num
clause_arr num_of_clauses =
SELECT_GOAL
(EVERY1
[rtac ccontr, ResLib.atomize_tac, skolemize_tac,
METAHYPS(fn negs =>
- (Recon_Transfer.proverString_to_lemmaString proofextract thmstring
+ (Recon_Transfer.proverString_to_lemmaString proofextract
goalstring toParent ppid negs clause_arr num_of_clauses))]) sg_num
@@ -47,7 +47,7 @@
(*********************************************************************************)
fun startTransfer (startS,endS)
- (fromChild, toParent, ppid, thmstring,goalstring,childCmd,
+ (fromChild, toParent, ppid, goalstring,childCmd,
thm, sg_num,clause_arr, num_of_clauses) =
let val thisLine = TextIO.inputLine fromChild
fun transferInput currentString =
@@ -63,7 +63,7 @@
then let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
in
File.write (File.tmp_path (Path.basic"extracted_prf")) proofextract;
- reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num
+ reconstruct_tac proofextract goalstring toParent ppid sg_num
clause_arr num_of_clauses thm
end
else transferInput (currentString^thisLine)
@@ -78,12 +78,12 @@
true) handle EOF => false
else
startTransfer (startS,endS)
- (fromChild, toParent, ppid, thmstring, goalstring,
+ (fromChild, toParent, ppid, goalstring,
childCmd, thm, sg_num,clause_arr, num_of_clauses)
end
-fun checkVampProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd,
+fun checkVampProofFound (fromChild, toParent, ppid, goalstring, childCmd,
thm, sg_num, clause_arr, num_of_clauses) =
let val proof_file = TextIO.openAppend
(File.platform_path(File.tmp_path (Path.basic "atp_proof")))
@@ -99,7 +99,7 @@
then
(File.write (File.tmp_path (Path.basic "atp_response")) thisLine;
startTransfer (Recon_Parse.start_V6, Recon_Parse.end_V6)
- (fromChild, toParent, ppid, thmstring, goalstring,
+ (fromChild, toParent, ppid, goalstring,
childCmd, thm, sg_num, clause_arr, num_of_clauses))
else if (thisLine = "% Unprovable.\n" ) orelse
(thisLine = "% Proof not found. Time limit expired.\n")
@@ -111,7 +111,6 @@
TextIO.closeOut proof_file;
TextIO.output (toParent, thisLine^"\n");
- TextIO.output (toParent, thmstring^"\n");
TextIO.output (toParent, goalstring^"\n");
TextIO.flushOut toParent;
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
@@ -121,16 +120,16 @@
else
(TextIO.output (proof_file, thisLine);
TextIO.flushOut proof_file;
- checkVampProofFound (fromChild, toParent, ppid, thmstring,
+ checkVampProofFound (fromChild, toParent, ppid,
goalstring,childCmd, thm, sg_num, clause_arr, num_of_clauses))
end
-fun checkEProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd,
+fun checkEProofFound (fromChild, toParent, ppid,goalstring, childCmd,
thm, sg_num, clause_arr, num_of_clauses) =
let val E_proof_file = TextIO.openAppend
- (File.platform_path(File.tmp_path (Path.basic "eprover_proof")))
- val _ = File.write (File.tmp_path (Path.basic "eprover_checking_prf"))
+ (File.platform_path(File.tmp_path (Path.basic "atp_proof")))
+ val _ = File.write (File.tmp_path (Path.basic "atp_checking_prf"))
("checking if proof found, thm is: " ^ string_of_thm thm)
val thisLine = TextIO.inputLine fromChild
in
@@ -140,20 +139,19 @@
false)
else if thisLine = "# TSTP exit status: Unsatisfiable\n"
then
- (File.write (File.tmp_path (Path.basic "eprover_response")) thisLine;
+ (File.write (File.tmp_path (Path.basic "atp_response")) thisLine;
startTransfer (Recon_Parse.start_E, Recon_Parse.end_E)
- (fromChild, toParent, ppid, thmstring, goalstring,
+ (fromChild, toParent, ppid, goalstring,
childCmd, thm, sg_num, clause_arr, num_of_clauses))
else if thisLine= "# Problem is satisfiable (or invalid), generating saturation derivation\n"
then
- (File.write (File.tmp_path (Path.basic "eprover_response")) thisLine;
+ (File.write (File.tmp_path (Path.basic "atp_response")) thisLine;
TextIO.output (toParent,childCmd^"\n" );
TextIO.flushOut toParent;
TextIO.output (E_proof_file, thisLine);
TextIO.closeOut E_proof_file;
TextIO.output (toParent, thisLine^"\n");
- TextIO.output (toParent, thmstring^"\n");
TextIO.output (toParent, goalstring^"\n");
TextIO.flushOut toParent;
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
@@ -162,9 +160,8 @@
true)
else if thisLine = "# Failure: Resource limit exceeded (time)\n"
then
- (File.write (File.tmp_path (Path.basic "eprover_response")) thisLine;
+ (File.write (File.tmp_path (Path.basic "atp_response")) thisLine;
TextIO.output (toParent, thisLine^"\n");
- TextIO.output (toParent, thmstring^"\n");
TextIO.output (toParent, goalstring^"\n");
TextIO.flushOut toParent;
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
@@ -184,7 +181,7 @@
else
(TextIO.output (E_proof_file, thisLine);
TextIO.flushOut E_proof_file;
- checkEProofFound (fromChild, toParent, ppid, thmstring,goalstring,
+ checkEProofFound (fromChild, toParent, ppid, goalstring,
childCmd, thm, sg_num, clause_arr, num_of_clauses))
end
@@ -197,21 +194,19 @@
let val thisLine = TextIO.inputLine instr
val _ = File.write (File.tmp_path (Path.basic "atp_line")) thisLine
in (* reconstructed proof string *)
- if thisLine = "" then ("No output from reconstruction process.\n","","")
+ if thisLine = "" then ("No output from reconstruction process.\n","")
else if String.sub (thisLine, 0) = #"[" orelse
thisLine = "% Unprovable.\n" orelse
thisLine ="% Proof not found. Time limit expired.\n" orelse
String.isPrefix "Rules from" thisLine
then
- let val thmstring = TextIO.inputLine instr
- val goalstring = TextIO.inputLine instr
- in (thisLine, thmstring, goalstring) end
+ let val goalstring = TextIO.inputLine instr
+ in (thisLine, goalstring) end
else if thisLine = "Proof found but translation failed!"
then
- let val thmstring = TextIO.inputLine instr
- val goalstring = TextIO.inputLine instr
+ let val goalstring = TextIO.inputLine instr
val _ = debug "getVampInput: translation of proof failed"
- in (thisLine, thmstring, goalstring) end
+ in (thisLine, goalstring) end
else getVampInput instr
end
@@ -224,20 +219,18 @@
let val thisLine = TextIO.inputLine instr
val _ = File.write (File.tmp_path (Path.basic "atp_line")) thisLine
in (* reconstructed proof string *)
- if thisLine = "" then ("No output from reconstruction process.\n","","")
+ if thisLine = "" then ("No output from reconstruction process.\n","")
else if String.isPrefix "# Problem is satisfiable" thisLine orelse
String.isPrefix "# Cannot determine problem status" thisLine orelse
String.isPrefix "# Failure:" thisLine
then
- let val thmstring = TextIO.inputLine instr
- val goalstring = TextIO.inputLine instr
- in (thisLine, thmstring, goalstring) end
+ let val goalstring = TextIO.inputLine instr
+ in (thisLine, goalstring) end
else if thisLine = "Proof found but translation failed!"
then
- let val thmstring = TextIO.inputLine instr
- val goalstring = TextIO.inputLine instr
+ let val goalstring = TextIO.inputLine instr
val _ = debug "getEInput: translation of proof failed"
- in (thisLine, thmstring, goalstring) end
+ in (thisLine, goalstring) end
else getEInput instr
end
--- a/src/HOL/Tools/ATP/recon_parse.ML Thu Sep 15 17:45:17 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_parse.ML Thu Sep 15 17:46:00 2005 +0200
@@ -118,6 +118,8 @@
val end_E = "# Proof object ends here."
val start_V6 = "%================== Proof: ======================"
val end_V6 = "%============== End of proof. =================="
+val start_V8 = "=========== Refutation =========="
+val end_V8 = "======= End of refutation ======="
(*Identifies the start/end lines of an ATP's output*)
--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Thu Sep 15 17:45:17 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Thu Sep 15 17:46:00 2005 +0200
@@ -134,9 +134,6 @@
(*Flattens a list of list of strings to one string*)
fun onestr ls = String.concat (map String.concat ls);
-fun thmstrings [] str = str
-| thmstrings (x::xs) str = thmstrings xs (str^(string_of_thm x))
-
fun is_clasimp_ax clasimp_num n = n <= clasimp_num
fun subone x = x - 1
@@ -268,10 +265,9 @@
val restore_linebreaks = subst_for #"\t" #"\n";
-fun proverString_to_lemmaString_aux proofstr thmstring goalstring toParent ppid thms clause_arr num_of_clauses getax =
- let val _ = File.append(File.tmp_path (Path.basic "thmstringfile"))
- ("thmstring is " ^ thmstring ^
- "\nproofstr is " ^ proofstr ^
+fun proverString_to_lemmaString_aux proofstr goalstring toParent ppid thms clause_arr num_of_clauses getax =
+ let val _ = File.append(File.tmp_path (Path.basic "spass_lemmastring"))
+ ("proofstr is " ^ proofstr ^
"\ngoalstr is " ^ goalstring ^
"\nnum of clauses is " ^ string_of_int num_of_clauses)
@@ -279,11 +275,10 @@
val ax_str = "Rules from clasimpset used in automatic proof: " ^
rules_to_string axiom_names
in
- File.append(File.tmp_path (Path.basic "reconstrfile"))
+ File.append(File.tmp_path (Path.basic "spass_lemmastring"))
("reconstring is: "^ax_str^" "^goalstring);
TextIO.output (toParent, ax_str^"\n");
TextIO.output (toParent, "goalstring: "^goalstring^"\n");
- TextIO.output (toParent, "thmstring: "^thmstring^"\n");
TextIO.flushOut toParent;
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
@@ -294,29 +289,28 @@
(File.write(File.tmp_path (Path.basic "proverString_handler")) "In exception handler";
TextIO.output (toParent, "Proof found but translation failed : " ^
remove_linebreaks proofstr ^ "\n");
- TextIO.output (toParent, remove_linebreaks thmstring ^ "\n");
TextIO.output (toParent, remove_linebreaks 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); all_tac);
-fun proverString_to_lemmaString proofstr thmstring goalstring toParent ppid thms
+fun proverString_to_lemmaString proofstr goalstring toParent ppid thms
clause_arr num_of_clauses =
- proverString_to_lemmaString_aux proofstr thmstring goalstring toParent ppid thms
+ proverString_to_lemmaString_aux proofstr goalstring toParent ppid thms
clause_arr num_of_clauses get_axiom_names_vamp_E;
-fun spassString_to_lemmaString proofstr thmstring goalstring toParent ppid thms
+fun spassString_to_lemmaString proofstr goalstring toParent ppid thms
clause_arr num_of_clauses =
- proverString_to_lemmaString_aux proofstr thmstring goalstring toParent ppid thms
+ proverString_to_lemmaString_aux proofstr goalstring toParent ppid thms
clause_arr num_of_clauses get_axiom_names_spass;
(**** Full proof reconstruction for SPASS (not really working) ****)
-fun spassString_to_reconString proofstr thmstring goalstring toParent ppid thms clause_arr num_of_clauses =
- let val _ = File.write(File.tmp_path (Path.basic "thmstringfile"))
- (" thmstring is: "^thmstring^"proofstr is: "^proofstr)
+fun spassString_to_reconString proofstr goalstring toParent ppid thms clause_arr num_of_clauses =
+ let val _ = File.write(File.tmp_path (Path.basic "spass_reconstruction"))
+ ("proofstr is: "^proofstr)
val tokens = #1(lex proofstr)
(***********************************)
@@ -324,11 +318,9 @@
(***********************************)
val proof_steps = parse tokens
- val _ = File.write (File.tmp_path (Path.basic "foo_parse"))
+ val _ = File.append (File.tmp_path (Path.basic "spass_reconstruction"))
("Did parsing on "^proofstr)
- val _ = File.write (File.tmp_path (Path.basic "foo_thmstring_at_parse"))
- ("Parsing for thmstring: "^thmstring)
(************************************)
(* recreate original subgoal as thm *)
(************************************)
@@ -340,16 +332,16 @@
val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps thms clause_arr num_of_clauses
(*val numcls_string = numclstr ( vars, numcls) ""*)
- val _ = File.write (File.tmp_path (Path.basic "foo_axiom")) "got axioms"
+ val _ = File.append (File.tmp_path (Path.basic "spass_reconstruction")) "got axioms"
(************************************)
(* translate proof *)
(************************************)
- val _ = File.write (File.tmp_path (Path.basic "foo_steps"))
+ val _ = File.append (File.tmp_path (Path.basic "spass_reconstruction"))
("about to translate proof, steps: "
^(init_proofsteps_to_string proof_steps ""))
val (newthm,proof) = translate_proof numcls proof_steps vars
- val _ = File.write (File.tmp_path (Path.basic "foo_steps2"))
+ val _ = File.append (File.tmp_path (Path.basic "spass_reconstruction"))
("translated proof, steps: "^(init_proofsteps_to_string proof_steps ""))
(***************************************************)
(* transfer necessary steps as strings to Isabelle *)
@@ -372,9 +364,6 @@
val reconstr = (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr)
in
TextIO.output (toParent, reconstr^"\n");
- TextIO.flushOut toParent;
- TextIO.output (toParent, thmstring^"\n");
- TextIO.flushOut toParent;
TextIO.output (toParent, goalstring^"\n");
TextIO.flushOut toParent;
@@ -383,19 +372,14 @@
Posix.Process.sleep(Time.fromSeconds 1) ; all_tac
end
handle _ =>
- let val _ = File.write(File.tmp_path (Path.basic "foo_handler")) "In exception handler"
- in
- TextIO.output (toParent,"Proof found but translation failed for resolution proof:"^(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); all_tac
- end
-
+ (File.append(File.tmp_path (Path.basic "spass_reconstruction")) "In exception handler";
+ TextIO.output (toParent,"Proof found but translation failed for resolution proof:"^
+ (remove_linebreaks proofstr) ^"\n");
+ 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); all_tac)
(**********************************************************************************)
(* At other end, want to turn back into datatype so can apply reconstruct_proof. *)
--- a/src/HOL/Tools/ATP/watcher.ML Thu Sep 15 17:45:17 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML Thu Sep 15 17:46:00 2005 +0200
@@ -23,7 +23,7 @@
(*****************************************************************************************)
val callResProvers :
- TextIO.outstream * (string*string*string*string*string*string*string*string) list
+ TextIO.outstream * (string*string*string*string*string) list
-> unit
(************************************************************************)
@@ -73,7 +73,6 @@
datatype cmdproc = CMDPROC of {
prover: string, (* Name of the resolution prover used, e.g. Vampire, SPASS *)
cmd: string, (* The file containing the goal for res prover to prove *)
- thmstring: string, (* string representation of subgoal after negation, skolemization*)
goalstring: string, (* string representation of subgoal*)
proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc,
instr : TextIO.instream, (* Input stream to child process *)
@@ -123,19 +122,16 @@
fun cmdInStream (CMDPROC{instr,outstr,...}) = instr;
-fun cmdchildInfo (CMDPROC{prover,cmd,thmstring,proc_handle,goalstring,instr,outstr}) =
+fun cmdchildInfo (CMDPROC{prover,cmd,proc_handle,goalstring,instr,outstr}) =
(prover,(cmd, (instr,outstr)));
-fun cmdchildHandle (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr}) =
+fun cmdchildHandle (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr}) =
proc_handle;
-fun cmdProver (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr}) =
+fun cmdProver (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr}) =
prover;
-fun cmdThm (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr}) =
- thmstring;
-
-fun cmdGoal (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr}) =
+fun cmdGoal (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr}) =
goalstring;
@@ -166,14 +162,14 @@
fun callResProvers (toWatcherStr, []) =
(TextIO.output (toWatcherStr, "End of calls\n"); TextIO.flushOut toWatcherStr)
| callResProvers (toWatcherStr,
- (prover,thmstring,goalstring, proverCmd,settings,
- axfile, hypsfile,probfile) :: args) =
+ (prover,goalstring, proverCmd,settings,
+ probfile) :: args) =
let val _ = File.write (File.tmp_path (Path.basic "tog_comms"))
- (prover^thmstring^goalstring^proverCmd^settings^
- hypsfile^probfile)
+ (prover^goalstring^proverCmd^settings^
+ probfile)
in TextIO.output (toWatcherStr,
- (prover^"$"^thmstring^"$"^goalstring^"$"^proverCmd^"$"^
- settings^"$"^hypsfile^"$"^probfile^"\n"));
+ (prover^"$"^goalstring^"$"^proverCmd^"$"^
+ settings^"$"^probfile^"\n"));
goals_being_watched := (!goals_being_watched) + 1;
TextIO.flushOut toWatcherStr;
callResProvers (toWatcherStr,args)
@@ -198,68 +194,52 @@
fun separateFields str =
let val _ = File.append (File.tmp_path (Path.basic "sep_field"))
("In separateFields, str is: " ^ str ^ "\n\n")
- val [prover,thmstring,goalstring,proverCmd,settingstr,hypsfile,probfile] =
+ val [prover,goalstring,proverCmd,settingstr,probfile] =
String.tokens (fn c => c = #"$") str
val settings = String.tokens (fn c => c = #"%") settingstr
val _ = File.append (File.tmp_path (Path.basic "sep_comms"))
("Sep comms are: "^ str ^"**"^
- prover^" thmstring: "^thmstring^"\n goalstr: "^goalstring^
- " \n provercmd: "^proverCmd^
- " \n hyps "^hypsfile^"\n prob "^probfile^"\n\n")
+ prover^" goalstr: "^goalstring^
+ "\n provercmd: "^proverCmd^
+ "\n prob "^probfile^"\n\n")
in
- (prover,thmstring,goalstring, proverCmd, settings, hypsfile, probfile)
+ (prover,goalstring, proverCmd, settings, probfile)
end
-
-fun formatCmd (prover,thmstring,goalstring, proverCmd, settings, hypsfile ,probfile) =
- let
- val _ = File.append (File.tmp_path (Path.basic"thmstring_in_watcher"))
- (thmstring ^ "\n goals_watched" ^
- (string_of_int(!goals_being_watched)) ^ probfile^"\n")
- in
- (prover, thmstring, goalstring, proverCmd, settings, probfile)
- end;
-
val remove_newlines = String.translate (fn c => if c = #"\n" then "" else str c);
fun getCmd cmdStr =
let val cmdStr' = remove_newlines cmdStr
in
File.write (File.tmp_path (Path.basic"sepfields_call"))
- ("about to call sepfields with " ^ cmdStr');
- formatCmd (separateFields cmdStr')
+ ("about to call separateFields with " ^ cmdStr');
+ separateFields cmdStr'
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
val _ = File.append (File.tmp_path (Path.basic "parent_comms")) thisLine
in
- if (thisLine = "End of calls\n")
- then cmdList
- else if (thisLine = "Kill children\n")
+ 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)
+ (("","","Kill children",[],"")::cmdList)
)
- else let val thisCmd = getCmd thisLine
+ else let val thisCmd = getCmd thisLine
(*********************************************************)
- (* thisCmd = (prover,thmstring,proverCmd, settings, file)*)
+ (* thisCmd = (prover,proverCmd, settings, file)*)
(* i.e. put back into tuple format *)
(*********************************************************)
in
(*TextIO.output (toParentStr, thisCmd);
TextIO.flushOut toParentStr;*)
- getCmds (toParentStr, fromParentStr, (thisCmd::cmdList))
+ getCmds (toParentStr, fromParentStr, thisCmd::cmdList)
end
end
@@ -286,6 +266,8 @@
(* Set up a Watcher Process *)
(*************************************)
+fun getProofCmd (a,c,d,e,f) = d
+
fun setupWatcher (thm,clause_arr, num_of_clauses) =
let
(** pipes for communication between parent and watcher **)
@@ -405,25 +387,24 @@
("finished polling child \n")
val parentID = Posix.ProcEnv.getppid()
val prover = cmdProver childProc
- val thmstring = cmdThm childProc
val sign = sign_of_thm thm
val prems = prems_of thm
val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems)
val _ = debug("subgoals forked to checkChildren: "^prems_string)
val goalstring = cmdGoal childProc
val _ = File.append (File.tmp_path (Path.basic "child_comms"))
- (prover^thmstring^goalstring^childCmd^"\n")
+ (prover^goalstring^childCmd^"\n")
in
if isSome childIncoming
then
(* check here for prover label on child*)
let val _ = File.write (File.tmp_path (Path.basic "child_incoming"))
("subgoals forked to checkChildren:"^
- prems_string^prover^thmstring^goalstring^childCmd)
+ prems_string^prover^goalstring^childCmd)
val childDone = (case prover of
- "vampire" => VampComm.checkVampProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)
- | "E" => VampComm.checkEProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)
- |"spass" => SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) )
+ "vampire" => VampComm.checkVampProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)
+ | "E" => VampComm.checkEProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)
+ |"spass" => SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) )
in
if childDone (**********************************************)
then (* child has found a proof and transferred it *)
@@ -453,7 +434,7 @@
(*** add subgoal id num to this *)
fun execCmds [] procList = procList
- | execCmds ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList =
+ | execCmds ((prover, goalstring,proverCmd,settings,file)::cmds) procList =
let val _ = File.write (File.tmp_path (Path.basic "exec_child"))
(space_implode "\n"
(["About to execute command for goal:",
@@ -466,7 +447,6 @@
val newProcList = (CMDPROC{
prover = prover,
cmd = file,
- thmstring = thmstring,
goalstring = goalstring,
proc_handle = childhandle,
instr = instr,
@@ -488,11 +468,11 @@
(****************************************)
(* fun execRemoteCmds [] procList = procList
- | execRemoteCmds ((prover, thmstring,goalstring,proverCmd ,settings,file)::cmds) procList =
- let val newProcList = mySshExecuteToList ("/usr/bin/ssh",([prover,thmstring,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
- in
- execRemoteCmds cmds newProcList
- end
+ | execRemoteCmds ((prover, goalstring,proverCmd ,settings,file)::cmds) procList =
+ let val newProcList = mySshExecuteToList ("/usr/bin/ssh",([prover,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
+ in
+ execRemoteCmds cmds newProcList
+ end
*)
(**********************************************)
@@ -648,11 +628,11 @@
(Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
VampComm.getVampInput childin; Pretty.writeln(Pretty.str (oct_char "361")))
fun spass_proofHandler n = (
- let val _ = File.append (File.tmp_path (Path.basic "spass_signal_in"))
+ let val _ = File.append (File.tmp_path (Path.basic "spass_signal"))
"Starting SPASS signal handler\n"
- val (reconstr, goalstring, thmstring) = SpassComm.getSpassInput childin
- val _ = File.append (File.tmp_path (Path.basic "spass_signal_out"))
- ("In SPASS signal handler "^reconstr^thmstring^goalstring^
+ val (reconstr, goalstring) = SpassComm.getSpassInput childin
+ val _ = File.append (File.tmp_path (Path.basic "spass_signal"))
+ ("In SPASS signal handler "^reconstr^goalstring^
"goals_being_watched: "^ string_of_int (!goals_being_watched))
in (* if a proof has been found and sent back as a reconstruction proof *)
if substring (reconstr, 0,1) = "["
--- a/src/HOL/Tools/res_atp.ML Thu Sep 15 17:45:17 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML Thu Sep 15 17:46:00 2005 +0200
@@ -7,7 +7,6 @@
signature RES_ATP =
sig
- val axiom_file : Path.T
val prover: string ref
val custom_spass: string list ref
val hook_count: int ref
@@ -27,8 +26,6 @@
ref ["Auto=0","-FullRed=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub",
"-DocProof","-TimeLimit=60"];
-val axiom_file = File.tmp_path (Path.basic "axioms");
-val hyps_file = File.tmp_path (Path.basic "hyps");
val prob_file = File.tmp_path (Path.basic "prob");
@@ -58,42 +55,18 @@
(*********************************************************************)
-(* convert clauses from "assume" to conjecture. write to file "hyps" *)
-(* hypotheses of the goal currently being proved *)
-(*********************************************************************)
-(*perhaps have 2 different versions of this, depending on whether or not spass is set *)
-fun isar_atp_h thms =
- let val prems = map (skolemize o make_nnf o ObjectLogic.atomize_thm) thms
- val prems' = map repeat_someI_ex prems
- val prems'' = make_clauses prems'
- val prems''' = ResAxioms.rm_Eps [] prems''
- val clss = map ResClause.make_conjecture_clause prems'''
- val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss)
- val tfree_lits = ResLib.flat_noDup tfree_litss
- (* tfree clause is different in tptp and dfg versions *)
- val tfree_clss = map ResClause.tfree_clause tfree_lits
- val hypsfile = File.platform_path hyps_file
- val out = TextIO.openOut(hypsfile)
- in
- ResLib.writeln_strs out (tfree_clss @ tptp_clss);
- TextIO.closeOut out; debug hypsfile;
- tfree_lits
- end;
-
-
-(*********************************************************************)
(* write out a subgoal as tptp clauses to the file "probN" *)
(* where N is the number of this subgoal *)
(*********************************************************************)
-fun tptp_inputs_tfrees thms n tfrees axclauses =
+fun tptp_inputs_tfrees thms n axclauses =
let
val _ = debug ("in tptp_inputs_tfrees 0")
val clss = map (ResClause.make_conjecture_clause_thm) thms
val _ = debug ("in tptp_inputs_tfrees 1")
val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss)
val _ = debug ("in tptp_inputs_tfrees 2")
- val tfree_clss = map ResClause.tfree_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees)
+ val tfree_clss = map ResClause.tfree_clause (ResLib.flat_noDup tfree_litss)
val _ = debug ("in tptp_inputs_tfrees 3")
val probfile = File.platform_path prob_file ^ "_" ^ string_of_int n
val out = TextIO.openOut(probfile)
@@ -110,14 +83,12 @@
(* where N is the number of this subgoal *)
(*********************************************************************)
-fun dfg_inputs_tfrees thms n tfrees axclauses =
+fun dfg_inputs_tfrees thms n axclauses =
let val clss = map (ResClause.make_conjecture_clause_thm) thms
val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
val _ = debug ("about to write out dfg prob file " ^ probfile)
- (*val (dfg_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2dfg clss)
- val tfree_clss = map ResClause.tfree_dfg_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees) *)
val probN = ResClause.clauses2dfg clss ("prob" ^ (string_of_int n))
- axclauses [] [] [] tfrees
+ axclauses [] [] []
val out = TextIO.openOut(probfile)
in
(ResLib.writeln_strs out [probN]; TextIO.closeOut out; debug probfile )
@@ -129,23 +100,16 @@
(* call prover with settings and problem file for the current subgoal *)
(*********************************************************************)
(* now passing in list of skolemized thms and list of sgterms to go with them *)
-fun call_resolve_tac (thms: thm list list) sign (sg_terms: term list) (childin, childout,pid) n =
+fun watcher_call_provers sign sg_terms (childin, childout,pid) =
let
- val axfile = (File.platform_path axiom_file)
-
- val hypsfile = (File.platform_path hyps_file)
-
- fun make_atp_list [] sign n = []
- | make_atp_list ((sko_thm, sg_term)::xs) sign n =
+ fun make_atp_list [] n = []
+ | make_atp_list ((sg_term)::xs) n =
let
- val thmstr = proofstring (Meson.concat_with_and (map string_of_thm sko_thm))
- val _ = debug ("thmstring in make_atp_lists is " ^ thmstr)
-
val goalstring = proofstring (Sign.string_of_term sign sg_term)
val _ = debug ("goalstring in make_atp_lists is " ^ goalstring)
val probfile = File.platform_path prob_file ^ "_" ^ (string_of_int n)
- val _ = debug ("prob file in call_resolve_tac is " ^ probfile)
+ val _ = debug ("prob file in watcher_call_provers is " ^ probfile)
in
(*Avoid command arguments containing spaces: Poly/ML and SML/NJ
versions of Unix.execute treat them differently!*)
@@ -161,93 +125,60 @@
val _ = ResLib.helper_path "SPASS_HOME" "SPASS"
(*We've checked that SPASS is there for ATP/spassshell to run.*)
in
- ([("spass", thmstr, goalstring,
+ ([("spass", goalstring,
getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell",
- optionline, axfile, hypsfile, probfile)] @
- (make_atp_list xs sign (n+1)))
+ optionline, probfile)] @
+ (make_atp_list xs (n+1)))
end
else if !prover = "vampire"
then
let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel"
in
- ([("vampire", thmstr, goalstring, vampire, "-t60%-m100000",
- axfile, hypsfile, probfile)] @
- (make_atp_list xs sign (n+1)))
+ ([("vampire", goalstring, vampire, "-t60%-m100000",
+ probfile)] @
+ (make_atp_list xs (n+1)))
end
else if !prover = "E"
then
let val Eprover = ResLib.helper_path "E_HOME" "eproof"
in
- ([("E", thmstr, goalstring, Eprover,
+ ([("E", goalstring, Eprover,
"--tptp-in%-l5%-xAuto%-tAuto%--soft-cpu-limit=60",
- axfile, hypsfile, probfile)] @
- (make_atp_list xs sign (n+1)))
+ probfile)] @
+ (make_atp_list xs (n+1)))
end
else error ("Invalid prover name: " ^ !prover)
end
- val atp_list = make_atp_list (ListPair.zip (thms, sg_terms)) sign 1
+ val atp_list = make_atp_list sg_terms 1
in
Watcher.callResProvers(childout,atp_list);
- debug "Sent commands to watcher!";
- all_tac
+ debug "Sent commands to watcher!"
end
-(**********************************************************)
-(* write out the current subgoal as a tptp file, probN, *)
-(* then call all_tac - should be call_res_tac *)
-(**********************************************************)
-
-
-fun get_sko_thms tfrees sign sg_terms (childin, childout,pid) thm n sko_thms axclauses =
- if n=0 then
- (call_resolve_tac (rev sko_thms)
- sign sg_terms (childin, childout, pid) (List.length sg_terms);
- all_tac thm)
+(*We write out problem files for each subgoal, but work is repeated (skolemize)*)
+fun write_problem_files axclauses thm n =
+ if n=0 then ()
else
-
- (SELECT_GOAL
+ (SELECT_GOAL
(EVERY1 [rtac ccontr, ResLib.atomize_tac, skolemize_tac,
METAHYPS(fn negs =>
(if !prover = "spass"
- then dfg_inputs_tfrees (make_clauses negs) n tfrees axclauses
- else tptp_inputs_tfrees (make_clauses negs) n tfrees axclauses;
- get_sko_thms tfrees sign sg_terms (childin, childout, pid)
- thm (n-1) (negs::sko_thms) axclauses;
- all_tac))]) n thm)
-
-
-
-(**********************************************)
-(* recursively call atp_tac_g on all subgoals *)
-(* sg_term is the nth subgoal as a term - used*)
-(* in proof reconstruction *)
-(**********************************************)
+ then dfg_inputs_tfrees (make_clauses negs) n axclauses
+ else tptp_inputs_tfrees (make_clauses negs) n axclauses;
+ write_problem_files axclauses thm (n-1);
+ all_tac))]) n thm;
+ ());
-fun isar_atp_aux thms thm n_subgoals (childin, childout, pid) axclauses =
- let val tfree_lits = isar_atp_h thms
- val prems = Thm.prems_of thm
- val sign = sign_of_thm thm
- val thmstring = string_of_thm thm
- in
- debug ("in isar_atp_aux");
- debug("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_subgoals [] axclauses
- end;
(******************************************************************)
(* called in Isar automatically *)
(* writes out the current clasimpset to a tptp file *)
-(* passes all subgoals on to isar_atp_aux for further processing *)
(* turns off xsymbol at start of function, restoring it at end *)
(******************************************************************)
(*FIX changed to clasimp_file *)
-val isar_atp' = setmp print_mode [] (fn (ctxt, thms, thm) =>
+val isar_atp' = setmp print_mode []
+ (fn (ctxt, thms, thm) =>
if Thm.no_prems thm then ()
else
let
@@ -260,18 +191,34 @@
(*set up variables for writing out the clasimps to a tptp file*)
val (clause_arr, num_of_clauses, axclauses) =
ResClasimp.get_clasimp_lemmas thy (hd prems) (*FIXME: hack!! need to do all prems*)
- val _ = debug ("claset and simprules total " ^ (string_of_int num_of_clauses)^ " clauses")
- val (childin, childout, pid) = Watcher.createWatcher (thm, clause_arr, num_of_clauses)
+ val _ = debug ("claset and simprules total " ^ (string_of_int num_of_clauses)^
+ " clauses")
+ val (childin, childout, pid) =
+ Watcher.createWatcher (thm, clause_arr, num_of_clauses)
val pid_string =
string_of_int (Word.toInt (Word.fromLargeWord (Posix.Process.pidToWord pid)))
in
debug ("initial thms: " ^ thms_string);
debug ("subgoals: " ^ prems_string);
debug ("pid: "^ pid_string);
- isar_atp_aux thms thm (length prems) (childin, childout, pid) axclauses;
- ()
+ write_problem_files axclauses thm (length prems);
+ watcher_call_provers (sign_of_thm thm) (Thm.prems_of thm) (childin, childout, pid)
end);
+val isar_atp_writeonly = setmp print_mode []
+ (fn (ctxt, thms, thm) =>
+ if Thm.no_prems thm then ()
+ else
+ let
+ val thy = ProofContext.theory_of ctxt
+ val prems = Thm.prems_of thm
+
+ (*set up variables for writing out the clasimps to a tptp file*)
+ val (clause_arr, num_of_clauses, axclauses) =
+ ResClasimp.get_clasimp_lemmas thy (hd prems) (*FIXME: hack!! need to do all prems*)
+ in
+ write_problem_files axclauses thm (length prems)
+ end);
fun get_thms_cs claset =
let val {safeEs, safeIs, hazEs, hazIs, ...} = rep_cs claset
--- a/src/HOL/Tools/res_clause.ML Thu Sep 15 17:45:17 2005 +0200
+++ b/src/HOL/Tools/res_clause.ML Thu Sep 15 17:46:00 2005 +0200
@@ -35,7 +35,7 @@
val dfg_clauses2str : string list -> string
val clause2dfg : clause -> string * string list
val clauses2dfg : clause list -> string -> clause list -> clause list ->
- (string * int) list -> (string * int) list -> string list -> string
+ (string * int) list -> (string * int) list -> string
val tfree_dfg_clause : string -> string
val tptp_arity_clause : arityClause -> string
@@ -878,16 +878,16 @@
fun tfree_dfg_clause tfree_lit =
- "clause( %(conjecture)\n" ^ "or( " ^ tfree_lit ^ ")),\n" ^ "tfree_tcs" ^ ")."
+ "clause( %(conjecture)\n" ^ "or( " ^ tfree_lit ^ "),\n" ^ "tfree_tcs" ^ ")."
-fun gen_dfg_file probname axioms conjectures funcs preds tfrees=
+fun gen_dfg_file probname axioms conjectures funcs preds =
let val axstrs_tfrees = (map clause2dfg axioms)
val (axstrs, atfrees) = ListPair.unzip axstrs_tfrees
val axstr = ResLib.list2str_sep delim axstrs
val conjstrs_tfrees = (map clause2dfg conjectures)
val (conjstrs, atfrees) = ListPair.unzip conjstrs_tfrees
- val tfree_clss = map tfree_dfg_clause ((ResLib.flat_noDup atfrees) \\ tfrees)
+ val tfree_clss = map tfree_dfg_clause (ResLib.flat_noDup atfrees)
val conjstr = ResLib.list2str_sep delim (tfree_clss@conjstrs)
val funcstr = string_of_funcs funcs
val predstr = string_of_preds preds
@@ -898,14 +898,13 @@
(string_of_conjectures conjstr) ^ (string_of_end ())
end;
-fun clauses2dfg [] probname axioms conjectures funcs preds tfrees =
+fun clauses2dfg [] probname axioms conjectures funcs preds =
let val funcs' = (ResLib.flat_noDup(map funcs_of_cls axioms)) @ funcs
val preds' = (ResLib.flat_noDup(map preds_of_cls axioms)) @ preds
in
- gen_dfg_file probname axioms conjectures funcs' preds' tfrees
- (*(probname, axioms, conjectures, funcs, preds)*)
+ gen_dfg_file probname axioms conjectures funcs' preds'
end
- | clauses2dfg (cls::clss) probname axioms conjectures funcs preds tfrees =
+ | clauses2dfg (cls::clss) probname axioms conjectures funcs preds =
let val (lits,tfree_lits) = dfg_clause_aux cls
(*"lits" includes the typing assumptions (TVars)*)
val cls_id = get_clause_id cls
@@ -920,17 +919,10 @@
val conjectures' =
if knd = "conjecture" then (cls::conjectures) else conjectures
in
- clauses2dfg clss probname axioms' conjectures' funcs' preds' tfrees
+ clauses2dfg clss probname axioms' conjectures' funcs' preds'
end;
-fun fileout f str = let val out = TextIO.openOut f
- in
- ResLib.writeln_strs out str; TextIO.closeOut out
- end;
-
-
-
fun string_of_arClauseID (ArityClause arcls) =
arclause_prefix ^ string_of_int(#clause_id arcls);
@@ -997,7 +989,7 @@
"input_clause(" ^ string_of_type_clsname (cls_id,ax_name,idx) ^ "," ^
knd ^ ",[" ^ tfree_lit ^ "]).";
-fun tptp_clause_aux (Clause cls) =
+fun tptp_type_lits (Clause cls) =
let val lits = map tptp_literal (#literals cls)
val tvar_lits_strs =
if !keep_types
@@ -1012,7 +1004,7 @@
end;
fun tptp_clause cls =
- let val (lits,tfree_lits) = tptp_clause_aux cls
+ let val (lits,tfree_lits) = tptp_type_lits cls
(*"lits" includes the typing assumptions (TVars)*)
val cls_id = get_clause_id cls
val ax_name = get_axiomName cls
@@ -1028,7 +1020,7 @@
end;
fun clause2tptp cls =
- let val (lits,tfree_lits) = tptp_clause_aux cls
+ let val (lits,tfree_lits) = tptp_type_lits cls
(*"lits" includes the typing assumptions (TVars)*)
val cls_id = get_clause_id cls
val ax_name = get_axiomName cls