# HG changeset patch # User paulson # Date 1127147422 -7200 # Node ID 67376a311a2b84acf6913b64a09b6ce210fb9eab # Parent 940713ba9d2b20fbdea39084c126c12b28f6f579 further simplification of the Isabelle-ATP linkup diff -r 940713ba9d2b -r 67376a311a2b src/HOL/IsaMakefile --- 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 \ diff -r 940713ba9d2b -r 67376a311a2b src/HOL/Reconstruction.thy --- 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" diff -r 940713ba9d2b -r 67376a311a2b src/HOL/Tools/ATP/AtpCommunication.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) diff -r 940713ba9d2b -r 67376a311a2b src/HOL/Tools/ATP/recon_parse.ML --- 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 = diff -r 940713ba9d2b -r 67376a311a2b src/HOL/Tools/ATP/recon_prelim.ML --- 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; diff -r 940713ba9d2b -r 67376a311a2b src/HOL/Tools/ATP/recon_transfer_proof.ML --- 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) ****) diff -r 940713ba9d2b -r 67376a311a2b src/HOL/Tools/ATP/recon_translate_proof.ML --- 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 *) diff -r 940713ba9d2b -r 67376a311a2b src/HOL/Tools/ATP/watcher.ML --- 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, []); ()) diff -r 940713ba9d2b -r 67376a311a2b src/HOL/Tools/reconstruction.ML --- 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 diff -r 940713ba9d2b -r 67376a311a2b src/HOL/Tools/res_atp.ML --- 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); diff -r 940713ba9d2b -r 67376a311a2b src/HOL/Tools/res_lib.ML --- 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;