# HG changeset patch # User paulson # Date 1126799160 -7200 # Node ID 3b237822985df26492a75026f36eaf0166394288 # Parent 0382f6877b981d3201b84e126fed7ed953738a8e massive tidy-up and simplification diff -r 0382f6877b98 -r 3b237822985d src/HOL/Tools/ATP/SpassCommunication.ML --- 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 diff -r 0382f6877b98 -r 3b237822985d src/HOL/Tools/ATP/VampCommunication.ML --- 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 diff -r 0382f6877b98 -r 3b237822985d src/HOL/Tools/ATP/recon_parse.ML --- 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*) diff -r 0382f6877b98 -r 3b237822985d src/HOL/Tools/ATP/recon_transfer_proof.ML --- 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. *) diff -r 0382f6877b98 -r 3b237822985d src/HOL/Tools/ATP/watcher.ML --- 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) = "[" diff -r 0382f6877b98 -r 3b237822985d src/HOL/Tools/res_atp.ML --- 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 diff -r 0382f6877b98 -r 3b237822985d src/HOL/Tools/res_clause.ML --- 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