further tidying up of Isabelle-ATP link
authorpaulson
Fri Sep 02 17:55:24 2005 +0200 (2005-09-02)
changeset 1723412a9393c5d77
parent 17233 41eee2e7b465
child 17235 8e55ad29b690
further tidying up of Isabelle-ATP link
src/HOL/Tools/ATP/res_clasimpset.ML
src/HOL/Tools/ATP/watcher.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_clause.ML
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Sep 02 17:23:59 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Sep 02 17:55:24 2005 +0200
     1.3 @@ -6,7 +6,9 @@
     1.4  
     1.5  structure ReduceAxiomsN =
     1.6  (* Author: Jia Meng, Cambridge University Computer Laboratory
     1.7 -   Remove irrelevant axioms used for a proof of a goal, with with iteration control*)
     1.8 +   Remove irrelevant axioms used for a proof of a goal, with with iteration control
     1.9 +   
    1.10 +   Initial version. Needs elaboration. *)
    1.11  
    1.12  struct
    1.13  
    1.14 @@ -143,31 +145,6 @@
    1.15  (* outputs a list of (thm,clause) pairs *)
    1.16  
    1.17  
    1.18 -(* for tracing: encloses each string element in brackets. *)
    1.19 -fun concat_with_stop [] = ""
    1.20 -  | concat_with_stop [x] =  x
    1.21 -  | concat_with_stop (x::xs) = x^ "." ^ concat_with_stop xs;
    1.22 -
    1.23 -fun remove_symb str = 
    1.24 -    if String.isPrefix  "List.op @." str
    1.25 -    then  ((String.substring(str,0,5)) ^ (String.extract (str, 10, NONE)))
    1.26 -    else str;
    1.27 -
    1.28 -(*FIXME: this logic (especially concat_with_stop) needs to be replaced by code
    1.29 -to invert the function ascii_of.*)
    1.30 -fun remove_spaces str = 
    1.31 -    let val strlist = String.tokens Char.isSpace str
    1.32 -	val spaceless = concat strlist
    1.33 -	val strlist' = String.tokens Char.isPunct spaceless
    1.34 -    in
    1.35 -	concat_with_stop strlist'
    1.36 -    end
    1.37 -
    1.38 -fun remove_symb_pair (str, thm) = (remove_symb str, thm);
    1.39 -
    1.40 -fun remove_spaces_pair (str, thm) = (remove_spaces str, thm);
    1.41 -
    1.42 -
    1.43  (*Insert th into the result provided the name is not "".*)
    1.44  fun add_nonempty ((name,th), ths) = if name="" then ths else th::ths;
    1.45  
    1.46 @@ -187,16 +164,10 @@
    1.47  fun clause_numbering ((clause, theorem), cls) = 
    1.48      let val num_of_cls = length cls
    1.49  	val numbers = 0 upto (num_of_cls -1)
    1.50 -	val multi_name = multi (clause, theorem)  num_of_cls []
    1.51      in 
    1.52 -	(multi_name)
    1.53 +	multi (clause, theorem)  num_of_cls []
    1.54      end;
    1.55 -
    1.56 -
    1.57 -fun concat_with sep []  = ""
    1.58 -  | concat_with sep [x] = "(" ^ x ^ ")"
    1.59 -  | concat_with sep (x::xs) = "(" ^ x ^ ")" ^  sep ^ (concat_with sep xs);
    1.60 -
    1.61 +    
    1.62  
    1.63  (*Write out the claset and simpset rules of the supplied theory.
    1.64    FIXME: argument "goal" is a hack to allow relevance filtering.
    1.65 @@ -211,17 +182,12 @@
    1.66  	val simpset_rules =
    1.67  	      ReduceAxiomsN.relevant_filter (!relevant) goal 
    1.68                  (ResAxioms.simpset_rules_of_thy thy);
    1.69 -	val named_simpset = 
    1.70 -	      map remove_spaces_pair (map put_name_pair simpset_rules)
    1.71 -        val justnames = map #1 named_simpset
    1.72 -        val namestring = concat_with "\n" justnames
    1.73 -        val _ = File.append (File.tmp_path (Path.basic "clasimp_names"))
    1.74 -			  (namestring)
    1.75 +	val named_simpset = map put_name_pair simpset_rules
    1.76  	val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []);
    1.77  
    1.78 -	val cls_thms = if !use_simpset then (claset_cls_thms@simpset_cls_thms) else claset_cls_thms;
    1.79 +	val cls_thms = if !use_simpset then (claset_cls_thms@simpset_cls_thms) 
    1.80 +	               else claset_cls_thms;
    1.81  	val cls_thms_list = List.concat cls_thms;
    1.82 -        (* length 1429 *)
    1.83  	(*************************************************)
    1.84  	(* Write out clauses as tptp strings to filename *)
    1.85  	(*************************************************)
    1.86 @@ -239,10 +205,8 @@
    1.87  
    1.88  	(* list of lists of tptp string clauses *)
    1.89  	val stick_clasrls =   List.concat cls_tptp_strs;
    1.90 -        (* length 1581*)
    1.91  	val out = TextIO.openOut filename;
    1.92  	val _=   ResLib.writeln_strs out stick_clasrls;
    1.93 -	val _= TextIO.flushOut out;
    1.94  	val _= TextIO.closeOut out
    1.95    in
    1.96  	(clause_arr, num_of_clauses, clauses)
     2.1 --- a/src/HOL/Tools/ATP/watcher.ML	Fri Sep 02 17:23:59 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Fri Sep 02 17:55:24 2005 +0200
     2.3 @@ -236,7 +236,9 @@
     2.4  
     2.5        val _ = File.append (File.tmp_path (Path.basic "sep_comms"))                                                                                
     2.6                    ("Sep comms are: "^(implode str)^"**"^
     2.7 -                   prover^" thmstring: "^thmstring^"\n goalstr:  "^goalstring^" \n provercmd: "^proverCmd^" \n  clasimp "^clasimpfile^" \n hyps "^hypsfile^"\n prob  "^file^"\n\n")
     2.8 +                   prover^" thmstring: "^thmstring^"\n goalstr:  "^goalstring^
     2.9 +                   " \n provercmd: "^proverCmd^" \n  clasimp "^clasimpfile^
    2.10 +                   " \n hyps "^hypsfile^"\n prob  "^file^"\n\n")
    2.11    in
    2.12       (prover,thmstring,goalstring, proverCmd, settings, clasimpfile, hypsfile, file)
    2.13    end
    2.14 @@ -255,20 +257,9 @@
    2.15      (*** only include problem and clasimp for the moment, not sure 
    2.16  	 how to refer to hyps/local axioms just now ***)
    2.17      val whole_prob_file = Unix.execute("/bin/cat", 
    2.18 -	     [clasimpfile,(*axfile, hypsfile,*)probfile,  ">",
    2.19 +	     [clasimpfile,probfile,  ">",
    2.20  	      File.platform_path wholefile])
    2.21      
    2.22 -    val dfg_dir = File.tmp_path (Path.basic "dfg"); 
    2.23 -    val dfg_path = File.platform_path dfg_dir;
    2.24 -    
    2.25 -    (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***)
    2.26 -    val probID = List.last(explode probfile)
    2.27 -    val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID))
    2.28 -
    2.29 -    (*** only include problem and clasimp for the moment, not sure how to refer to ***)
    2.30 -    (*** hyps/local axioms just now                                                ***)
    2.31 -    val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*axfile, hypsfile,*)probfile,  ">", (File.platform_path wholefile)])
    2.32 -
    2.33      (* if using spass prob_n already contains whole DFG file, otherwise need to mash axioms*)
    2.34      (* from clasimpset onto problem file *)
    2.35      val newfile =   if !SpassComm.spass 
    2.36 @@ -276,7 +267,8 @@
    2.37                      else (File.platform_path wholefile)
    2.38  
    2.39      val _ =  File.append (File.tmp_path (Path.basic"thmstring_in_watcher"))
    2.40 -	       (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^newfile^"\n")
    2.41 +	       (thmstring^"\n goals_watched"^
    2.42 +	       (string_of_int(!goals_being_watched))^newfile^"\n")
    2.43    in
    2.44      (prover,thmstring,goalstring, proverCmd, settings,newfile)	
    2.45    end;
    2.46 @@ -378,317 +370,317 @@
    2.47      (****** fork a watcher process and get it set up and going *)
    2.48      (***********************************************************)
    2.49      fun startWatcher (procList) =
    2.50 -	     (case  Posix.Process.fork() (***************************************)
    2.51 -	   of SOME pid =>  pid           (* parent - i.e. main Isabelle process *)
    2.52 -					 (***************************************)
    2.53 +     (case  Posix.Process.fork() (***************************************)
    2.54 +      of SOME pid =>  pid           (* parent - i.e. main Isabelle process *)
    2.55 +				    (***************************************)
    2.56  
    2.57 -					   (*************************)
    2.58 -	    | NONE => let                  (* child - i.e. watcher  *)
    2.59 -		val oldchildin = #infd p1  (*************************)
    2.60 -		val fromParent = Posix.FileSys.wordToFD 0w0
    2.61 -		val oldchildout = #outfd p2
    2.62 -		val toParent = Posix.FileSys.wordToFD 0w1
    2.63 -		val fromParentIOD = Posix.FileSys.fdToIOD fromParent
    2.64 -		val fromParentStr = openInFD ("_exec_in_parent", fromParent)
    2.65 -		val toParentStr = openOutFD ("_exec_out_parent", toParent)
    2.66 -		val sign = sign_of_thm thm
    2.67 -		val prems = prems_of thm
    2.68 -		val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
    2.69 -		val _ = (warning ("subgoals forked to startWatcher: "^prems_string));
    2.70 -	       (* tracing *)
    2.71 -	      (*val tenth_ax = fst( Array.sub(clause_arr, 1))  
    2.72 -		val tenth_ax_thms = memo_find_clause (tenth_ax, clause_tab)
    2.73 -		val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms)
    2.74 -		val _ = (warning ("tenth axiom in array in watcher is: "^tenth_ax))         
    2.75 -		val _ = (warning ("tenth axiom in table in watcher is: "^clause_str))         
    2.76 -		val _ = (warning ("num_of_clauses in watcher is: "^(string_of_int (num_of_clauses))) )       
    2.77 -			 *)
    2.78 -		(*val goalstr = string_of_thm (the_goal)
    2.79 -		 val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "goal_in_watcher")));  
    2.80 -		val _ = TextIO.output (outfile,goalstr )
    2.81 -		val _ =  TextIO.closeOut outfile*)
    2.82 -		fun killChildren [] = ()
    2.83 -	     |      killChildren  (child_handle::children) = (killChild child_handle; killChildren children)
    2.84 +				      (*************************)
    2.85 +       | NONE => let                  (* child - i.e. watcher  *)
    2.86 +	   val oldchildin = #infd p1  (*************************)
    2.87 +	   val fromParent = Posix.FileSys.wordToFD 0w0
    2.88 +	   val oldchildout = #outfd p2
    2.89 +	   val toParent = Posix.FileSys.wordToFD 0w1
    2.90 +	   val fromParentIOD = Posix.FileSys.fdToIOD fromParent
    2.91 +	   val fromParentStr = openInFD ("_exec_in_parent", fromParent)
    2.92 +	   val toParentStr = openOutFD ("_exec_out_parent", toParent)
    2.93 +	   val sign = sign_of_thm thm
    2.94 +	   val prems = prems_of thm
    2.95 +	   val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
    2.96 +	   val _ = (warning ("subgoals forked to startWatcher: "^prems_string));
    2.97 +	  (* tracing *)
    2.98 +	 (*val tenth_ax = fst( Array.sub(clause_arr, 1))  
    2.99 +	   val tenth_ax_thms = memo_find_clause (tenth_ax, clause_tab)
   2.100 +	   val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms)
   2.101 +	   val _ = (warning ("tenth axiom in array in watcher is: "^tenth_ax))         
   2.102 +	   val _ = (warning ("tenth axiom in table in watcher is: "^clause_str))         
   2.103 +	   val _ = (warning ("num_of_clauses in watcher is: "^(string_of_int (num_of_clauses))) )       
   2.104 +		    *)
   2.105 +	   (*val goalstr = string_of_thm (the_goal)
   2.106 +	    val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "goal_in_watcher")));  
   2.107 +	   val _ = TextIO.output (outfile,goalstr )
   2.108 +	   val _ =  TextIO.closeOut outfile*)
   2.109 +	   fun killChildren [] = ()
   2.110 +	|      killChildren  (child_handle::children) = (killChild child_handle; killChildren children)
   2.111  
   2.112 -	      (*************************************************************)
   2.113 -	      (* take an instream and poll its underlying reader for input *)
   2.114 -	      (*************************************************************)
   2.115 +	 (*************************************************************)
   2.116 +	 (* take an instream and poll its underlying reader for input *)
   2.117 +	 (*************************************************************)
   2.118  
   2.119 -	      fun pollParentInput () = 
   2.120 -		 let val pd = OS.IO.pollDesc (fromParentIOD)
   2.121 -		 in 
   2.122 -		   if (isSome pd ) then 
   2.123 -		       let val pd' = OS.IO.pollIn (valOf pd)
   2.124 -			   val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
   2.125 -			   val _ = File.append (File.tmp_path (Path.basic "parent_poll")) 
   2.126 -			     ("In parent_poll\n")	
   2.127 -		       in
   2.128 -			  if null pdl 
   2.129 -			  then
   2.130 -			     NONE
   2.131 -			  else if (OS.IO.isIn (hd pdl)) 
   2.132 -			       then SOME (getCmds (toParentStr, fromParentStr, []))
   2.133 -			       else NONE
   2.134 -		       end
   2.135 -		     else NONE
   2.136 -		 end
   2.137 -		      
   2.138 -	       fun pollChildInput (fromStr) = 
   2.139 -		 let val _ = File.append (File.tmp_path (Path.basic "child_poll")) 
   2.140 -			       ("In child_poll\n")
   2.141 -		     val iod = getInIoDesc fromStr
   2.142 -		 in 
   2.143 -		   if isSome iod 
   2.144 -		   then 
   2.145 -		     let val pd = OS.IO.pollDesc (valOf iod)
   2.146 -		     in 
   2.147 -		     if (isSome pd ) then 
   2.148 -			 let val pd' = OS.IO.pollIn (valOf pd)
   2.149 -			     val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
   2.150 -			 in
   2.151 -			    if null pdl 
   2.152 +	 fun pollParentInput () = 
   2.153 +	    let val pd = OS.IO.pollDesc (fromParentIOD)
   2.154 +	    in 
   2.155 +	      if (isSome pd ) then 
   2.156 +		  let val pd' = OS.IO.pollIn (valOf pd)
   2.157 +		      val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
   2.158 +		      val _ = File.append (File.tmp_path (Path.basic "parent_poll")) 
   2.159 +			("In parent_poll\n")	
   2.160 +		  in
   2.161 +		     if null pdl 
   2.162 +		     then
   2.163 +			NONE
   2.164 +		     else if (OS.IO.isIn (hd pdl)) 
   2.165 +			  then SOME (getCmds (toParentStr, fromParentStr, []))
   2.166 +			  else NONE
   2.167 +		  end
   2.168 +		else NONE
   2.169 +	    end
   2.170 +		 
   2.171 +	  fun pollChildInput (fromStr) = 
   2.172 +	    let val _ = File.append (File.tmp_path (Path.basic "child_poll")) 
   2.173 +			  ("In child_poll\n")
   2.174 +		val iod = getInIoDesc fromStr
   2.175 +	    in 
   2.176 +	      if isSome iod 
   2.177 +	      then 
   2.178 +		let val pd = OS.IO.pollDesc (valOf iod)
   2.179 +		in 
   2.180 +		if (isSome pd ) then 
   2.181 +		    let val pd' = OS.IO.pollIn (valOf pd)
   2.182 +			val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
   2.183 +		    in
   2.184 +		       if null pdl 
   2.185 +		       then
   2.186 +			 ( File.append (File.tmp_path (Path.basic "child_poll_res")) 
   2.187 +			  ("Null pdl \n");NONE)
   2.188 +		       else if (OS.IO.isIn (hd pdl)) 
   2.189  			    then
   2.190 -			      ( File.append (File.tmp_path (Path.basic "child_poll_res")) 
   2.191 -			       ("Null pdl \n");NONE)
   2.192 -			    else if (OS.IO.isIn (hd pdl)) 
   2.193 -				 then
   2.194 -				     (let val inval =  (TextIO.inputLine fromStr)
   2.195 -					  val _ = File.append (File.tmp_path (Path.basic "child_poll_res")) (inval^"\n")
   2.196 -				      in
   2.197 -					    SOME inval
   2.198 -				      end)
   2.199 -				 else
   2.200 -				       ( File.append (File.tmp_path (Path.basic "child_poll_res")) 
   2.201 -			       ("Null pdl \n");NONE)
   2.202 -			 end
   2.203 -		       else  NONE
   2.204 -		       end
   2.205 -		   else NONE
   2.206 -	     end
   2.207 +				(let val inval =  (TextIO.inputLine fromStr)
   2.208 +				     val _ = File.append (File.tmp_path (Path.basic "child_poll_res")) (inval^"\n")
   2.209 +				 in
   2.210 +				       SOME inval
   2.211 +				 end)
   2.212 +			    else
   2.213 +				  ( File.append (File.tmp_path (Path.basic "child_poll_res")) 
   2.214 +			  ("Null pdl \n");NONE)
   2.215 +		    end
   2.216 +		  else  NONE
   2.217 +		  end
   2.218 +	      else NONE
   2.219 +	end
   2.220  
   2.221  
   2.222 -	     (****************************************************************************)
   2.223 -	     (* Check all vampire processes currently running for output                 *)
   2.224 -	     (****************************************************************************) 
   2.225 -							(*********************************)
   2.226 -	      fun checkChildren ([], toParentStr) = []  (*** no children to check ********)
   2.227 -							(*********************************)
   2.228 -	      |   checkChildren ((childProc::otherChildren), toParentStr) = 
   2.229 -		    let val _ = File.append (File.tmp_path (Path.basic "child_check")) 
   2.230 -			           ("In check child, length of queue:"^(string_of_int (length (childProc::otherChildren)))^"\n")
   2.231 -                        val (childInput,childOutput) =  cmdstreamsOf childProc
   2.232 -			val child_handle= cmdchildHandle childProc
   2.233 -			(* childCmd is the .dfg file that the problem is in *)
   2.234 -			val childCmd = fst(snd (cmdchildInfo childProc))
   2.235 -                        val _ = File.append (File.tmp_path (Path.basic "child_command")) 
   2.236 -			           (childCmd^"\n")
   2.237 -			(* now get the number of the subgoal from the filename *)
   2.238 -			val sg_num = (*if (!SpassComm.spass )
   2.239 -				     then 
   2.240 -					int_of_string(ReconOrderClauses.get_nth 5 (rev(explode childCmd)))
   2.241 -				     else*)
   2.242 -					int_of_string(hd (rev(explode childCmd)))
   2.243 +	(****************************************************************************)
   2.244 +	(* Check all vampire processes currently running for output                 *)
   2.245 +	(****************************************************************************) 
   2.246 +						   (*********************************)
   2.247 +	 fun checkChildren ([], toParentStr) = []  (*** no children to check ********)
   2.248 +						   (*********************************)
   2.249 +	 |   checkChildren ((childProc::otherChildren), toParentStr) = 
   2.250 +	       let val _ = File.append (File.tmp_path (Path.basic "child_check")) 
   2.251 +			      ("In check child, length of queue:"^(string_of_int (length (childProc::otherChildren)))^"\n")
   2.252 +		   val (childInput,childOutput) =  cmdstreamsOf childProc
   2.253 +		   val child_handle= cmdchildHandle childProc
   2.254 +		   (* childCmd is the .dfg file that the problem is in *)
   2.255 +		   val childCmd = fst(snd (cmdchildInfo childProc))
   2.256 +		   val _ = File.append (File.tmp_path (Path.basic "child_command")) 
   2.257 +			      (childCmd^"\n")
   2.258 +		   (* now get the number of the subgoal from the filename *)
   2.259 +		   val sg_num = (*if (!SpassComm.spass )
   2.260 +				then 
   2.261 +				   int_of_string(ReconOrderClauses.get_nth 5 (rev(explode childCmd)))
   2.262 +				else*)
   2.263 +				   int_of_string(hd (rev(explode childCmd)))
   2.264  
   2.265 -			val childIncoming = pollChildInput childInput
   2.266 - 			val _ = File.append (File.tmp_path (Path.basic "child_check_polled")) 
   2.267 -			           ("finished polling child \n")
   2.268 -			val parentID = Posix.ProcEnv.getppid()
   2.269 -			val prover = cmdProver childProc
   2.270 -			val thmstring = cmdThm childProc
   2.271 -			val sign = sign_of_thm thm
   2.272 -			val prems = prems_of thm
   2.273 -			val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   2.274 -			val _ = warning("subgoals forked to checkChildren: "^prems_string)
   2.275 -			val goalstring = cmdGoal childProc							
   2.276 -			val _ = File.append (File.tmp_path (Path.basic "child_comms")) 
   2.277 -			           (prover^thmstring^goalstring^childCmd^"\n")
   2.278 -		    in 
   2.279 -		      if (isSome childIncoming) 
   2.280 -		      then 
   2.281 -			  (* check here for prover label on child*)
   2.282 -			  let val _ = File.write (File.tmp_path (Path.basic "child_incoming")) 
   2.283 -			             ("subgoals forked to checkChildren:"^
   2.284 -			             prems_string^prover^thmstring^goalstring^childCmd) 
   2.285 -		              val childDone = (case prover of
   2.286 -	                          "vampire" => (VampComm.checkVampProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) )                                              
   2.287 -                                 |"spass" => (SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)     ) )
   2.288 -			   in
   2.289 -			    if childDone      (**********************************************)
   2.290 -			    then (* child has found a proof and transferred it *)
   2.291 -			       (* Remove this child and go on to check others*)
   2.292 -			       (**********************************************)
   2.293 -			       (Unix.reap child_handle;
   2.294 -				checkChildren(otherChildren, toParentStr))
   2.295 -			    else 
   2.296 -			       (**********************************************)
   2.297 -			       (* Keep this child and go on to check others  *)
   2.298 -			       (**********************************************)
   2.299 -			      (childProc::(checkChildren (otherChildren, toParentStr)))
   2.300 -			 end
   2.301 -		       else
   2.302 -			 (File.append (File.tmp_path (Path.basic "child_incoming")) "No child output ";
   2.303 -			  childProc::(checkChildren (otherChildren, toParentStr)))
   2.304 +		   val childIncoming = pollChildInput childInput
   2.305 +		   val _ = File.append (File.tmp_path (Path.basic "child_check_polled")) 
   2.306 +			      ("finished polling child \n")
   2.307 +		   val parentID = Posix.ProcEnv.getppid()
   2.308 +		   val prover = cmdProver childProc
   2.309 +		   val thmstring = cmdThm childProc
   2.310 +		   val sign = sign_of_thm thm
   2.311 +		   val prems = prems_of thm
   2.312 +		   val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   2.313 +		   val _ = warning("subgoals forked to checkChildren: "^prems_string)
   2.314 +		   val goalstring = cmdGoal childProc							
   2.315 +		   val _ = File.append (File.tmp_path (Path.basic "child_comms")) 
   2.316 +			      (prover^thmstring^goalstring^childCmd^"\n")
   2.317 +	       in 
   2.318 +		 if (isSome childIncoming) 
   2.319 +		 then 
   2.320 +		     (* check here for prover label on child*)
   2.321 +		     let val _ = File.write (File.tmp_path (Path.basic "child_incoming")) 
   2.322 +				("subgoals forked to checkChildren:"^
   2.323 +				prems_string^prover^thmstring^goalstring^childCmd) 
   2.324 +			 val childDone = (case prover of
   2.325 +			     "vampire" => (VampComm.checkVampProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) )                                              
   2.326 +			    |"spass" => (SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)     ) )
   2.327 +		      in
   2.328 +		       if childDone      (**********************************************)
   2.329 +		       then (* child has found a proof and transferred it *)
   2.330 +			  (* Remove this child and go on to check others*)
   2.331 +			  (**********************************************)
   2.332 +			  (Unix.reap child_handle;
   2.333 +			   checkChildren(otherChildren, toParentStr))
   2.334 +		       else 
   2.335 +			  (**********************************************)
   2.336 +			  (* Keep this child and go on to check others  *)
   2.337 +			  (**********************************************)
   2.338 +			 (childProc::(checkChildren (otherChildren, toParentStr)))
   2.339  		    end
   2.340 +		  else
   2.341 +		    (File.append (File.tmp_path (Path.basic "child_incoming")) "No child output ";
   2.342 +		     childProc::(checkChildren (otherChildren, toParentStr)))
   2.343 +	       end
   2.344  
   2.345 -	     
   2.346 -	  (********************************************************************)                  
   2.347 -	  (* call resolution processes                                        *)
   2.348 -	  (* settings should be a list of strings                             *)
   2.349 -	  (* e.g. ["-t 300", "-m 100000"]         (TextIO.input instr)^                            *)
   2.350 -	  (* takes list of (string, string, string list, string)list proclist *)
   2.351 -	  (********************************************************************)
   2.352 +	
   2.353 +     (********************************************************************)                  
   2.354 +     (* call resolution processes                                        *)
   2.355 +     (* settings should be a list of strings                             *)
   2.356 +     (* e.g. ["-t 300", "-m 100000"]         (TextIO.input instr)^                            *)
   2.357 +     (* takes list of (string, string, string list, string)list proclist *)
   2.358 +     (********************************************************************)
   2.359  
   2.360  
   2.361  (*** add subgoal id num to this *)
   2.362 -	     fun execCmds  [] procList = procList
   2.363 -	     |   execCmds  ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList  =             let val _ = File.append (File.tmp_path (Path.basic "pre_exec_child"))  ("\nAbout to execute command for goal:\n"^goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
   2.364 -	       in 
   2.365 -		 if (prover = "spass") 
   2.366 -		 then 
   2.367 -		   let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = 
   2.368 -		            (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
   2.369 -		       val (instr, outstr) = Unix.streamsOf childhandle
   2.370 -		       val newProcList =    (((CMDPROC{
   2.371 -					    prover = prover,
   2.372 -					    cmd = file,
   2.373 -					    thmstring = thmstring,
   2.374 -					    goalstring = goalstring,
   2.375 -					    proc_handle = childhandle,
   2.376 -					    instr = instr,
   2.377 -					    outstr = outstr })::procList))
   2.378 -			val _ = File.append (File.tmp_path (Path.basic "exec_child"))  
   2.379 -			     ("\nexecuting command for goal:\n"^
   2.380 -			      goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
   2.381 -		   in
   2.382 -		      Posix.Process.sleep (Time.fromSeconds 1);execCmds cmds newProcList
   2.383 -		   end
   2.384 -		 else 
   2.385 -		   let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = 
   2.386 -		            (Unix.execute(proverCmd, (settings@[file])))
   2.387 -		       val (instr, outstr) = Unix.streamsOf childhandle
   2.388 -		       
   2.389 -		       val newProcList = (CMDPROC{
   2.390 -					    prover = prover,
   2.391 -					    cmd = file,
   2.392 -					    thmstring = thmstring,
   2.393 -					    goalstring = goalstring,
   2.394 -					    proc_handle = childhandle,
   2.395 -					    instr = instr,
   2.396 -					    outstr = outstr }) :: procList
   2.397 -	  
   2.398 -		       val _ = File.append (File.tmp_path (Path.basic "exec_child")) 
   2.399 -		                 ("executing command for goal:\n"^
   2.400 -		                  goalstring^proverCmd^(concat settings)^file^
   2.401 -		                  " at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
   2.402 -		   in
   2.403 -		     Posix.Process.sleep (Time.fromSeconds 1); execCmds cmds newProcList
   2.404 -		   end
   2.405 -		end
   2.406 +	fun execCmds  [] procList = procList
   2.407 +	|   execCmds  ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList  =             let val _ = File.append (File.tmp_path (Path.basic "pre_exec_child"))  ("\nAbout to execute command for goal:\n"^goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
   2.408 +	  in 
   2.409 +	    if (prover = "spass") 
   2.410 +	    then 
   2.411 +	      let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = 
   2.412 +		       (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
   2.413 +		  val (instr, outstr) = Unix.streamsOf childhandle
   2.414 +		  val newProcList =    (((CMDPROC{
   2.415 +				       prover = prover,
   2.416 +				       cmd = file,
   2.417 +				       thmstring = thmstring,
   2.418 +				       goalstring = goalstring,
   2.419 +				       proc_handle = childhandle,
   2.420 +				       instr = instr,
   2.421 +				       outstr = outstr })::procList))
   2.422 +		   val _ = File.append (File.tmp_path (Path.basic "exec_child"))  
   2.423 +			("\nexecuting command for goal:\n"^
   2.424 +			 goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
   2.425 +	      in
   2.426 +		 Posix.Process.sleep (Time.fromSeconds 1);
   2.427 +		 execCmds cmds newProcList
   2.428 +	      end
   2.429 +	    else 
   2.430 +	      let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = 
   2.431 +		       (Unix.execute(proverCmd, (settings@[file])))
   2.432 +		  val (instr, outstr) = Unix.streamsOf childhandle
   2.433 +		  
   2.434 +		  val newProcList = (CMDPROC{
   2.435 +				       prover = prover,
   2.436 +				       cmd = file,
   2.437 +				       thmstring = thmstring,
   2.438 +				       goalstring = goalstring,
   2.439 +				       proc_handle = childhandle,
   2.440 +				       instr = instr,
   2.441 +				       outstr = outstr }) :: procList
   2.442 +     
   2.443 +		  val _ = File.append (File.tmp_path (Path.basic "exec_child")) 
   2.444 +			    ("executing command for goal:\n"^
   2.445 +			     goalstring^proverCmd^(concat settings)^file^
   2.446 +			     " at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
   2.447 +	      in
   2.448 +		Posix.Process.sleep (Time.fromSeconds 1); 
   2.449 +		execCmds cmds newProcList
   2.450 +	      end
   2.451 +	   end
   2.452  
   2.453  
   2.454 -	  (****************************************)                  
   2.455 -	  (* call resolution processes remotely   *)
   2.456 -	  (* settings should be a list of strings *)
   2.457 -	  (* e.g. ["-t 300", "-m 100000"]         *)
   2.458 -	  (****************************************)
   2.459 +     (****************************************)                  
   2.460 +     (* call resolution processes remotely   *)
   2.461 +     (* settings should be a list of strings *)
   2.462 +     (* e.g. ["-t 300", "-m 100000"]         *)
   2.463 +     (****************************************)
   2.464  
   2.465 -	   (*  fun execRemoteCmds  [] procList = procList
   2.466 -	     |   execRemoteCmds ((prover, thmstring,goalstring,proverCmd ,settings,file)::cmds) procList  =  
   2.467 -				       let val  newProcList =  mySshExecuteToList ("/usr/bin/ssh",([prover,thmstring,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
   2.468 -					   in
   2.469 -						execRemoteCmds  cmds newProcList
   2.470 -					   end
   2.471 +      (*  fun execRemoteCmds  [] procList = procList
   2.472 +	|   execRemoteCmds ((prover, thmstring,goalstring,proverCmd ,settings,file)::cmds) procList  =  
   2.473 +				  let val  newProcList =  mySshExecuteToList ("/usr/bin/ssh",([prover,thmstring,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
   2.474 +				      in
   2.475 +					   execRemoteCmds  cmds newProcList
   2.476 +				      end
   2.477  *)
   2.478  
   2.479 -	     fun printList (outStr, []) = ()
   2.480 -	     |   printList (outStr, (x::xs)) = (TextIO.output (outStr, x);TextIO.flushOut outStr; printList (outStr,xs))                  
   2.481 +	fun printList (outStr, []) = ()
   2.482 +	|   printList (outStr, (x::xs)) = (TextIO.output (outStr, x);TextIO.flushOut outStr; printList (outStr,xs))                  
   2.483  
   2.484  
   2.485 -	  (**********************************************)                  
   2.486 -	  (* Watcher Loop                               *)
   2.487 -	  (**********************************************)
   2.488 +     (**********************************************)                  
   2.489 +     (* Watcher Loop                               *)
   2.490 +     (**********************************************)
   2.491  
   2.492 -	      fun keepWatching (toParentStr, fromParentStr,procList) = 
   2.493 -		let fun loop (procList) =  
   2.494 -		     let val cmdsFromIsa = pollParentInput ()
   2.495 -			 fun killchildHandler (n:int)  = 
   2.496 -			       (TextIO.output(toParentStr, "Killing child proof processes!\n");
   2.497 -				TextIO.flushOut toParentStr;
   2.498 -				killChildren (map (cmdchildHandle) procList);
   2.499 -				())
   2.500 -		     in 
   2.501 -			(*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*)
   2.502 -									   (**********************************)
   2.503 -			if (isSome cmdsFromIsa) 
   2.504 -			then (*  deal with input from Isabelle *)
   2.505 -			  if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" )
   2.506 -			  then 
   2.507 -			    let val child_handles = map cmdchildHandle procList 
   2.508 -			    in
   2.509 -			       killChildren child_handles;
   2.510 -			       (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*)    
   2.511 -			       loop ([])
   2.512 -			    end
   2.513 -			  else
   2.514 -			    if ((length procList)<10)    (********************)
   2.515 -			    then                        (* Execute locally  *)
   2.516 -			      let 
   2.517 -				val newProcList = execCmds (valOf cmdsFromIsa) procList
   2.518 -				val parentID = Posix.ProcEnv.getppid()
   2.519 -				   val _ = (File.append (File.tmp_path (Path.basic "prekeep_watch")) "Just execed a child\n ")
   2.520 -				val newProcList' =checkChildren (newProcList, toParentStr) 
   2.521 +	 fun keepWatching (toParentStr, fromParentStr,procList) = 
   2.522 +	   let fun loop (procList) =  
   2.523 +		let val _ = Posix.Process.sleep (Time.fromMilliseconds 200)
   2.524 +		    val cmdsFromIsa = pollParentInput ()
   2.525 +		    fun killchildHandler (n:int)  = 
   2.526 +			  (TextIO.output(toParentStr, "Killing child proof processes!\n");
   2.527 +			   TextIO.flushOut toParentStr;
   2.528 +			   killChildren (map (cmdchildHandle) procList);
   2.529 +			   ())
   2.530 +		in 
   2.531 +		   (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*)
   2.532 +								      (**********************************)
   2.533 +		   if (isSome cmdsFromIsa) 
   2.534 +		   then (*  deal with input from Isabelle *)
   2.535 +		     if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" )
   2.536 +		     then 
   2.537 +		       let val child_handles = map cmdchildHandle procList 
   2.538 +		       in
   2.539 +			  killChildren child_handles;
   2.540 +			  (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*)    
   2.541 +			  loop ([])
   2.542 +		       end
   2.543 +		     else
   2.544 +		       if ((length procList)<10)    (********************)
   2.545 +		       then                        (* Execute locally  *)
   2.546 +			 let 
   2.547 +			   val newProcList = execCmds (valOf cmdsFromIsa) procList
   2.548 +			   val parentID = Posix.ProcEnv.getppid()
   2.549 +			      val _ = (File.append (File.tmp_path (Path.basic "prekeep_watch")) "Just execed a child\n ")
   2.550 +			   val newProcList' =checkChildren (newProcList, toParentStr) 
   2.551  
   2.552 -				val _ = warning("off to keep watching...")
   2.553 -			       val _ = (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching...\n ")
   2.554 -			      in
   2.555 -				(*Posix.Process.sleep (Time.fromSeconds 1);*)
   2.556 -				loop (newProcList') 
   2.557 -			      end
   2.558 -			    else  (* Execute remotely              *)
   2.559 -                                  (* (actually not remote for now )*)
   2.560 -			      let 
   2.561 -				val newProcList = execCmds (valOf cmdsFromIsa) procList
   2.562 -				val parentID = Posix.ProcEnv.getppid()
   2.563 -				val newProcList' =checkChildren (newProcList, toParentStr) 
   2.564 -			      in
   2.565 -				(*Posix.Process.sleep (Time.fromSeconds 1);*)
   2.566 -				loop (newProcList') 
   2.567 -			      end
   2.568 -			else (* No new input from Isabelle *)
   2.569 -			  let val newProcList = checkChildren ((procList), toParentStr)
   2.570 -			  in
   2.571 -			    (*Posix.Process.sleep (Time.fromSeconds 1);*)
   2.572 -			   (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching.2..\n ");
   2.573 -			    loop (newProcList)
   2.574 -			  end
   2.575 -		      end
   2.576 -		in  
   2.577 -		    loop (procList)
   2.578 -		end
   2.579 -		
   2.580 -    
   2.581 -		in
   2.582 -		 (***************************)
   2.583 -		 (*** Sort out pipes ********)
   2.584 -		 (***************************)
   2.585 +			   val _ = warning("off to keep watching...")
   2.586 +			  val _ = (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching...\n ")
   2.587 +			 in
   2.588 +			   loop (newProcList') 
   2.589 +			 end
   2.590 +		       else  (* Execute remotely              *)
   2.591 +			     (* (actually not remote for now )*)
   2.592 +			 let 
   2.593 +			   val newProcList = execCmds (valOf cmdsFromIsa) procList
   2.594 +			   val parentID = Posix.ProcEnv.getppid()
   2.595 +			   val newProcList' =checkChildren (newProcList, toParentStr) 
   2.596 +			 in
   2.597 +			   loop (newProcList') 
   2.598 +			 end
   2.599 +		   else (* No new input from Isabelle *)
   2.600 +		     let val newProcList = checkChildren ((procList), toParentStr)
   2.601 +		     in
   2.602 +		      (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching.2..\n ");
   2.603 +		       loop (newProcList)
   2.604 +		     end
   2.605 +		 end
   2.606 +	   in  
   2.607 +	       loop (procList)
   2.608 +	   end
   2.609 +	   
   2.610  
   2.611 -		  Posix.IO.close (#outfd p1);
   2.612 -		  Posix.IO.close (#infd p2);
   2.613 -		  Posix.IO.dup2{old = oldchildin, new = fromParent};
   2.614 -		  Posix.IO.close oldchildin;
   2.615 -		  Posix.IO.dup2{old = oldchildout, new = toParent};
   2.616 -		  Posix.IO.close oldchildout;
   2.617 +	   in
   2.618 +	    (***************************)
   2.619 +	    (*** Sort out pipes ********)
   2.620 +	    (***************************)
   2.621  
   2.622 -		  (***************************)
   2.623 -		  (* start the watcher loop  *)
   2.624 -		  (***************************)
   2.625 -		  keepWatching (toParentStr, fromParentStr, procList);
   2.626 -		  (****************************************************************************)
   2.627 -   (* fake return value - actually want the watcher to loop until killed *)
   2.628 -		  (****************************************************************************)
   2.629 -		  Posix.Process.wordToPid 0w0
   2.630 -		end);
   2.631 -	  (* end case *)
   2.632 +	     Posix.IO.close (#outfd p1);
   2.633 +	     Posix.IO.close (#infd p2);
   2.634 +	     Posix.IO.dup2{old = oldchildin, new = fromParent};
   2.635 +	     Posix.IO.close oldchildin;
   2.636 +	     Posix.IO.dup2{old = oldchildout, new = toParent};
   2.637 +	     Posix.IO.close oldchildout;
   2.638 +
   2.639 +	     (***************************)
   2.640 +	     (* start the watcher loop  *)
   2.641 +	     (***************************)
   2.642 +	     keepWatching (toParentStr, fromParentStr, procList);
   2.643 +	     (****************************************************************************)
   2.644 +(* fake return value - actually want the watcher to loop until killed *)
   2.645 +	     (****************************************************************************)
   2.646 +	     Posix.Process.wordToPid 0w0
   2.647 +	   end);
   2.648 +     (* end case *)
   2.649  
   2.650  
   2.651      val _ = TextIO.flushOut TextIO.stdOut
     3.1 --- a/src/HOL/Tools/res_atp.ML	Fri Sep 02 17:23:59 2005 +0200
     3.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Sep 02 17:55:24 2005 +0200
     3.3 @@ -8,8 +8,6 @@
     3.4  signature RES_ATP =
     3.5  sig
     3.6    val axiom_file : Path.T
     3.7 -  val hyps_file : Path.T
     3.8 -  val prob_file : Path.T;
     3.9  (*val atp_ax_tac : thm list -> int -> Tactical.tactic*)
    3.10  (*val atp_tac : int -> Tactical.tactic*)
    3.11    val full_spass: bool ref
    3.12 @@ -53,16 +51,10 @@
    3.13            REPEAT_DETERM_N (length ts) o (etac thin_rl)]
    3.14       end);
    3.15  
    3.16 -(* temporarily use these files, which will be loaded by Vampire *)
    3.17 -val file_id_num = ref 0;
    3.18 -fun new_prob_file () = "prob" ^ string_of_int (inc file_id_num);
    3.19 -
    3.20  val axiom_file = File.tmp_path (Path.basic "axioms");
    3.21  val clasimp_file = File.tmp_path (Path.basic "clasimp");
    3.22  val hyps_file = File.tmp_path (Path.basic "hyps");
    3.23  val prob_file = File.tmp_path (Path.basic "prob");
    3.24 -val dummy_tac = all_tac;
    3.25 -val _ =debug  (File.platform_path prob_file);
    3.26  
    3.27  
    3.28  (**** for Isabelle/ML interface  ****)
    3.29 @@ -149,11 +141,11 @@
    3.30          val _ = debug ("about to write out dfg prob file " ^ probfile)
    3.31         	(*val (dfg_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2dfg clss)
    3.32          val tfree_clss = map ResClause.tfree_dfg_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees) *)   
    3.33 -        val filestr = ResClause.clauses2dfg clss ("prob" ^ (string_of_int n)) 
    3.34 +        val probN = ResClause.clauses2dfg clss ("prob" ^ (string_of_int n)) 
    3.35                          axclauses [] [] [] tfrees   
    3.36  	val out = TextIO.openOut(probfile)
    3.37      in
    3.38 -	(ResLib.writeln_strs out [filestr]; TextIO.closeOut out; debug probfile )
    3.39 +	(ResLib.writeln_strs out [probN]; TextIO.closeOut out; debug probfile )
    3.40  (* (ResLib.writeln_strs out (tfree_clss @ dfg_clss); *)
    3.41      end;
    3.42  
    3.43 @@ -210,12 +202,12 @@
    3.44    in
    3.45      Watcher.callResProvers(childout,atp_list);
    3.46      debug "Sent commands to watcher!";
    3.47 -    dummy_tac
    3.48 +    all_tac
    3.49    end
    3.50  
    3.51  (**********************************************************)
    3.52  (* write out the current subgoal as a tptp file, probN,   *)
    3.53 -(* then call dummy_tac - should be call_res_tac           *)
    3.54 +(* then call all_tac - should be call_res_tac           *)
    3.55  (**********************************************************)
    3.56  
    3.57  
    3.58 @@ -223,7 +215,7 @@
    3.59      if n=0 then 
    3.60         (call_resolve_tac  (rev sko_thms)
    3.61          sign  sg_terms (childin, childout, pid) (List.length sg_terms);
    3.62 -        dummy_tac thm)
    3.63 +        all_tac thm)
    3.64       else
    3.65  	
    3.66       ( SELECT_GOAL
    3.67 @@ -234,7 +226,7 @@
    3.68               else tptp_inputs_tfrees (make_clauses negs) n tfrees;
    3.69               get_sko_thms tfrees sign sg_terms (childin, childout, pid) 
    3.70                            thm  (n -1) (negs::sko_thms) axclauses; 
    3.71 -             dummy_tac))]) n thm )
    3.72 +             all_tac))]) n thm )
    3.73  
    3.74  
    3.75  
     4.1 --- a/src/HOL/Tools/res_clause.ML	Fri Sep 02 17:23:59 2005 +0200
     4.2 +++ b/src/HOL/Tools/res_clause.ML	Fri Sep 02 17:55:24 2005 +0200
     4.3 @@ -226,8 +226,12 @@
     4.4  
     4.5  (*** make clauses ***)
     4.6  
     4.7 -fun make_clause (clause_id,axiom_name,kind,literals,types_sorts,tvar_type_literals,
     4.8 +fun make_clause (clause_id,axiom_name,kind,literals,
     4.9 +                 types_sorts,tvar_type_literals,
    4.10                   tfree_type_literals,tvars, predicates, functions) =
    4.11 +  if null literals 
    4.12 +  then error "Problem too trivial for resolution (empty clause)"
    4.13 +  else
    4.14       Clause {clause_id = clause_id, axiom_name = axiom_name, kind = kind, 
    4.15               literals = literals, types_sorts = types_sorts,
    4.16               tvar_type_literals = tvar_type_literals,
    4.17 @@ -400,28 +404,29 @@
    4.18  		   | _ => pred_of_nonEq (pred,args)
    4.19      end;
    4.20  
    4.21 - 
    4.22 -
    4.23 -fun literals_of_term ((Const("Trueprop",_) $ P),lits_ts, preds, funcs) = literals_of_term(P,lits_ts, preds, funcs)
    4.24 +fun literals_of_term ((Const("Trueprop",_) $ P),lits_ts, preds, funcs) =    
    4.25 +      literals_of_term(P,lits_ts, preds, funcs)
    4.26    | literals_of_term ((Const("op |",_) $ P $ Q),(lits,ts), preds,funcs) = 
    4.27 -    let val (lits',ts', preds', funcs') = literals_of_term(P,(lits,ts), preds,funcs)
    4.28 -    in
    4.29 -        literals_of_term(Q,(lits',ts'), distinct(preds'@preds), distinct(funcs'@funcs))
    4.30 -    end
    4.31 +      let val (lits',ts', preds', funcs') = 
    4.32 +            literals_of_term(P,(lits,ts), preds,funcs)
    4.33 +      in
    4.34 +	  literals_of_term(Q, (lits',ts'), distinct(preds'@preds), 
    4.35 +	                   distinct(funcs'@funcs))
    4.36 +      end
    4.37    | literals_of_term ((Const("Not",_) $ P),(lits,ts), preds, funcs) = 
    4.38 -    let val (pred,ts', preds', funcs') = predicate_of P
    4.39 -        val lits' = Literal(false,pred,false) :: lits
    4.40 -        val ts'' = ResLib.no_rep_app ts ts'
    4.41 -    in
    4.42 -        (lits',ts'', distinct(preds'@preds), distinct(funcs'@funcs))
    4.43 -    end
    4.44 +      let val (pred,ts', preds', funcs') = predicate_of P
    4.45 +	  val lits' = Literal(false,pred,false) :: lits
    4.46 +	  val ts'' = ResLib.no_rep_app ts ts'
    4.47 +      in
    4.48 +	  (lits',ts'', distinct(preds'@preds), distinct(funcs'@funcs))
    4.49 +      end
    4.50    | literals_of_term (P,(lits,ts), preds, funcs) = 
    4.51 -    let val (pred,ts', preds', funcs') = predicate_of P
    4.52 -        val lits' = Literal(true,pred,false) :: lits
    4.53 -        val ts'' = ResLib.no_rep_app ts ts' 
    4.54 -    in
    4.55 -        (lits',ts'', distinct(preds'@preds), distinct(funcs'@funcs))
    4.56 -    end;
    4.57 +      let val (pred,ts', preds', funcs') = predicate_of P
    4.58 +	  val lits' = Literal(true,pred,false) :: lits
    4.59 +	  val ts'' = ResLib.no_rep_app ts ts' 
    4.60 +      in
    4.61 +	  (lits',ts'', distinct(preds'@preds), distinct(funcs'@funcs))
    4.62 +      end;
    4.63  
    4.64  
    4.65  fun literals_of_thm thm = literals_of_term (prop_of thm, ([],[]), [], []);
    4.66 @@ -690,7 +695,8 @@
    4.67        end;
    4.68  
    4.69  (* before output the string of the predicate, check if the predicate corresponds to an equality or not. *)
    4.70 -fun string_of_predicate (Predicate("equal",typ,terms)) = string_of_equality(typ,terms)
    4.71 +fun string_of_predicate (Predicate("equal",typ,terms)) = 
    4.72 +      string_of_equality(typ,terms)
    4.73    | string_of_predicate (Predicate(name,_,[])) = name 
    4.74    | string_of_predicate (Predicate(name,typ,terms)) = 
    4.75        let val terms_as_strings = map string_of_term terms
    4.76 @@ -708,9 +714,8 @@
    4.77  
    4.78  fun dfg_literal (Literal(pol,pred,tag)) =
    4.79      let val pred_string = string_of_predicate pred
    4.80 -	val tagged_pol =if pol then pred_string else "not(" ^pred_string ^ ")"
    4.81 -     in
    4.82 -	tagged_pol  
    4.83 +    in
    4.84 +	if pol then pred_string else "not(" ^pred_string ^ ")"  
    4.85      end;
    4.86  
    4.87  
    4.88 @@ -755,7 +760,7 @@
    4.89            if !keep_types then map dfg_of_typeLit (#tfree_type_literals cls)
    4.90            else []
    4.91    in
    4.92 -      (tvar_lits_strs @ lits,tfree_lits)
    4.93 +      (tvar_lits_strs @ lits, tfree_lits)
    4.94    end; 
    4.95  
    4.96  
    4.97 @@ -766,7 +771,7 @@
    4.98    end
    4.99  
   4.100   
   4.101 -fun get_uvars (UVar(str,typ)) =(*if (substring (str, 0,2))= "V_" then  *)[str] (*else []*)
   4.102 +fun get_uvars (UVar(str,typ)) = [str] 
   4.103  |   get_uvars (Fun (str,typ,tlist)) = ResLib.flat_noDup(map get_uvars tlist)
   4.104  
   4.105  
   4.106 @@ -819,12 +824,8 @@
   4.107    | concat_with sep [x] = "(" ^ x ^ ")"
   4.108    | concat_with sep (x::xs) = "(" ^ x ^ ")" ^  sep ^ (concat_with sep xs);
   4.109  
   4.110 -fun concat_with_comma []  = ""
   4.111 -  | concat_with_comma [x] =  x 
   4.112 -  | concat_with_comma (x::xs) =  x  ^ ", " ^ (concat_with_comma xs);
   4.113 -
   4.114 -
   4.115 -fun dfg_pred (Literal(pol,pred,tag)) ax_name = (string_of_predname pred)^" "^ax_name
   4.116 +fun dfg_pred (Literal(pol,pred,tag)) ax_name = 
   4.117 +    (string_of_predname pred) ^ " " ^ ax_name
   4.118  
   4.119  fun dfg_clause cls =
   4.120      let val (lits,tfree_lits) = dfg_clause_aux cls 
   4.121 @@ -834,11 +835,12 @@
   4.122  	val cls_id = string_of_clauseID cls
   4.123  	val ax_name = string_of_axiomName cls
   4.124  	val knd = string_of_kind cls
   4.125 -	val lits_str = concat_with_comma lits
   4.126 +	val lits_str = commas lits
   4.127  	val cls_str = gen_dfg_cls(cls_id,ax_name,knd,lits_str,tvars, vars) 			
   4.128          fun typ_clss k [] = []
   4.129            | typ_clss k (tfree :: tfrees) = 
   4.130 -            (gen_dfg_type_cls(cls_id,knd,tfree,k, tvars,vars)) ::  (typ_clss (k+1) tfrees)
   4.131 +              (gen_dfg_type_cls(cls_id,knd,tfree,k, tvars,vars)) :: 
   4.132 +              (typ_clss (k+1) tfrees)
   4.133      in 
   4.134  	cls_str :: (typ_clss 0 tfree_lits)
   4.135      end;
   4.136 @@ -851,21 +853,26 @@
   4.137  
   4.138  fun string_of_arity (name, num) =  name ^"," ^ (string_of_int num) 
   4.139  
   4.140 +fun string_of_preds preds = 
   4.141 +  "predicates[" ^ (concat_with ", " (map string_of_arity preds)) ^ "].\n";
   4.142  
   4.143 -fun string_of_preds preds =  "predicates[" ^ (concat_with ", " (map string_of_arity preds)) ^ "].\n";
   4.144 -
   4.145 -fun string_of_funcs funcs ="functions[" ^ (concat_with ", " (map string_of_arity funcs)) ^ "].\n" ;
   4.146 +fun string_of_funcs funcs =
   4.147 +  "functions[" ^ (concat_with ", " (map string_of_arity funcs)) ^ "].\n" ;
   4.148  
   4.149  
   4.150 -fun string_of_symbols predstr funcstr = "list_of_symbols.\n" ^ predstr  ^ funcstr  ^ "end_of_list.\n\n";
   4.151 +fun string_of_symbols predstr funcstr = 
   4.152 +  "list_of_symbols.\n" ^ predstr  ^ funcstr  ^ "end_of_list.\n\n";
   4.153  
   4.154  
   4.155 -fun string_of_axioms axstr = "list_of_clauses(axioms,cnf).\n" ^ axstr ^ "end_of_list.\n\n";
   4.156 +fun string_of_axioms axstr = 
   4.157 +  "list_of_clauses(axioms,cnf).\n" ^ axstr ^ "end_of_list.\n\n";
   4.158  
   4.159  
   4.160 -fun string_of_conjectures conjstr = "list_of_clauses(conjectures,cnf).\n" ^ conjstr ^ "end_of_list.\n\n";
   4.161 +fun string_of_conjectures conjstr = 
   4.162 +  "list_of_clauses(conjectures,cnf).\n" ^ conjstr ^ "end_of_list.\n\n";
   4.163  
   4.164 -fun string_of_descrip () = "list_of_descriptions.\nname({*[ File     : ],[ Names    :]*}).\nauthor({*[ Source   :]*}).\nstatus(unknown).\ndescription({*[ Refs     :]*}).\nend_of_list.\n\n"
   4.165 +fun string_of_descrip () = 
   4.166 +  "list_of_descriptions.\nname({*[ File     : ],[ Names    :]*}).\nauthor({*[ Source   :]*}).\nstatus(unknown).\ndescription({*[ Refs     :]*}).\nend_of_list.\n\n"
   4.167  
   4.168  
   4.169  fun string_of_start name = "%------------------------------------------------------------------------------\nbegin_problem(" ^ name ^ ").\n\n";
   4.170 @@ -878,7 +885,8 @@
   4.171       
   4.172  
   4.173  fun clause2dfg cls =
   4.174 -    let val (lits,tfree_lits) = dfg_clause_aux cls (*"lits" includes the typing assumptions (TVars)*)
   4.175 +    let val (lits,tfree_lits) = dfg_clause_aux cls 
   4.176 +            (*"lits" includes the typing assumptions (TVars)*)
   4.177  	val cls_id = string_of_clauseID cls
   4.178  	val ax_name = string_of_axiomName cls
   4.179          val vars = dfg_vars cls
   4.180 @@ -886,7 +894,7 @@
   4.181          val funcs = funcs_of_cls cls
   4.182          val preds = preds_of_cls cls
   4.183  	val knd = string_of_kind cls
   4.184 -	val lits_str = concat_with_comma lits
   4.185 +	val lits_str = commas lits
   4.186  	val cls_str = gen_dfg_cls(cls_id,ax_name,knd,lits_str,tvars,vars) 
   4.187      in
   4.188  	(cls_str,tfree_lits) 
   4.189 @@ -894,7 +902,8 @@
   4.190  
   4.191  
   4.192  
   4.193 -fun tfree_dfg_clause tfree_lit = "clause( %(conjecture)\n" ^  "or( " ^ tfree_lit ^ ")),\n" ^ "tfree_tcs" ^  ")."
   4.194 +fun tfree_dfg_clause tfree_lit =
   4.195 +  "clause( %(conjecture)\n" ^ "or( " ^ tfree_lit ^ ")),\n" ^ "tfree_tcs" ^ ")."
   4.196  
   4.197  
   4.198  fun gen_dfg_file probname axioms conjectures funcs preds tfrees= 
   4.199 @@ -1113,8 +1122,8 @@
   4.200  
   4.201  fun string_of_conclLit (ArityClause arcls) = string_of_arLit (#conclLit arcls);
   4.202       
   4.203 -
   4.204 -fun strings_of_premLits (ArityClause arcls) = map string_of_arLit (#premLits arcls);
   4.205 +fun strings_of_premLits (ArityClause arcls) =
   4.206 + map string_of_arLit (#premLits arcls);
   4.207  		
   4.208  
   4.209  fun string_of_arKind (ArityClause arcls) = name_of_kind(#kind arcls);
   4.210 @@ -1127,13 +1136,11 @@
   4.211  	val all_lits = concl_lit :: prems_lits
   4.212      in
   4.213  	"input_clause(" ^ arcls_id ^ "," ^ knd ^ "," ^ (ResLib.list_to_string' all_lits) ^ ")."
   4.214 -	
   4.215      end;
   4.216  
   4.217  
   4.218  val clrelclause_prefix = "relcls_";
   4.219  
   4.220 -
   4.221  fun tptp_classrelLits sub sup = 
   4.222      let val tvar = "(T)"
   4.223      in