--- a/src/HOL/IsaMakefile Mon Sep 19 14:20:45 2005 +0200
+++ b/src/HOL/IsaMakefile Mon Sep 19 15:12:13 2005 +0200
@@ -93,8 +93,7 @@
Orderings.ML Orderings.thy Power.thy PreList.thy Product_Type.thy \
ROOT.ML Recdef.thy Reconstruction.thy Record.thy Refute.thy \
Relation.ML Relation.thy Relation_Power.thy Ring_and_Field.thy Set.ML \
- Set.thy SetInterval.thy Sum_Type.thy Tools/ATP/SpassCommunication.ML \
- Tools/ATP/VampCommunication.ML \
+ Set.thy SetInterval.thy Sum_Type.thy Tools/ATP/AtpCommunication.ML \
Tools/ATP/recon_order_clauses.ML Tools/ATP/recon_parse.ML \
Tools/ATP/recon_prelim.ML Tools/ATP/recon_transfer_proof.ML \
Tools/ATP/recon_translate_proof.ML Tools/ATP/res_clasimpset.ML \
--- a/src/HOL/Reconstruction.thy Mon Sep 19 14:20:45 2005 +0200
+++ b/src/HOL/Reconstruction.thy Mon Sep 19 15:12:13 2005 +0200
@@ -20,8 +20,7 @@
"Tools/ATP/recon_translate_proof.ML"
"Tools/ATP/recon_parse.ML"
"Tools/ATP/recon_transfer_proof.ML"
- "Tools/ATP/VampCommunication.ML"
- "Tools/ATP/SpassCommunication.ML"
+ "Tools/ATP/AtpCommunication.ML"
"Tools/ATP/watcher.ML"
"Tools/ATP/res_clasimpset.ML"
"Tools/res_atp.ML"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/AtpCommunication.ML Mon Sep 19 15:12:13 2005 +0200
@@ -0,0 +1,311 @@
+(* Title: VampCommunication.ml
+ ID: $Id$
+ Author: Claire Quigley
+ Copyright 2004 University of Cambridge
+*)
+
+(***************************************************************************)
+(* Code to deal with the transfer of proofs from a Vampire process *)
+(***************************************************************************)
+signature ATP_COMMUNICATION =
+ sig
+ val reconstruct : bool ref
+ val checkEProofFound:
+ TextIO.instream * TextIO.outstream * Posix.Process.pid *
+ string * string * thm * int * (ResClause.clause * thm) Array.array -> bool
+ val checkVampProofFound:
+ TextIO.instream * TextIO.outstream * Posix.Process.pid *
+ string * string * thm * int * (ResClause.clause * thm) Array.array -> bool
+ val checkSpassProofFound:
+ TextIO.instream * TextIO.outstream * Posix.Process.pid *
+ string * string * thm * int * (ResClause.clause * thm) Array.array -> bool
+ end;
+
+structure AtpCommunication : ATP_COMMUNICATION =
+struct
+
+(* switch for whether to reconstruct a proof found, or just list the lemmas used *)
+val reconstruct = ref false;
+
+exception EOF;
+
+val start_E = "# Proof object starts here."
+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*)
+local open Recon_Parse in
+fun extract_proof s =
+ if cut_exists "Here is a proof with" s then
+ (kill_lines 0
+ o snd o cut_after ":"
+ o snd o cut_after "Here is a proof with"
+ o fst o cut_after " || -> .") s
+ else if cut_exists start_V8 s then
+ (kill_lines 0 (*Vampire 8.0*)
+ o snd o cut_after start_V8
+ o fst o cut_before end_V8) s
+ else if cut_exists end_E s then
+ (kill_lines 0 (*eproof*)
+ o snd o cut_after start_E
+ o fst o cut_before end_E) s
+ else "??extract_proof failed" (*Couldn't find a proof*)
+end;
+
+(**********************************************************************)
+(* Reconstruct the Vampire/E proof w.r.t. thmstring (string version of *)
+(* Isabelle goal to be proved), then transfer the reconstruction *)
+(* steps as a string to the input pipe of the main Isabelle process *)
+(**********************************************************************)
+
+fun reconstruct_tac proofextract goalstring toParent ppid sg_num clause_arr =
+ SELECT_GOAL
+ (EVERY1
+ [rtac ccontr, ResLib.atomize_tac, skolemize_tac,
+ METAHYPS(fn negs =>
+ (Recon_Transfer.prover_lemma_list proofextract
+ goalstring toParent ppid negs clause_arr))]) sg_num
+
+
+(*********************************************************************************)
+(* Inspect the output of an ATP process to see if it has found a proof, *)
+(* and if so, transfer output to the input pipe of the main Isabelle process *)
+(*********************************************************************************)
+
+fun startTransfer (startS,endS)
+ (fromChild, toParent, ppid, goalstring, childCmd, thm, sg_num, clause_arr) =
+ let val thisLine = TextIO.inputLine fromChild
+ fun transferInput currentString =
+ let val thisLine = TextIO.inputLine fromChild
+ in
+ if thisLine = "" (*end of file?*)
+ then (File.write (File.tmp_path (Path.basic"extraction_failed"))
+ ("start bracket: " ^ startS ^
+ "\nend bracket: " ^ endS ^
+ "\naccumulated text: " ^ currentString);
+ raise EOF)
+ else if String.isPrefix endS thisLine
+ then let val proofextract = extract_proof (currentString^thisLine)
+ in
+ File.write (File.tmp_path (Path.basic"extracted_prf")) proofextract;
+ reconstruct_tac proofextract goalstring toParent ppid sg_num
+ clause_arr thm
+ end
+ else transferInput (currentString^thisLine)
+ end
+ in
+ if thisLine = "" then false
+ else if String.isPrefix startS thisLine
+ then
+ (File.append (File.tmp_path (Path.basic "transfer_start"))
+ ("about to transfer proof, thm is: " ^ string_of_thm thm);
+ transferInput thisLine;
+ true) handle EOF => false
+ else
+ startTransfer (startS,endS)
+ (fromChild, toParent, ppid, goalstring,
+ childCmd, thm, sg_num,clause_arr)
+ end
+
+(*Called from watcher. Returns true if the Vampire process has returned a verdict.*)
+fun checkVampProofFound (fromChild, toParent, ppid, goalstring, childCmd,
+ thm, sg_num, clause_arr) =
+ let val proof_file = TextIO.openAppend
+ (File.platform_path(File.tmp_path (Path.basic "vampire_proof")))
+ val _ = File.write (File.tmp_path (Path.basic "vampire_checking_prf"))
+ ("checking if proof found, thm is: " ^ string_of_thm thm)
+ val thisLine = TextIO.inputLine fromChild
+ in
+ File.write (File.tmp_path (Path.basic "vampire_response")) thisLine;
+ if thisLine = ""
+ then (TextIO.output (proof_file, "No proof output seen \n");
+ TextIO.closeOut proof_file;
+ false)
+ else if String.isPrefix "Refutation found. Thanks to Tanya" thisLine
+ then
+ startTransfer (start_V8, end_V8)
+ (fromChild, toParent, ppid, goalstring,
+ childCmd, thm, sg_num, clause_arr)
+ else if (String.isPrefix "Satisfiability detected" thisLine) orelse
+ (String.isPrefix "Refutation not found" thisLine)
+ then
+ (TextIO.output (toParent, "Failure\n");
+ TextIO.output (toParent, goalstring^"\n");
+ TextIO.flushOut toParent;
+ TextIO.output (proof_file, thisLine);
+ TextIO.closeOut proof_file;
+ 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);
+ true)
+ else
+ (TextIO.output (proof_file, thisLine);
+ TextIO.flushOut proof_file;
+ checkVampProofFound (fromChild, toParent, ppid,
+ goalstring,childCmd, thm, sg_num, clause_arr))
+ end
+
+
+(*Called from watcher. Returns true if the E process has returned a verdict.*)
+fun checkEProofFound (fromChild, toParent, ppid,goalstring, childCmd,
+ thm, sg_num, clause_arr) =
+ let val E_proof_file = TextIO.openAppend
+ (File.platform_path(File.tmp_path (Path.basic "e_proof")))
+ val _ = File.write (File.tmp_path (Path.basic "e_checking_prf"))
+ ("checking if proof found. childCmd is " ^ childCmd ^
+ "\nthm is: " ^ string_of_thm thm)
+ val thisLine = TextIO.inputLine fromChild
+ in
+ File.write (File.tmp_path (Path.basic "e_response")) thisLine;
+ if thisLine = ""
+ then (TextIO.output (E_proof_file, "No proof output seen \n");
+ TextIO.closeOut E_proof_file;
+ false)
+ else if thisLine = "# TSTP exit status: Unsatisfiable\n"
+ then
+ startTransfer (start_E, end_E)
+ (fromChild, toParent, ppid, goalstring,
+ childCmd, thm, sg_num, clause_arr)
+ else if String.isPrefix "# Problem is satisfiable" thisLine
+ then
+ (TextIO.output (toParent, "Invalid\n");
+ TextIO.output (toParent, goalstring^"\n");
+ TextIO.flushOut toParent;
+ TextIO.output (E_proof_file, thisLine);
+ TextIO.closeOut E_proof_file;
+ 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);
+ true)
+ else if String.isPrefix "# Failure: Resource limit exceeded" thisLine
+ then (*In fact, E distingishes "out of time" and "out of memory"*)
+ (File.write (File.tmp_path (Path.basic "e_response")) thisLine;
+ TextIO.output (toParent, "Failure\n");
+ TextIO.output (toParent, goalstring^"\n");
+ TextIO.flushOut toParent;
+ Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
+ TextIO.output (E_proof_file, "signalled parent\n");
+ TextIO.closeOut E_proof_file;
+ (* Attempt to prevent several signals from turning up simultaneously *)
+ Posix.Process.sleep(Time.fromSeconds 1);
+ true)
+ else
+ (TextIO.output (E_proof_file, thisLine);
+ TextIO.flushOut E_proof_file;
+ checkEProofFound (fromChild, toParent, ppid, goalstring,
+ childCmd, thm, sg_num, clause_arr))
+ end
+
+
+(**********************************************************************)
+(* Reconstruct the Spass proof w.r.t. thmstring (string version of *)
+(* Isabelle goal to be proved), then transfer the reconstruction *)
+(* steps as a string to the input pipe of the main Isabelle process *)
+(**********************************************************************)
+
+fun spass_reconstruct_tac proofextract goalstring toParent ppid sg_num
+ clause_arr =
+ let val f = if !reconstruct then Recon_Transfer.spass_reconstruct
+ else Recon_Transfer.spass_lemma_list
+ in
+ SELECT_GOAL
+ (EVERY1 [rtac ccontr, ResLib.atomize_tac, skolemize_tac,
+ METAHYPS(fn negs =>
+ f proofextract goalstring toParent ppid negs clause_arr)]) sg_num
+ end;
+
+
+fun transferSpassInput (fromChild, toParent, ppid, goalstring,
+ currentString, thm, sg_num, clause_arr) =
+ let val thisLine = TextIO.inputLine fromChild
+ in
+ if thisLine = "" (*end of file?*)
+ then (File.write (File.tmp_path (Path.basic"spass_extraction_failed")) currentString;
+ raise EOF)
+ else if thisLine = "--------------------------SPASS-STOP------------------------------\n"
+ then
+ let val proofextract = extract_proof (currentString^thisLine)
+ in
+ File.write (File.tmp_path (Path.basic"spass_extracted_prf")) proofextract;
+ spass_reconstruct_tac proofextract goalstring toParent ppid sg_num
+ clause_arr thm
+ end
+ else transferSpassInput (fromChild, toParent, ppid, goalstring,
+ (currentString^thisLine), thm, sg_num, clause_arr)
+ end;
+
+
+(*********************************************************************************)
+(* Inspect the output of a Spass process to see if it has found a proof, *)
+(* and if so, transfer output to the input pipe of the main Isabelle process *)
+(*********************************************************************************)
+
+
+fun startSpassTransfer (fromChild, toParent, ppid, goalstring,childCmd,
+ thm, sg_num,clause_arr) =
+ let val thisLine = TextIO.inputLine fromChild
+ in
+ if thisLine = "" then false
+ 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, goalstring,thisLine,
+ thm, sg_num,clause_arr);
+ true) handle EOF => false
+ else startSpassTransfer (fromChild, toParent, ppid, goalstring,
+ childCmd, thm, sg_num,clause_arr)
+ end
+
+
+(*Called from watcher. Returns true if the E process has returned a verdict.*)
+fun checkSpassProofFound (fromChild, toParent, ppid, goalstring, childCmd,
+ thm, sg_num, clause_arr) =
+ let val spass_proof_file = TextIO.openAppend
+ (File.platform_path(File.tmp_path (Path.basic "spass_proof")))
+ val _ = File.write(File.tmp_path (Path.basic "spass_checking_prf"))
+ ("checking if proof found, thm is: "^(string_of_thm thm))
+ val thisLine = TextIO.inputLine fromChild
+ in
+ File.write (File.tmp_path (Path.basic "spass_response")) thisLine;
+ if thisLine = ""
+ then (TextIO.output (spass_proof_file, ("No proof output seen \n"));
+ TextIO.closeOut spass_proof_file;
+ false)
+ else if thisLine = "SPASS beiseite: Proof found.\n"
+ then
+ startSpassTransfer (fromChild, toParent, ppid, goalstring,
+ childCmd, thm, sg_num, clause_arr)
+ else if thisLine = "SPASS beiseite: Completion found.\n"
+ then
+ (TextIO.output (spass_proof_file, thisLine);
+ TextIO.closeOut spass_proof_file;
+ TextIO.output (toParent, "Invalid\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);
+ true)
+ else if thisLine = "SPASS beiseite: Ran out of time.\n" orelse
+ thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n"
+ then
+ (TextIO.output (toParent, "Failure\n");
+ TextIO.output (toParent, goalstring^"\n");
+ TextIO.flushOut toParent;
+ Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
+ TextIO.output (spass_proof_file, "signalled parent\n");
+ TextIO.closeOut spass_proof_file;
+ (* Attempt to prevent several signals from turning up simultaneously *)
+ Posix.Process.sleep(Time.fromSeconds 1);
+ true)
+ else
+ (TextIO.output (spass_proof_file, thisLine);
+ TextIO.flushOut spass_proof_file;
+ checkSpassProofFound (fromChild, toParent, ppid, goalstring,
+ childCmd, thm, sg_num, clause_arr))
+ end
+
+end;
--- a/src/HOL/Tools/ATP/SpassCommunication.ML Mon Sep 19 14:20:45 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,176 +0,0 @@
-(* Title: SpassCommunication.ml
- ID: $Id$
- Author: Claire Quigley
- Copyright 2004 University of Cambridge
-*)
-
-(***************************************************************************)
-(* Code to deal with the transfer of proofs from a Spass process *)
-(***************************************************************************)
-signature SPASS_COMM =
- sig
- val reconstruct : bool ref
- val getSpassInput : TextIO.instream -> string * string
- val checkSpassProofFound:
- TextIO.instream * TextIO.outstream * Posix.Process.pid *
- string * string * thm * int * (ResClause.clause * thm) Array.array * int -> bool
- end;
-
-structure SpassComm : SPASS_COMM =
-struct
-
-(* switch for whether to reconstruct a proof found, or just list the lemmas used *)
-val reconstruct = ref false;
-
-exception EOF;
-
-(**********************************************************************)
-(* Reconstruct the Spass proof w.r.t. thmstring (string version of *)
-(* Isabelle goal to be proved), then transfer the reconstruction *)
-(* steps as a string to the input pipe of the main Isabelle process *)
-(**********************************************************************)
-
-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
- in
- SELECT_GOAL
- (EVERY1 [rtac ccontr, ResLib.atomize_tac, skolemize_tac,
- METAHYPS(fn negs =>
- f proofextract goalstring toParent ppid negs clause_arr num_of_clauses)]) sg_num
- end;
-
-
-fun transferSpassInput (fromChild, toParent, ppid, goalstring,
- currentString, thm, sg_num,clause_arr, num_of_clauses) =
- let val thisLine = TextIO.inputLine fromChild
- in
- if thisLine = "" (*end of file?*)
- then (File.write (File.tmp_path (Path.basic"spass_extraction_failed")) currentString;
- raise EOF)
- else if thisLine = "--------------------------SPASS-STOP------------------------------\n"
- then
- let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
- in
- File.write (File.tmp_path (Path.basic"spass_extracted_prf")) proofextract;
- reconstruct_tac proofextract goalstring toParent ppid sg_num
- clause_arr num_of_clauses thm
- end
- else transferSpassInput (fromChild, toParent, ppid, goalstring,
- (currentString^thisLine), thm, sg_num, clause_arr,
- num_of_clauses)
- end;
-
-
-(*********************************************************************************)
-(* Inspect the output of a Spass process to see if it has found a proof, *)
-(* and if so, transfer output to the input pipe of the main Isabelle process *)
-(*********************************************************************************)
-
-
-fun startSpassTransfer (fromChild, toParent, ppid, goalstring,childCmd,
- thm, sg_num,clause_arr, num_of_clauses) =
- let val thisLine = TextIO.inputLine fromChild
- in
- if thisLine = "" then false
- 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, goalstring,thisLine,
- thm, sg_num,clause_arr, num_of_clauses);
- true) handle EOF => false
- else startSpassTransfer (fromChild, toParent, ppid, goalstring,
- childCmd, thm, sg_num,clause_arr, num_of_clauses)
- end
-
-
-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")))
- val _ = File.write(File.tmp_path (Path.basic "spass_checking_prf"))
- ("checking if proof found, thm is: "^(string_of_thm thm))
- val thisLine = TextIO.inputLine fromChild
- in
- if thisLine = ""
- then (TextIO.output (spass_proof_file, ("No proof output seen \n"));
- TextIO.closeOut spass_proof_file;
- false)
- else if thisLine = "SPASS beiseite: Proof found.\n"
- then
- (File.write (File.tmp_path (Path.basic "spass_response")) thisLine;
- startSpassTransfer (fromChild, toParent, ppid, goalstring,
- childCmd, thm, sg_num, clause_arr, num_of_clauses))
- else if thisLine = "SPASS beiseite: Completion found.\n"
- then
- (File.write (File.tmp_path (Path.basic "spass_response")) thisLine;
- TextIO.output (toParent,childCmd^"\n" );
- TextIO.flushOut toParent;
- TextIO.output (spass_proof_file, thisLine);
- TextIO.flushOut spass_proof_file;
- TextIO.closeOut spass_proof_file;
-
- TextIO.output (toParent, thisLine^"\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);
- true)
- else if thisLine = "SPASS beiseite: Ran out of time.\n"
- then
- (File.write (File.tmp_path (Path.basic "spass_response")) thisLine;
- TextIO.output (toParent, thisLine^"\n");
- TextIO.output (toParent, goalstring^"\n");
- TextIO.flushOut toParent;
- Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
- TextIO.output (spass_proof_file, "signalled parent\n");
- TextIO.closeOut spass_proof_file;
- (* Attempt to prevent several signals from turning up simultaneously *)
- Posix.Process.sleep(Time.fromSeconds 1);
- true)
- else if thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n"
- then
- (Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
- TextIO.output (toParent,childCmd^"\n" );
- TextIO.flushOut toParent;
- TextIO.output (toParent, thisLine);
- TextIO.flushOut toParent;
- true)
- else
- (TextIO.output (spass_proof_file, thisLine);
- TextIO.flushOut spass_proof_file;
- checkSpassProofFound (fromChild, toParent, ppid, goalstring,
- childCmd, thm, sg_num, clause_arr, num_of_clauses))
- end
-
-
-(***********************************************************************)
-(* Function used by the Isabelle process to read in a spass proof *)
-(***********************************************************************)
-
-fun getSpassInput instr =
- 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","")
- else if String.sub (thisLine, 0) = #"[" orelse
- String.isPrefix "SPASS beiseite:" thisLine orelse
- String.isPrefix "Rules from" thisLine
- then
- 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 goalstring = TextIO.inputLine instr
- in
- File.write (File.tmp_path (Path.basic "getSpassInput")) thisLine;
- (thisLine, goalstring)
- end
- else getSpassInput instr
- end
-
-
-end;
--- a/src/HOL/Tools/ATP/VampCommunication.ML Mon Sep 19 14:20:45 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,236 +0,0 @@
-(* Title: VampCommunication.ml
- ID: $Id$
- Author: Claire Quigley
- Copyright 2004 University of Cambridge
-*)
-
-(***************************************************************************)
-(* Code to deal with the transfer of proofs from a Vampire process *)
-(***************************************************************************)
-signature VAMP_COMM =
- sig
- val getEInput : TextIO.instream -> string * string
- val checkEProofFound:
- TextIO.instream * TextIO.outstream * Posix.Process.pid *
- string * string * thm * int * (ResClause.clause * thm) Array.array * int -> bool
-
- val getVampInput : TextIO.instream -> string * string
- val checkVampProofFound:
- TextIO.instream * TextIO.outstream * Posix.Process.pid *
- string * string * thm * int * (ResClause.clause * thm) Array.array * int -> bool
- end;
-
-structure VampComm : VAMP_COMM =
-struct
-
-exception EOF;
-
-(**********************************************************************)
-(* Reconstruct the Vampire/E proof w.r.t. thmstring (string version of *)
-(* Isabelle goal to be proved), then transfer the reconstruction *)
-(* steps as a string to the input pipe of the main Isabelle process *)
-(**********************************************************************)
-
-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
- goalstring toParent ppid negs clause_arr num_of_clauses))]) sg_num
-
-
-(*********************************************************************************)
-(* Inspect the output of an ATP process to see if it has found a proof, *)
-(* and if so, transfer output to the input pipe of the main Isabelle process *)
-(*********************************************************************************)
-
-fun startTransfer (startS,endS)
- (fromChild, toParent, ppid, goalstring,childCmd,
- thm, sg_num,clause_arr, num_of_clauses) =
- let val thisLine = TextIO.inputLine fromChild
- fun transferInput currentString =
- let val thisLine = TextIO.inputLine fromChild
- in
- if thisLine = "" (*end of file?*)
- then (File.write (File.tmp_path (Path.basic"extraction_failed"))
- ("start bracket: " ^ startS ^
- "\nend bracket: " ^ endS ^
- "\naccumulated text: " ^ currentString);
- raise EOF)
- else if String.isPrefix endS thisLine
- then let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
- in
- File.write (File.tmp_path (Path.basic"extracted_prf")) proofextract;
- reconstruct_tac proofextract goalstring toParent ppid sg_num
- clause_arr num_of_clauses thm
- end
- else transferInput (currentString^thisLine)
- end
- in
- if thisLine = "" then false
- else if String.isPrefix startS thisLine
- then
- (File.append (File.tmp_path (Path.basic "transfer_start"))
- ("about to transfer proof, thm is: " ^ string_of_thm thm);
- transferInput thisLine;
- true) handle EOF => false
- else
- startTransfer (startS,endS)
- (fromChild, toParent, ppid, goalstring,
- childCmd, thm, sg_num,clause_arr, num_of_clauses)
- end
-
-
-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")))
- 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
- if thisLine = ""
- then (TextIO.output (proof_file, "No proof output seen \n");
- TextIO.closeOut proof_file;
- false)
- else if String.isPrefix "Refutation found. Thanks to Tanya" thisLine
- then
- (File.write (File.tmp_path (Path.basic "atp_response")) thisLine;
- startTransfer (Recon_Parse.start_V8, Recon_Parse.end_V8)
- (fromChild, toParent, ppid, goalstring,
- childCmd, thm, sg_num, clause_arr, num_of_clauses))
- else if (String.isPrefix "Satisfiability detected" thisLine) orelse
- (String.isPrefix "Refutation not found" thisLine)
- then
- (File.write (File.tmp_path (Path.basic "atp_response")) thisLine;
- TextIO.output (toParent,childCmd^"\n");
- TextIO.flushOut toParent;
- TextIO.output (proof_file, thisLine);
- TextIO.closeOut proof_file;
-
- TextIO.output (toParent, thisLine^"\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);
- true)
- else
- (TextIO.output (proof_file, thisLine);
- TextIO.flushOut proof_file;
- checkVampProofFound (fromChild, toParent, ppid,
- goalstring,childCmd, thm, sg_num, clause_arr, num_of_clauses))
- end
-
-
-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 "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
- if thisLine = ""
- then (TextIO.output (E_proof_file, ("No proof output seen \n"));
- TextIO.closeOut E_proof_file;
- false)
- else if thisLine = "# TSTP exit status: Unsatisfiable\n"
- then
- (File.write (File.tmp_path (Path.basic "atp_response")) thisLine;
- startTransfer (Recon_Parse.start_E, Recon_Parse.end_E)
- (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 "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, 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);
- true)
- else if thisLine = "# Failure: Resource limit exceeded (time)\n"
- then
- (File.write (File.tmp_path (Path.basic "atp_response")) thisLine;
- TextIO.output (toParent, thisLine^"\n");
- TextIO.output (toParent, goalstring^"\n");
- TextIO.flushOut toParent;
- Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
- TextIO.output (E_proof_file, "signalled parent\n");
- TextIO.closeOut E_proof_file;
- (* Attempt to prevent several signals from turning up simultaneously *)
- Posix.Process.sleep(Time.fromSeconds 1);
- true)
- else if thisLine = "# Failure: Resource limit exceeded (memory)\n"
- then
- (Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
- TextIO.output (toParent,childCmd^"\n" );
- TextIO.output (toParent, thisLine);
- TextIO.flushOut toParent;
- true)
- else
- (TextIO.output (E_proof_file, thisLine);
- TextIO.flushOut E_proof_file;
- checkEProofFound (fromChild, toParent, ppid, goalstring,
- childCmd, thm, sg_num, clause_arr, num_of_clauses))
- end
-
-
-(***********************************************************************)
-(* Function used by the Isabelle process to read in a Vampire proof *)
-(***********************************************************************)
-
-fun getVampInput instr =
- 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","")
- else if String.sub (thisLine, 0) = #"[" orelse (*FIXME: for SPASS?*)
- String.isPrefix "Satisfiability detected" thisLine orelse
- String.isPrefix "Refutation not found" thisLine orelse
- String.isPrefix "Rules from" thisLine
- then
- let val goalstring = TextIO.inputLine instr
- in (thisLine, goalstring) end
- else if thisLine = "Proof found but translation failed!"
- then
- let val goalstring = TextIO.inputLine instr
- val _ = debug "getVampInput: translation of proof failed"
- in (thisLine, goalstring) end
- else getVampInput instr
- end
-
-
-(***********************************************************************)
-(* Function used by the Isabelle process to read in an E proof *)
-(***********************************************************************)
-
-fun getEInput instr =
- 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","")
- else if String.isPrefix "# Problem is satisfiable" thisLine orelse
- String.isPrefix "# Cannot determine problem status" thisLine orelse
- String.isPrefix "# Failure:" thisLine
- then
- let val goalstring = TextIO.inputLine instr
- in (thisLine, goalstring) end
- else if thisLine = "Proof found but translation failed!"
- then
- let val goalstring = TextIO.inputLine instr
- val _ = debug "getEInput: translation of proof failed"
- in (thisLine, goalstring) end
- else getEInput instr
- end
-
-end;
--- a/src/HOL/Tools/ATP/recon_parse.ML Mon Sep 19 14:20:45 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_parse.ML Mon Sep 19 15:12:13 2005 +0200
@@ -66,9 +66,6 @@
fun finished input = if input = [] then (0, input) else raise Noparse;
-
-
-
(* Parsing the output from gandalf *)
datatype token = Word of string
| Number of int
@@ -105,39 +102,6 @@
fun kill_lines 0 = Library.I
| kill_lines n = kill_lines (n - 1) o snd o cut_after "\n";
- (*fun extract_proof s
- = if cut_exists "EMPTY CLAUSE DERIVED" s then
- (kill_lines 6
- o snd o cut_after "EMPTY CLAUSE DERIVED"
- o fst o cut_after "contradiction.\n") s
- else
- raise (GandalfError "Couldn't find a proof.")
-*)
-
-val start_E = "# Proof object starts here."
-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*)
-fun extract_proof s =
- if cut_exists "Here is a proof with" s then
- (kill_lines 0
- o snd o cut_after ":"
- o snd o cut_after "Here is a proof with"
- o fst o cut_after " || -> .") s
- else if cut_exists start_V8 s then
- (kill_lines 0 (*Vampire 8.0*)
- o snd o cut_after start_V8
- o fst o cut_before end_V8) s
- else if cut_exists end_E s then
- (kill_lines 0 (*eproof*)
- o snd o cut_after start_E
- o fst o cut_before end_E) s
- else "??extract_proof failed" (*Couldn't find a proof*)
fun several p = many (some p)
fun collect (h, t) = h ^ (fold_rev (fn s1 => fn s2 => s1 ^ s2) t "")
@@ -163,17 +127,6 @@
fun lex s = alltokens (explode s)
-
-(*String contains multiple lines, terminated with newline characters.
- A list consisting of the first number in each line is returned. *)
-fun get_linenums proofstr =
- let val numerics = String.tokens (not o Char.isDigit)
- fun firstno [] = NONE
- | firstno (x::xs) = Int.fromString x
- val lines = String.tokens (fn c => c = #"\n") proofstr
- in List.mapPartial (firstno o numerics) lines end
-
-
(************************************************************)
(**************************************************)
--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Mon Sep 19 14:20:45 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Mon Sep 19 15:12:13 2005 +0200
@@ -39,12 +39,10 @@
(*| proofstep_to_string (Rewrite((a,b),(c,d))) =
"Rewrite(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))"*)
-fun list_to_string [] liststr = liststr
-| list_to_string (x::[]) liststr = liststr^(string_of_int x)
-| list_to_string (x::xs) liststr = list_to_string xs (liststr^(string_of_int x)^",")
-
-fun proof_to_string (num,(step,clause_strs, thmvars)) = (string_of_int num)^(proofstep_to_string step)^"["^(clause_strs_to_string clause_strs "")^"]["^(thmvars_to_string thmvars "")^"]"
+fun proof_to_string (num,(step,clause_strs, thmvars)) =
+ (string_of_int num)^(proofstep_to_string step)^
+ "["^(clause_strs_to_string clause_strs "")^"]["^(thmvars_to_string thmvars "")^"]"
fun proofs_to_string [] str = str
@@ -55,7 +53,9 @@
-fun init_proofstep_to_string (num, step, clause_strs) = (string_of_int num)^" "^(proofstep_to_string step)^" "^(clause_strs_to_string clause_strs "")^" "
+fun init_proofstep_to_string (num, step, clause_strs) =
+ (string_of_int num)^" "^(proofstep_to_string step)^" "^
+ (clause_strs_to_string clause_strs "")^" "
fun init_proofsteps_to_string [] str = str
| init_proofsteps_to_string (x::xs) str = let val newstr = init_proofstep_to_string x
@@ -144,12 +144,11 @@
(* retrieve the axioms that were obtained from the clasimpset *)
-fun get_clasimp_cls (clause_arr: (ResClause.clause * thm) array) clasimp_num step_nums =
- let val realnums = map subone step_nums
- val clasimp_nums = List.filter (is_clasimp_ax (clasimp_num - 1)) realnums
-(* val axnums = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "axnums")))
- val _ = TextIO.output(axnums,(numstr clasimp_nums))
- val _ = TextIO.closeOut(axnums)*)
+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))
+ (map subone step_nums)
+(* val _ = File.write (File.tmp_path (Path.basic "axnums"))
+ (numstr clasimp_nums) *)
in
map (fn x => Array.sub(clause_arr, x)) clasimp_nums
end
@@ -159,7 +158,7 @@
(* get names of clasimp axioms used *)
(*****************************************************)
- fun get_axiom_names step_nums thms clause_arr num_of_clauses =
+ fun get_axiom_names step_nums thms clause_arr =
let
(* not sure why this is necessary again, but seems to be *)
val _ = (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
@@ -168,7 +167,7 @@
(* here need to add the clauses from clause_arr*)
(***********************************************)
- val clasimp_names_cls = get_clasimp_cls clause_arr num_of_clauses step_nums
+ val clasimp_names_cls = get_clasimp_cls clause_arr step_nums
val clasimp_names = map (ResClause.get_axiomName o #1) clasimp_names_cls
val _ = File.write (File.tmp_path (Path.basic "clasimp_names"))
(concat clasimp_names)
@@ -178,20 +177,30 @@
end
-fun get_axiom_names_spass proofstr thms clause_arr num_of_clauses =
+fun get_axiom_names_spass proofstr thms clause_arr =
let (* parse spass proof into datatype *)
+ val _ = File.write (File.tmp_path (Path.basic "parsing_progress"))
+ ("Started parsing:\n" ^ proofstr)
val tokens = #1(lex proofstr)
val proof_steps = parse tokens
- val _ = File.write (File.tmp_path (Path.basic "parsing_done"))
- ("Did parsing on "^proofstr)
+ val _ = File.append (File.tmp_path (Path.basic "parsing_progress")) "\nFinished!"
(* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
in
get_axiom_names (get_step_nums (List.filter is_axiom proof_steps) [])
- thms clause_arr num_of_clauses
+ thms clause_arr
end;
- fun get_axiom_names_vamp_E proofstr thms clause_arr num_of_clauses =
- get_axiom_names (get_linenums proofstr) thms clause_arr num_of_clauses;
+ (*String contains multiple lines, terminated with newline characters.
+ A list consisting of the first number in each line is returned. *)
+fun get_linenums proofstr =
+ let val numerics = String.tokens (not o Char.isDigit)
+ fun firstno [] = NONE
+ | firstno (x::xs) = Int.fromString x
+ val lines = String.tokens (fn c => c = #"\n") proofstr
+ in List.mapPartial (firstno o numerics) lines end
+
+fun get_axiom_names_vamp_E proofstr thms clause_arr =
+ get_axiom_names (get_linenums proofstr) thms clause_arr;
(***********************************************)
@@ -206,13 +215,13 @@
fun addvars c (a,b) = (a,b,c)
-fun get_axioms_used proof_steps thms clause_arr num_of_clauses =
+fun get_axioms_used proof_steps thms clause_arr =
let
val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
val axioms = (List.filter is_axiom) proof_steps
val step_nums = get_step_nums axioms []
- val clauses =(*(clasimp_cls)@*)( make_clauses thms)
+ val clauses = make_clauses thms (*FIXME: must this be repeated??*)
val vars = map thm_vars clauses
@@ -265,19 +274,19 @@
val restore_linebreaks = subst_for #"\t" #"\n";
-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"))
+fun prover_lemma_list_aux proofstr goalstring toParent ppid thms clause_arr getax =
+ let val _ = File.append(File.tmp_path (Path.basic "prover_lemmastring"))
("proofstr is " ^ proofstr ^
"\ngoalstr is " ^ goalstring ^
- "\nnum of clauses is " ^ string_of_int num_of_clauses)
+ "\nnum of clauses is " ^ string_of_int (Array.length clause_arr))
- val axiom_names = getax proofstr thms clause_arr num_of_clauses
- val ax_str = "Rules from clasimpset used in automatic proof: " ^
- rules_to_string axiom_names
+ val axiom_names = getax proofstr thms clause_arr
+ val ax_str = rules_to_string axiom_names
in
- File.append(File.tmp_path (Path.basic "spass_lemmastring"))
- ("reconstring is: "^ax_str^" "^goalstring);
- TextIO.output (toParent, ax_str^"\n");
+ File.append(File.tmp_path (Path.basic "prover_lemmastring"))
+ ("\nlemma list is: " ^ ax_str);
+ TextIO.output (toParent, "Success. Lemmas used in automatic proof: " ^
+ ax_str ^ "\n");
TextIO.output (toParent, "goalstring: "^goalstring^"\n");
TextIO.flushOut toParent;
@@ -285,9 +294,10 @@
(* Attempt to prevent several signals from turning up simultaneously *)
Posix.Process.sleep(Time.fromSeconds 1) ; all_tac
end
- handle _ => (*FIXME: exn handler is too general!*)
- (File.write(File.tmp_path (Path.basic "proverString_handler")) "In exception handler";
- TextIO.output (toParent, "Proof found but translation failed : " ^
+ handle exn => (*FIXME: exn handler is too general!*)
+ (File.write(File.tmp_path (Path.basic "proverString_handler"))
+ ("In exception handler: " ^ Toplevel.exn_message exn);
+ TextIO.output (toParent, "Translation failed for the proof: " ^
remove_linebreaks proofstr ^ "\n");
TextIO.output (toParent, remove_linebreaks goalstring ^ "\n");
TextIO.flushOut toParent;
@@ -295,21 +305,19 @@
(* Attempt to prevent several signals from turning up simultaneously *)
Posix.Process.sleep(Time.fromSeconds 1); all_tac);
-fun proverString_to_lemmaString proofstr goalstring toParent ppid thms
- clause_arr num_of_clauses =
- proverString_to_lemmaString_aux proofstr goalstring toParent ppid thms
- clause_arr num_of_clauses get_axiom_names_vamp_E;
+fun prover_lemma_list proofstr goalstring toParent ppid thms clause_arr =
+ prover_lemma_list_aux proofstr goalstring toParent ppid thms
+ clause_arr get_axiom_names_vamp_E;
-fun spassString_to_lemmaString proofstr goalstring toParent ppid thms
- clause_arr num_of_clauses =
- proverString_to_lemmaString_aux proofstr goalstring toParent ppid thms
- clause_arr num_of_clauses get_axiom_names_spass;
+fun spass_lemma_list proofstr goalstring toParent ppid thms clause_arr =
+ prover_lemma_list_aux proofstr goalstring toParent ppid thms
+ clause_arr get_axiom_names_spass;
(**** Full proof reconstruction for SPASS (not really working) ****)
-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"))
+fun spass_reconstruct proofstr goalstring toParent ppid thms clause_arr =
+ let val _ = File.write(File.tmp_path (Path.basic "prover_reconstruction"))
("proofstr is: "^proofstr)
val tokens = #1(lex proofstr)
@@ -318,7 +326,7 @@
(***********************************)
val proof_steps = parse tokens
- val _ = File.append (File.tmp_path (Path.basic "spass_reconstruction"))
+ val _ = File.append (File.tmp_path (Path.basic "prover_reconstruction"))
("Did parsing on "^proofstr)
(************************************)
@@ -329,19 +337,19 @@
(* 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 num_of_clauses
+ val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps thms clause_arr
(*val numcls_string = numclstr ( vars, numcls) ""*)
- val _ = File.append (File.tmp_path (Path.basic "spass_reconstruction")) "got axioms"
+ val _ = File.append (File.tmp_path (Path.basic "prover_reconstruction")) "got axioms"
(************************************)
(* translate proof *)
(************************************)
- val _ = File.append (File.tmp_path (Path.basic "spass_reconstruction"))
+ val _ = File.append (File.tmp_path (Path.basic "prover_reconstruction"))
("about to translate proof, steps: "
^(init_proofsteps_to_string proof_steps ""))
val (newthm,proof) = translate_proof numcls proof_steps vars
- val _ = File.append (File.tmp_path (Path.basic "spass_reconstruction"))
+ val _ = File.append (File.tmp_path (Path.basic "prover_reconstruction"))
("translated proof, steps: "^(init_proofsteps_to_string proof_steps ""))
(***************************************************)
(* transfer necessary steps as strings to Isabelle *)
@@ -371,9 +379,10 @@
(* Attempt to prevent several signals from turning up simultaneously *)
Posix.Process.sleep(Time.fromSeconds 1) ; all_tac
end
- handle _ =>
- (File.append(File.tmp_path (Path.basic "spass_reconstruction")) "In exception handler";
- TextIO.output (toParent,"Proof found but translation failed for resolution proof:"^
+ handle exn => (*FIXME: exn handler is too general!*)
+ (File.append(File.tmp_path (Path.basic "prover_reconstruction"))
+ ("In exception handler: " ^ Toplevel.exn_message exn);
+ TextIO.output (toParent,"Translation failed for the proof:"^
(remove_linebreaks proofstr) ^"\n");
TextIO.output (toParent, goalstring^"\n");
TextIO.flushOut toParent;
--- a/src/HOL/Tools/ATP/res_clasimpset.ML Mon Sep 19 14:20:45 2005 +0200
+++ b/src/HOL/Tools/ATP/res_clasimpset.ML Mon Sep 19 15:12:13 2005 +0200
@@ -112,8 +112,8 @@
val use_simpset: bool ref
val use_nameless: bool ref
val get_clasimp_lemmas :
- theory -> term ->
- (ResClause.clause * thm) Array.array * int * ResClause.clause list
+ Proof.context -> term ->
+ (ResClause.clause * thm) Array.array * ResClause.clause list
end;
structure ResClasimp : RES_CLASIMP =
@@ -155,16 +155,16 @@
(*Write out the claset and simpset rules of the supplied theory.
FIXME: argument "goal" is a hack to allow relevance filtering.
To reduce the number of clauses produced, set ResClasimp.relevant:=1*)
-fun get_clasimp_lemmas thy goal =
+fun get_clasimp_lemmas ctxt goal =
let val claset_rules =
map put_name_pair
(ReduceAxiomsN.relevant_filter (!relevant) goal
- (ResAxioms.claset_rules_of_thy thy));
+ (ResAxioms.claset_rules_of_ctxt ctxt));
val claset_cls_thms = #1 (ResAxioms.clausify_rules_pairs claset_rules []);
val simpset_rules =
ReduceAxiomsN.relevant_filter (!relevant) goal
- (ResAxioms.simpset_rules_of_thy thy);
+ (ResAxioms.simpset_rules_of_ctxt ctxt);
val named_simpset = map put_name_pair simpset_rules
val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []);
@@ -184,7 +184,7 @@
(*********************************************************)
val clause_arr = Array.fromList whole_list;
in
- (clause_arr, List.length whole_list, clauses)
+ (clause_arr, clauses)
end;
--- a/src/HOL/Tools/ATP/watcher.ML Mon Sep 19 14:20:45 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML Mon Sep 19 15:12:13 2005 +0200
@@ -13,7 +13,6 @@
(* Hardwired version of where to pick up the tptp files for the moment *)
(***************************************************************************)
-
signature WATCHER =
sig
@@ -36,7 +35,9 @@
(* Start a watcher and set up signal handlers *)
(**********************************************************)
-val createWatcher : thm*(ResClause.clause * thm) Array.array * int -> TextIO.instream * TextIO.outstream * Posix.Process.pid
+val createWatcher :
+ thm * (ResClause.clause * thm) Array.array ->
+ TextIO.instream * TextIO.outstream * Posix.Process.pid
(**********************************************************)
(* Kill watcher process *)
@@ -48,9 +49,8 @@
-
structure Watcher: WATCHER =
- struct
+struct
open ReconPrelim Recon_Transfer
@@ -268,7 +268,10 @@
fun getProofCmd (a,c,d,e,f) = d
-fun setupWatcher (thm,clause_arr, num_of_clauses) =
+fun prems_string_of th =
+ Meson.concat_with_and (map (Sign.string_of_term (sign_of_thm th)) (prems_of th))
+
+fun setupWatcher (thm,clause_arr) =
let
(** pipes for communication between parent and watcher **)
val p1 = Posix.IO.pipe ()
@@ -295,10 +298,7 @@
val fromParentIOD = Posix.FileSys.fdToIOD fromParent
val fromParentStr = openInFD ("_exec_in_parent", fromParent)
val toParentStr = openOutFD ("_exec_out_parent", toParent)
- 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 startWatcher: "^prems_string);
+ val _ = debug ("subgoals forked to startWatcher: "^ prems_string_of thm);
fun killChildren [] = ()
| killChildren (child_handle::children) =
(killChild child_handle; killChildren children)
@@ -367,46 +367,45 @@
| checkChildren ((childProc::otherChildren), toParentStr) =
let val _ = File.append (File.tmp_path (Path.basic "child_check"))
("In check child, length of queue:"^
- (string_of_int (length (childProc::otherChildren)))^"\n")
+ string_of_int (length (childProc::otherChildren)))
val (childInput,childOutput) = cmdstreamsOf childProc
val child_handle= cmdchildHandle childProc
(* childCmd is the .dfg file that the problem is in *)
val childCmd = fst(snd (cmdchildInfo childProc))
- val _ = File.append (File.tmp_path (Path.basic "child_command"))
- (childCmd^"\n")
+ val _ = File.append (File.tmp_path (Path.basic "child_check"))
+ ("\nchildCmd = " ^ childCmd)
(* now get the number of the subgoal from the filename *)
val path_parts = String.tokens(fn c => c = #"/") childCmd
val digits = String.translate
(fn c => if Char.isDigit c then str c else "")
(List.last path_parts);
- val sg_num = (case Int.fromString digits of SOME n => n
- | NONE => error ("Watcher could not read subgoal nunber: " ^ childCmd));
-
+ val sg_num =
+ (case Int.fromString digits of SOME n => n
+ | NONE => (File.append (File.tmp_path (Path.basic "child_check"))
+ "\nWatcher could not read subgoal nunber!!";
+ raise ERROR));
val childIncoming = pollChildInput childInput
- val _ = File.append (File.tmp_path (Path.basic "child_check_polled"))
- ("finished polling child \n")
+ val _ = File.append (File.tmp_path (Path.basic "child_check"))
+ "\nfinished polling child"
val parentID = Posix.ProcEnv.getppid()
val prover = cmdProver 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 prems_string = prems_string_of thm
val goalstring = cmdGoal childProc
- val _ = File.append (File.tmp_path (Path.basic "child_comms"))
- (prover^goalstring^childCmd^"\n")
+ val _ = File.append (File.tmp_path (Path.basic "child_check"))
+ ("\nsubgoals forked to checkChildren: " ^
+ space_implode "\n" [prems_string,prover,goalstring])
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^goalstring^childCmd)
+ let val _ = File.append (File.tmp_path (Path.basic "child_check"))
+ "\nInput available from childIncoming"
val childDone = (case prover of
- "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) )
+ "vampire" => AtpCommunication.checkVampProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr)
+ | "E" => AtpCommunication.checkEProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr)
+ |"spass" => AtpCommunication.checkSpassProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr) )
in
- if childDone (**********************************************)
+ if childDone
then (* child has found a proof and transferred it *)
(* Remove this child and go on to check others*)
(**********************************************)
@@ -419,7 +418,8 @@
(childProc::(checkChildren (otherChildren, toParentStr)))
end
else
- (File.append (File.tmp_path (Path.basic "child_incoming")) "No child output ";
+ (File.append (File.tmp_path (Path.basic "child_check"))
+ "No child output";
childProc::(checkChildren (otherChildren, toParentStr)))
end
@@ -509,12 +509,12 @@
let
val newProcList = execCmds (valOf cmdsFromIsa) procList
val parentID = Posix.ProcEnv.getppid()
- val _ = (File.append (File.tmp_path (Path.basic "prekeep_watch")) "Just execed a child\n ")
- val newProcList' =checkChildren (newProcList, toParentStr)
-
- val _ = debug("off to keep watching...")
- val _ = (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching...\n ")
+ val _ = File.append (File.tmp_path (Path.basic "prekeep_watch"))
+ "Just execed a child\n"
+ val newProcList' = checkChildren (newProcList, toParentStr)
in
+ File.append (File.tmp_path (Path.basic "keep_watch"))
+ "Off to keep watching...\n";
loop newProcList'
end
else (* Execute remotely *)
@@ -529,7 +529,7 @@
else (* No new input from Isabelle *)
let val newProcList = checkChildren (procList, toParentStr)
in
- (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching.2..\n ");
+ (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching...2\n ");
loop newProcList
end
end
@@ -602,20 +602,14 @@
(* Start a watcher and set up signal handlers *)
(**********************************************************)
-fun killWatcher pid= Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill);
+fun killWatcher pid = Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill);
fun reapWatcher(pid, instr, outstr) =
- let val u = TextIO.closeIn instr;
- val u = TextIO.closeOut outstr;
- val (_, status) = Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
- in
- status
- end
+ (TextIO.closeIn instr; TextIO.closeOut outstr;
+ Posix.Process.waitpid(Posix.Process.W_CHILD pid, []); ())
-
-fun createWatcher (thm,clause_arr, num_of_clauses) =
- let val (childpid,(childin,childout)) =
- childInfo (setupWatcher(thm,clause_arr, num_of_clauses))
+fun createWatcher (thm, clause_arr) =
+ let val (childpid,(childin,childout)) = childInfo (setupWatcher(thm,clause_arr))
fun decr_watched() =
(goals_being_watched := (!goals_being_watched) - 1;
if !goals_being_watched = 0
@@ -623,63 +617,54 @@
(File.append (File.tmp_path (Path.basic "reap_found"))
("Reaping a watcher, childpid = "^
LargeWord.toString (Posix.Process.pidToWord childpid)^"\n");
- killWatcher childpid; reapWatcher (childpid,childin, childout); ())
+ killWatcher childpid; reapWatcher (childpid,childin, childout))
else ())
- 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 createWatcher: "^prems_string);
-(*FIXME: do we need an E proofHandler??*)
- fun vampire_proofHandler n =
- (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"))
- "Starting SPASS signal handler\n"
- 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))
+ val _ = debug ("subgoals forked to createWatcher: "^ prems_string_of thm);
+ fun proofHandler n =
+ let val outcome = TextIO.inputLine childin
+ val goalstring = TextIO.inputLine childin
+ val _ = debug ("In signal handler. outcome = \"" ^ outcome ^
+ "\"\ngoalstring = " ^ goalstring ^
+ "\ngoals_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) = "["
+ if String.isPrefix "[" outcome
then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
- Recon_Transfer.apply_res_thm reconstr goalstring;
+ Recon_Transfer.apply_res_thm outcome goalstring;
Pretty.writeln(Pretty.str (oct_char "361"));
decr_watched())
- (* if there's no proof, but a message from Spass *)
- else if substring (reconstr, 0,5) = "SPASS"
+ (* if there's no proof, but a message from the signalling process*)
+ else if String.isPrefix "Invalid" outcome
then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
- Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring)^reconstr));
+ Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring)
+ ^ "is not provable"));
+ Pretty.writeln(Pretty.str (oct_char "361"));
+ decr_watched())
+ else if String.isPrefix "Failure" outcome
+ then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
+ Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring)
+ ^ "proof attempt failed"));
Pretty.writeln(Pretty.str (oct_char "361"));
decr_watched())
(* print out a list of rules used from clasimpset*)
- else if substring (reconstr, 0,5) = "Rules"
+ else if String.isPrefix "Success" outcome
then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
- Pretty.writeln(Pretty.str (goalstring^reconstr));
+ Pretty.writeln(Pretty.str (goalstring^outcome));
Pretty.writeln(Pretty.str (oct_char "361"));
decr_watched())
(* if proof translation failed *)
- else if substring (reconstr, 0,5) = "Proof"
+ else if String.isPrefix "Translation failed" outcome
then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
- Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
- Pretty.writeln(Pretty.str (oct_char "361"));
- decr_watched())
- else if substring (reconstr, 0,1) = "%"
- then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
- Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
+ Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks outcome)));
Pretty.writeln(Pretty.str (oct_char "361"));
decr_watched())
- else (* add something here ?*)
+ else
(Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
- Pretty.writeln(Pretty.str ("Ran out of options in handler"));
+ Pretty.writeln(Pretty.str ("System error in proof handler"));
Pretty.writeln(Pretty.str (oct_char "361"));
decr_watched())
- end)
-
- in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);
- IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler);
+ end
+ in IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler);
(childin, childout, childpid)
-
end
end (* structure Watcher *)
--- a/src/HOL/Tools/res_atp.ML Mon Sep 19 14:20:45 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML Mon Sep 19 15:12:13 2005 +0200
@@ -9,24 +9,30 @@
sig
val prover: string ref
val custom_spass: string list ref
+ val destdir: string ref
val hook_count: int ref
+ val problem_name: string ref
end;
structure ResAtp: RES_ATP =
struct
-
val call_atp = ref false;
val hook_count = ref 0;
-fun debug_tac tac = (debug "testing"; tac);
-
val prover = ref "E"; (* use E as the default prover *)
val custom_spass = (*specialized options for SPASS*)
ref ["Auto=0","-FullRed=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub",
"-DocProof","-TimeLimit=60"];
-val prob_file = File.tmp_path (Path.basic "prob");
+val destdir = ref ""; (*Empty means write files to /tmp*)
+val problem_name = ref "prob";
+
+fun prob_pathname() =
+ if !destdir = "" then File.platform_path (File.tmp_path (Path.basic (!problem_name)))
+ else if File.exists (File.unpack_platform_path (!destdir))
+ then !destdir ^ "/" ^ !problem_name
+ else error ("No such directory: " ^ !destdir);
(**** for Isabelle/ML interface ****)
@@ -68,7 +74,7 @@
val _ = debug ("in tptp_inputs_tfrees 2")
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 probfile = prob_pathname() ^ "_" ^ string_of_int n
val out = TextIO.openOut(probfile)
in
ResLib.writeln_strs out (List.concat (map ResClause.tptp_clause axclauses));
@@ -85,7 +91,7 @@
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 probfile = prob_pathname() ^ "_" ^ (string_of_int n)
val _ = debug ("about to write out dfg prob file " ^ probfile)
val probN = ResClause.clauses2dfg clss ("prob" ^ (string_of_int n))
axclauses [] [] []
@@ -108,7 +114,7 @@
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 probfile = prob_pathname() ^ "_" ^ string_of_int n
val _ = debug ("prob file in watcher_call_provers is " ^ probfile)
in
(*Avoid command arguments containing spaces: Poly/ML and SML/NJ
@@ -116,7 +122,7 @@
if !prover = "spass"
then
let val optionline =
- if !SpassComm.reconstruct
+ if !AtpCommunication.reconstruct
(*Proof reconstruction works for only a limited set of
inference rules*)
then "-" ^ space_implode "%-" (!custom_spass)
@@ -170,30 +176,31 @@
());
+(*FIXME: WHAT IS THMS FOR????*)
+
(******************************************************************)
(* called in Isar automatically *)
(* writes out the current clasimpset to a tptp file *)
(* turns off xsymbol at start of function, restoring it at end *)
(******************************************************************)
(*FIX changed to clasimp_file *)
-val isar_atp' = setmp print_mode []
+val isar_atp = setmp print_mode []
(fn (ctxt, thms, thm) =>
if Thm.no_prems thm then ()
else
let
- val _= debug ("in isar_atp'")
+ val _= debug ("in isar_atp")
val thy = ProofContext.theory_of ctxt
val prems = Thm.prems_of thm
val thms_string = Meson.concat_with_and (map string_of_thm thms)
val prems_string = Meson.concat_with_and (map (Sign.string_of_term thy) prems)
(*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 (clause_arr, axclauses) = ResClasimp.get_clasimp_lemmas ctxt (hd prems)
+ (*FIXME: hack!! need to consider relevance for all prems*)
+ val _ = debug ("claset and simprules total clauses = " ^
+ string_of_int (Array.length clause_arr))
+ val (childin, childout, pid) = Watcher.createWatcher (thm, clause_arr)
val pid_string =
string_of_int (Word.toInt (Word.fromLargeWord (Posix.Process.pidToWord pid)))
in
@@ -205,43 +212,17 @@
end);
val isar_atp_writeonly = setmp print_mode []
- (fn (ctxt, thms, thm) =>
+ (fn (ctxt, thms: thm list, 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*)
+ let val prems = Thm.prems_of thm
+ val (_, axclauses) = ResClasimp.get_clasimp_lemmas ctxt (hd prems)
in
write_problem_files axclauses thm (length prems)
end);
-fun get_thms_cs claset =
- let val {safeEs, safeIs, hazEs, hazIs, ...} = rep_cs claset
- in safeEs @ safeIs @ hazEs @ hazIs end;
-fun append_name name [] _ = []
- | append_name name (thm :: thms) k =
- Thm.name_thm ((name ^ "_" ^ string_of_int k), thm) :: append_name name thms (k + 1);
-
-fun append_names (name :: names) (thms :: thmss) =
- append_name name thms 0 :: append_names names thmss;
-
-fun get_thms_ss [] = []
- | get_thms_ss thms =
- let
- val names = map Thm.name_of_thm thms
- val thms' = map (mksimps mksimps_pairs) thms
- val thms'' = append_names names thms'
- in
- ResLib.flat_noDup thms''
- end;
-
-
-(* convert locally declared rules to axiom clauses *)
+(* convert locally declared rules to axiom clauses: UNUSED *)
fun subtract_simpset thy ctxt =
let
@@ -265,12 +246,7 @@
val proof = Toplevel.proof_of state
val (ctxt, (_, goal)) = Proof.get_goal proof
handle Proof.STATE _ => error "No goal present";
-
val thy = ProofContext.theory_of ctxt;
-
- (* FIXME presently unused *)
- val ss_thms = subtract_simpset thy ctxt;
- val cs_thms = subtract_claset thy ctxt;
in
debug ("initial thm in isar_atp: " ^
Pretty.string_of (ProofContext.pretty_thm ctxt goal));
@@ -278,10 +254,12 @@
Pretty.string_of (ProofContext.pretty_term ctxt
(Logic.mk_conjunction_list (Thm.prems_of goal))));
debug ("number of subgoals in isar_atp: " ^ string_of_int (Thm.nprems_of goal));
+ debug ("current theory: " ^ Context.theory_name thy);
hook_count := !hook_count +1;
debug ("in hook for time: " ^(string_of_int (!hook_count)) );
ResClause.init thy;
- isar_atp' (ctxt, ProofContext.prems_of ctxt, goal)
+ if !destdir = "" then isar_atp (ctxt, ProofContext.prems_of ctxt, goal)
+ else isar_atp_writeonly (ctxt, ProofContext.prems_of ctxt, goal)
end);
val call_atpP =
--- a/src/HOL/Tools/res_axioms.ML Mon Sep 19 14:20:45 2005 +0200
+++ b/src/HOL/Tools/res_axioms.ML Mon Sep 19 15:12:13 2005 +0200
@@ -18,7 +18,10 @@
val rm_Eps : (term * term) list -> thm list -> term list
val claset_rules_of_thy : theory -> (string * thm) list
val simpset_rules_of_thy : theory -> (string * thm) list
- val clausify_rules_pairs : (string*thm) list -> thm list -> (ResClause.clause*thm) list list * thm list
+ val claset_rules_of_ctxt: Proof.context -> (string * thm) list
+ val simpset_rules_of_ctxt : Proof.context -> (string * thm) list
+ val clausify_rules_pairs :
+ (string*thm) list -> thm list -> (ResClause.clause*thm) list list * thm list
val clause_setup : (theory -> theory) list
val meson_method_setup : (theory -> theory) list
end;
@@ -357,19 +360,31 @@
val tag_intro = preserve_name (fn th => th RS tagI);
val tag_elim = preserve_name (fn th => tagD RS th);
-fun claset_rules_of_thy thy =
- let val cs = rep_cs (claset_of thy)
- val intros = (#safeIs cs) @ (#hazIs cs)
- val elims = (#safeEs cs) @ (#hazEs cs)
+fun rules_of_claset cs =
+ let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs
+ val intros = safeIs @ hazIs
+ val elims = safeEs @ hazEs
in
+ debug ("rules_of_claset intros: " ^ Int.toString(length intros) ^
+ " elims: " ^ Int.toString(length elims));
if tagging_enabled
then map pairname (map tag_intro intros @ map tag_elim elims)
- else map pairname (intros @ elims)
+ else map pairname (intros @ elims)
end;
-fun simpset_rules_of_thy thy =
- let val rules = #rules (fst (rep_ss (simpset_of thy)))
- in map (fn r => (#name r, #thm r)) (Net.entries rules) end;
+fun rules_of_simpset ss =
+ let val ({rules,...}, _) = rep_ss ss
+ val simps = Net.entries rules
+ in
+ debug ("rules_of_simpset: " ^ Int.toString(length simps));
+ map (fn r => (#name r, #thm r)) simps
+ end;
+
+fun claset_rules_of_thy thy = rules_of_claset (claset_of thy);
+fun simpset_rules_of_thy thy = rules_of_simpset (simpset_of thy);
+
+fun claset_rules_of_ctxt ctxt = rules_of_claset (local_claset_of ctxt);
+fun simpset_rules_of_ctxt ctxt = rules_of_simpset (local_simpset_of ctxt);
(**** Translate a set of classical/simplifier rules into CNF (still as type "thm") ****)