src/HOL/Tools/ATP/watcher.ML
changeset 15658 2edb384bf61f
parent 15652 a9d65894962e
child 15681 b667c22edb36
     1.1 --- a/src/HOL/Tools/ATP/watcher.ML	Tue Apr 05 16:32:47 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Wed Apr 06 12:01:37 2005 +0200
     1.3 @@ -97,7 +97,7 @@
     1.4                                                       let 
     1.5                                                          val dfg_dir = File.tmp_path (Path.basic "dfg");
     1.6                                                          (* need to check here if the directory exists and, if not, create it*)
     1.7 -                                                         val  outfile = TextIO.openAppend("thmstring_in_watcher");                                                                                    
     1.8 +                                                         val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic"thmstring_in_watcher")));                                                                                    
     1.9                                                           val _ = TextIO.output (outfile, (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n"))
    1.10                                                           val _ =  TextIO.closeOut outfile
    1.11                                                           val dfg_create =if File.exists dfg_dir 
    1.12 @@ -172,7 +172,7 @@
    1.13                                val settings = getSettings settings []
    1.14                                val (file, rest) =  takeUntil "*" rest []
    1.15                                val file = implode file
    1.16 -                              val  outfile = TextIO.openOut("sep_comms");                                                                                    
    1.17 +                              val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "sep_comms")));                                                                                    
    1.18                                val _ = TextIO.output (outfile,(prover^thmstring^goalstring^proverCmd^file) )
    1.19                                val _ =  TextIO.closeOut outfile
    1.20                                
    1.21 @@ -248,7 +248,7 @@
    1.22  
    1.23  
    1.24  
    1.25 -fun setupWatcher (the_goal) = let
    1.26 +fun setupWatcher () = let
    1.27            (** pipes for communication between parent and watcher **)
    1.28            val p1 = Posix.IO.pipe ()
    1.29            val p2 = Posix.IO.pipe ()
    1.30 @@ -275,10 +275,10 @@
    1.31                        val fromParentIOD = Posix.FileSys.fdToIOD fromParent
    1.32                        val fromParentStr = openInFD ("_exec_in_parent", fromParent)
    1.33                        val toParentStr = openOutFD ("_exec_out_parent", toParent)
    1.34 -                      val goalstr = string_of_thm (the_goal)
    1.35 -                       val  outfile = TextIO.openOut("goal_in_watcher");  
    1.36 +                      (*val goalstr = string_of_thm (the_goal)
    1.37 +                       val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "goal_in_watcher")));  
    1.38                        val _ = TextIO.output (outfile,goalstr )
    1.39 -                      val _ =  TextIO.closeOut outfile
    1.40 +                      val _ =  TextIO.closeOut outfile*)
    1.41                        fun killChildren [] = ()
    1.42                     |      killChildren  (childPid::children) = (killChild childPid; killChildren children)
    1.43  
    1.44 @@ -354,7 +354,7 @@
    1.45                                                  val prover = cmdProver childProc
    1.46                                                  val thmstring = cmdThm childProc
    1.47                                                  val goalstring = cmdGoal childProc
    1.48 -                                                val  outfile = TextIO.openOut("child_comms");  
    1.49 +                                                val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_comms")));  
    1.50                                                  val _ = TextIO.output (outfile,(prover^thmstring^goalstring^childCmd) )
    1.51                                                  val _ =  TextIO.closeOut outfile
    1.52                                              in 
    1.53 @@ -362,7 +362,7 @@
    1.54                                                then 
    1.55                                                    (* check here for prover label on child*)
    1.56                                                     
    1.57 -                                                  let val  outfile = TextIO.openOut("child_incoming");  
    1.58 +                                                  let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_incoming")));  
    1.59                                                  val _ = TextIO.output (outfile,(prover^thmstring^goalstring^childCmd) )
    1.60                                                  val _ =  TextIO.closeOut outfile
    1.61                                                val childDone = (case prover of
    1.62 @@ -385,7 +385,7 @@
    1.63                                                           (childProc::(checkChildren (otherChildren, toParentStr)))
    1.64                                                   end
    1.65                                                 else
    1.66 -                                                   let val  outfile = TextIO.openAppend("child_incoming");  
    1.67 +                                                   let val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "child_incoming")));  
    1.68                                                  val _ = TextIO.output (outfile,"No child output " )
    1.69                                                  val _ =  TextIO.closeOut outfile
    1.70                                                   in
    1.71 @@ -578,7 +578,7 @@
    1.72  (**********************************************************)
    1.73  fun killWatcher pid= killChild pid;
    1.74  
    1.75 -fun createWatcher (the_goal) = let val mychild = childInfo (setupWatcher(the_goal))
    1.76 +fun createWatcher () = let val mychild = childInfo (setupWatcher())
    1.77  			   val streams =snd mychild
    1.78                             val childin = fst streams
    1.79                             val childout = snd streams
    1.80 @@ -590,7 +590,7 @@
    1.81                            
    1.82                            (* fun spass_proofHandler (n:int) = (
    1.83                                                        let val (reconstr, thmstring, goalstring) = getSpassInput childin
    1.84 -                                                          val  outfile = TextIO.openOut("foo_signal");
    1.85 +                                                          val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal")));
    1.86  
    1.87                                                           val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^"  "^thmstring))
    1.88                                                           val _ =  TextIO.closeOut outfile
    1.89 @@ -605,12 +605,12 @@
    1.90  (*
    1.91  
    1.92  fun spass_proofHandler (n:int) = (
    1.93 -                                                      let  val  outfile = TextIO.openOut("foo_signal1");
    1.94 +                                                      let  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal1")));
    1.95  
    1.96                                                           val _ = TextIO.output (outfile, ("In signal handler now\n"))
    1.97                                                           val _ =  TextIO.closeOut outfile
    1.98                                                            val (reconstr, thmstring, goalstring) = getSpassInput childin
    1.99 -                                                         val  outfile = TextIO.openOut("foo_signal");
   1.100 +                                                         val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal")));
   1.101  
   1.102                                                           val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^"  "^thmstring^goalstring))
   1.103                                                           val _ =  TextIO.closeOut outfile
   1.104 @@ -637,11 +637,11 @@
   1.105  *)
   1.106  
   1.107  fun spass_proofHandler (n:int) = (
   1.108 -                                 let  val  outfile = TextIO.openOut("foo_signal1");
   1.109 +                                 let  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal1")));
   1.110                                        val _ = TextIO.output (outfile, ("In signal handler now\n"))
   1.111                                        val _ =  TextIO.closeOut outfile
   1.112                                        val (reconstr, thmstring, goalstring) = getSpassInput childin
   1.113 -                                      val  outfile = TextIO.openAppend("foo_signal");
   1.114 +                                      val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "foo_signal")));
   1.115  
   1.116                                        val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched))))
   1.117                                        val _ =  TextIO.closeOut outfile
   1.118 @@ -658,7 +658,7 @@
   1.119                                                           
   1.120                                                                   if ((!goals_being_watched) = 0)
   1.121                                                                   then 
   1.122 -                                                                    (let val  outfile = TextIO.openOut("foo_reap_found");
   1.123 +                                                                    (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_found")));
   1.124                                                                           val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   1.125                                                                           val _ =  TextIO.closeOut outfile
   1.126                                                                       in
   1.127 @@ -677,7 +677,7 @@
   1.128                                                                        Pretty.writeln(Pretty.str  (oct_char "361"));
   1.129                                                                        if (!goals_being_watched = 0)
   1.130                                                                        then 
   1.131 -                                                                          (let val  outfile = TextIO.openOut("foo_reap_comp");
   1.132 +                                                                          (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_comp")));
   1.133                                                                                 val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   1.134                                                                                 val _ =  TextIO.closeOut outfile
   1.135                                                                             in
   1.136 @@ -696,7 +696,7 @@
   1.137                                                                        Pretty.writeln(Pretty.str  (oct_char "361"));
   1.138                                                                        if (!goals_being_watched = 0)
   1.139                                                                        then 
   1.140 -                                                                          (let val  outfile = TextIO.openOut("foo_reap_comp");
   1.141 +                                                                          (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_comp")));
   1.142                                                                                 val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   1.143                                                                                 val _ =  TextIO.closeOut outfile
   1.144                                                                             in