src/HOL/Tools/ATP/watcher.ML
changeset 16260 4a1f36eafe17
parent 16185 bb71c91e781e
child 16357 f1275d2a1dee
     1.1 --- a/src/HOL/Tools/ATP/watcher.ML	Sun Jun 05 11:31:22 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Sun Jun 05 11:31:23 2005 +0200
     1.3 @@ -168,19 +168,19 @@
     1.4  	  (*** only include problem and clasimp for the moment, not sure how to refer to ***)
     1.5  
     1.6  	  (*** hyps/local axioms just now (*,axfile, hypsfile,*)                                               ***)
     1.7 -	  val whole_prob_file = system ("/bin/cat " ^ clasimpfile ^" "^ probfile ^ " > " ^ (File.sysify_path wholefile))
     1.8 +	  val whole_prob_file = system ("cat " ^ clasimpfile ^" "^ probfile ^ " > " ^ File.shell_path wholefile)
     1.9  
    1.10  	  val dfg_create = if File.exists dfg_dir 
    1.11  			   then warning("dfg dir exists")
    1.12  			   else File.mkdir dfg_dir; 
    1.13  	  
    1.14 -	  val dfg_path = File.sysify_path dfg_dir;
    1.15 +	  val dfg_path = File.platform_path dfg_dir;
    1.16  	 (* val exec_tptp2x = 
    1.17  	        Unix.execute(getenv "TPTP2X_HOME" ^ "/tptp2X",  
    1.18 -	                     ["-fdfg", "-d " ^ dfg_path, File.sysify_path wholefile]) *)
    1.19 +	                     ["-fdfg", "-d " ^ dfg_path, File.platform_path wholefile]) *)
    1.20          val tptp_home = getenv "TPTP2X_HOME" ^ "/tptp2X"
    1.21         
    1.22 -        val systemcall = system (tptp_home^" -fdfg -d " ^ dfg_path^" "^( File.sysify_path wholefile))
    1.23 +        val systemcall = system (tptp_home ^ " -fdfg -d " ^ File.shell_path dfg_dir ^ " " ^ File.shell_path wholefile)
    1.24          val _ =  warning("systemcall is "^ (string_of_int systemcall))
    1.25  	(*val _ = Posix.Process.wait ()*)
    1.26  	(*val _ =Unix.reap exec_tptp2x*)
    1.27 @@ -191,7 +191,7 @@
    1.28  	  Posix.Process.sleep(Time.fromSeconds 1); 
    1.29  	  (warning ("probfile is: "^probfile));
    1.30  	  (warning("dfg file is: "^newfile));
    1.31 -	  (warning ("wholefile is: "^(File.sysify_path wholefile)));
    1.32 +	  (warning ("wholefile is: "^(File.platform_path wholefile)));
    1.33  	  sendOutput (toWatcherStr,
    1.34  	       prover ^ "*" ^ thmstring ^ "*" ^ goalstring ^ "*" ^ proverCmd ^ 
    1.35  	       "*" ^ settings ^ "*" ^ newfile ^ "\n");
    1.36 @@ -202,7 +202,7 @@
    1.37  	        (Path.append dfg_dir (Path.basic ("ax_prob"^"_" ^ probID ^ ".dfg")))
    1.38  	  then callResProvers (toWatcherStr, args)
    1.39  	  else error ("tptp2X failed: " ^ getenv "TPTP2X_HOME" ^ "/tptp2X" ^
    1.40 -	              " -fdfg " ^ File.sysify_path wholefile ^ " -d " ^ dfg_path)
    1.41 +	              " -fdfg " ^ File.platform_path wholefile ^ " -d " ^ dfg_path)
    1.42        end
    1.43  (*
    1.44  fun callResProversStr (toWatcherStr,  []) =  "End of calls\n" 
    1.45 @@ -369,7 +369,7 @@
    1.46  		val _ = (warning ("num_of_clauses in watcher is: "^(string_of_int (num_of_clauses))) )       
    1.47  			 *)
    1.48  		(*val goalstr = string_of_thm (the_goal)
    1.49 -		 val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "goal_in_watcher")));  
    1.50 +		 val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "goal_in_watcher")));  
    1.51  		val _ = TextIO.output (outfile,goalstr )
    1.52  		val _ =  TextIO.closeOut outfile*)
    1.53  		fun killChildren [] = ()
    1.54 @@ -722,11 +722,11 @@
    1.55                            
    1.56  
    1.57  fun spass_proofHandler (n) = (
    1.58 -                                 let  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal1")));
    1.59 +                                 let  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_signal1")));
    1.60                                        val _ = TextIO.output (outfile, ("In signal handler now\n"))
    1.61                                        val _ =  TextIO.closeOut outfile
    1.62                                        val (reconstr, thmstring, goalstring) = SpassComm.getSpassInput childin
    1.63 -                                      val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "foo_signal")));
    1.64 +                                      val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal")));
    1.65  
    1.66                                        val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched))))
    1.67                                        val _ =  TextIO.closeOut outfile
    1.68 @@ -743,7 +743,7 @@
    1.69                                                           
    1.70                                                                   if ((!goals_being_watched) = 0)
    1.71                                                                   then 
    1.72 -                                                                    (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_found")));
    1.73 +                                                                    (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_found")));
    1.74                                                                           val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
    1.75                                                                           val _ =  TextIO.closeOut outfile
    1.76                                                                       in
    1.77 @@ -762,7 +762,7 @@
    1.78                                                                        Pretty.writeln(Pretty.str  (oct_char "361"));
    1.79                                                                        if (!goals_being_watched = 0)
    1.80                                                                        then 
    1.81 -                                                                          (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_comp")));
    1.82 +                                                                          (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_comp")));
    1.83                                                                                 val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
    1.84                                                                                 val _ =  TextIO.closeOut outfile
    1.85                                                                             in
    1.86 @@ -781,7 +781,7 @@
    1.87                                                                        Pretty.writeln(Pretty.str  (oct_char "361"));
    1.88                                                                        if (!goals_being_watched = 0)
    1.89                                                                        then 
    1.90 -                                                                          (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_comp")));
    1.91 +                                                                          (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_comp")));
    1.92                                                                                 val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
    1.93                                                                                 val _ =  TextIO.closeOut outfile
    1.94                                                                             in
    1.95 @@ -801,7 +801,7 @@
    1.96                                                                        Pretty.writeln(Pretty.str  (oct_char "361"));
    1.97                                                                        if (!goals_being_watched = 0)
    1.98                                                                        then 
    1.99 -                                                                          (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_comp")));
   1.100 +                                                                          (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_comp")));
   1.101                                                                                 val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   1.102                                                                                 val _ =  TextIO.closeOut outfile
   1.103                                                                             in