# HG changeset patch # User paulson # Date 1128951329 -7200 # Node ID 1241e5d31d5b9d79e148ace0636aee4ffc0284b5 # Parent 38c889d77282b467414ab39fd247954e94a2bfe0 small tidy-up of utility functions diff -r 38c889d77282 -r 1241e5d31d5b src/HOL/IsaMakefile --- 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 \ diff -r 38c889d77282 -r 1241e5d31d5b src/HOL/Reconstruction.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 diff -r 38c889d77282 -r 1241e5d31d5b src/HOL/Tools/ATP/watcher.ML --- 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); diff -r 38c889d77282 -r 1241e5d31d5b src/HOL/Tools/res_atp.ML --- 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); diff -r 38c889d77282 -r 1241e5d31d5b src/HOL/Tools/res_axioms.ML --- 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; diff -r 38c889d77282 -r 1241e5d31d5b src/HOL/Tools/res_lib.ML --- 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; diff -r 38c889d77282 -r 1241e5d31d5b src/HOL/Tools/res_skolem_function.ML --- 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; diff -r 38c889d77282 -r 1241e5d31d5b src/Pure/library.ML --- 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 *)