1.1 --- a/src/HOL/Import/replay.ML Wed May 30 23:32:54 2007 +0200
1.2 +++ b/src/HOL/Import/replay.ML Thu May 31 01:25:24 2007 +0200
1.3 @@ -291,10 +291,10 @@
1.4 let
1.5 fun get_facts facts =
1.6 case TextIO.inputLine is of
1.7 - "" => (case facts of
1.8 + NONE => (case facts of
1.9 i::facts => (valOf (Int.fromString i),map P.protect_factname (rev facts))
1.10 | _ => raise ERR "replay_thm" "Bad facts.lst file")
1.11 - | fact => get_facts ((String.substring(fact,0,String.size fact -1 ))::facts)
1.12 + | SOME fact => get_facts ((String.substring(fact,0,String.size fact -1 ))::facts)
1.13 in
1.14 get_facts []
1.15 end
2.1 --- a/src/HOL/Matrix/cplex/Cplex_tools.ML Wed May 30 23:32:54 2007 +0200
2.2 +++ b/src/HOL/Matrix/cplex/Cplex_tools.ML Thu May 31 01:25:24 2007 +0200
2.3 @@ -320,8 +320,9 @@
2.4 )
2.5 end
2.6 else
2.7 - let val s = TextIO.inputLine f in
2.8 - if s = "" then NONE else
2.9 + (case TextIO.inputLine f of
2.10 + NONE => NONE
2.11 + | SOME s =>
2.12 let val t = tokenize s in
2.13 if (length t >= 2 andalso
2.14 snd(hd (tl t)) = ":")
2.15 @@ -334,8 +335,7 @@
2.16 else
2.17 rest := t;
2.18 readToken_helper ()
2.19 - end
2.20 - end
2.21 + end)
2.22
2.23 fun readToken_helper2 () =
2.24 let val c = readToken_helper () in
2.25 @@ -872,9 +872,9 @@
2.26 )
2.27 end
2.28 else
2.29 - let val s = TextIO.inputLine f in
2.30 - if s = "" then NONE else (rest := tokenize s; readToken_helper())
2.31 - end
2.32 + (case TextIO.inputLine f of
2.33 + NONE => NONE
2.34 + | SOME s => (rest := tokenize s; readToken_helper()))
2.35
2.36 fun is_tt tok ty = (tok <> NONE andalso (fst (the tok)) = ty)
2.37
2.38 @@ -1007,11 +1007,9 @@
2.39 )
2.40 end
2.41 else
2.42 - let
2.43 - val s = TextIO.inputLine f
2.44 - in
2.45 - if s = "" then NONE else (rest := tokenize s; readToken_helper())
2.46 - end
2.47 + (case TextIO.inputLine f of
2.48 + NONE => NONE
2.49 + | SOME s => (rest := tokenize s; readToken_helper()))
2.50
2.51 fun is_tt tok ty = (tok <> NONE andalso (fst (the tok)) = ty)
2.52
3.1 --- a/src/HOL/Tools/ATP/watcher.ML Wed May 30 23:32:54 2007 +0200
3.2 +++ b/src/HOL/Tools/ATP/watcher.ML Thu May 31 01:25:24 2007 +0200
3.3 @@ -23,7 +23,7 @@
3.4
3.5 (* Start a watcher and set up signal handlers*)
3.6 val createWatcher :
3.7 - Proof.context * thm * string Vector.vector list ->
3.8 + Proof.context * thm * string Vector.vector list ->
3.9 TextIO.instream * TextIO.outstream * Posix.Process.pid
3.10 val killWatcher : Posix.Process.pid -> unit
3.11 val killChild : ('a, 'b) Unix.proc -> OS.Process.status
3.12 @@ -45,7 +45,7 @@
3.13
3.14 val trace_path = Path.basic "watcher_trace";
3.15
3.16 -fun trace s = if !Output.debugging then File.append (File.tmp_path trace_path) s
3.17 +fun trace s = if !Output.debugging then File.append (File.tmp_path trace_path) s
3.18 else ();
3.19
3.20 (*Representation of a watcher process*)
3.21 @@ -56,7 +56,7 @@
3.22 (*Representation of a child (ATP) process*)
3.23 type cmdproc = {
3.24 prover: string, (* Name of the resolution prover used, e.g. "spass"*)
3.25 - file: string, (* The file containing the goal for the ATP to prove *)
3.26 + file: string, (* The file containing the goal for the ATP to prove *)
3.27 proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc,
3.28 instr : TextIO.instream, (*Output of the child process *)
3.29 outstr : TextIO.outstream}; (*Input to the child process *)
3.30 @@ -69,7 +69,7 @@
3.31 Posix.IO.mkTextWriter {
3.32 appendMode = false,
3.33 initBlkMode = true,
3.34 - name = name,
3.35 + name = name,
3.36 chunkSize=4096,
3.37 fd = fd};
3.38
3.39 @@ -83,14 +83,14 @@
3.40 TextIO.StreamIO.mkInstream (
3.41 fdReader (name, fd), ""));
3.42
3.43 -
3.44 +
3.45 (* Send request to Watcher for a vampire to be called for filename in arg*)
3.46 -fun callResProver (toWatcherStr, arg) =
3.47 - (TextIO.output (toWatcherStr, arg^"\n");
3.48 +fun callResProver (toWatcherStr, arg) =
3.49 + (TextIO.output (toWatcherStr, arg^"\n");
3.50 TextIO.flushOut toWatcherStr)
3.51
3.52 (* Send request to Watcher for multiple provers to be called*)
3.53 -fun callResProvers (toWatcherStr, []) =
3.54 +fun callResProvers (toWatcherStr, []) =
3.55 (TextIO.output (toWatcherStr, "End of calls\n"); TextIO.flushOut toWatcherStr)
3.56 | callResProvers (toWatcherStr,
3.57 (prover,proverCmd,settings,probfile) :: args) =
3.58 @@ -101,45 +101,45 @@
3.59 inc goals_being_watched;
3.60 TextIO.flushOut toWatcherStr;
3.61 callResProvers (toWatcherStr,args))
3.62 -
3.63 +
3.64
3.65 (*Send message to watcher to kill currently running vampires. NOT USED and possibly
3.66 buggy. Note that killWatcher kills the entire process group anyway.*)
3.67 -fun callSlayer toWatcherStr = (TextIO.output (toWatcherStr, "Kill children\n");
3.68 +fun callSlayer toWatcherStr = (TextIO.output (toWatcherStr, "Kill children\n");
3.69 TextIO.flushOut toWatcherStr)
3.70
3.71 -
3.72 +
3.73 (* Get commands from Isabelle*)
3.74 -fun getCmds (toParentStr, fromParentStr, cmdList) =
3.75 - let val thisLine = TextIO.inputLine fromParentStr
3.76 +fun getCmds (toParentStr, fromParentStr, cmdList) =
3.77 + let val thisLine = the_default "" (TextIO.inputLine fromParentStr)
3.78 in
3.79 trace("\nGot command from parent: " ^ thisLine);
3.80 if thisLine = "End of calls\n" orelse thisLine = "" then cmdList
3.81 else if thisLine = "Kill children\n"
3.82 - then (TextIO.output (toParentStr,thisLine);
3.83 + then (TextIO.output (toParentStr,thisLine);
3.84 TextIO.flushOut toParentStr;
3.85 [("","Kill children",[],"")])
3.86 else
3.87 - let val [prover,proverCmd,settingstr,probfile,_] =
3.88 + let val [prover,proverCmd,settingstr,probfile,_] =
3.89 String.tokens (fn c => c = command_sep) thisLine
3.90 val settings = String.tokens (fn c => c = setting_sep) settingstr
3.91 in
3.92 trace ("\nprover: " ^ prover ^ " prover path: " ^ proverCmd ^
3.93 "\n problem file: " ^ probfile);
3.94 - getCmds (toParentStr, fromParentStr,
3.95 - (prover, proverCmd, settings, probfile)::cmdList)
3.96 + getCmds (toParentStr, fromParentStr,
3.97 + (prover, proverCmd, settings, probfile)::cmdList)
3.98 end
3.99 - handle Bind =>
3.100 + handle Bind =>
3.101 (trace "\ngetCmds: command parsing failed!";
3.102 getCmds (toParentStr, fromParentStr, cmdList))
3.103 end
3.104 -
3.105 -
3.106 +
3.107 +
3.108 (*Get Io-descriptor for polling of an input stream*)
3.109 -fun getInIoDesc someInstr =
3.110 +fun getInIoDesc someInstr =
3.111 let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr)
3.112 val _ = TextIO.output (TextIO.stdOut, buf)
3.113 - val ioDesc =
3.114 + val ioDesc =
3.115 case rd
3.116 of TextPrimIO.RD{ioDesc = SOME iod, ...} => SOME iod
3.117 | _ => NONE
3.118 @@ -149,9 +149,9 @@
3.119 ioDesc
3.120 end
3.121
3.122 -fun pollChild fromStr =
3.123 +fun pollChild fromStr =
3.124 case getInIoDesc fromStr of
3.125 - SOME iod =>
3.126 + SOME iod =>
3.127 (case OS.IO.pollDesc iod of
3.128 SOME pd =>
3.129 let val pd' = OS.IO.pollIn pd in
3.130 @@ -179,7 +179,7 @@
3.131 Posix.Process.exit 0w0);
3.132
3.133 (* take an instream and poll its underlying reader for input *)
3.134 -fun pollParentInput (fromParentIOD, fromParentStr, toParentStr) =
3.135 +fun pollParentInput (fromParentIOD, fromParentStr, toParentStr) =
3.136 case OS.IO.pollDesc fromParentIOD of
3.137 SOME pd =>
3.138 (case OS.IO.poll ([OS.IO.pollIn pd], SOME (Time.fromSeconds 2)) of
3.139 @@ -192,7 +192,7 @@
3.140 (*get the number of the subgoal from the filename: the last digit string*)
3.141 fun number_from_filename s =
3.142 case String.tokens (not o Char.isDigit) s of
3.143 - [] => (trace ("\nWatcher could not read subgoal nunber! " ^ s);
3.144 + [] => (trace ("\nWatcher could not read subgoal nunber! " ^ s);
3.145 error "")
3.146 | numbers => valOf (Int.fromString (List.last numbers));
3.147
3.148 @@ -204,7 +204,7 @@
3.149 | execCmds ((prover,proverCmd,settings,file)::cmds) procList =
3.150 let val _ = trace ("\nAbout to execute command: " ^ proverCmd ^ " " ^ file)
3.151 val settings' = List.concat (map (String.tokens Char.isSpace) settings)
3.152 - val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc =
3.153 + val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc =
3.154 Unix.execute(proverCmd, settings' @ [file])
3.155 val (instr, outstr) = Unix.streamsOf childhandle
3.156 val newProcList = {prover=prover, file=file, proc_handle=childhandle,
3.157 @@ -213,42 +213,42 @@
3.158 Date.toString(Date.fromTimeLocal(Time.now())))
3.159 in execCmds cmds newProcList end
3.160
3.161 -fun checkChildren (ctxt, th, thm_names_list) toParentStr children =
3.162 +fun checkChildren (ctxt, th, thm_names_list) toParentStr children =
3.163 let fun check [] = [] (* no children to check *)
3.164 - | check (child::children) =
3.165 + | check (child::children) =
3.166 let val {prover, file, proc_handle, instr=childIn, ...} : cmdproc = child
3.167 val _ = trace ("\nprobfile = " ^ file)
3.168 val sgno = number_from_filename file (*subgoal number*)
3.169 val thm_names = List.nth(thm_names_list, sgno-1);
3.170 val ppid = Posix.ProcEnv.getppid()
3.171 - in
3.172 + in
3.173 if pollChild childIn
3.174 then (* check here for prover label on child*)
3.175 let val _ = trace ("\nInput available from child: " ^ file)
3.176 val childDone = (case prover of
3.177 "vampire" => ResReconstruct.checkVampProofFound
3.178 - (childIn, toParentStr, ppid, file, ctxt, th, sgno, thm_names)
3.179 + (childIn, toParentStr, ppid, file, ctxt, th, sgno, thm_names)
3.180 | "E" => ResReconstruct.checkEProofFound
3.181 - (childIn, toParentStr, ppid, file, ctxt, th, sgno, thm_names)
3.182 + (childIn, toParentStr, ppid, file, ctxt, th, sgno, thm_names)
3.183 | "spass" => ResReconstruct.checkSpassProofFound
3.184 - (childIn, toParentStr, ppid, file, ctxt, th, sgno, thm_names)
3.185 + (childIn, toParentStr, ppid, file, ctxt, th, sgno, thm_names)
3.186 | _ => (trace ("\nBad prover! " ^ prover); true) )
3.187 in
3.188 if childDone (*ATP has reported back (with success OR failure)*)
3.189 - then (Unix.reap proc_handle;
3.190 + then (Unix.reap proc_handle;
3.191 if !Output.debugging then () else OS.FileSys.remove file;
3.192 check children)
3.193 else child :: check children
3.194 end
3.195 else (trace "\nNo child output"; child :: check children)
3.196 end
3.197 - in
3.198 + in
3.199 trace ("\nIn checkChildren, length of queue: " ^ Int.toString(length children));
3.200 - check children
3.201 + check children
3.202 end;
3.203
3.204
3.205 -fun setupWatcher (ctxt, th, thm_names_list) =
3.206 +fun setupWatcher (ctxt, th, thm_names_list) =
3.207 let
3.208 val checkc = checkChildren (ctxt, th, thm_names_list)
3.209 val p1 = Posix.IO.pipe() (*pipes for communication between parent and watcher*)
3.210 @@ -257,9 +257,9 @@
3.211 fun startWatcher procList =
3.212 case Posix.Process.fork() of
3.213 SOME pid => pid (* parent - i.e. main Isabelle process *)
3.214 - | NONE =>
3.215 + | NONE =>
3.216 let (* child - i.e. watcher *)
3.217 - val oldchildin = #infd p1
3.218 + val oldchildin = #infd p1
3.219 val fromParent = Posix.FileSys.wordToFD 0w0
3.220 val oldchildout = #outfd p2
3.221 val toParent = Posix.FileSys.wordToFD 0w1
3.222 @@ -272,27 +272,27 @@
3.223 val () = trace "\nsubgoals forked to startWatcher"
3.224 val limit = ref 200; (*don't let watcher run forever*)
3.225 (*Watcher Loop : Check running ATP processes for output*)
3.226 - fun keepWatching procList =
3.227 - (trace ("\npollParentInput. Limit = " ^ Int.toString (!limit) ^
3.228 + fun keepWatching procList =
3.229 + (trace ("\npollParentInput. Limit = " ^ Int.toString (!limit) ^
3.230 " length(procList) = " ^ Int.toString(length procList));
3.231 OS.Process.sleep (Time.fromMilliseconds 100); limit := !limit - 1;
3.232 - if !limit < 0 then killWatcher (toParentStr, procList)
3.233 - else
3.234 + if !limit < 0 then killWatcher (toParentStr, procList)
3.235 + else
3.236 case pollParentInput(fromParentIOD, fromParentStr, toParentStr) of
3.237 - SOME [(_,"Kill children",_,_)] =>
3.238 - (trace "\nReceived Kill command";
3.239 + SOME [(_,"Kill children",_,_)] =>
3.240 + (trace "\nReceived Kill command";
3.241 killChildren procList; keepWatching [])
3.242 | SOME cmds => (* deal with commands from Isabelle process *)
3.243 - if length procList < 40 then (* Execute locally *)
3.244 - let val _ = trace("\nCommands from parent: " ^
3.245 + if length procList < 40 then (* Execute locally *)
3.246 + let val _ = trace("\nCommands from parent: " ^
3.247 Int.toString(length cmds))
3.248 - val newProcList' = checkc toParentStr (execCmds cmds procList)
3.249 + val newProcList' = checkc toParentStr (execCmds cmds procList)
3.250 in trace "\nCommands executed"; keepWatching newProcList' end
3.251 else (* Execute remotely [FIXME: NOT REALLY] *)
3.252 - let val newProcList' = checkc toParentStr (execCmds cmds procList)
3.253 + let val newProcList' = checkc toParentStr (execCmds cmds procList)
3.254 in keepWatching newProcList' end
3.255 | NONE => (* No new input from Isabelle *)
3.256 - (trace "\nNothing from parent...";
3.257 + (trace "\nNothing from parent...";
3.258 keepWatching(checkc toParentStr procList)))
3.259 handle exn => (*FIXME: exn handler is too general!*)
3.260 (trace ("\nkeepWatching exception handler: " ^ Toplevel.exn_message exn);
3.261 @@ -305,7 +305,7 @@
3.262 Posix.IO.dup2{old = oldchildout, new = toParent};
3.263 Posix.IO.close oldchildout;
3.264 keepWatching (procList)
3.265 - end;
3.266 + end;
3.267
3.268 val _ = TextIO.flushOut TextIO.stdOut
3.269 val pid = startWatcher []
3.270 @@ -328,15 +328,15 @@
3.271 (**********************************************************)
3.272
3.273 (*Signal handler to tidy away zombie processes*)
3.274 -fun reapAll() =
3.275 +fun reapAll() =
3.276 (case Posix.Process.waitpid_nh(Posix.Process.W_ANY_CHILD, []) of
3.277 - SOME _ => reapAll() | NONE => ())
3.278 + SOME _ => reapAll() | NONE => ())
3.279 handle OS.SysErr _ => ()
3.280
3.281 (*FIXME: does the main process need something like this?
3.282 IsaSignal.signal (IsaSignal.chld, IsaSignal.SIG_HANDLE reap)??*)
3.283
3.284 -fun killWatcher pid =
3.285 +fun killWatcher pid =
3.286 (goals_being_watched := 0;
3.287 Posix.Process.kill(Posix.Process.K_GROUP pid, Posix.Signal.kill);
3.288 reapAll());
3.289 @@ -357,19 +357,19 @@
3.290 fun decr_watched() =
3.291 (goals_being_watched := !goals_being_watched - 1;
3.292 if !goals_being_watched = 0
3.293 - then
3.294 + then
3.295 (Output.debug (fn () => ("\nReaping a watcher, childpid = " ^ string_of_pid childpid));
3.296 killWatcher childpid (*???; reapWatcher (childpid, childin, childout)*) )
3.297 else ())
3.298 - fun proofHandler _ =
3.299 + fun proofHandler _ =
3.300 let val _ = trace("\nIn signal handler for pid " ^ string_of_pid childpid)
3.301 - val outcome = ResReconstruct.restore_newlines (TextIO.inputLine childin)
3.302 - val probfile = TextIO.inputLine childin
3.303 + val outcome = ResReconstruct.restore_newlines (the_default "" (TextIO.inputLine childin))
3.304 + val probfile = the_default "" (TextIO.inputLine childin)
3.305 val sgno = number_from_filename probfile
3.306 val text = string_of_subgoal th sgno
3.307 fun report s = priority ("Subgoal " ^ Int.toString sgno ^ ": " ^ s);
3.308 - in
3.309 - Output.debug (fn () => ("In signal handler. outcome = \"" ^ outcome ^
3.310 + in
3.311 + Output.debug (fn () => ("In signal handler. outcome = \"" ^ outcome ^
3.312 "\"\nprobfile = " ^ probfile ^
3.313 "\nGoals being watched: "^ Int.toString (!goals_being_watched)));
3.314 if String.isPrefix "Invalid" outcome
3.315 @@ -377,7 +377,7 @@
3.316 decr_watched())
3.317 else if String.isPrefix "Failure" outcome
3.318 then (report ("Proof attempt failed:\n" ^ text);
3.319 - decr_watched())
3.320 + decr_watched())
3.321 (* print out a list of rules used from clasimpset*)
3.322 else if String.isPrefix "Success" outcome
3.323 then (report (outcome ^ text);
4.1 --- a/src/HOL/Tools/res_atp_provers.ML Wed May 30 23:32:54 2007 +0200
4.2 +++ b/src/HOL/Tools/res_atp_provers.ML Thu May 31 01:25:24 2007 +0200
4.3 @@ -4,20 +4,17 @@
4.4 Functions used for ATP Oracle.
4.5 *)
4.6
4.7 -
4.8 structure ResAtpProvers =
4.9 -
4.10 struct
4.11
4.12 fun seek_line s instr =
4.13 - let val thisLine = TextIO.inputLine instr
4.14 - in thisLine <> "" andalso
4.15 - (thisLine = s orelse seek_line s instr)
4.16 - end;
4.17 + (case TextIO.inputLine instr of
4.18 + NONE => false
4.19 + | SOME thisLine => thisLine = s orelse seek_line s instr);
4.20
4.21 fun location s = warning ("ATP input at: " ^ s);
4.22
4.23 -fun call_vampire (file:string, time: int) =
4.24 +fun call_vampire (file:string, time: int) =
4.25 let val _ = location file
4.26 val runtime = "-t " ^ (string_of_int time)
4.27 val vampire = ResAtp.helper_path "VAMPIRE_HOME" "vampire"
4.28 @@ -29,35 +26,33 @@
4.29 let val _ = location file
4.30 val eprover = ResAtp.helper_path "E_HOME" "eprover"
4.31 val runtime = "--cpu-limit=" ^ (string_of_int time)
4.32 - val (instr,outstr) = Unix.streamsOf (Unix.execute(eprover,
4.33 + val (instr,outstr) = Unix.streamsOf (Unix.execute(eprover,
4.34 [runtime,"--tstp-in","-tAutoDev","-xAutoDev",file]))
4.35 in seek_line "# Proof found!\n" instr
4.36 - end;
4.37 + end;
4.38
4.39 fun call_spass (file:string, time:int) =
4.40 let val _ = location file
4.41 val runtime = "-TimeLimit=" ^ (string_of_int time)
4.42 val spass = ResAtp.helper_path "SPASS_HOME" "SPASS"
4.43 - val (instr,outstr) = Unix.streamsOf (Unix.execute(spass,
4.44 + val (instr,outstr) = Unix.streamsOf (Unix.execute(spass,
4.45 [runtime,"-Splits=0", "-FullRed=0", "-SOS=1",file]))
4.46 in seek_line "SPASS beiseite: Proof found.\n" instr
4.47 end;
4.48
4.49 -fun vampire_o _ (file,time) =
4.50 - if call_vampire (file,time)
4.51 - then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const)
4.52 +fun vampire_o _ (file,time) =
4.53 + if call_vampire (file,time)
4.54 + then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const)
4.55 else (ResAtp.cond_rm_tmp file; raise Fail ("vampire oracle failed"));
4.56
4.57 -fun eprover_o _ (file,time) =
4.58 - if call_eprover (file,time)
4.59 +fun eprover_o _ (file,time) =
4.60 + if call_eprover (file,time)
4.61 then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const)
4.62 else (ResAtp.cond_rm_tmp file; raise Fail ("eprover oracle failed"));
4.63
4.64 fun spass_o _ (file,time) =
4.65 - if call_spass (file,time)
4.66 - then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const)
4.67 - else (ResAtp.cond_rm_tmp file; raise Fail ("SPASS oracle failed"));
4.68 -
4.69 + if call_spass (file,time)
4.70 + then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const)
4.71 + else (ResAtp.cond_rm_tmp file; raise Fail ("SPASS oracle failed"));
4.72
4.73 end;
4.74 -
5.1 --- a/src/HOL/Tools/res_reconstruct.ML Wed May 30 23:32:54 2007 +0200
5.2 +++ b/src/HOL/Tools/res_reconstruct.ML Thu May 31 01:25:24 2007 +0200
5.3 @@ -8,16 +8,16 @@
5.4 (***************************************************************************)
5.5 signature RES_RECONSTRUCT =
5.6 sig
5.7 - val checkEProofFound:
5.8 - TextIO.instream * TextIO.outstream * Posix.Process.pid *
5.9 + val checkEProofFound:
5.10 + TextIO.instream * TextIO.outstream * Posix.Process.pid *
5.11 string * Proof.context * thm * int * string Vector.vector -> bool
5.12 - val checkVampProofFound:
5.13 - TextIO.instream * TextIO.outstream * Posix.Process.pid *
5.14 + val checkVampProofFound:
5.15 + TextIO.instream * TextIO.outstream * Posix.Process.pid *
5.16 string * Proof.context * thm * int * string Vector.vector -> bool
5.17 - val checkSpassProofFound:
5.18 - TextIO.instream * TextIO.outstream * Posix.Process.pid *
5.19 + val checkSpassProofFound:
5.20 + TextIO.instream * TextIO.outstream * Posix.Process.pid *
5.21 string * Proof.context * thm * int * string Vector.vector -> bool
5.22 - val signal_parent:
5.23 + val signal_parent:
5.24 TextIO.outstream * Posix.Process.pid * string * string -> unit
5.25
5.26 end;
5.27 @@ -27,7 +27,7 @@
5.28
5.29 val trace_path = Path.basic "atp_trace";
5.30
5.31 -fun trace s = if !Output.debugging then File.append (File.tmp_path trace_path) s
5.32 +fun trace s = if !Output.debugging then File.append (File.tmp_path trace_path) s
5.33 else ();
5.34
5.35 (*Full proof reconstruction wanted*)
5.36 @@ -74,7 +74,7 @@
5.37 | syn_equal (t1, SOME (SOME _, t2)) = negate (equate (t1,t2));
5.38
5.39 (*Literals can involve negation, = and !=.*)
5.40 -val literal = $$"~" |-- term >> negate ||
5.41 +val literal = $$"~" |-- term >> negate ||
5.42 (term -- Scan.option (Scan.option ($$"!") --| $$"=" -- term) >> syn_equal) ;
5.43
5.44 val literals = literal -- Scan.repeat ($$"|" |-- literal) >> op:: ;
5.45 @@ -86,8 +86,8 @@
5.46
5.47 (*<cnf_annotated> ::=Êcnf(<name>,<formula_role>,<cnf_formula><annotations>).
5.48 The <name> could be an identifier, but we assume integers.*)
5.49 -val tstp_line = (Scan.this_string "cnf" -- $$"(") |--
5.50 - integer --| $$"," -- Symbol.scan_id --| $$"," --
5.51 +val tstp_line = (Scan.this_string "cnf" -- $$"(") |--
5.52 + integer --| $$"," -- Symbol.scan_id --| $$"," --
5.53 clause -- Scan.option annotations --| $$ ")";
5.54
5.55
5.56 @@ -121,7 +121,7 @@
5.57 else if check_valid_int sti
5.58 then (Char.chr (cList2int sti) :: s)
5.59 else (sti @ (#"_" :: s))
5.60 - in normalise_s s' cs false []
5.61 + in normalise_s s' cs false []
5.62 end
5.63 else normalise_s s cs true []
5.64 | normalise_s s (c::cs) true sti =
5.65 @@ -147,7 +147,7 @@
5.66 exception STREE of stree;
5.67
5.68 (*If string s has the prefix s1, return the result of deleting it.*)
5.69 -fun strip_prefix s1 s =
5.70 +fun strip_prefix s1 s =
5.71 if String.isPrefix s1 s then SOME (normalise_string (String.extract (s, size s1, NONE)))
5.72 else NONE;
5.73
5.74 @@ -168,17 +168,17 @@
5.75 fun type_of_stree t =
5.76 case t of
5.77 Int _ => raise STREE t
5.78 - | Br (a,ts) =>
5.79 + | Br (a,ts) =>
5.80 let val Ts = map type_of_stree ts
5.81 - in
5.82 + in
5.83 case strip_prefix ResClause.tconst_prefix a of
5.84 SOME b => Type(invert_type_const b, Ts)
5.85 - | NONE =>
5.86 + | NONE =>
5.87 if not (null ts) then raise STREE t (*only tconsts have type arguments*)
5.88 - else
5.89 + else
5.90 case strip_prefix ResClause.tfree_prefix a of
5.91 SOME b => TFree("'" ^ b, HOLogic.typeS)
5.92 - | NONE =>
5.93 + | NONE =>
5.94 case strip_prefix ResClause.tvar_prefix a of
5.95 SOME b => make_tvar b
5.96 | NONE => make_tvar a (*Variable from the ATP, say X1*)
5.97 @@ -186,7 +186,7 @@
5.98
5.99 (*Invert the table of translations between Isabelle and ATPs*)
5.100 val const_trans_table_inv =
5.101 - Symtab.update ("fequal", "op =")
5.102 + Symtab.update ("fequal", "op =")
5.103 (Symtab.make (map swap (Symtab.dest ResClause.const_trans_table)));
5.104
5.105 fun invert_const c =
5.106 @@ -207,11 +207,11 @@
5.107 Int _ => raise STREE t
5.108 | Br ("hBOOL",[t]) => term_of_stree [] thy t (*ignore hBOOL*)
5.109 | Br ("hAPP",[t,u]) => term_of_stree (u::args) thy t
5.110 - | Br (a,ts) =>
5.111 + | Br (a,ts) =>
5.112 case strip_prefix ResClause.const_prefix a of
5.113 - SOME "equal" =>
5.114 + SOME "equal" =>
5.115 list_comb(Const ("op =", HOLogic.typeT), List.map (term_of_stree [] thy) ts)
5.116 - | SOME b =>
5.117 + | SOME b =>
5.118 let val c = invert_const b
5.119 val nterms = length ts - num_typargs thy c
5.120 val us = List.map (term_of_stree [] thy) (List.take(ts,nterms) @ args)
5.121 @@ -224,17 +224,17 @@
5.122 val opr = (*a Free variable is typically a Skolem function*)
5.123 case strip_prefix ResClause.fixed_var_prefix a of
5.124 SOME b => Free(b,T)
5.125 - | NONE =>
5.126 + | NONE =>
5.127 case strip_prefix ResClause.schematic_var_prefix a of
5.128 SOME b => make_var (b,T)
5.129 | NONE => make_var (a,T) (*Variable from the ATP, say X1*)
5.130 in list_comb (opr, List.map (term_of_stree [] thy) (args@ts)) end;
5.131
5.132 -(*Type class literal applied to a type. Returns triple of polarity, class, type.*)
5.133 +(*Type class literal applied to a type. Returns triple of polarity, class, type.*)
5.134 fun constraint_of_stree pol (Br("c_Not",[t])) = constraint_of_stree (not pol) t
5.135 | constraint_of_stree pol t = case t of
5.136 Int _ => raise STREE t
5.137 - | Br (a,ts) =>
5.138 + | Br (a,ts) =>
5.139 (case (strip_prefix ResClause.class_prefix a, map type_of_stree ts) of
5.140 (SOME b, [T]) => (pol, b, T)
5.141 | _ => raise STREE t);
5.142 @@ -252,16 +252,16 @@
5.143
5.144 (*Final treatment of the list of "real" literals from a clause.*)
5.145 fun finish [] = HOLogic.true_const (*No "real" literals means only type information*)
5.146 - | finish lits =
5.147 + | finish lits =
5.148 case nofalses lits of
5.149 [] => HOLogic.false_const (*The empty clause, since we started with real literals*)
5.150 | xs => foldr1 HOLogic.mk_disj (rev xs);
5.151
5.152 (*Accumulate sort constraints in vt, with "real" literals in lits.*)
5.153 fun lits_of_strees ctxt (vt, lits) [] = (vt, finish lits)
5.154 - | lits_of_strees ctxt (vt, lits) (t::ts) =
5.155 + | lits_of_strees ctxt (vt, lits) (t::ts) =
5.156 lits_of_strees ctxt (add_constraint (constraint_of_stree true t, vt), lits) ts
5.157 - handle STREE _ =>
5.158 + handle STREE _ =>
5.159 lits_of_strees ctxt (vt, term_of_stree [] (ProofContext.theory_of ctxt) t :: lits) ts;
5.160
5.161 (*Update TVars/TFrees with detected sort constraints.*)
5.162 @@ -279,7 +279,7 @@
5.163
5.164 (*Interpret a list of syntax trees as a clause, given by "real" literals and sort constraints.
5.165 vt0 holds the initial sort constraints, from the conjecture clauses.*)
5.166 -fun clause_of_strees_aux ctxt vt0 ts =
5.167 +fun clause_of_strees_aux ctxt vt0 ts =
5.168 let val (vt, dt) = lits_of_strees ctxt (vt0,[]) ts in
5.169 singleton (ProofContext.infer_types ctxt) (TypeInfer.constrain (fix_sorts vt dt) HOLogic.boolT)
5.170 end;
5.171 @@ -315,7 +315,7 @@
5.172 | add_tfree_constraint (_, vt) = vt;
5.173
5.174 fun tfree_constraints_of_clauses vt [] = vt
5.175 - | tfree_constraints_of_clauses vt ([lit]::tss) =
5.176 + | tfree_constraints_of_clauses vt ([lit]::tss) =
5.177 (tfree_constraints_of_clauses (add_tfree_constraint (constraint_of_stree true lit, vt)) tss
5.178 handle STREE _ => (*not a positive type constraint: ignore*)
5.179 tfree_constraints_of_clauses vt tss)
5.180 @@ -341,13 +341,13 @@
5.181 | smash_types (f$t) = smash_types f $ smash_types t
5.182 | smash_types t = t;
5.183
5.184 -val sort_lits = sort Term.fast_term_ord o dest_disj o
5.185 +val sort_lits = sort Term.fast_term_ord o dest_disj o
5.186 smash_types o HOLogic.dest_Trueprop o strip_all_body;
5.187
5.188 fun permuted_clause t =
5.189 let val lits = sort_lits t
5.190 fun perm [] = NONE
5.191 - | perm (ctm::ctms) =
5.192 + | perm (ctm::ctms) =
5.193 if forall (op aconv) (ListPair.zip (lits, sort_lits ctm)) then SOME ctm
5.194 else perm ctms
5.195 in perm end;
5.196 @@ -364,7 +364,7 @@
5.197 SOME u => "assume " ^ lname ^ ": \"" ^ string_of u ^ "\"\n"
5.198 | NONE => "assume? " ^ lname ^ ": \"" ^ string_of t ^ "\"\n") (*no match!!*)
5.199 | doline have (lname, t, deps) =
5.200 - have_or_show have lname ^ string_of t ^
5.201 + have_or_show have lname ^ string_of t ^
5.202 "\"\n by (metis " ^ space_implode " " deps ^ ")\n"
5.203 fun dolines [(lname, t, deps)] = [doline "show " (lname, t, deps)]
5.204 | dolines ((lname, t, deps)::lines) = doline "have " (lname, t, deps) :: dolines lines
5.205 @@ -377,14 +377,14 @@
5.206
5.207 fun replace_dep (old:int, new) dep = if dep=old then new else [dep];
5.208
5.209 -fun replace_deps (old:int, new) (lno, t, deps) =
5.210 +fun replace_deps (old:int, new) (lno, t, deps) =
5.211 (lno, t, foldl (op union_int) [] (map (replace_dep (old, new)) deps));
5.212
5.213 (*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ
5.214 only in type information.*)
5.215 fun add_prfline ((lno, "axiom", t, []), lines) = (*axioms are not proof lines*)
5.216 if eq_types t (*must be clsrel/clsarity: type information, so delete refs to it*)
5.217 - then map (replace_deps (lno, [])) lines
5.218 + then map (replace_deps (lno, [])) lines
5.219 else
5.220 (case take_prefix (notequal t) lines of
5.221 (_,[]) => lines (*no repetition of proof line*)
5.222 @@ -398,22 +398,22 @@
5.223 else (*FIXME: Doesn't this code risk conflating proofs involving different types??*)
5.224 case take_prefix (notequal t) lines of
5.225 (_,[]) => (lno, t, deps) :: lines (*no repetition of proof line*)
5.226 - | (pre, (lno',t',deps')::post) =>
5.227 + | (pre, (lno',t',deps')::post) =>
5.228 (lno, t', deps) :: (*repetition: replace later line by earlier one*)
5.229 (pre @ map (replace_deps (lno', [lno])) post);
5.230
5.231 (*Recursively delete empty lines (type information) from the proof.*)
5.232 fun add_nonnull_prfline ((lno, t, []), lines) = (*no dependencies, so a conjecture clause*)
5.233 if eq_types t (*must be type information, tfree_tcs, clsrel, clsarity: delete refs to it*)
5.234 - then delete_dep lno lines
5.235 - else (lno, t, []) :: lines
5.236 + then delete_dep lno lines
5.237 + else (lno, t, []) :: lines
5.238 | add_nonnull_prfline ((lno, t, deps), lines) = (lno, t, deps) :: lines
5.239 and delete_dep lno lines = foldr add_nonnull_prfline [] (map (replace_deps (lno, [])) lines);
5.240
5.241 fun bad_free (Free (a,_)) = String.isPrefix "llabs_" a orelse String.isPrefix "sko_" a
5.242 | bad_free _ = false;
5.243
5.244 -(*TVars are forbidden in goals. Also, we don't want lines with <2 dependencies.
5.245 +(*TVars are forbidden in goals. Also, we don't want lines with <2 dependencies.
5.246 To further compress proofs, setting modulus:=n deletes every nth line, and nlines
5.247 counts the number of proof lines processed so far.
5.248 Deleted lines are replaced by their own dependencies. Note that the "add_nonnull_prfline"
5.249 @@ -423,7 +423,7 @@
5.250 | add_wanted_prfline (line, (nlines, [])) = (nlines, [line]) (*final line must be kept*)
5.251 | add_wanted_prfline ((lno, t, deps), (nlines, lines)) =
5.252 if eq_types t orelse not (null (term_tvars t)) orelse
5.253 - length deps < 2 orelse nlines mod !modulus <> 0 orelse
5.254 + length deps < 2 orelse nlines mod !modulus <> 0 orelse
5.255 exists bad_free (term_frees t)
5.256 then (nlines+1, map (replace_deps (lno, deps)) lines) (*Delete line*)
5.257 else (nlines+1, (lno, t, deps) :: lines);
5.258 @@ -432,9 +432,9 @@
5.259 fun stringify_deps thm_names deps_map [] = []
5.260 | stringify_deps thm_names deps_map ((lno, t, deps) :: lines) =
5.261 if lno <= Vector.length thm_names (*axiom*)
5.262 - then (Vector.sub(thm_names,lno-1), t, []) :: stringify_deps thm_names deps_map lines
5.263 + then (Vector.sub(thm_names,lno-1), t, []) :: stringify_deps thm_names deps_map lines
5.264 else let val lname = Int.toString (length deps_map)
5.265 - fun fix lno = if lno <= Vector.length thm_names
5.266 + fun fix lno = if lno <= Vector.length thm_names
5.267 then SOME(Vector.sub(thm_names,lno-1))
5.268 else AList.lookup op= deps_map lno;
5.269 in (lname, t, List.mapPartial fix (distinct (op=) deps)) ::
5.270 @@ -448,15 +448,15 @@
5.271
5.272 fun decode_tstp_file cnfs ctxt th sgno thm_names =
5.273 let val tuples = map (dest_tstp o tstp_line o explode) cnfs
5.274 - val nonnull_lines =
5.275 - foldr add_nonnull_prfline []
5.276 + val nonnull_lines =
5.277 + foldr add_nonnull_prfline []
5.278 (foldr add_prfline [] (decode_tstp_list ctxt tuples))
5.279 val (_,lines) = foldr add_wanted_prfline (0,[]) nonnull_lines
5.280 val (ccls,fixes) = ResAxioms.neg_conjecture_clauses th sgno
5.281 val ccls = map forall_intr_vars ccls
5.282 - in
5.283 + in
5.284 app (fn th => Output.debug (fn () => string_of_thm th)) ccls;
5.285 - isar_header (map #1 fixes) ^
5.286 + isar_header (map #1 fixes) ^
5.287 String.concat (isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines))
5.288 end;
5.289
5.290 @@ -469,17 +469,17 @@
5.291 val encode_newlines = String.translate (fn c => if c = #"\n" then "\t" else str c);
5.292 val restore_newlines = String.translate (fn c => if c = #"\t" then "\n" else str c);
5.293
5.294 -fun signal_success probfile toParent ppid msg =
5.295 +fun signal_success probfile toParent ppid msg =
5.296 (trace ("\nReporting Success for " ^ probfile ^ "\n" ^ msg);
5.297 TextIO.output (toParent, "Success. " ^ encode_newlines msg ^ "\n");
5.298 TextIO.output (toParent, probfile ^ "\n");
5.299 TextIO.flushOut toParent;
5.300 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2));
5.301
5.302 -fun tstp_extract proofextract probfile toParent ppid ctxt th sgno thm_names =
5.303 +fun tstp_extract proofextract probfile toParent ppid ctxt th sgno thm_names =
5.304 let val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract))
5.305 - in
5.306 - signal_success probfile toParent ppid
5.307 + in
5.308 + signal_success probfile toParent ppid
5.309 (decode_tstp_file cnfs ctxt th sgno thm_names)
5.310 end;
5.311
5.312 @@ -487,8 +487,8 @@
5.313 (**** retrieve the axioms that were used in the proof ****)
5.314
5.315 (*Get names of axioms used. Axioms are indexed from 1, while the vector is indexed from 0*)
5.316 -fun get_axiom_names (thm_names: string vector) step_nums =
5.317 - let fun is_axiom n = n <= Vector.length thm_names
5.318 +fun get_axiom_names (thm_names: string vector) step_nums =
5.319 + let fun is_axiom n = n <= Vector.length thm_names
5.320 fun index i = Vector.sub(thm_names, i-1)
5.321 val axnums = List.filter is_axiom step_nums
5.322 val axnames = sort_distinct string_ord (map index axnums)
5.323 @@ -497,10 +497,10 @@
5.324 else axnames
5.325 end
5.326
5.327 - (*String contains multiple lines. We want those of the form
5.328 + (*String contains multiple lines. We want those of the form
5.329 "253[0:Inp] et cetera..."
5.330 A list consisting of the first number in each line is returned. *)
5.331 -fun get_spass_linenums proofstr =
5.332 +fun get_spass_linenums proofstr =
5.333 let val toks = String.tokens (not o Char.isAlphaNum)
5.334 fun inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok
5.335 | inputno _ = NONE
5.336 @@ -509,7 +509,7 @@
5.337
5.338 fun get_axiom_names_spass proofstr thm_names =
5.339 get_axiom_names thm_names (get_spass_linenums proofstr);
5.340 -
5.341 +
5.342 fun not_comma c = c <> #",";
5.343
5.344 (*A valid TSTP axiom line has the form cnf(NNN,axiom,...) where NNN is a positive integer.*)
5.345 @@ -520,18 +520,18 @@
5.346 (*We only allow negated_conjecture because the line number will be removed in
5.347 get_axiom_names above, while suppressing the UNSOUND warning*)
5.348 val ints = if Substring.string rolef mem_string ["axiom","negated_conjecture"]
5.349 - then Substring.string intf
5.350 - else "error"
5.351 + then Substring.string intf
5.352 + else "error"
5.353 in Int.fromString ints end
5.354 - handle Fail _ => NONE;
5.355 + handle Fail _ => NONE;
5.356
5.357 fun get_axiom_names_tstp proofstr thm_names =
5.358 get_axiom_names thm_names (List.mapPartial parse_tstp_line (split_lines proofstr));
5.359 -
5.360 - (*String contains multiple lines. We want those of the form
5.361 +
5.362 + (*String contains multiple lines. We want those of the form
5.363 "*********** [448, input] ***********".
5.364 A list consisting of the first number in each line is returned. *)
5.365 -fun get_vamp_linenums proofstr =
5.366 +fun get_vamp_linenums proofstr =
5.367 let val toks = String.tokens (not o Char.isAlphaNum)
5.368 fun inputno [ntok,"input"] = Int.fromString ntok
5.369 | inputno _ = NONE
5.370 @@ -540,21 +540,21 @@
5.371
5.372 fun get_axiom_names_vamp proofstr thm_names =
5.373 get_axiom_names thm_names (get_vamp_linenums proofstr);
5.374 -
5.375 +
5.376 fun rules_to_metis [] = "metis"
5.377 | rules_to_metis xs = "(metis " ^ space_implode " " xs ^ ")"
5.378
5.379
5.380 (*The signal handler in watcher.ML must be able to read the output of this.*)
5.381 -fun prover_lemma_list_aux getax proofstr probfile toParent ppid thm_names =
5.382 +fun prover_lemma_list_aux getax proofstr probfile toParent ppid thm_names =
5.383 (trace ("\n\nGetting lemma names. proofstr is " ^ proofstr ^
5.384 " num of clauses is " ^ string_of_int (Vector.length thm_names));
5.385 - signal_success probfile toParent ppid
5.386 + signal_success probfile toParent ppid
5.387 ("Try this command: \n apply " ^ rules_to_metis (getax proofstr thm_names))
5.388 )
5.389 handle e => (*FIXME: exn handler is too general!*)
5.390 (trace ("\nprover_lemma_list_aux: In exception handler: " ^ Toplevel.exn_message e);
5.391 - TextIO.output (toParent, "Translation failed for the proof: " ^
5.392 + TextIO.output (toParent, "Translation failed for the proof: " ^
5.393 String.toString proofstr ^ "\n");
5.394 TextIO.output (toParent, probfile);
5.395 TextIO.flushOut toParent;
5.396 @@ -570,9 +570,9 @@
5.397 (**** Extracting proofs from an ATP's output ****)
5.398
5.399 (*Return everything in s that comes before the string t*)
5.400 -fun cut_before t s =
5.401 +fun cut_before t s =
5.402 let val (s1,s2) = Substring.position t (Substring.full s)
5.403 - in if Substring.size s2 = 0 then error "cut_before: string not found"
5.404 + in if Substring.size s2 = 0 then error "cut_before: string not found"
5.405 else Substring.string s2
5.406 end;
5.407
5.408 @@ -593,29 +593,28 @@
5.409 return value is currently never used!*)
5.410 fun startTransfer endS (fromChild, toParent, ppid, probfile, ctxt, th, sgno, thm_names) =
5.411 let fun transferInput currentString =
5.412 - let val thisLine = TextIO.inputLine fromChild
5.413 - in
5.414 - if thisLine = "" (*end of file?*)
5.415 - then (trace ("\n extraction_failed. End bracket: " ^ endS ^
5.416 - "\naccumulated text: " ^ currentString);
5.417 - false)
5.418 - else if String.isPrefix endS thisLine
5.419 + (case TextIO.inputLine fromChild of
5.420 + NONE => (*end of file?*)
5.421 + (trace ("\n extraction_failed. End bracket: " ^ endS ^
5.422 + "\naccumulated text: " ^ currentString);
5.423 + false)
5.424 + | SOME thisLine =>
5.425 + if String.isPrefix endS thisLine
5.426 then let val proofextract = currentString ^ cut_before endS thisLine
5.427 val lemma_list = if endS = end_V8 then vamp_lemma_list
5.428 else if endS = end_SPASS then spass_lemma_list
5.429 else e_lemma_list
5.430 in
5.431 - trace ("\nExtracted proof:\n" ^ proofextract);
5.432 + trace ("\nExtracted proof:\n" ^ proofextract);
5.433 if !full andalso String.isPrefix "cnf(" proofextract
5.434 then tstp_extract proofextract probfile toParent ppid ctxt th sgno thm_names
5.435 else lemma_list proofextract probfile toParent ppid thm_names;
5.436 true
5.437 end
5.438 - else transferInput (currentString^thisLine)
5.439 - end
5.440 + else transferInput (currentString^thisLine))
5.441 in
5.442 transferInput ""
5.443 - end
5.444 + end
5.445
5.446
5.447 (*The signal handler in watcher.ML must be able to read the output of this.*)
5.448 @@ -632,27 +631,23 @@
5.449
5.450 (*Called from watcher. Returns true if the Vampire process has returned a verdict.*)
5.451 fun checkVampProofFound (arg as (fromChild, toParent, ppid, probfile, ctxt, th, sgno, thm_names)) =
5.452 - let val thisLine = TextIO.inputLine fromChild
5.453 - in
5.454 - trace thisLine;
5.455 - if thisLine = ""
5.456 - then (trace "\nNo proof output seen"; false)
5.457 - else if String.isPrefix start_V8 thisLine
5.458 + (case TextIO.inputLine fromChild of
5.459 + NONE => (trace "\nNo proof output seen"; false)
5.460 + | SOME thisLine =>
5.461 + if String.isPrefix start_V8 thisLine
5.462 then startTransfer end_V8 arg
5.463 else if (String.isPrefix "Satisfiability detected" thisLine) orelse
5.464 (String.isPrefix "Refutation not found" thisLine)
5.465 then (signal_parent (toParent, ppid, "Failure\n", probfile);
5.466 true)
5.467 - else checkVampProofFound arg
5.468 - end
5.469 + else checkVampProofFound arg);
5.470
5.471 (*Called from watcher. Returns true if the E process has returned a verdict.*)
5.472 -fun checkEProofFound (arg as (fromChild, toParent, ppid, probfile, ctxt, th, sgno, thm_names)) =
5.473 - let val thisLine = TextIO.inputLine fromChild
5.474 - in
5.475 - trace thisLine;
5.476 - if thisLine = "" then (trace "\nNo proof output seen"; false)
5.477 - else if String.isPrefix start_E thisLine
5.478 +fun checkEProofFound (arg as (fromChild, toParent, ppid, probfile, ctxt, th, sgno, thm_names)) =
5.479 + (case TextIO.inputLine fromChild of
5.480 + NONE => (trace "\nNo proof output seen"; false)
5.481 + | SOME thisLine =>
5.482 + if String.isPrefix start_E thisLine
5.483 then startTransfer end_E arg
5.484 else if String.isPrefix "# Problem is satisfiable" thisLine
5.485 then (signal_parent (toParent, ppid, "Invalid\n", probfile);
5.486 @@ -660,16 +655,14 @@
5.487 else if String.isPrefix "# Cannot determine problem status within resource limit" thisLine
5.488 then (signal_parent (toParent, ppid, "Failure\n", probfile);
5.489 true)
5.490 - else checkEProofFound arg
5.491 - end;
5.492 + else checkEProofFound arg);
5.493
5.494 (*Called from watcher. Returns true if the SPASS process has returned a verdict.*)
5.495 -fun checkSpassProofFound (arg as (fromChild, toParent, ppid, probfile, ctxt, th, sgno, thm_names)) =
5.496 - let val thisLine = TextIO.inputLine fromChild
5.497 - in
5.498 - trace thisLine;
5.499 - if thisLine = "" then (trace "\nNo proof output seen"; false)
5.500 - else if String.isPrefix "Here is a proof" thisLine
5.501 +fun checkSpassProofFound (arg as (fromChild, toParent, ppid, probfile, ctxt, th, sgno, thm_names)) =
5.502 + (case TextIO.inputLine fromChild of
5.503 + NONE => (trace "\nNo proof output seen"; false)
5.504 + | SOME thisLine =>
5.505 + if String.isPrefix "Here is a proof" thisLine
5.506 then startTransfer end_SPASS arg
5.507 else if thisLine = "SPASS beiseite: Completion found.\n"
5.508 then (signal_parent (toParent, ppid, "Invalid\n", probfile);
5.509 @@ -678,7 +671,6 @@
5.510 thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n"
5.511 then (signal_parent (toParent, ppid, "Failure\n", probfile);
5.512 true)
5.513 - else checkSpassProofFound arg
5.514 - end
5.515 + else checkSpassProofFound arg);
5.516
5.517 end;
6.1 --- a/src/Pure/General/source.ML Wed May 30 23:32:54 2007 +0200
6.2 +++ b/src/Pure/General/source.ML Thu May 31 01:25:24 2007 +0200
6.3 @@ -124,7 +124,9 @@
6.4 else
6.5 (TextIO.output (outstream, prompt);
6.6 TextIO.flushOut outstream;
6.7 - (input @ explode (TextIO.inputLine instream), ()))
6.8 + (case TextIO.inputLine instream of
6.9 + SOME line => (input @ explode line, ())
6.10 + | NONE => (input, ())))
6.11 end;
6.12
6.13 fun of_stream instream outstream =
7.1 --- a/src/Pure/ML-Systems/alice.ML Wed May 30 23:32:54 2007 +0200
7.2 +++ b/src/Pure/ML-Systems/alice.ML Thu May 31 01:25:24 2007 +0200
7.3 @@ -104,11 +104,7 @@
7.4 structure TextIO =
7.5 struct
7.6 open TextIO;
7.7 -
7.8 - fun inputLine is =
7.9 - (case TextIO.inputLine is of
7.10 - SOME str => str
7.11 - | NONE => "")
7.12 + fun inputLine is = TextIO.inputLine is
7.13 handle IO.Io _ => raise Interrupt;
7.14 end;
7.15
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/src/Pure/ML-Systems/polyml-4.1.3.ML Thu May 31 01:25:24 2007 +0200
8.3 @@ -0,0 +1,8 @@
8.4 +(* Title: Pure/ML-Systems/polyml-4.1.3.ML
8.5 + ID: $Id$
8.6 +
8.7 +Compatibility wrapper for Poly/ML 4.1.3.
8.8 +*)
8.9 +
8.10 +use "ML-Systems/polyml-old-basis.ML";
8.11 +use "ML-Systems/polyml.ML";
9.1 --- a/src/Pure/ML-Systems/polyml-4.1.4-patch.ML Wed May 30 23:32:54 2007 +0200
9.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
9.3 @@ -1,28 +0,0 @@
9.4 -(* Title: Pure/ML-Systems/polyml-4.1.4-patch.ML
9.5 - ID: $Id$
9.6 -
9.7 -Basis library fixes for Poly/ML 4.2.0 or later.
9.8 -*)
9.9 -
9.10 -structure Posix =
9.11 -struct
9.12 - open Posix;
9.13 - structure IO =
9.14 - struct
9.15 - open IO;
9.16 - val mkReader = mkTextReader;
9.17 - val mkWriter = mkTextWriter;
9.18 - end;
9.19 -end;
9.20 -
9.21 -structure TextIO =
9.22 -struct
9.23 - open TextIO;
9.24 - fun inputLine is = Option.getOpt (TextIO.inputLine is, "");
9.25 -end;
9.26 -
9.27 -structure Substring =
9.28 -struct
9.29 - open Substring;
9.30 - val all = full;
9.31 -end;
10.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
10.2 +++ b/src/Pure/ML-Systems/polyml-4.1.4.ML Thu May 31 01:25:24 2007 +0200
10.3 @@ -0,0 +1,8 @@
10.4 +(* Title: Pure/ML-Systems/polyml-4.1.4.ML
10.5 + ID: $Id$
10.6 +
10.7 +Compatibility wrapper for Poly/ML 4.1.4.
10.8 +*)
10.9 +
10.10 +use "ML-Systems/polyml-old-basis.ML";
10.11 +use "ML-Systems/polyml.ML";
11.1 --- a/src/Pure/ML-Systems/polyml-4.2.0.ML Wed May 30 23:32:54 2007 +0200
11.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
11.3 @@ -1,8 +0,0 @@
11.4 -(* Title: Pure/ML-Systems/polyml-4.2.0.ML
11.5 - ID: $Id$
11.6 -
11.7 -Compatibility wrapper for Poly/ML 4.2.0.
11.8 -*)
11.9 -
11.10 -use "ML-Systems/polyml-4.1.4-patch.ML";
11.11 -use "ML-Systems/polyml.ML";
12.1 --- a/src/Pure/ML-Systems/polyml-5.0.ML Wed May 30 23:32:54 2007 +0200
12.2 +++ b/src/Pure/ML-Systems/polyml-5.0.ML Thu May 31 01:25:24 2007 +0200
12.3 @@ -4,7 +4,6 @@
12.4 Compatibility wrapper for Poly/ML 5.0.
12.5 *)
12.6
12.7 -use "ML-Systems/polyml-4.1.4-patch.ML";
12.8 use "ML-Systems/polyml.ML";
12.9
12.10 val pointer_eq = PolyML.pointerEq;
13.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
13.2 +++ b/src/Pure/ML-Systems/polyml-old-basis.ML Thu May 31 01:25:24 2007 +0200
13.3 @@ -0,0 +1,30 @@
13.4 +(* Title: Pure/ML-Systems/polyml-old-basis.ML
13.5 + ID: $Id$
13.6 +
13.7 +Fixes for the old SML basis library (before Poly/ML 4.2.0).
13.8 +*)
13.9 +
13.10 +structure String =
13.11 +struct
13.12 + open String;
13.13 + fun isSuffix s1 s2 =
13.14 + let val n1 = size s1 and n2 = size s2
13.15 + in if n1 = n2 then s1 = s2 else n1 <= n2 andalso String.substring (s2, n2 - n1, n1) = s1 end;
13.16 +end;
13.17 +
13.18 +structure Substring =
13.19 +struct
13.20 + open Substring;
13.21 + val full = all;
13.22 +end;
13.23 +
13.24 +structure Posix =
13.25 +struct
13.26 + open Posix;
13.27 + structure IO =
13.28 + struct
13.29 + open IO;
13.30 + val mkTextReader = mkReader;
13.31 + val mkTextWriter = mkWriter;
13.32 + end;
13.33 +end;
14.1 --- a/src/Pure/ML-Systems/polyml-posix.ML Wed May 30 23:32:54 2007 +0200
14.2 +++ b/src/Pure/ML-Systems/polyml-posix.ML Thu May 31 01:25:24 2007 +0200
14.3 @@ -4,20 +4,6 @@
14.4 Posix patches for Poly/ML.
14.5 *)
14.6
14.7 -structure OriginalPosix = Posix;
14.8 -structure OriginalIO = Posix.IO;
14.9 -
14.10 -structure Posix =
14.11 -struct
14.12 - open OriginalPosix
14.13 - structure IO =
14.14 - struct
14.15 - open OriginalIO
14.16 - val mkTextReader = mkReader
14.17 - val mkTextWriter = mkWriter
14.18 - end;
14.19 -end;
14.20 -
14.21 (*This extension of the Poly/ML Signal structure is only necessary
14.22 because in SML/NJ, types Posix.Signal.signal and Signals.signal differ.*)
14.23 structure IsaSignal =
15.1 --- a/src/Pure/ML-Systems/polyml.ML Wed May 30 23:32:54 2007 +0200
15.2 +++ b/src/Pure/ML-Systems/polyml.ML Thu May 31 01:25:24 2007 +0200
15.3 @@ -1,28 +1,13 @@
15.4 (* Title: Pure/ML-Systems/polyml.ML
15.5 ID: $Id$
15.6
15.7 -Compatibility file for Poly/ML (version 4.0, 4.1, 4.1.x).
15.8 +Compatibility file for Poly/ML (version 4.1.x and 4.2.0).
15.9 *)
15.10
15.11 (** ML system and platform related **)
15.12
15.13 (* String compatibility *)
15.14
15.15 -structure String =
15.16 -struct
15.17 - fun isSuffix s1 s2 =
15.18 - let val n1 = size s1 and n2 = size s2
15.19 - in if n1 = n2 then s1 = s2 else n1 <= n2 andalso String.substring (s2, n2 - n1, n1) = s1 end;
15.20 - open String;
15.21 -end;
15.22 -
15.23 -structure Substring =
15.24 -struct
15.25 - open Substring;
15.26 - val full = all;
15.27 -end;
15.28 -
15.29 -
15.30 (*low-level pointer equality*)
15.31 val pointer_eq = Address.wordEq;
15.32
15.33 @@ -189,7 +174,7 @@
15.34
15.35 (*Convert a process ID to a decimal string (chiefly for tracing)*)
15.36 fun string_of_pid pid =
15.37 - Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord pid));
15.38 + Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord pid));
15.39
15.40
15.41 (* getenv *)
16.1 --- a/src/Pure/ML-Systems/smlnj.ML Wed May 30 23:32:54 2007 +0200
16.2 +++ b/src/Pure/ML-Systems/smlnj.ML Thu May 31 01:25:24 2007 +0200
16.3 @@ -159,11 +159,7 @@
16.4 structure TextIO =
16.5 struct
16.6 open TextIO;
16.7 -
16.8 - fun inputLine is =
16.9 - (case TextIO.inputLine is of
16.10 - SOME str => str
16.11 - | NONE => "")
16.12 + fun inputLine is = TextIO.inputLine is
16.13 handle IO.Io _ => raise Interrupt;
16.14 end;
16.15
17.1 --- a/src/Pure/tctical.ML Wed May 30 23:32:54 2007 +0200
17.2 +++ b/src/Pure/tctical.ML Thu May 31 01:25:24 2007 +0200
17.3 @@ -203,7 +203,7 @@
17.4 (*Pause until a line is typed -- if non-empty then fail. *)
17.5 fun pause_tac st =
17.6 (tracing "** Press RETURN to continue:";
17.7 - if TextIO.inputLine TextIO.stdIn = "\n" then Seq.single st
17.8 + if TextIO.inputLine TextIO.stdIn = SOME "\n" then Seq.single st
17.9 else (tracing "Goodbye"; Seq.empty));
17.10
17.11 exception TRACE_EXIT of thm
17.12 @@ -215,13 +215,13 @@
17.13
17.14 (*Handle all tracing commands for current state and tactic *)
17.15 fun exec_trace_command flag (tac, st) =
17.16 - case TextIO.inputLine(TextIO.stdIn) of
17.17 - "\n" => tac st
17.18 - | "f\n" => Seq.empty
17.19 - | "o\n" => (flag:=false; tac st)
17.20 - | "s\n" => (suppress_tracing:=true; tac st)
17.21 - | "x\n" => (tracing "Exiting now"; raise (TRACE_EXIT st))
17.22 - | "quit\n" => raise TRACE_QUIT
17.23 + case TextIO.inputLine TextIO.stdIn of
17.24 + SOME "\n" => tac st
17.25 + | SOME "f\n" => Seq.empty
17.26 + | SOME "o\n" => (flag:=false; tac st)
17.27 + | SOME "s\n" => (suppress_tracing:=true; tac st)
17.28 + | SOME "x\n" => (tracing "Exiting now"; raise (TRACE_EXIT st))
17.29 + | SOME "quit\n" => raise TRACE_QUIT
17.30 | _ => (tracing
17.31 "Type RETURN to continue or...\n\
17.32 \ f - to fail here\n\