1.1 --- a/src/HOL/Tools/ATP/recon_order_clauses.ML Tue Apr 12 13:38:08 2005 +0200
1.2 +++ b/src/HOL/Tools/ATP/recon_order_clauses.ML Wed Apr 13 09:48:41 2005 +0200
1.3 @@ -1,5 +1,3 @@
1.4 -
1.5 -
1.6 (*----------------------------------------------*)
1.7 (* Reorder clauses for use in binary resolution *)
1.8 (*----------------------------------------------*)
1.9 @@ -7,9 +5,6 @@
1.10 fun drop n [] = []
1.11 | drop n (x::xs) = (if n = 0 then (x::xs) else drop (n-1) xs)
1.12
1.13 -fun remove n [] = []
1.14 -| remove n (x::xs) = List.filter (not_equal n) (x::xs);
1.15 -
1.16 fun remove_nth n [] = []
1.17 | remove_nth n xs = (List.take (xs, n-1)) @ (List.drop (xs, n))
1.18
2.1 --- a/src/HOL/Tools/ATP/watcher.ML Tue Apr 12 13:38:08 2005 +0200
2.2 +++ b/src/HOL/Tools/ATP/watcher.ML Wed Apr 13 09:48:41 2005 +0200
2.3 @@ -19,27 +19,12 @@
2.4 use "modUnix";*)
2.5 (*use "/homes/clq20/Jia_Code/TransStartIsar";*)
2.6
2.7 -use "~~/src/HOL/Tools/ATP/VampireCommunication.ML";
2.8 -use "~~/src/HOL/Tools/ATP/SpassCommunication.ML";
2.9 -
2.10 -
2.11 -use "~~/src/HOL/Tools/ATP/modUnix.ML";
2.12 -
2.13
2.14 structure Watcher: WATCHER =
2.15 struct
2.16
2.17 -fun fst (a,b) = a;
2.18 -fun snd (a,b) = b;
2.19 -
2.20 val goals_being_watched = ref 0;
2.21
2.22 -fun remove y [] = []
2.23 -| remove y (x::xs) = (if y = x
2.24 - then
2.25 - remove y xs
2.26 - else ((x::(remove y xs))))
2.27 -
2.28
2.29
2.30 fun sendOutput (outstr,str) = (TextIO.outputSubstr (outstr, (Substring.all str));TextIO.flushOut outstr);
2.31 @@ -230,7 +215,7 @@
2.32
2.33 fun getInIoDesc someInstr =
2.34 let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr)
2.35 - val _ = print (TextIO.stdOut, buf)
2.36 + val _ = TextIO.output (TextIO.stdOut, buf)
2.37 val ioDesc =
2.38 case rd
2.39 of TextPrimIO.RD{ioDesc = SOME iod, ...} =>SOME iod
2.40 @@ -584,7 +569,7 @@
2.41 val childout = snd streams
2.42 val childpid = fst mychild
2.43
2.44 - fun vampire_proofHandler (n:int) =
2.45 + fun vampire_proofHandler (n) =
2.46 (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
2.47 getVampInput childin; Pretty.writeln(Pretty.str (oct_char "361"));() )
2.48
2.49 @@ -636,7 +621,7 @@
2.50 end )
2.51 *)
2.52
2.53 -fun spass_proofHandler (n:int) = (
2.54 +fun spass_proofHandler (n) = (
2.55 let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal1")));
2.56 val _ = TextIO.output (outfile, ("In signal handler now\n"))
2.57 val _ = TextIO.closeOut outfile
2.58 @@ -715,8 +700,8 @@
2.59
2.60
2.61 in
2.62 - Signal.signal (Posix.Signal.usr1, Signal.SIG_HANDLE vampire_proofHandler);
2.63 - Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE spass_proofHandler);
2.64 + IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);
2.65 + IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler);
2.66 (childin, childout, childpid)
2.67
2.68 end
3.1 --- a/src/Pure/ML-Systems/polyml.ML Tue Apr 12 13:38:08 2005 +0200
3.2 +++ b/src/Pure/ML-Systems/polyml.ML Wed Apr 13 09:48:41 2005 +0200
3.3 @@ -179,3 +179,14 @@
3.4 val mkTextWriter = mkWriter
3.5 end;
3.6 end;
3.7 +
3.8 +(** This extension of the Poly/ML Signal structure is only necessary
3.9 + because in SML/NJ, types Posix.Signal.signal and Signals.signal differ.**)
3.10 +
3.11 +structure IsaSignal =
3.12 +struct
3.13 +open Signal
3.14 +val usr1 = Posix.Signal.usr1
3.15 +val usr2 = Posix.Signal.usr2
3.16 +end;
3.17 +
4.1 --- a/src/Pure/ML-Systems/smlnj.ML Tue Apr 12 13:38:08 2005 +0200
4.2 +++ b/src/Pure/ML-Systems/smlnj.ML Wed Apr 13 09:48:41 2005 +0200
4.3 @@ -127,6 +127,35 @@
4.4
4.5 end;
4.6
4.7 +(** Signal handling: emulation of the Poly/ML Signal structure. Note that types
4.8 + Posix.Signal.signal and Signals.signal differ **)
4.9 +
4.10 +structure IsaSignal =
4.11 +struct
4.12 +
4.13 +datatype sig_handle = SIG_DFL | SIG_IGN | SIG_HANDLE of Signals.signal -> unit;
4.14 +
4.15 +(*From the SML/NJ documentation:
4.16 +"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."*)
4.17 +
4.18 +fun toAction SIG_DFL = Signals.DEFAULT
4.19 + | toAction SIG_IGN = Signals.IGNORE
4.20 + | toAction (SIG_HANDLE iu) =
4.21 + Signals.HANDLER (fn (signo,_,cont) => (iu signo; cont));
4.22 +
4.23 +(*The types are correct, but I'm not sure about the semantics!*)
4.24 +fun fromAction Signals.DEFAULT = SIG_DFL
4.25 + | fromAction Signals.IGNORE = SIG_IGN
4.26 + | fromAction (Signals.HANDLER f) =
4.27 + SIG_HANDLE (fn signo => SMLofNJ.Cont.callcc (fn k => (f (signo,0,k); ())));
4.28 +
4.29 +(*Poly/ML version has type int * sig_handle -> sig_handle*)
4.30 +fun signal (signo, sh) = fromAction (Signals.setHandler (signo, toAction sh));
4.31 +
4.32 +val usr1 = UnixSignals.sigUSR1
4.33 +val usr2 = UnixSignals.sigUSR2
4.34 +
4.35 +end;
4.36
4.37
4.38 (** OS related **)