Proof reconstruction now only takes names of theorems as input.
authormengj
Tue Mar 07 04:01:25 2006 +0100 (2006-03-07)
changeset 19199b338c218cc6e
parent 19198 e6f1ff40ba99
child 19200 1da6b9a1575d
Proof reconstruction now only takes names of theorems as input.
src/HOL/Tools/ATP/AtpCommunication.ML
src/HOL/Tools/ATP/recon_transfer_proof.ML
src/HOL/Tools/ATP/watcher.ML
     1.1 --- a/src/HOL/Tools/ATP/AtpCommunication.ML	Tue Mar 07 03:59:48 2006 +0100
     1.2 +++ b/src/HOL/Tools/ATP/AtpCommunication.ML	Tue Mar 07 04:01:25 2006 +0100
     1.3 @@ -12,13 +12,13 @@
     1.4      val reconstruct : bool ref
     1.5      val checkEProofFound: 
     1.6            TextIO.instream * TextIO.outstream * Posix.Process.pid * 
     1.7 -          string * (ResClause.clause * thm) Array.array -> bool
     1.8 +          string * string Array.array -> bool
     1.9      val checkVampProofFound: 
    1.10            TextIO.instream * TextIO.outstream * Posix.Process.pid * 
    1.11 -          string * (ResClause.clause * thm) Array.array -> bool
    1.12 +          string * string Array.array -> bool
    1.13      val checkSpassProofFound:  
    1.14            TextIO.instream * TextIO.outstream * Posix.Process.pid * 
    1.15 -          string * thm * int * (ResClause.clause * thm) Array.array -> bool
    1.16 +          string * thm * int * string Array.array -> bool
    1.17      val signal_parent:  
    1.18            TextIO.outstream * Posix.Process.pid * string * string -> unit
    1.19    end;
    1.20 @@ -64,7 +64,7 @@
    1.21  (*  and if so, transfer output to the input pipe of the main Isabelle process    *)
    1.22  (*********************************************************************************)
    1.23  
    1.24 -fun startTransfer (endS, fromChild, toParent, ppid, probfile, clause_arr) =
    1.25 +fun startTransfer (endS, fromChild, toParent, ppid, probfile, names_arr) =
    1.26   let fun transferInput currentString =
    1.27        let val thisLine = TextIO.inputLine fromChild
    1.28        in
    1.29 @@ -79,7 +79,7 @@
    1.30  			  	  else Recon_Transfer.e_lemma_list
    1.31  	     in
    1.32  	       trace ("\nExtracted proof:\n" ^ proofextract); 
    1.33 -	       lemma_list proofextract probfile toParent ppid clause_arr
    1.34 +	       lemma_list proofextract probfile toParent ppid names_arr
    1.35  	     end
    1.36  	else transferInput (currentString^thisLine)
    1.37        end
    1.38 @@ -99,25 +99,25 @@
    1.39    OS.Process.sleep (Time.fromMilliseconds 600));
    1.40  
    1.41  (*Called from watcher. Returns true if the Vampire process has returned a verdict.*)
    1.42 -fun checkVampProofFound (fromChild, toParent, ppid, probfile, clause_arr) =
    1.43 +fun checkVampProofFound (fromChild, toParent, ppid, probfile, names_arr) =
    1.44   let val thisLine = TextIO.inputLine fromChild
    1.45   in   
    1.46       trace thisLine;
    1.47       if thisLine = "" 
    1.48       then (trace "\nNo proof output seen"; false)
    1.49       else if String.isPrefix start_V8 thisLine
    1.50 -     then startTransfer (end_V8, fromChild, toParent, ppid, probfile, clause_arr)
    1.51 +     then startTransfer (end_V8, fromChild, toParent, ppid, probfile, names_arr)
    1.52       else if (String.isPrefix "Satisfiability detected" thisLine) orelse
    1.53               (String.isPrefix "Refutation not found" thisLine)
    1.54       then (signal_parent (toParent, ppid, "Failure\n", probfile);
    1.55  	   true)
    1.56       else
    1.57 -        checkVampProofFound  (fromChild, toParent, ppid, probfile, clause_arr)
    1.58 +        checkVampProofFound  (fromChild, toParent, ppid, probfile, names_arr)
    1.59    end
    1.60  
    1.61  
    1.62  (*Called from watcher. Returns true if the E process has returned a verdict.*)
    1.63 -fun checkEProofFound (fromChild, toParent, ppid, probfile, clause_arr) = 
    1.64 +fun checkEProofFound (fromChild, toParent, ppid, probfile, names_arr) = 
    1.65   let val thisLine = TextIO.inputLine fromChild  
    1.66   in   
    1.67       trace thisLine;
    1.68 @@ -125,7 +125,7 @@
    1.69       then (trace "\nNo proof output seen"; false)
    1.70       else if String.isPrefix start_E thisLine
    1.71       then      
    1.72 -       startTransfer (end_E, fromChild, toParent, ppid, probfile, clause_arr)
    1.73 +       startTransfer (end_E, fromChild, toParent, ppid, probfile, names_arr)
    1.74       else if String.isPrefix "# Problem is satisfiable" thisLine
    1.75       then (signal_parent (toParent, ppid, "Invalid\n", probfile);
    1.76  	   true)
    1.77 @@ -133,7 +133,7 @@
    1.78       then (signal_parent (toParent, ppid, "Failure\n", probfile);
    1.79  	   true)
    1.80       else
    1.81 -	checkEProofFound (fromChild, toParent, ppid, probfile, clause_arr)
    1.82 +	checkEProofFound (fromChild, toParent, ppid, probfile, names_arr)
    1.83   end
    1.84  
    1.85  
    1.86 @@ -143,16 +143,16 @@
    1.87  (*  steps as a string to the input pipe of the main Isabelle process  *)
    1.88  (**********************************************************************)
    1.89  
    1.90 -fun spass_reconstruct_tac proofextract toParent ppid probfile sg_num clause_arr = 
    1.91 +fun spass_reconstruct_tac proofextract toParent ppid probfile sg_num names_arr = 
    1.92   SELECT_GOAL
    1.93    (EVERY1 [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac, 
    1.94  	   METAHYPS(fn negs => 
    1.95  		  Recon_Transfer.spass_reconstruct proofextract probfile 
    1.96 -				toParent ppid negs clause_arr)]) sg_num;
    1.97 +				toParent ppid negs names_arr)]) sg_num;
    1.98  
    1.99  
   1.100  fun transferSpassInput (fromChild, toParent, ppid, probfile,
   1.101 -                        currentString, thm, sg_num, clause_arr) = 
   1.102 +                        currentString, thm, sg_num, names_arr) = 
   1.103   let val thisLine = TextIO.inputLine fromChild 
   1.104   in 
   1.105      trace thisLine;
   1.106 @@ -166,12 +166,12 @@
   1.107  	 trace ("\nextracted spass proof: " ^ proofextract);
   1.108  	 if !reconstruct 
   1.109  	 then (spass_reconstruct_tac proofextract toParent ppid probfile sg_num 
   1.110 -		clause_arr thm; ())
   1.111 +		names_arr thm; ())
   1.112  	 else Recon_Transfer.spass_lemma_list proofextract probfile toParent
   1.113 -	        ppid clause_arr 
   1.114 +	        ppid names_arr 
   1.115        end
   1.116      else transferSpassInput (fromChild, toParent, ppid, probfile,
   1.117 -			     (currentString^thisLine), thm, sg_num, clause_arr)
   1.118 +			     (currentString^thisLine), thm, sg_num, names_arr)
   1.119   end;
   1.120  
   1.121  
   1.122 @@ -182,29 +182,29 @@
   1.123  
   1.124   
   1.125  fun startSpassTransfer (fromChild, toParent, ppid, probfile,
   1.126 -                        thm, sg_num,clause_arr) = 
   1.127 +                        thm, sg_num,names_arr) = 
   1.128     let val thisLine = TextIO.inputLine fromChild  
   1.129     in                 
   1.130        if thisLine = "" then false
   1.131        else if String.isPrefix "Here is a proof" thisLine then     
   1.132  	 (trace ("\nabout to transfer SPASS proof:\n");
   1.133  	  transferSpassInput (fromChild, toParent, ppid, probfile, thisLine, 
   1.134 - 	                     thm, sg_num,clause_arr);
   1.135 + 	                     thm, sg_num,names_arr);
   1.136  	  true) handle EOF => false
   1.137 -      else startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num,clause_arr)
   1.138 +      else startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num,names_arr)
   1.139      end
   1.140  
   1.141  
   1.142  (*Called from watcher. Returns true if the SPASS process has returned a verdict.*)
   1.143  fun checkSpassProofFound (fromChild, toParent, ppid, probfile,
   1.144 -                          thm, sg_num, clause_arr) = 
   1.145 +                          thm, sg_num, names_arr) = 
   1.146   let val thisLine = TextIO.inputLine fromChild  
   1.147   in    
   1.148       trace thisLine;
   1.149       if thisLine = "" then (trace "\nNo proof output seen"; false)
   1.150       else if thisLine = "SPASS beiseite: Proof found.\n"
   1.151       then      
   1.152 -        startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num, clause_arr)
   1.153 +        startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num, names_arr)
   1.154       else if thisLine = "SPASS beiseite: Completion found.\n"
   1.155       then (signal_parent (toParent, ppid, "Invalid\n", probfile);
   1.156  	   true)
   1.157 @@ -212,7 +212,7 @@
   1.158               thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n"
   1.159       then (signal_parent (toParent, ppid, "Failure\n", probfile);
   1.160  	   true)
   1.161 -    else checkSpassProofFound (fromChild, toParent, ppid, probfile, thm, sg_num, clause_arr)
   1.162 +    else checkSpassProofFound (fromChild, toParent, ppid, probfile, thm, sg_num, names_arr)
   1.163   end
   1.164  
   1.165  end;
     2.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Tue Mar 07 03:59:48 2006 +0100
     2.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Tue Mar 07 04:01:25 2006 +0100
     2.3 @@ -149,17 +149,17 @@
     2.4  
     2.5  (* retrieve the axioms that were obtained from the clasimpset *)
     2.6  
     2.7 -fun get_clasimp_cls (clause_arr: (ResClause.clause * thm) array) step_nums = 
     2.8 -    let val clasimp_nums = List.filter (is_clasimp_ax (Array.length clause_arr - 1)) 
     2.9 +fun get_clasimp_cls (names_arr: string array) step_nums = 
    2.10 +    let val clasimp_nums = List.filter (is_clasimp_ax (Array.length names_arr - 1)) 
    2.11  	                   (map subone step_nums)
    2.12      in
    2.13 -	map (fn x =>  Array.sub(clause_arr, x)) clasimp_nums
    2.14 +	map (fn x =>  Array.sub(names_arr, x)) clasimp_nums
    2.15      end
    2.16  
    2.17  (* get names of clasimp axioms used*)
    2.18 -fun get_axiom_names step_nums clause_arr =
    2.19 +fun get_axiom_names step_nums names_arr =
    2.20    sort_distinct string_ord
    2.21 -    (map (ResClause.get_axiomName o #1) (get_clasimp_cls clause_arr step_nums));
    2.22 +    (get_clasimp_cls names_arr step_nums);
    2.23  
    2.24   (*String contains multiple lines. We want those of the form 
    2.25       "253[0:Inp] et cetera..."
    2.26 @@ -171,8 +171,8 @@
    2.27        val lines = String.tokens (fn c => c = #"\n") proofstr
    2.28    in  List.mapPartial (inputno o toks) lines  end
    2.29  
    2.30 -fun get_axiom_names_spass proofstr clause_arr  =
    2.31 -   get_axiom_names (get_spass_linenums proofstr) clause_arr;
    2.32 +fun get_axiom_names_spass proofstr names_arr  =
    2.33 +   get_axiom_names (get_spass_linenums proofstr) names_arr;
    2.34      
    2.35   (*String contains multiple lines.
    2.36    A list consisting of the first number in each line is returned. *)
    2.37 @@ -183,8 +183,8 @@
    2.38        val lines = String.tokens (fn c => c = #"\n") proofstr
    2.39    in  List.mapPartial (firstno o numerics) lines  end
    2.40  
    2.41 -fun get_axiom_names_e proofstr clause_arr  =
    2.42 -   get_axiom_names (get_linenums proofstr) clause_arr;
    2.43 +fun get_axiom_names_e proofstr names_arr  =
    2.44 +   get_axiom_names (get_linenums proofstr) names_arr;
    2.45      
    2.46   (*String contains multiple lines. We want those of the form 
    2.47       "*********** [448, input] ***********".
    2.48 @@ -196,8 +196,8 @@
    2.49        val lines = String.tokens (fn c => c = #"\n") proofstr
    2.50    in  List.mapPartial (inputno o toks) lines  end
    2.51  
    2.52 -fun get_axiom_names_vamp proofstr clause_arr  =
    2.53 -   get_axiom_names (get_vamp_linenums proofstr) clause_arr;
    2.54 +fun get_axiom_names_vamp proofstr names_arr  =
    2.55 +   get_axiom_names (get_vamp_linenums proofstr) names_arr;
    2.56      
    2.57  
    2.58  (***********************************************)
    2.59 @@ -212,7 +212,7 @@
    2.60  
    2.61  fun addvars c (a,b)  = (a,b,c)
    2.62  
    2.63 -fun get_axioms_used proof_steps thms clause_arr  =
    2.64 +fun get_axioms_used proof_steps thms names_arr  =
    2.65   let val axioms = (List.filter is_axiom) proof_steps
    2.66       val step_nums = get_step_nums axioms []
    2.67  
    2.68 @@ -265,12 +265,12 @@
    2.69  
    2.70  
    2.71  (*The signal handler in watcher.ML must be able to read the output of this.*)
    2.72 -fun prover_lemma_list_aux getax proofstr probfile toParent ppid clause_arr = 
    2.73 +fun prover_lemma_list_aux getax proofstr probfile toParent ppid names_arr = 
    2.74   let val _ = trace
    2.75                 ("\n\nGetting lemma names. proofstr is " ^ proofstr ^
    2.76                  "\nprobfile is " ^ probfile ^
    2.77 -                "  num of clauses is " ^ string_of_int (Array.length clause_arr))
    2.78 -     val axiom_names = getax proofstr clause_arr
    2.79 +                "  num of clauses is " ^ string_of_int (Array.length names_arr))
    2.80 +     val axiom_names = getax proofstr names_arr
    2.81       val ax_str = rules_to_string axiom_names
    2.82      in 
    2.83  	 trace ("\nDone. Lemma list is " ^ ax_str);
    2.84 @@ -298,7 +298,7 @@
    2.85  
    2.86  (**** Full proof reconstruction for SPASS (not really working) ****)
    2.87  
    2.88 -fun spass_reconstruct proofstr probfile toParent ppid thms clause_arr = 
    2.89 +fun spass_reconstruct proofstr probfile toParent ppid thms names_arr = 
    2.90    let val _ = trace ("\nspass_reconstruct. Proofstr is "^proofstr)
    2.91        val tokens = #1(lex proofstr)
    2.92  
    2.93 @@ -315,7 +315,7 @@
    2.94        (* subgoal this is, and turn it into meta_clauses *)
    2.95        (* should prob add array and table here, so that we can get axioms*)
    2.96        (* produced from the clasimpset rather than the problem *)
    2.97 -      val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps  thms clause_arr
    2.98 +      val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps  thms names_arr
    2.99        
   2.100        (*val numcls_string = numclstr ( vars, numcls) ""*)
   2.101        val _ = trace "\ngot axioms"
     3.1 --- a/src/HOL/Tools/ATP/watcher.ML	Tue Mar 07 03:59:48 2006 +0100
     3.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Tue Mar 07 04:01:25 2006 +0100
     3.3 @@ -23,7 +23,7 @@
     3.4  
     3.5  (* Start a watcher and set up signal handlers             *)
     3.6  val createWatcher : 
     3.7 -    thm * (ResClause.clause * thm) Array.array -> 
     3.8 +    thm * string Array.array -> 
     3.9      TextIO.instream * TextIO.outstream * Posix.Process.pid
    3.10  val killWatcher : Posix.Process.pid -> unit
    3.11  val setting_sep : char
    3.12 @@ -206,7 +206,7 @@
    3.13  			 Date.toString(Date.fromTimeLocal(Time.now())))
    3.14        in execCmds cmds newProcList end
    3.15  
    3.16 -fun checkChildren (th, clause_arr, toParentStr, children) = 
    3.17 +fun checkChildren (th, names_arr, toParentStr, children) = 
    3.18    let fun check [] = []  (* no children to check *)
    3.19  	| check (child::children) = 
    3.20  	   let val {prover, file, proc_handle, instr=childIn, ...} : cmdproc =
    3.21 @@ -220,11 +220,11 @@
    3.22  	       let val _ = trace ("\nInput available from child: " ^ file)
    3.23  		   val childDone = (case prover of
    3.24  		       "vampire" => AtpCommunication.checkVampProofFound
    3.25 -			    (childIn, toParentStr, ppid, file, clause_arr)  
    3.26 +			    (childIn, toParentStr, ppid, file, names_arr)  
    3.27  		     | "E" => AtpCommunication.checkEProofFound
    3.28 -			    (childIn, toParentStr, ppid, file, clause_arr)             
    3.29 +			    (childIn, toParentStr, ppid, file, names_arr)             
    3.30  		     | "spass" => AtpCommunication.checkSpassProofFound
    3.31 -			    (childIn, toParentStr, ppid, file, th, sgno,clause_arr)  
    3.32 +			    (childIn, toParentStr, ppid, file, th, sgno,names_arr)  
    3.33  		     | _ => (trace ("\nBad prover! " ^ prover); true) )
    3.34  		in
    3.35  		 if childDone (*child has found a proof and transferred it*)
    3.36 @@ -240,7 +240,7 @@
    3.37    end;
    3.38  
    3.39  
    3.40 -fun setupWatcher (th,clause_arr) = 
    3.41 +fun setupWatcher (th,names_arr) = 
    3.42    let
    3.43      val p1 = Posix.IO.pipe()   (*pipes for communication between parent and watcher*)
    3.44      val p2 = Posix.IO.pipe()
    3.45 @@ -277,16 +277,16 @@
    3.46  		    if length procList < 40 then    (* Execute locally  *)                    
    3.47  		      let val _ = trace("\nCommands from parent: " ^ 
    3.48  					Int.toString(length cmds))
    3.49 -			  val newProcList' = checkChildren(th, clause_arr, toParentStr, 
    3.50 +			  val newProcList' = checkChildren(th, names_arr, toParentStr, 
    3.51  						execCmds cmds procList) 
    3.52  		      in trace "\nCommands executed"; keepWatching newProcList' end
    3.53  		    else  (* Execute remotely [FIXME: NOT REALLY]  *)
    3.54 -		      let val newProcList' = checkChildren (th, clause_arr, toParentStr, 
    3.55 +		      let val newProcList' = checkChildren (th, names_arr, toParentStr, 
    3.56  						execCmds cmds procList) 
    3.57  		      in keepWatching newProcList' end
    3.58  		| NONE => (* No new input from Isabelle *)
    3.59  		    (trace "\nNothing from parent...";  
    3.60 -		     keepWatching(checkChildren(th, clause_arr, toParentStr, procList))))
    3.61 +		     keepWatching(checkChildren(th, names_arr, toParentStr, procList))))
    3.62  	     handle exn => (*FIXME: exn handler is too general!*)
    3.63  	       (trace ("\nkeepWatching exception handler: " ^ Toplevel.exn_message exn);
    3.64  		keepWatching procList);
    3.65 @@ -344,8 +344,8 @@
    3.66  
    3.67  fun prems_string_of th = space_implode "\n" (map string_of_cterm (cprems_of th))
    3.68  
    3.69 -fun createWatcher (th, clause_arr) =
    3.70 - let val {pid=childpid, instr=childin, outstr=childout} = setupWatcher (th,clause_arr)
    3.71 +fun createWatcher (th, names_arr) =
    3.72 + let val {pid=childpid, instr=childin, outstr=childout} = setupWatcher (th,names_arr)
    3.73       fun decr_watched() =
    3.74  	  (goals_being_watched := !goals_being_watched - 1;
    3.75  	   if !goals_being_watched = 0