--- a/src/HOL/IsaMakefile Mon Sep 19 16:42:11 2005 +0200
+++ b/src/HOL/IsaMakefile Mon Sep 19 18:30:22 2005 +0200
@@ -95,7 +95,7 @@
Relation.ML Relation.thy Relation_Power.thy Ring_and_Field.thy Set.ML \
Set.thy SetInterval.thy Sum_Type.thy Tools/ATP/AtpCommunication.ML \
Tools/ATP/recon_order_clauses.ML Tools/ATP/recon_parse.ML \
- Tools/ATP/recon_prelim.ML Tools/ATP/recon_transfer_proof.ML \
+ Tools/ATP/recon_transfer_proof.ML \
Tools/ATP/recon_translate_proof.ML Tools/ATP/res_clasimpset.ML \
Tools/ATP/watcher.ML Tools/comm_ring.ML \
Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \
--- a/src/HOL/Reconstruction.thy Mon Sep 19 16:42:11 2005 +0200
+++ b/src/HOL/Reconstruction.thy Mon Sep 19 18:30:22 2005 +0200
@@ -15,7 +15,6 @@
"Tools/res_axioms.ML"
"Tools/res_types_sorts.ML"
- "Tools/ATP/recon_prelim.ML"
"Tools/ATP/recon_order_clauses.ML"
"Tools/ATP/recon_translate_proof.ML"
"Tools/ATP/recon_parse.ML"
--- a/src/HOL/Tools/ATP/AtpCommunication.ML Mon Sep 19 16:42:11 2005 +0200
+++ b/src/HOL/Tools/ATP/AtpCommunication.ML Mon Sep 19 18:30:22 2005 +0200
@@ -12,10 +12,10 @@
val reconstruct : bool ref
val checkEProofFound:
TextIO.instream * TextIO.outstream * Posix.Process.pid *
- string * string * thm * int * (ResClause.clause * thm) Array.array -> bool
+ string * string * (ResClause.clause * thm) Array.array -> bool
val checkVampProofFound:
TextIO.instream * TextIO.outstream * Posix.Process.pid *
- string * string * thm * int * (ResClause.clause * thm) Array.array -> bool
+ string * string * (ResClause.clause * thm) Array.array -> bool
val checkSpassProofFound:
TextIO.instream * TextIO.outstream * Posix.Process.pid *
string * string * thm * int * (ResClause.clause * thm) Array.array -> bool
@@ -55,20 +55,6 @@
else "??extract_proof failed" (*Couldn't find a proof*)
end;
-(**********************************************************************)
-(* Reconstruct the Vampire/E proof w.r.t. thmstring (string version of *)
-(* Isabelle goal to be proved), then transfer the reconstruction *)
-(* steps as a string to the input pipe of the main Isabelle process *)
-(**********************************************************************)
-
-fun reconstruct_tac proofextract goalstring toParent ppid sg_num clause_arr =
- SELECT_GOAL
- (EVERY1
- [rtac ccontr, ResLib.atomize_tac, skolemize_tac,
- METAHYPS(fn negs =>
- (Recon_Transfer.prover_lemma_list proofextract
- goalstring toParent ppid negs clause_arr))]) sg_num
-
(*********************************************************************************)
(* Inspect the output of an ATP process to see if it has found a proof, *)
@@ -76,7 +62,7 @@
(*********************************************************************************)
fun startTransfer (startS,endS)
- (fromChild, toParent, ppid, goalstring, childCmd, thm, sg_num, clause_arr) =
+ (fromChild, toParent, ppid, goalstring, childCmd, clause_arr) =
let val thisLine = TextIO.inputLine fromChild
fun transferInput currentString =
let val thisLine = TextIO.inputLine fromChild
@@ -91,8 +77,7 @@
then let val proofextract = extract_proof (currentString^thisLine)
in
File.write (File.tmp_path (Path.basic"extracted_prf")) proofextract;
- reconstruct_tac proofextract goalstring toParent ppid sg_num
- clause_arr thm
+ Recon_Transfer.prover_lemma_list proofextract goalstring toParent ppid clause_arr
end
else transferInput (currentString^thisLine)
end
@@ -101,22 +86,22 @@
else if String.isPrefix startS thisLine
then
(File.append (File.tmp_path (Path.basic "transfer_start"))
- ("about to transfer proof, thm is: " ^ string_of_thm thm);
+ ("about to transfer proof, first line is: " ^ thisLine);
transferInput thisLine;
true) handle EOF => false
else
startTransfer (startS,endS)
(fromChild, toParent, ppid, goalstring,
- childCmd, thm, sg_num,clause_arr)
+ childCmd, clause_arr)
end
(*Called from watcher. Returns true if the Vampire process has returned a verdict.*)
-fun checkVampProofFound (fromChild, toParent, ppid, goalstring, childCmd,
- thm, sg_num, clause_arr) =
+fun checkVampProofFound (fromChild, toParent, ppid, goalstring, childCmd, clause_arr) =
let val proof_file = TextIO.openAppend
(File.platform_path(File.tmp_path (Path.basic "vampire_proof")))
val _ = File.write (File.tmp_path (Path.basic "vampire_checking_prf"))
- ("checking if proof found, thm is: " ^ string_of_thm thm)
+ ("checking if proof found. childCmd is " ^ childCmd ^
+ "\ngoalstring is: " ^ goalstring)
val thisLine = TextIO.inputLine fromChild
in
File.write (File.tmp_path (Path.basic "vampire_response")) thisLine;
@@ -128,7 +113,7 @@
then
startTransfer (start_V8, end_V8)
(fromChild, toParent, ppid, goalstring,
- childCmd, thm, sg_num, clause_arr)
+ childCmd, clause_arr)
else if (String.isPrefix "Satisfiability detected" thisLine) orelse
(String.isPrefix "Refutation not found" thisLine)
then
@@ -145,18 +130,17 @@
(TextIO.output (proof_file, thisLine);
TextIO.flushOut proof_file;
checkVampProofFound (fromChild, toParent, ppid,
- goalstring,childCmd, thm, sg_num, clause_arr))
+ goalstring,childCmd, clause_arr))
end
(*Called from watcher. Returns true if the E process has returned a verdict.*)
-fun checkEProofFound (fromChild, toParent, ppid,goalstring, childCmd,
- thm, sg_num, clause_arr) =
+fun checkEProofFound (fromChild, toParent, ppid,goalstring, childCmd, clause_arr) =
let val E_proof_file = TextIO.openAppend
(File.platform_path(File.tmp_path (Path.basic "e_proof")))
val _ = File.write (File.tmp_path (Path.basic "e_checking_prf"))
("checking if proof found. childCmd is " ^ childCmd ^
- "\nthm is: " ^ string_of_thm thm)
+ "\ngoalstring is: " ^ goalstring)
val thisLine = TextIO.inputLine fromChild
in
File.write (File.tmp_path (Path.basic "e_response")) thisLine;
@@ -167,8 +151,7 @@
else if thisLine = "# TSTP exit status: Unsatisfiable\n"
then
startTransfer (start_E, end_E)
- (fromChild, toParent, ppid, goalstring,
- childCmd, thm, sg_num, clause_arr)
+ (fromChild, toParent, ppid, goalstring, childCmd, clause_arr)
else if String.isPrefix "# Problem is satisfiable" thisLine
then
(TextIO.output (toParent, "Invalid\n");
@@ -195,8 +178,7 @@
else
(TextIO.output (E_proof_file, thisLine);
TextIO.flushOut E_proof_file;
- checkEProofFound (fromChild, toParent, ppid, goalstring,
- childCmd, thm, sg_num, clause_arr))
+ checkEProofFound (fromChild, toParent, ppid, goalstring, childCmd, clause_arr))
end
@@ -208,14 +190,10 @@
fun spass_reconstruct_tac proofextract goalstring toParent ppid sg_num
clause_arr =
- let val f = if !reconstruct then Recon_Transfer.spass_reconstruct
- else Recon_Transfer.spass_lemma_list
- in
- SELECT_GOAL
- (EVERY1 [rtac ccontr, ResLib.atomize_tac, skolemize_tac,
- METAHYPS(fn negs =>
- f proofextract goalstring toParent ppid negs clause_arr)]) sg_num
- end;
+ SELECT_GOAL
+ (EVERY1 [rtac ccontr, ResLib.atomize_tac, skolemize_tac,
+ METAHYPS(fn negs =>
+ Recon_Transfer.spass_reconstruct proofextract goalstring toParent ppid negs clause_arr)]) sg_num;
fun transferSpassInput (fromChild, toParent, ppid, goalstring,
@@ -225,13 +203,16 @@
if thisLine = "" (*end of file?*)
then (File.write (File.tmp_path (Path.basic"spass_extraction_failed")) currentString;
raise EOF)
- else if thisLine = "--------------------------SPASS-STOP------------------------------\n"
+ else if String.isPrefix "--------------------------SPASS-STOP" thisLine
then
let val proofextract = extract_proof (currentString^thisLine)
in
- File.write (File.tmp_path (Path.basic"spass_extracted_prf")) proofextract;
- spass_reconstruct_tac proofextract goalstring toParent ppid sg_num
- clause_arr thm
+ File.write (File.tmp_path (Path.basic"spass_extracted_prf")) proofextract;
+ if !reconstruct
+ then (spass_reconstruct_tac proofextract goalstring toParent ppid sg_num
+ clause_arr thm; ())
+ else Recon_Transfer.spass_lemma_list proofextract goalstring
+ toParent ppid clause_arr
end
else transferSpassInput (fromChild, toParent, ppid, goalstring,
(currentString^thisLine), thm, sg_num, clause_arr)
--- a/src/HOL/Tools/ATP/recon_parse.ML Mon Sep 19 16:42:11 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_parse.ML Mon Sep 19 18:30:22 2005 +0200
@@ -10,7 +10,7 @@
structure Recon_Parse =
struct
-open ReconPrelim ReconTranslateProof;
+open ReconTranslateProof;
exception NOPARSE_WORD
exception NOPARSE_NUM
@@ -18,7 +18,7 @@
fun string2int s =
(case Int.fromString s of SOME i => i
- | NONE => raise ASSERTION "string -> int failed");
+ | NONE => error "string -> int failed");
(* Parser combinators *)
@@ -77,7 +77,7 @@
| is_prefix (h::t) [] = false
| is_prefix (h::t) (h'::t') = (h = h') andalso is_prefix t t'
fun remove_prefix [] l = l
- | remove_prefix (h::t) [] = raise (ASSERTION "can't remove prefix")
+ | remove_prefix (h::t) [] = error "can't remove prefix"
| remove_prefix (h::t) (h'::t') = remove_prefix t t'
fun ccut t [] = raise NOCUT
| ccut t s =
--- a/src/HOL/Tools/ATP/recon_prelim.ML Mon Sep 19 16:42:11 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,128 +0,0 @@
-(* ID: $Id$
- Author: Claire Quigley
- Copyright 2004 University of Cambridge
-*)
-
-structure ReconPrelim =
-struct
-
-fun USYN_ERR func mesg = Utils.ERR {module = "USyntax", func = func, mesg = mesg};
-
-fun dest_neg(Const("Not",_) $ M) = M
- | dest_neg _ = raise USYN_ERR "dest_neg" "not a negation";
-
-fun iscomb a =
- if is_Free a then
- false
- else if is_Var a then
- false
- else if USyntax.is_conj a then
- false
- else if USyntax.is_disj a then
- false
- else if USyntax.is_forall a then
- false
- else if USyntax.is_exists a then
- false
- else
- true;
-
-fun getstring (Var (v,T)) = fst v
- |getstring (Free (v,T))= v;
-
-fun twoisvar (a,b) = is_Var b;
-fun twoisfree (a,b) = is_Free b;
-fun twoiscomb (a,b) = iscomb b;
-
-fun strequalfirst a (b,c) = (getstring a) = (getstring b);
-
-fun fstequal a b = a = fst b;
-
-(* Presumably here, we would allow is_Var f for doing HOL, i.e. can subst for propositions *)
-fun is_Abs (Abs _) = true
- | is_Abs _ = false;
-fun is_Bound (Bound _) = true
- | is_Bound _ = false;
-
-fun is_hol_tm t =
- if (is_Free t) then
- true
- else if (is_Var t) then
- true
- else if (is_Const t) then
- true
- else if (is_Abs t) then
- true
- else if (is_Bound t) then
- true
- else
- let val (f, args) = strip_comb t in
- if ((is_Free f) orelse (is_Var f)) andalso (forall is_hol_tm args) then
- true (* should be is_const *)
- else
- false
- end;
-
-fun is_hol_fm f =
- if USyntax.is_neg f then
- let val newf = USyntax.dest_neg f in
- is_hol_fm newf
- end
- else if USyntax.is_disj f then
- let val {disj1,disj2} = USyntax.dest_disj f in
- (is_hol_fm disj1) andalso (is_hol_fm disj2) (* shouldn't this be and ? *)
- end
- else if USyntax.is_conj f then
- let val {conj1,conj2} = USyntax.dest_conj f in
- (is_hol_fm conj1) andalso (is_hol_fm conj2)
- end
- else if (USyntax.is_forall f) then
- let val {Body, Bvar} = USyntax.dest_forall f in
- is_hol_fm Body
- end
- else if (USyntax.is_exists f) then
- let val {Body, Bvar} = USyntax.dest_exists f in
- is_hol_fm Body
- end
- else if (iscomb f) then
- let val (P, args) = strip_comb f in
- ((is_hol_tm P)) andalso (forall is_hol_fm args)
- end
- else
- is_hol_tm f; (* should be is_const, need to check args *)
-
-fun hol_literal t =
- is_hol_fm t andalso
- (not (USyntax.is_conj t orelse USyntax.is_disj t orelse USyntax.is_forall t
- orelse USyntax.is_exists t));
-
-
-(*PROBLEM HERE WITH THINGS THAT HAVE TWO RANDS e.g. P x y *)
-fun getcombvar a =
- let val {Rand = rand, Rator = rator} = USyntax.dest_comb a in
- if (iscomb rand) then
- getcombvar rand
- else
- rand
- end;
-
-fun free2var v =
- let val (name, vtype) = dest_Free v
- in Var ((name, 0), vtype) end;
-
-fun var2free v =
- let val ((x, _), tv) = dest_Var v
- in Free (x, tv) end;
-
-val is_empty_seq = is_none o Seq.pull;
-
-fun getnewenv seq = fst (fst (the (Seq.pull seq)));
-fun getnewsubsts seq = snd (fst (the (Seq.pull seq)));
-
-fun prover s = prove_goal HOL.thy s (fn _ => [blast_tac HOL_cs 1]);
-
-val no_lines = filter_out (equal "\n");
-
-exception ASSERTION of string;
-
-end;
--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Mon Sep 19 16:42:11 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Mon Sep 19 18:30:22 2005 +0200
@@ -158,7 +158,7 @@
(* get names of clasimp axioms used *)
(*****************************************************)
- fun get_axiom_names step_nums thms clause_arr =
+ fun get_axiom_names step_nums clause_arr =
let
(* not sure why this is necessary again, but seems to be *)
val _ = (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
@@ -177,7 +177,7 @@
end
-fun get_axiom_names_spass proofstr thms clause_arr =
+fun get_axiom_names_spass proofstr clause_arr =
let (* parse spass proof into datatype *)
val _ = File.write (File.tmp_path (Path.basic "parsing_progress"))
("Started parsing:\n" ^ proofstr)
@@ -186,8 +186,7 @@
val _ = File.append (File.tmp_path (Path.basic "parsing_progress")) "\nFinished!"
(* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
in
- get_axiom_names (get_step_nums (List.filter is_axiom proof_steps) [])
- thms clause_arr
+ get_axiom_names (get_step_nums (List.filter is_axiom proof_steps) []) clause_arr
end;
(*String contains multiple lines, terminated with newline characters.
@@ -199,8 +198,8 @@
val lines = String.tokens (fn c => c = #"\n") proofstr
in List.mapPartial (firstno o numerics) lines end
-fun get_axiom_names_vamp_E proofstr thms clause_arr =
- get_axiom_names (get_linenums proofstr) thms clause_arr;
+fun get_axiom_names_vamp_E proofstr clause_arr =
+ get_axiom_names (get_linenums proofstr) clause_arr;
(***********************************************)
@@ -274,13 +273,12 @@
val restore_linebreaks = subst_for #"\t" #"\n";
-fun prover_lemma_list_aux proofstr goalstring toParent ppid thms clause_arr getax =
+fun prover_lemma_list_aux getax proofstr goalstring toParent ppid clause_arr =
let val _ = File.append(File.tmp_path (Path.basic "prover_lemmastring"))
("proofstr is " ^ proofstr ^
"\ngoalstr is " ^ goalstring ^
"\nnum of clauses is " ^ string_of_int (Array.length clause_arr))
-
- val axiom_names = getax proofstr thms clause_arr
+ val axiom_names = getax proofstr clause_arr
val ax_str = rules_to_string axiom_names
in
File.append(File.tmp_path (Path.basic "prover_lemmastring"))
@@ -292,7 +290,7 @@
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
(* Attempt to prevent several signals from turning up simultaneously *)
- Posix.Process.sleep(Time.fromSeconds 1) ; all_tac
+ Posix.Process.sleep(Time.fromSeconds 1); ()
end
handle exn => (*FIXME: exn handler is too general!*)
(File.write(File.tmp_path (Path.basic "proverString_handler"))
@@ -303,15 +301,11 @@
TextIO.flushOut toParent;
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
(* Attempt to prevent several signals from turning up simultaneously *)
- Posix.Process.sleep(Time.fromSeconds 1); all_tac);
+ Posix.Process.sleep(Time.fromSeconds 1); ());
-fun prover_lemma_list proofstr goalstring toParent ppid thms clause_arr =
- prover_lemma_list_aux proofstr goalstring toParent ppid thms
- clause_arr get_axiom_names_vamp_E;
+val prover_lemma_list = prover_lemma_list_aux get_axiom_names_vamp_E;
-fun spass_lemma_list proofstr goalstring toParent ppid thms clause_arr =
- prover_lemma_list_aux proofstr goalstring toParent ppid thms
- clause_arr get_axiom_names_spass;
+val spass_lemma_list = prover_lemma_list_aux get_axiom_names_spass;
(**** Full proof reconstruction for SPASS (not really working) ****)
--- a/src/HOL/Tools/ATP/recon_translate_proof.ML Mon Sep 19 16:42:11 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_translate_proof.ML Mon Sep 19 18:30:22 2005 +0200
@@ -6,8 +6,6 @@
structure ReconTranslateProof =
struct
-open ReconPrelim;
-
fun add_in_order (x:string) [] = [x]
| add_in_order (x:string) ((y:string)::ys) = if (x < y)
then
@@ -166,6 +164,8 @@
(* Reconstruct a factoring step *)
(*************************************)
+fun getnewenv seq = fst (fst (the (Seq.pull seq)));
+
(*FIXME: share code with that in Tools/reconstruction.ML*)
fun follow_factor clause lit1 lit2 allvars thml clause_strs =
let
@@ -361,7 +361,7 @@
(*| follow_proof clauses clausenum thml (Hyper l)
= follow_hyper l thml*)
| follow_proof clauses allvars clausenum thml _ _ =
- raise ASSERTION "proof step not implemented"
+ error "proof step not implemented"
@@ -370,13 +370,12 @@
(* reconstruct a single line of the res. proof - at the moment do only inference steps*)
(**************************************************************************************)
- fun follow_line clauses allvars thml (clause_num, proof_step, clause_strs) recons
- = let
- val (thm, recon_fun) = follow_proof clauses allvars clause_num thml proof_step clause_strs
- val recon_step = (recon_fun)
- in
- (((clause_num, thm)::thml), ((clause_num,recon_step)::recons))
- end
+ fun follow_line clauses allvars thml (clause_num, proof_step, clause_strs) recons =
+ let
+ val (thm, recon_fun) = follow_proof clauses allvars clause_num thml proof_step clause_strs
+ in
+ ((clause_num, thm)::thml, (clause_num,recon_fun)::recons)
+ end
(***************************************************************)
(* follow through the res. proof, creating an Isabelle theorem *)
--- a/src/HOL/Tools/ATP/watcher.ML Mon Sep 19 16:42:11 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML Mon Sep 19 18:30:22 2005 +0200
@@ -44,6 +44,7 @@
(**********************************************************)
val killWatcher : Posix.Process.pid -> unit
+val killWatcher' : int -> unit
end
@@ -52,7 +53,7 @@
structure Watcher: WATCHER =
struct
-open ReconPrelim Recon_Transfer
+open Recon_Transfer
val goals_being_watched = ref 0;
@@ -401,8 +402,8 @@
let val _ = File.append (File.tmp_path (Path.basic "child_check"))
"\nInput available from childIncoming"
val childDone = (case prover of
- "vampire" => AtpCommunication.checkVampProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr)
- | "E" => AtpCommunication.checkEProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr)
+ "vampire" => AtpCommunication.checkVampProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)
+ | "E" => AtpCommunication.checkEProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)
|"spass" => AtpCommunication.checkSpassProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr) )
in
if childDone
@@ -604,6 +605,8 @@
fun killWatcher pid = Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill);
+val killWatcher' = killWatcher o ResLib.pidOfInt;
+
fun reapWatcher(pid, instr, outstr) =
(TextIO.closeIn instr; TextIO.closeOut outstr;
Posix.Process.waitpid(Posix.Process.W_CHILD pid, []); ())
--- a/src/HOL/Tools/reconstruction.ML Mon Sep 19 16:42:11 2005 +0200
+++ b/src/HOL/Tools/reconstruction.ML Mon Sep 19 18:30:22 2005 +0200
@@ -55,8 +55,6 @@
then inst_single sign (snd (hd substs)) (fst (hd substs)) cl
else raise THM ("inst_subst", 0, [cl]);
-(*Grabs the environment from the result of Unify.unifiers*)
-fun getnewenv thisseq = fst (hd (Seq.list_of thisseq));
(** Factoring **)
@@ -67,7 +65,7 @@
val fac2 = List.nth (prems,lit2)
val sign = sign_of_thm cl
val unif_env = Unify.unifiers (sign, Envir.empty 0, [(fac1, fac2)])
- val newenv = getnewenv unif_env
+ val newenv = ReconTranslateProof.getnewenv unif_env
val envlist = Envir.alist_of newenv
in
inst_subst sign (mksubstlist envlist []) cl
--- a/src/HOL/Tools/res_atp.ML Mon Sep 19 16:42:11 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML Mon Sep 19 18:30:22 2005 +0200
@@ -201,12 +201,10 @@
val _ = debug ("claset and simprules total clauses = " ^
string_of_int (Array.length clause_arr))
val (childin, childout, pid) = Watcher.createWatcher (thm, clause_arr)
- val pid_string =
- string_of_int (Word.toInt (Word.fromLargeWord (Posix.Process.pidToWord pid)))
in
debug ("initial thms: " ^ thms_string);
debug ("subgoals: " ^ prems_string);
- debug ("pid: "^ pid_string);
+ debug ("pid: " ^ Int.toString (ResLib.intOfPid pid));
write_problem_files axclauses thm (length prems);
watcher_call_provers (sign_of_thm thm) (Thm.prems_of thm) (childin, childout, pid)
end);
--- a/src/HOL/Tools/res_lib.ML Mon Sep 19 16:42:11 2005 +0200
+++ b/src/HOL/Tools/res_lib.ML Mon Sep 19 18:30:22 2005 +0200
@@ -20,6 +20,8 @@
val trim_ends : string -> string
val write_strs : TextIO.outstream -> TextIO.vector list -> unit
val writeln_strs : TextIO.outstream -> TextIO.vector list -> unit
+val intOfPid : Posix.Process.pid -> Int.int
+val pidOfInt : Int.int -> Posix.Process.pid
end;
@@ -95,4 +97,10 @@
else error ("Could not find the file " ^ path)
end;
+(*** Converting between process ids and integers ***)
+
+fun intOfPid pid = Word.toInt (Word.fromLargeWord (Posix.Process.pidToWord pid));
+
+fun pidOfInt n = Posix.Process.wordToPid (Word.toLargeWord (Word.fromInt n));
+
end;