--- a/src/HOL/IsaMakefile Mon Oct 10 14:43:45 2005 +0200
+++ b/src/HOL/IsaMakefile Mon Oct 10 15:35:29 2005 +0200
@@ -107,8 +107,7 @@
Tools/recdef_package.ML Tools/recfun_codegen.ML \
Tools/reconstruction.ML Tools/record_package.ML Tools/refute.ML \
Tools/refute_isar.ML Tools/res_atp.ML Tools/res_axioms.ML \
- Tools/res_clause.ML Tools/res_lib.ML Tools/res_skolem_function.ML \
- Tools/res_types_sorts.ML Tools/rewrite_hol_proof.ML \
+ Tools/res_clause.ML Tools/res_types_sorts.ML Tools/rewrite_hol_proof.ML \
Tools/sat_funcs.ML \
Tools/sat_solver.ML Tools/specification_package.ML Tools/split_rule.ML \
Tools/typedef_package.ML Transitive_Closure.ML Transitive_Closure.thy \
--- a/src/HOL/Reconstruction.thy Mon Oct 10 14:43:45 2005 +0200
+++ b/src/HOL/Reconstruction.thy Mon Oct 10 15:35:29 2005 +0200
@@ -8,22 +8,18 @@
theory Reconstruction
imports Hilbert_Choice Map Infinite_Set Extraction
-uses "Tools/res_lib.ML"
-
- "Tools/res_clause.ML"
- "Tools/res_skolem_function.ML"
- "Tools/res_axioms.ML"
- "Tools/res_types_sorts.ML"
-
- "Tools/ATP/recon_order_clauses.ML"
- "Tools/ATP/recon_translate_proof.ML"
- "Tools/ATP/recon_parse.ML"
- "Tools/ATP/recon_transfer_proof.ML"
- "Tools/ATP/AtpCommunication.ML"
- "Tools/ATP/watcher.ML"
- "Tools/ATP/res_clasimpset.ML"
- "Tools/res_atp.ML"
- "Tools/reconstruction.ML"
+uses "Tools/res_clause.ML"
+ "Tools/res_axioms.ML"
+ "Tools/res_types_sorts.ML"
+ "Tools/ATP/recon_order_clauses.ML"
+ "Tools/ATP/recon_translate_proof.ML"
+ "Tools/ATP/recon_parse.ML"
+ "Tools/ATP/recon_transfer_proof.ML"
+ "Tools/ATP/AtpCommunication.ML"
+ "Tools/ATP/watcher.ML"
+ "Tools/ATP/res_clasimpset.ML"
+ "Tools/res_atp.ML"
+ "Tools/reconstruction.ML"
begin
--- a/src/HOL/Tools/ATP/watcher.ML Mon Oct 10 14:43:45 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML Mon Oct 10 15:35:29 2005 +0200
@@ -350,8 +350,7 @@
(goals_being_watched := !goals_being_watched - 1;
if !goals_being_watched = 0
then
- (debug ("\nReaping a watcher, childpid = "^
- Int.toString (ResLib.intOfPid childpid));
+ (debug ("\nReaping a watcher, childpid = " ^ string_of_pid childpid);
killWatcher childpid (*???; reapWatcher (childpid, childin, childout)*) )
else ())
val _ = debug ("subgoals forked to createWatcher: "^ prems_string_of th);
--- a/src/HOL/Tools/res_atp.ML Mon Oct 10 14:43:45 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML Mon Oct 10 15:35:29 2005 +0200
@@ -29,6 +29,17 @@
val destdir = ref ""; (*Empty means write files to /tmp*)
val problem_name = ref "prob";
+(*Return the path to a "helper" like SPASS or tptp2X, first checking that
+ it exists. FIXME: modify to use Path primitives and move to some central place.*)
+fun helper_path evar base =
+ case getenv evar of
+ "" => error ("Isabelle environment variable " ^ evar ^ " not defined")
+ | home =>
+ let val path = home ^ "/" ^ base
+ in if File.exists (File.unpack_platform_path path) then path
+ else error ("Could not find the file " ^ path)
+ end;
+
fun probfile_nosuffix _ =
if !destdir = "" then File.platform_path (File.tmp_path (Path.basic (!problem_name)))
else if File.exists (File.unpack_platform_path (!destdir))
@@ -106,7 +117,7 @@
"%-DocProof%-TimeLimit=" ^ time
else "-DocProof%-SOS%-FullRed=0%-TimeLimit=" ^ time (*Auto mode*)
val _ = debug ("SPASS option string is " ^ optionline)
- val _ = ResLib.helper_path "SPASS_HOME" "SPASS"
+ val _ = helper_path "SPASS_HOME" "SPASS"
(*We've checked that SPASS is there for ATP/spassshell to run.*)
in
([("spass",
@@ -116,14 +127,14 @@
end
else if !prover = "vampire"
then
- let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vampire"
+ let val vampire = helper_path "VAMPIRE_HOME" "vampire"
in
([("vampire", vampire, "-m 100000%-t " ^ time, probfile)] @
(make_atp_list xs (n+1))) (*BEWARE! spaces in options!*)
end
else if !prover = "E"
then
- let val Eprover = ResLib.helper_path "E_HOME" "eproof"
+ let val Eprover = helper_path "E_HOME" "eproof"
in
([("E", Eprover,
"--tptp-in%-l5%-xAuto%-tAuto%--cpu-limit=" ^ time,
@@ -172,7 +183,7 @@
(case !last_watcher_pid of
NONE => ()
| SOME (_, childout, pid, files) =>
- (debug ("Killing old watcher, pid = " ^ Int.toString (ResLib.intOfPid pid));
+ (debug ("Killing old watcher, pid = " ^ string_of_pid pid);
Watcher.killWatcher pid;
ignore (map (try OS.FileSys.remove) files)))
handle OS.SysErr _ => debug "Attempt to kill watcher failed";
@@ -190,7 +201,7 @@
in
last_watcher_pid := SOME (childin, childout, pid, files);
debug ("problem files: " ^ space_implode ", " files);
- debug ("pid: " ^ Int.toString (ResLib.intOfPid pid));
+ debug ("pid: " ^ string_of_pid pid);
watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid)
end);
--- a/src/HOL/Tools/res_axioms.ML Mon Oct 10 14:43:45 2005 +0200
+++ b/src/HOL/Tools/res_axioms.ML Mon Oct 10 15:35:29 2005 +0200
@@ -313,9 +313,24 @@
fun univ_vars_of t = univ_vars_of_aux t [];
+(**** Generating Skoklem Functions ****)
+
+val skolem_prefix = "sk_";
+val skolem_id = ref 0;
+
+fun gen_skolem_name () =
+ let val sk_fun = skolem_prefix ^ string_of_int (! skolem_id);
+ in inc skolem_id; sk_fun end;
+
+fun gen_skolem univ_vars tp =
+ let
+ val skolem_type = map Term.fastype_of univ_vars ---> tp
+ val skolem_term = Const (gen_skolem_name (), skolem_type)
+ in Term.list_comb (skolem_term, univ_vars) end;
+
fun get_new_skolem epss (t as (Const ("Hilbert_Choice.Eps",_) $ Abs(_,tp,_))) =
let val all_vars = univ_vars_of t
- val sk_term = ResSkolemFunction.gen_skolem all_vars tp
+ val sk_term = gen_skolem all_vars tp
in
(sk_term,(t,sk_term)::epss)
end;
--- a/src/HOL/Tools/res_lib.ML Mon Oct 10 14:43:45 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,37 +0,0 @@
-(* Title: HOL/Tools/res_lib.ML
- Author: Jia Meng, Cambridge University Computer Laboratory
- ID: $Id$
- Copyright 2004 University of Cambridge
-
-Some auxiliary functions frequently used by files in this directory.
-*)
-
-signature RES_LIB =
-sig
-val helper_path : string -> string -> string
-val intOfPid : Posix.Process.pid -> Int.int
-val pidOfInt : Int.int -> Posix.Process.pid
-end;
-
-
-structure ResLib : RES_LIB =
-struct
-
-(*Return the path to a "helper" like SPASS or tptp2X, first checking that
- it exists. --lcp *)
-fun helper_path evar base =
- case getenv evar of
- "" => error ("Isabelle environment variable " ^ evar ^ " not defined")
- | home =>
- let val path = home ^ "/" ^ base
- in if File.exists (File.unpack_platform_path path) then path
- 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;
--- a/src/HOL/Tools/res_skolem_function.ML Mon Oct 10 14:43:45 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-(* Author: Jia Meng, Cambridge University Computer Laboratory
- ID: $Id$
- Copyright 2004 University of Cambridge
-
-Generation of unique Skolem functions (with types) as term.
-*)
-
-signature RES_SKOLEM_FUNCTION =
-sig
- val gen_skolem: term list -> typ -> term
-end;
-
-structure ResSkolemFunction: RES_SKOLEM_FUNCTION =
-struct
-
-val skolem_prefix = "sk_";
-val skolem_id = ref 0;
-
-fun gen_skolem_name () =
- let val sk_fun = skolem_prefix ^ string_of_int (! skolem_id);
- in inc skolem_id; sk_fun end;
-
-fun gen_skolem univ_vars tp =
- let
- val skolem_type = map Term.fastype_of univ_vars ---> tp
- val skolem_term = Const (gen_skolem_name (), skolem_type)
- in Term.list_comb (skolem_term, univ_vars) end;
-
-end;
--- a/src/Pure/library.ML Mon Oct 10 14:43:45 2005 +0200
+++ b/src/Pure/library.ML Mon Oct 10 15:35:29 2005 +0200
@@ -266,6 +266,7 @@
val partition_list: (int -> 'a -> bool) -> int -> int -> 'a list -> 'a list list
val gensym: string -> string
val scanwords: (string -> bool) -> string list -> string list
+ val string_of_pid: Posix.Process.pid -> string
type stamp
val stamp: unit -> stamp
type serial
@@ -1284,6 +1285,10 @@
end;
+(*Convert a process ID to a decimal string (chiefly for tracing)*)
+fun string_of_pid pid =
+ Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord pid));
+
(* lexical scanning *)