--- a/src/HOL/Tools/ATP/recon_order_clauses.ML Tue Apr 12 13:38:08 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_order_clauses.ML Wed Apr 13 09:48:41 2005 +0200
@@ -1,5 +1,3 @@
-
-
(*----------------------------------------------*)
(* Reorder clauses for use in binary resolution *)
(*----------------------------------------------*)
@@ -7,9 +5,6 @@
fun drop n [] = []
| drop n (x::xs) = (if n = 0 then (x::xs) else drop (n-1) xs)
-fun remove n [] = []
-| remove n (x::xs) = List.filter (not_equal n) (x::xs);
-
fun remove_nth n [] = []
| remove_nth n xs = (List.take (xs, n-1)) @ (List.drop (xs, n))
--- a/src/HOL/Tools/ATP/watcher.ML Tue Apr 12 13:38:08 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML Wed Apr 13 09:48:41 2005 +0200
@@ -19,27 +19,12 @@
use "modUnix";*)
(*use "/homes/clq20/Jia_Code/TransStartIsar";*)
-use "~~/src/HOL/Tools/ATP/VampireCommunication.ML";
-use "~~/src/HOL/Tools/ATP/SpassCommunication.ML";
-
-
-use "~~/src/HOL/Tools/ATP/modUnix.ML";
-
structure Watcher: WATCHER =
struct
-fun fst (a,b) = a;
-fun snd (a,b) = b;
-
val goals_being_watched = ref 0;
-fun remove y [] = []
-| remove y (x::xs) = (if y = x
- then
- remove y xs
- else ((x::(remove y xs))))
-
fun sendOutput (outstr,str) = (TextIO.outputSubstr (outstr, (Substring.all str));TextIO.flushOut outstr);
@@ -230,7 +215,7 @@
fun getInIoDesc someInstr =
let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr)
- val _ = print (TextIO.stdOut, buf)
+ val _ = TextIO.output (TextIO.stdOut, buf)
val ioDesc =
case rd
of TextPrimIO.RD{ioDesc = SOME iod, ...} =>SOME iod
@@ -584,7 +569,7 @@
val childout = snd streams
val childpid = fst mychild
- fun vampire_proofHandler (n:int) =
+ fun vampire_proofHandler (n) =
(Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
getVampInput childin; Pretty.writeln(Pretty.str (oct_char "361"));() )
@@ -636,7 +621,7 @@
end )
*)
-fun spass_proofHandler (n:int) = (
+fun spass_proofHandler (n) = (
let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal1")));
val _ = TextIO.output (outfile, ("In signal handler now\n"))
val _ = TextIO.closeOut outfile
@@ -715,8 +700,8 @@
in
- Signal.signal (Posix.Signal.usr1, Signal.SIG_HANDLE vampire_proofHandler);
- Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE spass_proofHandler);
+ IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);
+ IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler);
(childin, childout, childpid)
end
--- a/src/Pure/ML-Systems/polyml.ML Tue Apr 12 13:38:08 2005 +0200
+++ b/src/Pure/ML-Systems/polyml.ML Wed Apr 13 09:48:41 2005 +0200
@@ -179,3 +179,14 @@
val mkTextWriter = mkWriter
end;
end;
+
+(** This extension of the Poly/ML Signal structure is only necessary
+ because in SML/NJ, types Posix.Signal.signal and Signals.signal differ.**)
+
+structure IsaSignal =
+struct
+open Signal
+val usr1 = Posix.Signal.usr1
+val usr2 = Posix.Signal.usr2
+end;
+
--- a/src/Pure/ML-Systems/smlnj.ML Tue Apr 12 13:38:08 2005 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML Wed Apr 13 09:48:41 2005 +0200
@@ -127,6 +127,35 @@
end;
+(** Signal handling: emulation of the Poly/ML Signal structure. Note that types
+ Posix.Signal.signal and Signals.signal differ **)
+
+structure IsaSignal =
+struct
+
+datatype sig_handle = SIG_DFL | SIG_IGN | SIG_HANDLE of Signals.signal -> unit;
+
+(*From the SML/NJ documentation:
+"HANDLER(f) installs a handler for a signal. When signal is delivered to the process, the execution state of the current thread will be bundled up as a continuation k, then f(signal,n,k) will be called. The number n is the number of times signal has been signalled since the last time f was invoked for it."*)
+
+fun toAction SIG_DFL = Signals.DEFAULT
+ | toAction SIG_IGN = Signals.IGNORE
+ | toAction (SIG_HANDLE iu) =
+ Signals.HANDLER (fn (signo,_,cont) => (iu signo; cont));
+
+(*The types are correct, but I'm not sure about the semantics!*)
+fun fromAction Signals.DEFAULT = SIG_DFL
+ | fromAction Signals.IGNORE = SIG_IGN
+ | fromAction (Signals.HANDLER f) =
+ SIG_HANDLE (fn signo => SMLofNJ.Cont.callcc (fn k => (f (signo,0,k); ())));
+
+(*Poly/ML version has type int * sig_handle -> sig_handle*)
+fun signal (signo, sh) = fromAction (Signals.setHandler (signo, toAction sh));
+
+val usr1 = UnixSignals.sigUSR1
+val usr2 = UnixSignals.sigUSR2
+
+end;
(** OS related **)