change from "Array" to "Vector"
authorpaulson
Wed Dec 20 17:03:46 2006 +0100 (2006-12-20)
changeset 21888c75a44597fb7
parent 21887 b1137bd73012
child 21889 682dbe947862
change from "Array" to "Vector"
src/HOL/Tools/ATP/AtpCommunication.ML
src/HOL/Tools/ATP/watcher.ML
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/ATP/AtpCommunication.ML	Tue Dec 19 19:34:35 2006 +0100
     1.2 +++ b/src/HOL/Tools/ATP/AtpCommunication.ML	Wed Dec 20 17:03:46 2006 +0100
     1.3 @@ -11,13 +11,13 @@
     1.4    sig
     1.5      val checkEProofFound: 
     1.6            TextIO.instream * TextIO.outstream * Posix.Process.pid * 
     1.7 -          string * string Array.array -> bool
     1.8 +          string * string Vector.vector -> bool
     1.9      val checkVampProofFound: 
    1.10            TextIO.instream * TextIO.outstream * Posix.Process.pid * 
    1.11 -          string * string Array.array -> bool
    1.12 +          string * string Vector.vector -> bool
    1.13      val checkSpassProofFound:  
    1.14            TextIO.instream * TextIO.outstream * Posix.Process.pid * 
    1.15 -          string * thm * int * string Array.array -> bool
    1.16 +          string * thm * int * string Vector.vector -> bool
    1.17      val signal_parent:  
    1.18            TextIO.outstream * Posix.Process.pid * string * string -> unit
    1.19    end;
    1.20 @@ -35,10 +35,10 @@
    1.21  
    1.22  (**** retrieve the axioms that were used in the proof ****)
    1.23  
    1.24 -(*Get names of axioms used. Axioms are indexed from 1, while the array is indexed from 0*)
    1.25 -fun get_axiom_names (names_arr: string array) step_nums = 
    1.26 -    let fun is_axiom n = n <= Array.length names_arr 
    1.27 -        fun index i = Array.sub(names_arr, i-1)
    1.28 +(*Get names of axioms used. Axioms are indexed from 1, while the vector is indexed from 0*)
    1.29 +fun get_axiom_names (thm_names: string vector) step_nums = 
    1.30 +    let fun is_axiom n = n <= Vector.length thm_names 
    1.31 +        fun index i = Vector.sub(thm_names, i-1)
    1.32          val axnums = List.filter is_axiom step_nums
    1.33          val axnames = sort_distinct string_ord (map index axnums)
    1.34      in
    1.35 @@ -56,8 +56,8 @@
    1.36        val lines = String.tokens (fn c => c = #"\n") proofstr
    1.37    in  List.mapPartial (inputno o toks) lines  end
    1.38  
    1.39 -fun get_axiom_names_spass proofstr names_arr =
    1.40 -   get_axiom_names names_arr (get_spass_linenums proofstr);
    1.41 +fun get_axiom_names_spass proofstr thm_names =
    1.42 +   get_axiom_names thm_names (get_spass_linenums proofstr);
    1.43      
    1.44   (*String contains multiple lines. We want those of the form 
    1.45     "number : ...: ...: initial..." *)
    1.46 @@ -71,8 +71,8 @@
    1.47        val lines = String.tokens (fn c => c = #"\n") proofstr
    1.48    in  List.mapPartial (firstno o fields) lines  end
    1.49  
    1.50 -fun get_axiom_names_e proofstr names_arr =
    1.51 -   get_axiom_names names_arr (get_e_linenums proofstr);
    1.52 +fun get_axiom_names_e proofstr thm_names =
    1.53 +   get_axiom_names thm_names (get_e_linenums proofstr);
    1.54      
    1.55   (*String contains multiple lines. We want those of the form 
    1.56       "*********** [448, input] ***********".
    1.57 @@ -84,20 +84,20 @@
    1.58        val lines = String.tokens (fn c => c = #"\n") proofstr
    1.59    in  List.mapPartial (inputno o toks) lines  end
    1.60  
    1.61 -fun get_axiom_names_vamp proofstr names_arr =
    1.62 -   get_axiom_names names_arr (get_vamp_linenums proofstr);
    1.63 +fun get_axiom_names_vamp proofstr thm_names =
    1.64 +   get_axiom_names thm_names (get_vamp_linenums proofstr);
    1.65      
    1.66  fun rules_to_string [] = "NONE"
    1.67    | rules_to_string xs = space_implode "  " xs
    1.68  
    1.69  
    1.70  (*The signal handler in watcher.ML must be able to read the output of this.*)
    1.71 -fun prover_lemma_list_aux getax proofstr probfile toParent ppid names_arr = 
    1.72 +fun prover_lemma_list_aux getax proofstr probfile toParent ppid thm_names = 
    1.73   let val _ = trace
    1.74                 ("\n\nGetting lemma names. proofstr is " ^ proofstr ^
    1.75                  "\nprobfile is " ^ probfile ^
    1.76 -                "  num of clauses is " ^ string_of_int (Array.length names_arr))
    1.77 -     val axiom_names = getax proofstr names_arr
    1.78 +                "  num of clauses is " ^ string_of_int (Vector.length thm_names))
    1.79 +     val axiom_names = getax proofstr thm_names
    1.80       val ax_str = rules_to_string axiom_names
    1.81      in 
    1.82  	 trace ("\nDone. Lemma list is " ^ ax_str);
    1.83 @@ -145,7 +145,7 @@
    1.84  (*  and if so, transfer output to the input pipe of the main Isabelle process    *)
    1.85  (*********************************************************************************)
    1.86  
    1.87 -fun startTransfer (endS, fromChild, toParent, ppid, probfile, names_arr) =
    1.88 +fun startTransfer (endS, fromChild, toParent, ppid, probfile, thm_names) =
    1.89   let fun transferInput currentString =
    1.90        let val thisLine = TextIO.inputLine fromChild
    1.91        in
    1.92 @@ -159,7 +159,7 @@
    1.93  			  	  else e_lemma_list
    1.94  	     in
    1.95  	       trace ("\nExtracted proof:\n" ^ proofextract); 
    1.96 -	       lemma_list proofextract probfile toParent ppid names_arr
    1.97 +	       lemma_list proofextract probfile toParent ppid thm_names
    1.98  	     end
    1.99  	else transferInput (currentString^thisLine)
   1.100        end
   1.101 @@ -179,41 +179,41 @@
   1.102    OS.Process.sleep (Time.fromMilliseconds 600));
   1.103  
   1.104  (*Called from watcher. Returns true if the Vampire process has returned a verdict.*)
   1.105 -fun checkVampProofFound (fromChild, toParent, ppid, probfile, names_arr) =
   1.106 +fun checkVampProofFound (fromChild, toParent, ppid, probfile, thm_names) =
   1.107   let val thisLine = TextIO.inputLine fromChild
   1.108   in   
   1.109       trace thisLine;
   1.110       if thisLine = "" 
   1.111       then (trace "\nNo proof output seen"; false)
   1.112       else if String.isPrefix start_V8 thisLine
   1.113 -     then startTransfer (end_V8, fromChild, toParent, ppid, probfile, names_arr)
   1.114 +     then startTransfer (end_V8, fromChild, toParent, ppid, probfile, thm_names)
   1.115       else if (String.isPrefix "Satisfiability detected" thisLine) orelse
   1.116               (String.isPrefix "Refutation not found" thisLine)
   1.117       then (signal_parent (toParent, ppid, "Failure\n", probfile);
   1.118  	   true)
   1.119 -     else checkVampProofFound  (fromChild, toParent, ppid, probfile, names_arr)
   1.120 +     else checkVampProofFound  (fromChild, toParent, ppid, probfile, thm_names)
   1.121    end
   1.122  
   1.123  (*Called from watcher. Returns true if the E process has returned a verdict.*)
   1.124 -fun checkEProofFound (fromChild, toParent, ppid, probfile, names_arr) = 
   1.125 +fun checkEProofFound (fromChild, toParent, ppid, probfile, thm_names) = 
   1.126   let val thisLine = TextIO.inputLine fromChild  
   1.127   in   
   1.128       trace thisLine;
   1.129       if thisLine = "" then (trace "\nNo proof output seen"; false)
   1.130       else if String.isPrefix start_E thisLine
   1.131 -     then startTransfer (end_E, fromChild, toParent, ppid, probfile, names_arr)
   1.132 +     then startTransfer (end_E, fromChild, toParent, ppid, probfile, thm_names)
   1.133       else if String.isPrefix "# Problem is satisfiable" thisLine
   1.134       then (signal_parent (toParent, ppid, "Invalid\n", probfile);
   1.135  	   true)
   1.136       else if String.isPrefix "# Cannot determine problem status within resource limit" thisLine
   1.137       then (signal_parent (toParent, ppid, "Failure\n", probfile);
   1.138  	   true)
   1.139 -     else checkEProofFound (fromChild, toParent, ppid, probfile, names_arr)
   1.140 +     else checkEProofFound (fromChild, toParent, ppid, probfile, thm_names)
   1.141   end
   1.142  
   1.143  (*FIXME: can't these two functions be replaced by startTransfer above?*)
   1.144  fun transferSpassInput (fromChild, toParent, ppid, probfile,
   1.145 -                        currentString, thm, sg_num, names_arr) = 
   1.146 +                        currentString, thm, sg_num, thm_names) = 
   1.147   let val thisLine = TextIO.inputLine fromChild 
   1.148   in 
   1.149      trace thisLine;
   1.150 @@ -225,36 +225,36 @@
   1.151        let val proofextract = currentString ^ cut_before end_SPASS thisLine
   1.152        in 
   1.153  	 trace ("\nextracted spass proof: " ^ proofextract);
   1.154 -	 spass_lemma_list proofextract probfile toParent ppid names_arr 
   1.155 +	 spass_lemma_list proofextract probfile toParent ppid thm_names 
   1.156        end
   1.157      else transferSpassInput (fromChild, toParent, ppid, probfile,
   1.158 -			     currentString ^ thisLine, thm, sg_num, names_arr)
   1.159 +			     currentString ^ thisLine, thm, sg_num, thm_names)
   1.160   end;
   1.161  
   1.162  (*Inspect the output of a SPASS process to see if it has found a proof,   
   1.163    and if so, transfer output to the input pipe of the main Isabelle process*)
   1.164 -fun startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num,names_arr) = 
   1.165 +fun startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num,thm_names) = 
   1.166     let val thisLine = TextIO.inputLine fromChild  
   1.167     in                 
   1.168        if thisLine = "" then false
   1.169        else if String.isPrefix "Here is a proof" thisLine then     
   1.170  	 (trace ("\nabout to transfer SPASS proof:\n");
   1.171  	  transferSpassInput (fromChild, toParent, ppid, probfile, thisLine, 
   1.172 - 	                     thm, sg_num,names_arr);
   1.173 + 	                     thm, sg_num,thm_names);
   1.174  	  true) handle EOF => false
   1.175 -      else startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num,names_arr)
   1.176 +      else startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num,thm_names)
   1.177      end
   1.178  
   1.179  
   1.180  (*Called from watcher. Returns true if the SPASS process has returned a verdict.*)
   1.181 -fun checkSpassProofFound (fromChild, toParent, ppid, probfile, thm, sg_num, names_arr) = 
   1.182 +fun checkSpassProofFound (fromChild, toParent, ppid, probfile, thm, sg_num, thm_names) = 
   1.183   let val thisLine = TextIO.inputLine fromChild  
   1.184   in    
   1.185       trace thisLine;
   1.186       if thisLine = "" then (trace "\nNo proof output seen"; false)
   1.187       else if thisLine = "SPASS beiseite: Proof found.\n"
   1.188       then      
   1.189 -        startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num, names_arr)
   1.190 +        startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num, thm_names)
   1.191       else if thisLine = "SPASS beiseite: Completion found.\n"
   1.192       then (signal_parent (toParent, ppid, "Invalid\n", probfile);
   1.193  	   true)
   1.194 @@ -262,7 +262,7 @@
   1.195               thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n"
   1.196       then (signal_parent (toParent, ppid, "Failure\n", probfile);
   1.197  	   true)
   1.198 -    else checkSpassProofFound (fromChild, toParent, ppid, probfile, thm, sg_num, names_arr)
   1.199 +    else checkSpassProofFound (fromChild, toParent, ppid, probfile, thm, sg_num, thm_names)
   1.200   end
   1.201  
   1.202  end;
     2.1 --- a/src/HOL/Tools/ATP/watcher.ML	Tue Dec 19 19:34:35 2006 +0100
     2.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Wed Dec 20 17:03:46 2006 +0100
     2.3 @@ -23,7 +23,7 @@
     2.4  
     2.5  (* Start a watcher and set up signal handlers*)
     2.6  val createWatcher : 
     2.7 -	thm * string Array.array list -> 
     2.8 +	thm * string Vector.vector list -> 
     2.9  	TextIO.instream * TextIO.outstream * Posix.Process.pid
    2.10  val killWatcher : Posix.Process.pid -> unit
    2.11  val killChild  : ('a, 'b) Unix.proc -> OS.Process.status
     3.1 --- a/src/HOL/Tools/res_atp.ML	Tue Dec 19 19:34:35 2006 +0100
     3.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Dec 20 17:03:46 2006 +0100
     3.3 @@ -819,9 +819,9 @@
     3.4      Output.debug "Sent commands to watcher!"
     3.5    end
     3.6  
     3.7 -fun trace_array fname =
     3.8 +fun trace_vector fname =
     3.9    let val path = File.explode_platform_path fname
    3.10 -  in  Array.app (File.append path o (fn s => s ^ "\n"))  end;
    3.11 +  in  Vector.app (File.append path o (fn s => s ^ "\n"))  end;
    3.12  
    3.13  (*Converting a subgoal into negated conjecture clauses*)
    3.14  fun neg_clauses th n =
    3.15 @@ -873,9 +873,9 @@
    3.16                  val arity_clauses = ResClause.arity_clause_thy thy tycons supers
    3.17                  val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
    3.18                  val clnames = writer logic ccls fname (axcls,classrel_clauses,arity_clauses) []
    3.19 -                val thm_names = Array.fromList clnames
    3.20 +                val thm_names = Vector.fromList clnames
    3.21                  val _ = if !Output.show_debug_msgs
    3.22 -                        then trace_array (fname ^ "_thm_names") thm_names else ()
    3.23 +                        then trace_vector (fname ^ "_thm_names") thm_names else ()
    3.24              in  (thm_names,fname) :: write_all ccls_list axcls_list (k+1)  end
    3.25        val (thm_names_list, filenames) = ListPair.unzip (write_all goal_cls axcls_list 1)
    3.26    in