--- a/src/HOL/IsaMakefile Tue Jul 27 17:10:27 2010 +0200
+++ b/src/HOL/IsaMakefile Tue Jul 27 20:16:14 2010 +0200
@@ -269,7 +269,7 @@
$(SRC)/Provers/Arith/extract_common_term.ML \
$(SRC)/Tools/Metis/metis.ML \
Tools/ATP_Manager/async_manager.ML \
- Tools/ATP_Manager/atp_manager.ML \
+ Tools/ATP_Manager/atp_problem.ML \
Tools/ATP_Manager/atp_systems.ML \
Tools/choice_specification.ML \
Tools/int_arith.ML \
@@ -319,11 +319,11 @@
Tools/Sledgehammer/meson_tactic.ML \
Tools/Sledgehammer/metis_clauses.ML \
Tools/Sledgehammer/metis_tactics.ML \
+ Tools/Sledgehammer/sledgehammer.ML \
Tools/Sledgehammer/sledgehammer_fact_filter.ML \
Tools/Sledgehammer/sledgehammer_fact_minimizer.ML \
Tools/Sledgehammer/sledgehammer_isar.ML \
Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML \
- Tools/Sledgehammer/sledgehammer_tptp_format.ML \
Tools/Sledgehammer/sledgehammer_util.ML \
Tools/SMT/cvc3_solver.ML \
Tools/SMT/smtlib_interface.ML \
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Jul 27 17:10:27 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Jul 27 20:16:14 2010 +0200
@@ -283,7 +283,7 @@
fun default_atp_name () =
hd (#atps (Sledgehammer_Isar.default_params thy []))
handle Empty => error "No ATP available."
- fun get_prover name = (name, ATP_Manager.get_prover thy name)
+ fun get_prover name = (name, Sledgehammer.get_prover_fun thy name)
in
(case AList.lookup (op =) args proverK of
SOME name => get_prover name
@@ -301,11 +301,11 @@
let
val {context = ctxt, facts, goal} = Proof.goal st
val thy = ProofContext.theory_of ctxt
- val change_dir = (fn SOME d => Config.put ATP_Systems.dest_dir d | _ => I)
+ val change_dir = (fn SOME d => Config.put Sledgehammer.dest_dir d | _ => I)
val ctxt' =
ctxt
|> change_dir dir
- |> Config.put ATP_Systems.measure_runtime true
+ |> Config.put Sledgehammer.measure_runtime true
val params = Sledgehammer_Isar.default_params thy []
val problem =
{subgoal = 1, goal = (ctxt', (facts, goal)),
@@ -315,13 +315,13 @@
(case hard_timeout of
NONE => I
| SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
- val ({outcome, message, relevant_thm_names,
- atp_run_time_in_msecs = time_atp, ...}: ATP_Manager.prover_result,
+ val ({outcome, message, used_thm_names,
+ atp_run_time_in_msecs = time_atp, ...} : Sledgehammer.prover_result,
time_isa) = time_limit (Mirabelle.cpu_time
(prover params (K "") (Time.fromSeconds timeout))) problem
in
case outcome of
- NONE => (message, SH_OK (time_isa, time_atp, relevant_thm_names))
+ NONE => (message, SH_OK (time_isa, time_atp, used_thm_names))
| SOME _ => (message, SH_FAIL (time_isa, time_atp))
end
handle ERROR msg => ("error: " ^ msg, SH_ERROR)
--- a/src/HOL/Sledgehammer.thy Tue Jul 27 17:10:27 2010 +0200
+++ b/src/HOL/Sledgehammer.thy Tue Jul 27 20:16:14 2010 +0200
@@ -1,6 +1,6 @@
(* Title: HOL/Sledgehammer.thy
- Author: Lawrence C Paulson
- Author: Jia Meng, NICTA
+ Author: Lawrence C. Paulson, Cambridge University Computer Laboratory
+ Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
Author: Fabian Immler, TU Muenchen
Author: Jasmin Blanchette, TU Muenchen
*)
@@ -10,18 +10,18 @@
theory Sledgehammer
imports Plain Hilbert_Choice
uses
- "~~/src/Tools/Metis/metis.ML"
+ ("Tools/ATP_Manager/async_manager.ML")
+ ("Tools/ATP_Manager/atp_problem.ML")
+ ("Tools/ATP_Manager/atp_systems.ML")
+ ("~~/src/Tools/Metis/metis.ML")
("Tools/Sledgehammer/clausifier.ML")
("Tools/Sledgehammer/meson_tactic.ML")
("Tools/Sledgehammer/metis_clauses.ML")
("Tools/Sledgehammer/metis_tactics.ML")
("Tools/Sledgehammer/sledgehammer_util.ML")
("Tools/Sledgehammer/sledgehammer_fact_filter.ML")
- ("Tools/Sledgehammer/sledgehammer_tptp_format.ML")
("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
- ("Tools/ATP_Manager/async_manager.ML")
- ("Tools/ATP_Manager/atp_manager.ML")
- ("Tools/ATP_Manager/atp_systems.ML")
+ ("Tools/Sledgehammer/sledgehammer.ML")
("Tools/Sledgehammer/sledgehammer_fact_minimizer.ML")
("Tools/Sledgehammer/sledgehammer_isar.ML")
begin
@@ -85,6 +85,12 @@
apply (simp add: COMBC_def)
done
+use "Tools/ATP_Manager/async_manager.ML"
+use "Tools/ATP_Manager/atp_problem.ML"
+use "Tools/ATP_Manager/atp_systems.ML"
+setup ATP_Systems.setup
+
+use "~~/src/Tools/Metis/metis.ML"
use "Tools/Sledgehammer/clausifier.ML"
use "Tools/Sledgehammer/meson_tactic.ML"
setup Meson_Tactic.setup
@@ -94,12 +100,9 @@
use "Tools/Sledgehammer/sledgehammer_util.ML"
use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
-use "Tools/Sledgehammer/sledgehammer_tptp_format.ML"
use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
-use "Tools/ATP_Manager/async_manager.ML"
-use "Tools/ATP_Manager/atp_manager.ML"
-use "Tools/ATP_Manager/atp_systems.ML"
-setup ATP_Systems.setup
+use "Tools/Sledgehammer/sledgehammer.ML"
+setup Sledgehammer.setup
use "Tools/Sledgehammer/sledgehammer_fact_minimizer.ML"
use "Tools/Sledgehammer/sledgehammer_isar.ML"
setup Metis_Tactics.setup
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Jul 27 17:10:27 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,171 +0,0 @@
-(* Title: HOL/Tools/ATP_Manager/atp_manager.ML
- Author: Fabian Immler, TU Muenchen
- Author: Makarius
- Author: Jasmin Blanchette, TU Muenchen
-
-Central manager component for ATP threads.
-*)
-
-signature ATP_MANAGER =
-sig
- type relevance_override = Sledgehammer_Fact_Filter.relevance_override
- type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
- type params =
- {debug: bool,
- verbose: bool,
- overlord: bool,
- atps: string list,
- full_types: bool,
- explicit_apply: bool,
- relevance_threshold: real,
- relevance_convergence: real,
- theory_relevant: bool option,
- defs_relevant: bool,
- isar_proof: bool,
- isar_shrink_factor: int,
- timeout: Time.time,
- minimize_timeout: Time.time}
- type problem =
- {subgoal: int,
- goal: Proof.context * (thm list * thm),
- relevance_override: relevance_override,
- axiom_clauses: (string * thm) list option,
- filtered_clauses: (string * thm) list option}
- datatype failure =
- Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
- OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError
- type prover_result =
- {outcome: failure option,
- message: string,
- pool: string Symtab.table,
- relevant_thm_names: string list,
- atp_run_time_in_msecs: int,
- output: string,
- proof: string,
- internal_thm_names: string Vector.vector,
- conjecture_shape: int list,
- filtered_clauses: (string * thm) list}
- type prover =
- params -> minimize_command -> Time.time -> problem -> prover_result
-
- val kill_atps: unit -> unit
- val running_atps: unit -> unit
- val messages: int option -> unit
- val add_prover: string * prover -> theory -> theory
- val get_prover: theory -> string -> prover
- val available_atps: theory -> unit
- val start_prover_thread :
- params -> int -> int -> relevance_override -> (string -> minimize_command)
- -> Proof.state -> string -> unit
-end;
-
-structure ATP_Manager : ATP_MANAGER =
-struct
-
-open Metis_Clauses
-open Sledgehammer_Fact_Filter
-open Sledgehammer_Proof_Reconstruct
-
-(** The Sledgehammer **)
-
-val das_Tool = "Sledgehammer"
-
-fun kill_atps () = Async_Manager.kill_threads das_Tool "ATPs"
-fun running_atps () = Async_Manager.running_threads das_Tool "ATPs"
-val messages = Async_Manager.thread_messages das_Tool "ATP"
-
-(** problems, results, provers, etc. **)
-
-type params =
- {debug: bool,
- verbose: bool,
- overlord: bool,
- atps: string list,
- full_types: bool,
- explicit_apply: bool,
- relevance_threshold: real,
- relevance_convergence: real,
- theory_relevant: bool option,
- defs_relevant: bool,
- isar_proof: bool,
- isar_shrink_factor: int,
- timeout: Time.time,
- minimize_timeout: Time.time}
-
-type problem =
- {subgoal: int,
- goal: Proof.context * (thm list * thm),
- relevance_override: relevance_override,
- axiom_clauses: (string * thm) list option,
- filtered_clauses: (string * thm) list option}
-
-datatype failure =
- Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
- OldSpass | MalformedInput | MalformedOutput | UnknownError
-
-type prover_result =
- {outcome: failure option,
- message: string,
- pool: string Symtab.table,
- relevant_thm_names: string list,
- atp_run_time_in_msecs: int,
- output: string,
- proof: string,
- internal_thm_names: string Vector.vector,
- conjecture_shape: int list,
- filtered_clauses: (string * thm) list}
-
-type prover =
- params -> minimize_command -> Time.time -> problem -> prover_result
-
-(* named provers *)
-
-structure Data = Theory_Data
-(
- type T = (prover * stamp) Symtab.table;
- val empty = Symtab.empty;
- val extend = I;
- fun merge data : T = Symtab.merge (eq_snd op =) data
- handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
-);
-
-fun add_prover (name, prover) thy =
- Data.map (Symtab.update_new (name, (prover, stamp ()))) thy
- handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
-
-fun get_prover thy name =
- the (Symtab.lookup (Data.get thy) name) |> fst
- handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
-
-fun available_atps thy =
- priority ("Available ATPs: " ^
- commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".")
-
-
-(* start prover thread *)
-
-fun start_prover_thread (params as {verbose, full_types, timeout, ...}) i n
- relevance_override minimize_command proof_state name =
- let
- val birth_time = Time.now ()
- val death_time = Time.+ (birth_time, timeout)
- val prover = get_prover (Proof.theory_of proof_state) name
- val {context = ctxt, facts, goal} = Proof.goal proof_state;
- val desc =
- "ATP " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
- Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));
- in
- Async_Manager.launch das_Tool verbose birth_time death_time desc
- (fn () =>
- let
- val problem =
- {subgoal = i, goal = (ctxt, (facts, goal)),
- relevance_override = relevance_override, axiom_clauses = NONE,
- filtered_clauses = NONE}
- in
- prover params (minimize_command name) timeout problem |> #message
- handle ERROR message => "Error: " ^ message ^ "\n"
- end)
- end
-
-end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP_Manager/atp_problem.ML Tue Jul 27 20:16:14 2010 +0200
@@ -0,0 +1,152 @@
+(* Title: HOL/Tools/ATP_Manager/atp_problem.ML
+ Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
+ Author: Jasmin Blanchette, TU Muenchen
+
+TPTP syntax.
+*)
+
+signature ATP_PROBLEM =
+sig
+ datatype 'a fo_term = ATerm of 'a * 'a fo_term list
+ datatype quantifier = AForall | AExists
+ datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
+ datatype ('a, 'b) formula =
+ AQuant of quantifier * 'a list * ('a, 'b) formula |
+ AConn of connective * ('a, 'b) formula list |
+ APred of 'b
+
+ datatype kind = Axiom | Conjecture
+ datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula
+ type 'a problem = (string * 'a problem_line list) list
+
+ val timestamp : unit -> string
+ val is_tptp_variable : string -> bool
+ val strings_for_tptp_problem :
+ (string * string problem_line list) list -> string list
+ val nice_tptp_problem :
+ bool -> ('a * (string * string) problem_line list) list
+ -> ('a * string problem_line list) list
+ * (string Symtab.table * string Symtab.table) option
+end;
+
+structure ATP_Problem : ATP_PROBLEM =
+struct
+
+(** ATP problem **)
+
+datatype 'a fo_term = ATerm of 'a * 'a fo_term list
+datatype quantifier = AForall | AExists
+datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
+datatype ('a, 'b) formula =
+ AQuant of quantifier * 'a list * ('a, 'b) formula |
+ AConn of connective * ('a, 'b) formula list |
+ APred of 'b
+
+datatype kind = Axiom | Conjecture
+datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula
+type 'a problem = (string * 'a problem_line list) list
+
+val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
+
+fun string_for_term (ATerm (s, [])) = s
+ | string_for_term (ATerm (s, ts)) =
+ if s = "equal" then space_implode " = " (map string_for_term ts)
+ else s ^ "(" ^ commas (map string_for_term ts) ^ ")"
+fun string_for_quantifier AForall = "!"
+ | string_for_quantifier AExists = "?"
+fun string_for_connective ANot = "~"
+ | string_for_connective AAnd = "&"
+ | string_for_connective AOr = "|"
+ | string_for_connective AImplies = "=>"
+ | string_for_connective AIf = "<="
+ | string_for_connective AIff = "<=>"
+ | string_for_connective ANotIff = "<~>"
+fun string_for_formula (AQuant (q, xs, phi)) =
+ string_for_quantifier q ^ "[" ^ commas xs ^ "] : " ^
+ string_for_formula phi
+ | string_for_formula (AConn (ANot, [APred (ATerm ("equal", ts))])) =
+ space_implode " != " (map string_for_term ts)
+ | string_for_formula (AConn (c, [phi])) =
+ string_for_connective c ^ " " ^ string_for_formula phi
+ | string_for_formula (AConn (c, phis)) =
+ "(" ^ space_implode (" " ^ string_for_connective c ^ " ")
+ (map string_for_formula phis) ^ ")"
+ | string_for_formula (APred tm) = string_for_term tm
+
+fun string_for_problem_line (Fof (ident, kind, phi)) =
+ "fof(" ^ ident ^ ", " ^
+ (case kind of Axiom => "axiom" | Conjecture => "conjecture") ^ ",\n" ^
+ " (" ^ string_for_formula phi ^ ")).\n"
+fun strings_for_tptp_problem problem =
+ "% This file was generated by Isabelle (most likely Sledgehammer)\n\
+ \% " ^ timestamp () ^ "\n" ::
+ maps (fn (_, []) => []
+ | (heading, lines) =>
+ "\n% " ^ heading ^ " (" ^ Int.toString (length lines) ^ ")\n" ::
+ map string_for_problem_line lines) problem
+
+fun is_tptp_variable s = Char.isUpper (String.sub (s, 0))
+
+
+(** Nice names **)
+
+fun empty_name_pool readable_names =
+ if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE
+
+fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs
+fun pool_map f xs =
+ pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs []
+
+(* "equal" is reserved by some ATPs. "op" is also reserved, to avoid the
+ unreadable "op_1", "op_2", etc., in the problem files. *)
+val reserved_nice_names = ["equal", "op"]
+fun readable_name full_name s =
+ if s = full_name then
+ s
+ else
+ let
+ val s = s |> Long_Name.base_name
+ |> Name.desymbolize (Char.isUpper (String.sub (full_name, 0)))
+ in if member (op =) reserved_nice_names s then full_name else s end
+
+fun nice_name (full_name, _) NONE = (full_name, NONE)
+ | nice_name (full_name, desired_name) (SOME the_pool) =
+ case Symtab.lookup (fst the_pool) full_name of
+ SOME nice_name => (nice_name, SOME the_pool)
+ | NONE =>
+ let
+ val nice_prefix = readable_name full_name desired_name
+ fun add j =
+ let
+ val nice_name = nice_prefix ^
+ (if j = 0 then "" else "_" ^ Int.toString j)
+ in
+ case Symtab.lookup (snd the_pool) nice_name of
+ SOME full_name' =>
+ if full_name = full_name' then (nice_name, the_pool)
+ else add (j + 1)
+ | NONE =>
+ (nice_name,
+ (Symtab.update_new (full_name, nice_name) (fst the_pool),
+ Symtab.update_new (nice_name, full_name) (snd the_pool)))
+ end
+ in add 0 |> apsnd SOME end
+
+
+fun nice_term (ATerm (name, ts)) =
+ nice_name name ##>> pool_map nice_term ts #>> ATerm
+fun nice_formula (AQuant (q, xs, phi)) =
+ pool_map nice_name xs ##>> nice_formula phi
+ #>> (fn (xs, phi) => AQuant (q, xs, phi))
+ | nice_formula (AConn (c, phis)) =
+ pool_map nice_formula phis #>> curry AConn c
+ | nice_formula (APred tm) = nice_term tm #>> APred
+fun nice_problem_line (Fof (ident, kind, phi)) =
+ nice_formula phi #>> (fn phi => Fof (ident, kind, phi))
+fun nice_problem problem =
+ pool_map (fn (heading, lines) =>
+ pool_map nice_problem_line lines #>> pair heading) problem
+fun nice_tptp_problem readable_names problem =
+ nice_problem problem (empty_name_pool readable_names)
+
+end;
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Tue Jul 27 17:10:27 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Tue Jul 27 20:16:14 2010 +0200
@@ -7,10 +7,23 @@
signature ATP_SYSTEMS =
sig
- val trace : bool Unsynchronized.ref
- val dest_dir : string Config.T
- val problem_prefix : string Config.T
- val measure_runtime : bool Config.T
+ datatype failure =
+ Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
+ OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError
+
+ type prover_config =
+ {home_var: string,
+ executable: string,
+ arguments: bool -> Time.time -> string,
+ proof_delims: (string * string) list,
+ known_failures: (failure * string) list,
+ max_new_relevant_facts_per_iter: int,
+ prefers_theory_relevant: bool,
+ explicit_forall: bool}
+
+ val add_prover: string * prover_config -> theory -> theory
+ val get_prover: theory -> string -> prover_config
+ val available_atps: theory -> unit
val refresh_systems_on_tptp : unit -> unit
val default_atps_param_value : unit -> string
val setup : theory -> theory
@@ -19,31 +32,11 @@
structure ATP_Systems : ATP_SYSTEMS =
struct
-open Metis_Clauses
-open Sledgehammer_Util
-open Sledgehammer_Fact_Filter
-open Sledgehammer_TPTP_Format
-open Sledgehammer_Proof_Reconstruct
-open ATP_Manager
-
-val trace = Unsynchronized.ref false
-fun trace_msg msg = if !trace then tracing (msg ()) else ()
-
-(** generic ATP **)
+(* prover configuration *)
-(* external problem files *)
-
-val (dest_dir, dest_dir_setup) = Attrib.config_string "atp_dest_dir" (K "");
- (*Empty string means create files in Isabelle's temporary files directory.*)
-
-val (problem_prefix, problem_prefix_setup) =
- Attrib.config_string "atp_problem_prefix" (K "prob");
-
-val (measure_runtime, measure_runtime_setup) =
- Attrib.config_bool "atp_measure_runtime" (K false);
-
-
-(* prover configuration *)
+datatype failure =
+ Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
+ OldSpass | MalformedInput | MalformedOutput | UnknownError
type prover_config =
{home_var: string,
@@ -56,460 +49,32 @@
explicit_forall: bool}
-(* basic template *)
-
-val remotify = prefix "remote_"
-
-fun with_path cleanup after f path =
- Exn.capture f path
- |> tap (fn _ => cleanup path)
- |> Exn.release
- |> tap (after path)
-
-(* Splits by the first possible of a list of delimiters. *)
-fun extract_proof delims output =
- case pairself (find_first (fn s => String.isSubstring s output))
- (ListPair.unzip delims) of
- (SOME begin_delim, SOME end_delim) =>
- (output |> first_field begin_delim |> the |> snd
- |> first_field end_delim |> the |> fst
- |> first_field "\n" |> the |> snd
- handle Option.Option => "")
- | _ => ""
-
-fun extract_proof_and_outcome complete res_code proof_delims known_failures
- output =
- case map_filter (fn (failure, pattern) =>
- if String.isSubstring pattern output then SOME failure
- else NONE) known_failures of
- [] => (case extract_proof proof_delims output of
- "" => ("", SOME UnknownError)
- | proof => if res_code = 0 then (proof, NONE)
- else ("", SOME UnknownError))
- | (failure :: _) =>
- ("", SOME (if failure = IncompleteUnprovable andalso complete then
- Unprovable
- else
- failure))
-
-fun string_for_failure Unprovable = "The ATP problem is unprovable."
- | string_for_failure IncompleteUnprovable =
- "The ATP cannot prove the problem."
- | string_for_failure CantConnect = "Can't connect to remote ATP."
- | string_for_failure TimedOut = "Timed out."
- | string_for_failure OutOfResources = "The ATP ran out of resources."
- | string_for_failure OldSpass =
- (* FIXME: Change the error message below to point to the Isabelle download
- page once the package is there. *)
- "Warning: Sledgehammer requires a more recent version of SPASS with \
- \support for the TPTP syntax. To install it, download and untar the \
- \package \"http://isabelle.in.tum.de/~blanchet/spass-3.7.tgz\" and add the \
- \\"spass-3.7\" directory's full path to \"" ^
- Path.implode (Path.expand (Path.appends
- (Path.variable "ISABELLE_HOME_USER" ::
- map Path.basic ["etc", "components"]))) ^
- "\" on a line of its own."
- | string_for_failure MalformedInput =
- "Internal Sledgehammer error: The ATP problem is malformed. Please report \
- \this to the Isabelle developers."
- | string_for_failure MalformedOutput = "Error: The ATP output is malformed."
- | string_for_failure UnknownError = "Error: An unknown ATP error occurred."
-
-
-(* Clause preparation *)
-
-fun make_clause_table xs =
- fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty
-
-(* Remove existing axiom clauses from the conjecture clauses, as this can
- dramatically boost an ATP's performance (for some reason). *)
-fun subtract_cls ax_clauses =
- filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of)
-
-fun combformula_for_prop thy =
- let
- val do_term = combterm_from_term thy
- fun do_quant bs q s T t' =
- do_formula ((s, T) :: bs) t'
- #>> (fn phi => AQuant (q, [`make_bound_var s], phi))
- and do_conn bs c t1 t2 =
- do_formula bs t1 ##>> do_formula bs t2
- #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2]))
- and do_formula bs t =
- case t of
- @{const Not} $ t1 =>
- do_formula bs t1 #>> (fn phi => AConn (ANot, [phi]))
- | Const (@{const_name All}, _) $ Abs (s, T, t') =>
- do_quant bs AForall s T t'
- | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
- do_quant bs AExists s T t'
- | @{const "op &"} $ t1 $ t2 => do_conn bs AAnd t1 t2
- | @{const "op |"} $ t1 $ t2 => do_conn bs AOr t1 t2
- | @{const "op -->"} $ t1 $ t2 => do_conn bs AImplies t1 t2
- | Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
- do_conn bs AIff t1 t2
- | _ => (fn ts => do_term bs (Envir.eta_contract t)
- |>> APred ||> union (op =) ts)
- in do_formula [] end
+(* named provers *)
-(* Converts an elim-rule into an equivalent theorem that does not have the
- predicate variable. Leaves other theorems unchanged. We simply instantiate
- the conclusion variable to False. (Cf. "transform_elim_term" in
- "ATP_Systems".) *)
-(* FIXME: test! *)
-fun transform_elim_term t =
- case Logic.strip_imp_concl t of
- @{const Trueprop} $ Var (z, @{typ bool}) =>
- subst_Vars [(z, @{const True})] t
- | Var (z, @{typ prop}) => subst_Vars [(z, @{prop True})] t
- | _ => t
-
-(* Removes the lambdas from an equation of the form "t = (%x. u)".
- (Cf. "extensionalize_theorem" in "Clausifier".) *)
-fun extensionalize_term t =
- let
- fun aux j (Const (@{const_name "op ="}, Type (_, [Type (_, [_, T']), _]))
- $ t2 $ Abs (s, var_T, t')) =
- let val var_t = Var (("x", j), var_T) in
- Const (@{const_name "op ="}, T' --> T' --> HOLogic.boolT)
- $ betapply (t2, var_t) $ subst_bound (var_t, t')
- |> aux (j + 1)
- end
- | aux _ t = t
- in aux (maxidx_of_term t + 1) t end
-
-(* FIXME: Guarantee freshness *)
-fun concealed_bound_name j = "Sledgehammer" ^ Int.toString j
-fun conceal_bounds Ts t =
- subst_bounds (map (Free o apfst concealed_bound_name)
- (length Ts - 1 downto 0 ~~ rev Ts), t)
-fun reveal_bounds Ts =
- subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
- (0 upto length Ts - 1 ~~ Ts))
-
-fun introduce_combinators_in_term ctxt kind t =
- let
- val thy = ProofContext.theory_of ctxt
- fun aux Ts t =
- case t of
- @{const Not} $ t1 => @{const Not} $ aux Ts t1
- | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
- t0 $ Abs (s, T, aux (T :: Ts) t')
- | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
- t0 $ Abs (s, T, aux (T :: Ts) t')
- | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
- | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
- | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
- | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])))
- $ t1 $ t2 =>
- t0 $ aux Ts t1 $ aux Ts t2
- | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
- t
- else
- let
- val t = t |> conceal_bounds Ts
- |> Envir.eta_contract
- val ([t], ctxt') = Variable.import_terms true [t] ctxt
- in
- t |> cterm_of thy
- |> Clausifier.introduce_combinators_in_cterm
- |> singleton (Variable.export ctxt' ctxt)
- |> prop_of |> Logic.dest_equals |> snd
- |> reveal_bounds Ts
- end
- in t |> not (Meson.is_fol_term thy t) ? aux [] end
- handle THM _ =>
- (* A type variable of sort "{}" will make abstraction fail. *)
- case kind of
- Axiom => HOLogic.true_const
- | Conjecture => HOLogic.false_const
-
-(* making axiom and conjecture clauses *)
-fun make_clause ctxt (formula_name, kind, t) =
- let
- val thy = ProofContext.theory_of ctxt
- (* ### FIXME: perform other transformations previously done by
- "Clausifier.to_nnf", e.g. "HOL.If" *)
- val t = t |> transform_elim_term
- |> Object_Logic.atomize_term thy
- |> extensionalize_term
- |> introduce_combinators_in_term ctxt kind
- val (combformula, ctypes_sorts) = combformula_for_prop thy t []
- in
- FOLFormula {formula_name = formula_name, combformula = combformula,
- kind = kind, ctypes_sorts = ctypes_sorts}
- end
-
-fun make_axiom_clause ctxt (name, th) =
- (name, make_clause ctxt (name, Axiom, prop_of th))
-fun make_conjecture_clauses ctxt ts =
- map2 (fn j => fn t => make_clause ctxt (Int.toString j, Conjecture, t))
- (0 upto length ts - 1) ts
-
-(** Helper clauses **)
-
-fun count_combterm (CombConst ((s, _), _, _)) =
- Symtab.map_entry s (Integer.add 1)
- | count_combterm (CombVar _) = I
- | count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2]
-fun count_combformula (AQuant (_, _, phi)) = count_combformula phi
- | count_combformula (AConn (_, phis)) = fold count_combformula phis
- | count_combformula (APred tm) = count_combterm tm
-fun count_fol_formula (FOLFormula {combformula, ...}) =
- count_combformula combformula
-
-val optional_helpers =
- [(["c_COMBI", "c_COMBK"], @{thms COMBI_def COMBK_def}),
- (["c_COMBB", "c_COMBC"], @{thms COMBB_def COMBC_def}),
- (["c_COMBS"], @{thms COMBS_def})]
-val optional_typed_helpers =
- [(["c_True", "c_False"], @{thms True_or_False}),
- (["c_If"], @{thms if_True if_False True_or_False})]
-val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
-
-val init_counters =
- Symtab.make (maps (maps (map (rpair 0) o fst))
- [optional_helpers, optional_typed_helpers])
+structure Data = Theory_Data
+(
+ type T = (prover_config * stamp) Symtab.table
+ val empty = Symtab.empty
+ val extend = I
+ fun merge data : T = Symtab.merge (eq_snd op =) data
+ handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
+)
-fun get_helper_clauses ctxt is_FO full_types conjectures axclauses =
- let
- val ct = fold (fold count_fol_formula) [conjectures, axclauses]
- init_counters
- fun is_needed c = the (Symtab.lookup ct c) > 0
- val cnfs =
- (optional_helpers
- |> full_types ? append optional_typed_helpers
- |> maps (fn (ss, ths) =>
- if exists is_needed ss then map (`Thm.get_name_hint) ths
- else [])) @
- (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers)
- in map (snd o make_axiom_clause ctxt) cnfs end
-
-fun s_not (@{const Not} $ t) = t
- | s_not t = @{const Not} $ t
-
-(* prepare for passing to writer,
- create additional clauses based on the information from extra_cls *)
-fun prepare_clauses ctxt full_types hyp_ts concl_t axcls extra_cls =
- let
- val thy = ProofContext.theory_of ctxt
- val goal_t = Logic.list_implies (hyp_ts, concl_t)
- val is_FO = Meson.is_fol_term thy goal_t
- val _ = trace_msg (fn _ => Syntax.string_of_term ctxt goal_t)
- val axtms = map (prop_of o snd) extra_cls
- val subs = tfree_classes_of_terms [goal_t]
- val supers = tvar_classes_of_terms axtms
- val tycons = type_consts_of_terms thy (goal_t :: axtms)
- (* TFrees in conjecture clauses; TVars in axiom clauses *)
- val conjectures =
- map (s_not o HOLogic.dest_Trueprop) hyp_ts @
- [HOLogic.dest_Trueprop concl_t]
- |> make_conjecture_clauses ctxt
- val extra_clauses = map (snd o make_axiom_clause ctxt) extra_cls
- val (clnames, axiom_clauses) =
- ListPair.unzip (map (make_axiom_clause ctxt) axcls)
- (* FIXME: Should it read "extra_clauses" or "axiom_clauses" in the
- "get_helper_clauses" call? *)
- val helper_clauses =
- get_helper_clauses ctxt is_FO full_types conjectures extra_clauses
- val (supers', arity_clauses) = make_arity_clauses thy tycons supers
- val class_rel_clauses = make_class_rel_clauses thy subs supers'
- in
- (Vector.fromList clnames,
- (conjectures, axiom_clauses, extra_clauses, helper_clauses,
- class_rel_clauses, arity_clauses))
- end
+fun add_prover (name, config) thy =
+ Data.map (Symtab.update_new (name, (config, stamp ()))) thy
+ handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
-fun extract_clause_sequence output =
- let
- val tokens_of = String.tokens (not o Char.isAlphaNum)
- fun extract_num ("clause" :: (ss as _ :: _)) =
- Int.fromString (List.last ss)
- | extract_num _ = NONE
- in output |> split_lines |> map_filter (extract_num o tokens_of) end
-
-val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation"
-
-val parse_clause_formula_pair =
- $$ "(" |-- scan_integer --| $$ "," -- Symbol.scan_id --| $$ ")"
- --| Scan.option ($$ ",")
-val parse_clause_formula_relation =
- Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
- |-- Scan.repeat parse_clause_formula_pair
-val extract_clause_formula_relation =
- Substring.full
- #> Substring.position set_ClauseFormulaRelationN
- #> snd #> Substring.string #> strip_spaces #> explode
- #> parse_clause_formula_relation #> fst
-
-fun repair_conjecture_shape_and_theorem_names output conjecture_shape
- thm_names =
- if String.isSubstring set_ClauseFormulaRelationN output then
- (* This is a hack required for keeping track of axioms after they have been
- clausified by SPASS's Flotter tool. The "SPASS_TPTP" script is also part
- of this hack. *)
- let
- val j0 = hd conjecture_shape
- val seq = extract_clause_sequence output
- val name_map = extract_clause_formula_relation output
- fun renumber_conjecture j =
- AList.find (op =) name_map (conjecture_prefix ^ Int.toString (j - j0))
- |> the_single
- |> (fn s => find_index (curry (op =) s) seq + 1)
- in
- (conjecture_shape |> map renumber_conjecture,
- seq |> map (the o AList.lookup (op =) name_map)
- |> map (fn s => case try (unprefix axiom_prefix) s of
- SOME s' => undo_ascii_of s'
- | NONE => "")
- |> Vector.fromList)
- end
- else
- (conjecture_shape, thm_names)
-
-
-(* generic TPTP-based provers *)
+fun get_prover thy name =
+ the (Symtab.lookup (Data.get thy) name) |> fst
+ handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
-fun generic_tptp_prover
- (name, {home_var, executable, arguments, proof_delims, known_failures,
- max_new_relevant_facts_per_iter, prefers_theory_relevant,
- explicit_forall})
- ({debug, overlord, full_types, explicit_apply, relevance_threshold,
- relevance_convergence, theory_relevant, defs_relevant, isar_proof,
- isar_shrink_factor, ...} : params)
- minimize_command timeout
- ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
- : problem) =
- let
- (* get clauses and prepare them for writing *)
- val (ctxt, (_, th)) = goal;
- val thy = ProofContext.theory_of ctxt
- (* ### FIXME: (1) preprocessing for "if" etc. *)
- val (params, hyp_ts, concl_t) = strip_subgoal th subgoal
- val the_filtered_clauses =
- case filtered_clauses of
- SOME fcls => fcls
- | NONE => relevant_facts full_types relevance_threshold
- relevance_convergence defs_relevant
- max_new_relevant_facts_per_iter
- (the_default prefers_theory_relevant theory_relevant)
- relevance_override goal hyp_ts concl_t
- val the_axiom_clauses = axiom_clauses |> the_default the_filtered_clauses
- val (internal_thm_names, clauses) =
- prepare_clauses ctxt full_types hyp_ts concl_t the_axiom_clauses
- the_filtered_clauses
-
- (* path to unique problem file *)
- val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
- else Config.get ctxt dest_dir;
- val the_problem_prefix = Config.get ctxt problem_prefix;
- fun prob_pathname nr =
- let
- val probfile =
- Path.basic ((if overlord then "prob_" ^ name
- else the_problem_prefix ^ serial_string ())
- ^ "_" ^ string_of_int nr)
- in
- if the_dest_dir = "" then File.tmp_path probfile
- else if File.exists (Path.explode the_dest_dir)
- then Path.append (Path.explode the_dest_dir) probfile
- else error ("No such directory: " ^ the_dest_dir ^ ".")
- end;
+fun available_atps thy =
+ priority ("Available ATPs: " ^
+ commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".")
- val home = getenv home_var
- val command = Path.explode (home ^ "/" ^ executable)
- (* write out problem file and call prover *)
- fun command_line complete probfile =
- let
- val core = File.shell_path command ^ " " ^ arguments complete timeout ^
- " " ^ File.shell_path probfile
- in
- (if Config.get ctxt measure_runtime then
- "TIMEFORMAT='%3U'; { time " ^ core ^ " ; }"
- else
- "exec " ^ core) ^ " 2>&1"
- end
- fun split_time s =
- let
- val split = String.tokens (fn c => str c = "\n");
- val (output, t) = s |> split |> split_last |> apfst cat_lines;
- fun as_num f = f >> (fst o read_int);
- val num = as_num (Scan.many1 Symbol.is_ascii_digit);
- val digit = Scan.one Symbol.is_ascii_digit;
- val num3 = as_num (digit ::: digit ::: (digit >> single));
- val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b);
- val as_time = the_default 0 o Scan.read Symbol.stopper time o explode;
- in (output, as_time t) end;
- fun run_on probfile =
- if home = "" then
- error ("The environment variable " ^ quote home_var ^ " is not set.")
- else if File.exists command then
- let
- fun do_run complete =
- let
- val command = command_line complete probfile
- val ((output, msecs), res_code) =
- bash_output command
- |>> (if overlord then
- prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
- else
- I)
- |>> (if Config.get ctxt measure_runtime then split_time
- else rpair 0)
- val (proof, outcome) =
- extract_proof_and_outcome complete res_code proof_delims
- known_failures output
- in (output, msecs, proof, outcome) end
- val readable_names = debug andalso overlord
- val (pool, conjecture_offset) =
- write_tptp_file thy readable_names explicit_forall full_types
- explicit_apply probfile clauses
- val conjecture_shape =
- conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
- val result =
- do_run false
- |> (fn (_, msecs0, _, SOME _) =>
- do_run true
- |> (fn (output, msecs, proof, outcome) =>
- (output, msecs0 + msecs, proof, outcome))
- | result => result)
- in ((pool, conjecture_shape), result) end
- else
- error ("Bad executable: " ^ Path.implode command ^ ".");
-
- (* If the problem file has not been exported, remove it; otherwise, export
- the proof file too. *)
- fun cleanup probfile =
- if the_dest_dir = "" then try File.rm probfile else NONE
- fun export probfile (_, (output, _, _, _)) =
- if the_dest_dir = "" then
- ()
- else
- File.write (Path.explode (Path.implode probfile ^ "_proof")) output
-
- val ((pool, conjecture_shape), (output, msecs, proof, outcome)) =
- with_path cleanup export run_on (prob_pathname subgoal)
- val (conjecture_shape, internal_thm_names) =
- repair_conjecture_shape_and_theorem_names output conjecture_shape
- internal_thm_names
-
- val (message, relevant_thm_names) =
- case outcome of
- NONE =>
- proof_text isar_proof
- (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
- (full_types, minimize_command, proof, internal_thm_names, th,
- subgoal)
- | SOME failure => (string_for_failure failure ^ "\n", [])
- in
- {outcome = outcome, message = message, pool = pool,
- relevant_thm_names = relevant_thm_names, atp_run_time_in_msecs = msecs,
- output = output, proof = proof, internal_thm_names = internal_thm_names,
- conjecture_shape = conjecture_shape,
- filtered_clauses = the_filtered_clauses}
- end
-
-fun tptp_prover name p = (name, generic_tptp_prover (name, p));
+fun available_atps thy =
+ priority ("Available ATPs: " ^
+ commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".")
fun to_generous_secs time = (Time.toMilliseconds time + 999) div 1000
@@ -537,7 +102,7 @@
max_new_relevant_facts_per_iter = 80 (* FIXME *),
prefers_theory_relevant = false,
explicit_forall = false}
-val e = tptp_prover "e" e_config
+val e = ("e", e_config)
(* The "-VarWeight=3" option helps the higher-order problems, probably by
@@ -562,7 +127,7 @@
max_new_relevant_facts_per_iter = 26 (* FIXME *),
prefers_theory_relevant = true,
explicit_forall = true}
-val spass = tptp_prover "spass" spass_config
+val spass = ("spass", spass_config)
(* Vampire *)
@@ -584,11 +149,11 @@
max_new_relevant_facts_per_iter = 40 (* FIXME *),
prefers_theory_relevant = false,
explicit_forall = false}
-val vampire = tptp_prover "vampire" vampire_config
+val vampire = ("vampire", vampire_config)
(* Remote prover invocation via SystemOnTPTP *)
-val systems = Synchronized.var "atp_systems" ([]: string list);
+val systems = Synchronized.var "atp_systems" ([]: string list)
fun get_systems () =
case bash_output "\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w" of
@@ -629,27 +194,23 @@
prefers_theory_relevant = prefers_theory_relevant,
explicit_forall = explicit_forall}
-fun remote_tptp_prover prover atp_prefix args config =
- tptp_prover (remotify (fst prover)) (remote_config atp_prefix args config)
+val remote_name = prefix "remote_"
-val remote_e = remote_tptp_prover e "EP---" "" e_config
-val remote_spass = remote_tptp_prover spass "SPASS---" "-x" spass_config
-val remote_vampire = remote_tptp_prover vampire "Vampire---9" "" vampire_config
+fun remote_prover prover atp_prefix args config =
+ (remote_name (fst prover), remote_config atp_prefix args config)
+
+val remote_e = remote_prover e "EP---" "" e_config
+val remote_spass = remote_prover spass "SPASS---" "-x" spass_config
+val remote_vampire = remote_prover vampire "Vampire---9" "" vampire_config
fun maybe_remote (name, _) ({home_var, ...} : prover_config) =
- name |> getenv home_var = "" ? remotify
+ name |> getenv home_var = "" ? remote_name
fun default_atps_param_value () =
space_implode " " [maybe_remote e e_config, maybe_remote spass spass_config,
- remotify (fst vampire)]
+ remote_name (fst vampire)]
val provers = [e, spass, vampire, remote_e, remote_spass, remote_vampire]
-val prover_setup = fold add_prover provers
-
-val setup =
- dest_dir_setup
- #> problem_prefix_setup
- #> measure_runtime_setup
- #> prover_setup
+val setup = fold add_prover provers
end;
--- a/src/HOL/Tools/Nitpick/kodkod.ML Tue Jul 27 17:10:27 2010 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Tue Jul 27 20:16:14 2010 +0200
@@ -847,7 +847,7 @@
out "solve "; out_outmost_f formula; out ";\n")
in
out ("// This file was generated by Isabelle (most likely Nitpick)\n" ^
- "// " ^ Sledgehammer_Util.timestamp () ^ "\n");
+ "// " ^ ATP_Problem.timestamp () ^ "\n");
map out_problem problems
end
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Tue Jul 27 17:10:27 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Tue Jul 27 20:16:14 2010 +0200
@@ -49,7 +49,6 @@
val plural_s : int -> string
val plural_s_for_list : 'a list -> string
val serial_commas : string -> string list -> string list
- val timestamp : unit -> string
val parse_bool_option : bool -> string -> string -> bool option
val parse_time_option : string -> string -> Time.time option
val flip_polarity : polarity -> polarity
@@ -223,7 +222,6 @@
val serial_commas = Sledgehammer_Util.serial_commas
-val timestamp = Sledgehammer_Util.timestamp
val parse_bool_option = Sledgehammer_Util.parse_bool_option
val parse_time_option = Sledgehammer_Util.parse_time_option
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML Tue Jul 27 17:10:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Tue Jul 27 20:16:14 2010 +0200
@@ -1,5 +1,5 @@
(* Title: HOL/Tools/Sledgehammer/clausifier.ML
- Author: Jia Meng, Cambridge University Computer Laboratory
+ Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
Author: Jasmin Blanchette, TU Muenchen
Transformation of axiom rules (elim/intro/etc) into CNF forms.
@@ -8,10 +8,8 @@
signature CLAUSIFIER =
sig
val introduce_combinators_in_cterm : cterm -> thm
- val cnf_axiom: theory -> bool -> thm -> thm list
- val cnf_rules_pairs :
- theory -> bool -> (string * thm) list -> ((string * int) * thm) list
- val neg_clausify: thm -> thm list
+ val introduce_combinators_in_theorem : thm -> thm
+ val cnf_axiom: theory -> thm -> thm list
end;
structure Clausifier : CLAUSIFIER =
@@ -198,7 +196,7 @@
(* Given the definition of a Skolem function, return a theorem to replace
an existential formula by a use of that function.
Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *)
-fun skolem_theorem_of_def thy cheat rhs0 =
+fun skolem_theorem_of_def thy rhs0 =
let
val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> Thm.cterm_of thy
val rhs' = rhs |> Thm.dest_comb |> snd
@@ -214,12 +212,8 @@
Drule.list_comb (rhs, frees)
|> Drule.beta_conv cabs |> Thm.capply cTrueprop
fun tacf [prem] =
- if cheat then
- Skip_Proof.cheat_tac thy
- else
- rewrite_goals_tac skolem_id_def_raw
- THEN rtac ((prem |> rewrite_rule skolem_id_def_raw)
- RS @{thm someI_ex}) 1
+ rewrite_goals_tac skolem_id_def_raw
+ THEN rtac ((prem |> rewrite_rule skolem_id_def_raw) RS @{thm someI_ex}) 1
in
Goal.prove_internal [ex_tm] conc tacf
|> forall_intr_list frees
@@ -238,11 +232,11 @@
in (th3, ctxt) end;
(* Skolemize a named theorem, with Skolem functions as additional premises. *)
-fun skolemize_theorem thy cheat th =
+fun skolemize_theorem thy th =
let
val ctxt0 = Variable.global_thm_context th
val (nnfth, ctxt) = to_nnf th ctxt0
- val sko_ths = map (skolem_theorem_of_def thy cheat)
+ val sko_ths = map (skolem_theorem_of_def thy)
(assume_skolem_funs nnfth)
val (cnfs, ctxt) = Meson.make_cnf sko_ths nnfth ctxt
in
@@ -255,36 +249,6 @@
(* Convert Isabelle theorems into axiom clauses. *)
(* FIXME: is transfer necessary? *)
-fun cnf_axiom thy cheat = skolemize_theorem thy cheat o Thm.transfer thy
-
-
-(**** Translate a set of theorems into CNF ****)
-
-(*The combination of rev and tail recursion preserves the original order*)
-(* ### FIXME: kill "cheat" *)
-fun cnf_rules_pairs thy cheat =
- let
- fun do_one _ [] = []
- | do_one ((name, k), th) (cls :: clss) =
- ((name, k), cls) :: do_one ((name, k + 1), th) clss
- fun do_all pairs [] = pairs
- | do_all pairs ((name, th) :: ths) =
- let
- val new_pairs = do_one ((name, 0), th) (cnf_axiom thy cheat th)
- handle THM _ => []
- in do_all (new_pairs @ pairs) ths end
- in do_all [] o rev end
-
-
-(*** Converting a subgoal into negated conjecture clauses. ***)
-
-fun neg_skolemize_tac ctxt =
- EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt]
-
-val neg_clausify =
- single
- #> Meson.make_clauses_unsorted
- #> map introduce_combinators_in_theorem
- #> Meson.finish_cnf
+fun cnf_axiom thy = skolemize_theorem thy o Thm.transfer thy
end;
--- a/src/HOL/Tools/Sledgehammer/meson_tactic.ML Tue Jul 27 17:10:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/meson_tactic.ML Tue Jul 27 20:16:14 2010 +0200
@@ -1,5 +1,5 @@
(* Title: HOL/Tools/Sledgehammer/meson_tactic.ML
- Author: Jia Meng, Cambridge University Computer Laboratory
+ Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
Author: Jasmin Blanchette, TU Muenchen
MESON general tactic and proof method.
@@ -18,7 +18,7 @@
let
val thy = ProofContext.theory_of ctxt
val ctxt0 = Classical.put_claset HOL_cs ctxt
- in Meson.meson_tac ctxt0 (maps (Clausifier.cnf_axiom thy false) ths) end
+ in Meson.meson_tac ctxt0 (maps (Clausifier.cnf_axiom thy) ths) end
val setup =
Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Tue Jul 27 17:10:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Tue Jul 27 20:16:14 2010 +0200
@@ -1,5 +1,5 @@
(* Title: HOL/Tools/Sledgehammer/metis_clauses.ML
- Author: Jia Meng, Cambridge University Computer Laboratory
+ Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
Author: Jasmin Blanchette, TU Muenchen
Storing/printing FOL clauses and arity clauses. Typed equality is
@@ -9,17 +9,16 @@
signature METIS_CLAUSES =
sig
type name = string * string
- datatype kind = Axiom | Conjecture
datatype type_literal =
TyLitVar of name * name |
TyLitFree of name * name
datatype arLit =
TConsLit of name * name * name list |
TVarLit of name * name
- datatype arity_clause = ArityClause of
- {axiom_name: string, conclLit: arLit, premLits: arLit list}
- datatype class_rel_clause = ClassRelClause of
- {axiom_name: string, subclass: name, superclass: name}
+ datatype arity_clause =
+ ArityClause of {axiom_name: string, conclLit: arLit, premLits: arLit list}
+ datatype class_rel_clause =
+ ClassRelClause of {axiom_name: string, subclass: name, superclass: name}
datatype combtyp =
CombTVar of name |
CombTFree of name |
@@ -29,9 +28,6 @@
CombVar of name * combtyp |
CombApp of combterm * combterm
datatype fol_literal = FOLLiteral of bool * combterm
- datatype fol_clause =
- FOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
- literals: fol_literal list, ctypes_sorts: typ list}
val type_wrapper_name : string
val bound_var_prefix : string
@@ -228,8 +224,6 @@
type name = string * string
-datatype kind = Axiom | Conjecture
-
(**** Isabelle FOL clauses ****)
(* The first component is the type class; the second is a TVar or TFree. *)
@@ -367,10 +361,6 @@
datatype fol_literal = FOLLiteral of bool * combterm
-datatype fol_clause =
- FOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
- literals: fol_literal list, ctypes_sorts: typ list}
-
(*********************************************************************)
(* convert a clause with type Term.term to a clause with type clause *)
(*********************************************************************)
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Jul 27 17:10:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Jul 27 20:16:14 2010 +0200
@@ -1,5 +1,7 @@
(* Title: HOL/Tools/Sledgehammer/metis_tactics.ML
- Author: Kong W. Susanto and Lawrence C. Paulson, CU Computer Laboratory
+ Author: Kong W. Susanto, Cambridge University Computer Laboratory
+ Author: Lawrence C. Paulson, Cambridge University Computer Laboratory
+ Author: Jasmin Blanchette, TU Muenchen
Copyright Cambridge University 2007
HOL setup for the Metis prover.
@@ -599,7 +601,7 @@
(* ------------------------------------------------------------------------- *)
fun cnf_helper_theorem thy raw th =
- if raw then th else the_single (Clausifier.cnf_axiom thy false th)
+ if raw then th else the_single (Clausifier.cnf_axiom thy th)
fun type_ext thy tms =
let val subs = tfree_classes_of_terms tms
@@ -715,7 +717,7 @@
fun FOL_SOLVE mode ctxt cls ths0 =
let val thy = ProofContext.theory_of ctxt
val th_cls_pairs =
- map (fn th => (Thm.get_name_hint th, Clausifier.cnf_axiom thy false th)) ths0
+ map (fn th => (Thm.get_name_hint th, Clausifier.cnf_axiom thy th)) ths0
val ths = maps #2 th_cls_pairs
val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
@@ -773,6 +775,12 @@
val type_has_top_sort =
exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
+val neg_clausify =
+ single
+ #> Meson.make_clauses_unsorted
+ #> map Clausifier.introduce_combinators_in_theorem
+ #> Meson.finish_cnf
+
fun generic_metis_tac mode ctxt ths i st0 =
let
val _ = trace_msg (fn () =>
@@ -781,7 +789,7 @@
if exists_type type_has_top_sort (prop_of st0) then
(warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
else
- Meson.MESON (maps Clausifier.neg_clausify)
+ Meson.MESON (maps neg_clausify)
(fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
ctxt i st0
handle ERROR msg => raise METIS ("generic_metis_tac", msg)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Jul 27 20:16:14 2010 +0200
@@ -0,0 +1,882 @@
+(* Title: HOL/Tools/Sledgehammer/sledgehammer.ML
+ Author: Fabian Immler, TU Muenchen
+ Author: Makarius
+ Author: Jasmin Blanchette, TU Muenchen
+
+Sledgehammer's heart.
+*)
+
+signature SLEDGEHAMMER =
+sig
+ type failure = ATP_Systems.failure
+ type relevance_override = Sledgehammer_Fact_Filter.relevance_override
+ type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
+ type params =
+ {debug: bool,
+ verbose: bool,
+ overlord: bool,
+ atps: string list,
+ full_types: bool,
+ explicit_apply: bool,
+ relevance_threshold: real,
+ relevance_convergence: real,
+ theory_relevant: bool option,
+ defs_relevant: bool,
+ isar_proof: bool,
+ isar_shrink_factor: int,
+ timeout: Time.time,
+ minimize_timeout: Time.time}
+ type problem =
+ {subgoal: int,
+ goal: Proof.context * (thm list * thm),
+ relevance_override: relevance_override,
+ axiom_clauses: (string * thm) list option,
+ filtered_clauses: (string * thm) list option}
+ type prover_result =
+ {outcome: failure option,
+ message: string,
+ pool: string Symtab.table,
+ used_thm_names: string list,
+ atp_run_time_in_msecs: int,
+ output: string,
+ proof: string,
+ internal_thm_names: string Vector.vector,
+ conjecture_shape: int list,
+ filtered_clauses: (string * thm) list}
+ type prover =
+ params -> minimize_command -> Time.time -> problem -> prover_result
+
+ val dest_dir : string Config.T
+ val problem_prefix : string Config.T
+ val measure_runtime : bool Config.T
+ val kill_atps: unit -> unit
+ val running_atps: unit -> unit
+ val messages: int option -> unit
+ val get_prover_fun : theory -> string -> prover
+ val start_prover_thread :
+ params -> int -> int -> relevance_override -> (string -> minimize_command)
+ -> Proof.state -> string -> unit
+ val setup : theory -> theory
+end;
+
+structure Sledgehammer : SLEDGEHAMMER =
+struct
+
+open ATP_Problem
+open ATP_Systems
+open Metis_Clauses
+open Sledgehammer_Util
+open Sledgehammer_Fact_Filter
+open Sledgehammer_Proof_Reconstruct
+
+
+(** The Sledgehammer **)
+
+val das_Tool = "Sledgehammer"
+
+fun kill_atps () = Async_Manager.kill_threads das_Tool "ATPs"
+fun running_atps () = Async_Manager.running_threads das_Tool "ATPs"
+val messages = Async_Manager.thread_messages das_Tool "ATP"
+
+(** problems, results, provers, etc. **)
+
+type params =
+ {debug: bool,
+ verbose: bool,
+ overlord: bool,
+ atps: string list,
+ full_types: bool,
+ explicit_apply: bool,
+ relevance_threshold: real,
+ relevance_convergence: real,
+ theory_relevant: bool option,
+ defs_relevant: bool,
+ isar_proof: bool,
+ isar_shrink_factor: int,
+ timeout: Time.time,
+ minimize_timeout: Time.time}
+
+type problem =
+ {subgoal: int,
+ goal: Proof.context * (thm list * thm),
+ relevance_override: relevance_override,
+ axiom_clauses: (string * thm) list option,
+ filtered_clauses: (string * thm) list option}
+
+type prover_result =
+ {outcome: failure option,
+ message: string,
+ pool: string Symtab.table,
+ used_thm_names: string list,
+ atp_run_time_in_msecs: int,
+ output: string,
+ proof: string,
+ internal_thm_names: string Vector.vector,
+ conjecture_shape: int list,
+ filtered_clauses: (string * thm) list}
+
+type prover =
+ params -> minimize_command -> Time.time -> problem -> prover_result
+
+(* configuration attributes *)
+
+val (dest_dir, dest_dir_setup) = Attrib.config_string "atp_dest_dir" (K "");
+ (*Empty string means create files in Isabelle's temporary files directory.*)
+
+val (problem_prefix, problem_prefix_setup) =
+ Attrib.config_string "atp_problem_prefix" (K "prob");
+
+val (measure_runtime, measure_runtime_setup) =
+ Attrib.config_bool "atp_measure_runtime" (K false);
+
+fun with_path cleanup after f path =
+ Exn.capture f path
+ |> tap (fn _ => cleanup path)
+ |> Exn.release
+ |> tap (after path)
+
+(* Splits by the first possible of a list of delimiters. *)
+fun extract_proof delims output =
+ case pairself (find_first (fn s => String.isSubstring s output))
+ (ListPair.unzip delims) of
+ (SOME begin_delim, SOME end_delim) =>
+ (output |> first_field begin_delim |> the |> snd
+ |> first_field end_delim |> the |> fst
+ |> first_field "\n" |> the |> snd
+ handle Option.Option => "")
+ | _ => ""
+
+fun extract_proof_and_outcome complete res_code proof_delims known_failures
+ output =
+ case map_filter (fn (failure, pattern) =>
+ if String.isSubstring pattern output then SOME failure
+ else NONE) known_failures of
+ [] => (case extract_proof proof_delims output of
+ "" => ("", SOME UnknownError)
+ | proof => if res_code = 0 then (proof, NONE)
+ else ("", SOME UnknownError))
+ | (failure :: _) =>
+ ("", SOME (if failure = IncompleteUnprovable andalso complete then
+ Unprovable
+ else
+ failure))
+
+fun string_for_failure Unprovable = "The ATP problem is unprovable."
+ | string_for_failure IncompleteUnprovable =
+ "The ATP cannot prove the problem."
+ | string_for_failure CantConnect = "Can't connect to remote ATP."
+ | string_for_failure TimedOut = "Timed out."
+ | string_for_failure OutOfResources = "The ATP ran out of resources."
+ | string_for_failure OldSpass =
+ (* FIXME: Change the error message below to point to the Isabelle download
+ page once the package is there. *)
+ "Warning: Sledgehammer requires a more recent version of SPASS with \
+ \support for the TPTP syntax. To install it, download and untar the \
+ \package \"http://isabelle.in.tum.de/~blanchet/spass-3.7.tgz\" and add the \
+ \\"spass-3.7\" directory's full path to \"" ^
+ Path.implode (Path.expand (Path.appends
+ (Path.variable "ISABELLE_HOME_USER" ::
+ map Path.basic ["etc", "components"]))) ^
+ "\" on a line of its own."
+ | string_for_failure MalformedInput =
+ "Internal Sledgehammer error: The ATP problem is malformed. Please report \
+ \this to the Isabelle developers."
+ | string_for_failure MalformedOutput = "Error: The ATP output is malformed."
+ | string_for_failure UnknownError = "Error: An unknown ATP error occurred."
+
+
+(* Clause preparation *)
+
+datatype fol_formula =
+ FOLFormula of {formula_name: string,
+ kind: kind,
+ combformula: (name, combterm) formula,
+ ctypes_sorts: typ list}
+
+fun mk_anot phi = AConn (ANot, [phi])
+fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
+fun mk_ahorn [] phi = phi
+ | mk_ahorn (phi :: phis) psi =
+ AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi])
+
+(* ### FIXME: reintroduce
+fun make_clause_table xs =
+ fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty
+(* Remove existing axiom clauses from the conjecture clauses, as this can
+ dramatically boost an ATP's performance (for some reason). *)
+fun subtract_cls ax_clauses =
+ filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of)
+*)
+
+fun combformula_for_prop thy =
+ let
+ val do_term = combterm_from_term thy
+ fun do_quant bs q s T t' =
+ do_formula ((s, T) :: bs) t'
+ #>> (fn phi => AQuant (q, [`make_bound_var s], phi))
+ and do_conn bs c t1 t2 =
+ do_formula bs t1 ##>> do_formula bs t2
+ #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2]))
+ and do_formula bs t =
+ case t of
+ @{const Not} $ t1 =>
+ do_formula bs t1 #>> (fn phi => AConn (ANot, [phi]))
+ | Const (@{const_name All}, _) $ Abs (s, T, t') =>
+ do_quant bs AForall s T t'
+ | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
+ do_quant bs AExists s T t'
+ | @{const "op &"} $ t1 $ t2 => do_conn bs AAnd t1 t2
+ | @{const "op |"} $ t1 $ t2 => do_conn bs AOr t1 t2
+ | @{const "op -->"} $ t1 $ t2 => do_conn bs AImplies t1 t2
+ | Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
+ do_conn bs AIff t1 t2
+ | _ => (fn ts => do_term bs (Envir.eta_contract t)
+ |>> APred ||> union (op =) ts)
+ in do_formula [] end
+
+(* Converts an elim-rule into an equivalent theorem that does not have the
+ predicate variable. Leaves other theorems unchanged. We simply instantiate
+ the conclusion variable to False. (Cf. "transform_elim_term" in
+ "ATP_Systems".) *)
+(* FIXME: test! *)
+fun transform_elim_term t =
+ case Logic.strip_imp_concl t of
+ @{const Trueprop} $ Var (z, @{typ bool}) =>
+ subst_Vars [(z, @{const True})] t
+ | Var (z, @{typ prop}) => subst_Vars [(z, @{prop True})] t
+ | _ => t
+
+(* Removes the lambdas from an equation of the form "t = (%x. u)".
+ (Cf. "extensionalize_theorem" in "Clausifier".) *)
+fun extensionalize_term t =
+ let
+ fun aux j (Const (@{const_name "op ="}, Type (_, [Type (_, [_, T']), _]))
+ $ t2 $ Abs (s, var_T, t')) =
+ let val var_t = Var (("x", j), var_T) in
+ Const (@{const_name "op ="}, T' --> T' --> HOLogic.boolT)
+ $ betapply (t2, var_t) $ subst_bound (var_t, t')
+ |> aux (j + 1)
+ end
+ | aux _ t = t
+ in aux (maxidx_of_term t + 1) t end
+
+(* FIXME: Guarantee freshness *)
+fun concealed_bound_name j = "Sledgehammer" ^ Int.toString j
+fun conceal_bounds Ts t =
+ subst_bounds (map (Free o apfst concealed_bound_name)
+ (length Ts - 1 downto 0 ~~ rev Ts), t)
+fun reveal_bounds Ts =
+ subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
+ (0 upto length Ts - 1 ~~ Ts))
+
+fun introduce_combinators_in_term ctxt kind t =
+ let
+ val thy = ProofContext.theory_of ctxt
+ fun aux Ts t =
+ case t of
+ @{const Not} $ t1 => @{const Not} $ aux Ts t1
+ | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
+ t0 $ Abs (s, T, aux (T :: Ts) t')
+ | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
+ t0 $ Abs (s, T, aux (T :: Ts) t')
+ | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+ | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+ | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+ | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])))
+ $ t1 $ t2 =>
+ t0 $ aux Ts t1 $ aux Ts t2
+ | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
+ t
+ else
+ let
+ val t = t |> conceal_bounds Ts
+ |> Envir.eta_contract
+ val ([t], ctxt') = Variable.import_terms true [t] ctxt
+ in
+ t |> cterm_of thy
+ |> Clausifier.introduce_combinators_in_cterm
+ |> singleton (Variable.export ctxt' ctxt)
+ |> prop_of |> Logic.dest_equals |> snd
+ |> reveal_bounds Ts
+ end
+ in t |> not (Meson.is_fol_term thy t) ? aux [] end
+ handle THM _ =>
+ (* A type variable of sort "{}" will make abstraction fail. *)
+ case kind of
+ Axiom => HOLogic.true_const
+ | Conjecture => HOLogic.false_const
+
+(* making axiom and conjecture clauses *)
+fun make_clause ctxt (formula_name, kind, t) =
+ let
+ val thy = ProofContext.theory_of ctxt
+ (* ### FIXME: perform other transformations previously done by
+ "Clausifier.to_nnf", e.g. "HOL.If" *)
+ val t = t |> transform_elim_term
+ |> Object_Logic.atomize_term thy
+ |> extensionalize_term
+ |> introduce_combinators_in_term ctxt kind
+ val (combformula, ctypes_sorts) = combformula_for_prop thy t []
+ in
+ FOLFormula {formula_name = formula_name, combformula = combformula,
+ kind = kind, ctypes_sorts = ctypes_sorts}
+ end
+
+fun make_axiom_clause ctxt (name, th) =
+ (name, make_clause ctxt (name, Axiom, prop_of th))
+fun make_conjecture_clauses ctxt ts =
+ map2 (fn j => fn t => make_clause ctxt (Int.toString j, Conjecture, t))
+ (0 upto length ts - 1) ts
+
+(** Helper clauses **)
+
+fun count_combterm (CombConst ((s, _), _, _)) =
+ Symtab.map_entry s (Integer.add 1)
+ | count_combterm (CombVar _) = I
+ | count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2]
+fun count_combformula (AQuant (_, _, phi)) = count_combformula phi
+ | count_combformula (AConn (_, phis)) = fold count_combformula phis
+ | count_combformula (APred tm) = count_combterm tm
+fun count_fol_formula (FOLFormula {combformula, ...}) =
+ count_combformula combformula
+
+val optional_helpers =
+ [(["c_COMBI", "c_COMBK"], @{thms COMBI_def COMBK_def}),
+ (["c_COMBB", "c_COMBC"], @{thms COMBB_def COMBC_def}),
+ (["c_COMBS"], @{thms COMBS_def})]
+val optional_typed_helpers =
+ [(["c_True", "c_False"], @{thms True_or_False}),
+ (["c_If"], @{thms if_True if_False True_or_False})]
+val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
+
+val init_counters =
+ Symtab.make (maps (maps (map (rpair 0) o fst))
+ [optional_helpers, optional_typed_helpers])
+
+fun get_helper_clauses ctxt is_FO full_types conjectures axclauses =
+ let
+ val ct = fold (fold count_fol_formula) [conjectures, axclauses]
+ init_counters
+ fun is_needed c = the (Symtab.lookup ct c) > 0
+ val cnfs =
+ (optional_helpers
+ |> full_types ? append optional_typed_helpers
+ |> maps (fn (ss, ths) =>
+ if exists is_needed ss then map (`Thm.get_name_hint) ths
+ else [])) @
+ (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers)
+ in map (snd o make_axiom_clause ctxt) cnfs end
+
+fun s_not (@{const Not} $ t) = t
+ | s_not t = @{const Not} $ t
+
+(* prepare for passing to writer,
+ create additional clauses based on the information from extra_cls *)
+fun prepare_clauses ctxt full_types hyp_ts concl_t axcls extra_cls =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val goal_t = Logic.list_implies (hyp_ts, concl_t)
+ val is_FO = Meson.is_fol_term thy goal_t
+ val axtms = map (prop_of o snd) extra_cls
+ val subs = tfree_classes_of_terms [goal_t]
+ val supers = tvar_classes_of_terms axtms
+ val tycons = type_consts_of_terms thy (goal_t :: axtms)
+ (* TFrees in conjecture clauses; TVars in axiom clauses *)
+ val conjectures =
+ map (s_not o HOLogic.dest_Trueprop) hyp_ts @
+ [HOLogic.dest_Trueprop concl_t]
+ |> make_conjecture_clauses ctxt
+ val extra_clauses = map (snd o make_axiom_clause ctxt) extra_cls
+ val (clnames, axiom_clauses) =
+ ListPair.unzip (map (make_axiom_clause ctxt) axcls)
+ (* FIXME: Should it read "extra_clauses" or "axiom_clauses" in the
+ "get_helper_clauses" call? *)
+ val helper_clauses =
+ get_helper_clauses ctxt is_FO full_types conjectures extra_clauses
+ val (supers', arity_clauses) = make_arity_clauses thy tycons supers
+ val class_rel_clauses = make_class_rel_clauses thy subs supers'
+ in
+ (Vector.fromList clnames,
+ (conjectures, axiom_clauses, extra_clauses, helper_clauses,
+ class_rel_clauses, arity_clauses))
+ end
+
+val axiom_prefix = "ax_"
+val conjecture_prefix = "conj_"
+val arity_clause_prefix = "clsarity_"
+val tfrees_name = "tfrees"
+
+fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
+
+fun fo_term_for_combtyp (CombTVar name) = ATerm (name, [])
+ | fo_term_for_combtyp (CombTFree name) = ATerm (name, [])
+ | fo_term_for_combtyp (CombType (name, tys)) =
+ ATerm (name, map fo_term_for_combtyp tys)
+
+fun fo_literal_for_type_literal (TyLitVar (class, name)) =
+ (true, ATerm (class, [ATerm (name, [])]))
+ | fo_literal_for_type_literal (TyLitFree (class, name)) =
+ (true, ATerm (class, [ATerm (name, [])]))
+
+fun formula_for_fo_literal (pos, t) = APred t |> not pos ? mk_anot
+
+fun fo_term_for_combterm full_types =
+ let
+ fun aux top_level u =
+ let
+ val (head, args) = strip_combterm_comb u
+ val (x, ty_args) =
+ case head of
+ CombConst (name, _, ty_args) =>
+ if fst name = "equal" then
+ (if top_level andalso length args = 2 then name
+ else ("c_fequal", @{const_name fequal}), [])
+ else
+ (name, if full_types then [] else ty_args)
+ | CombVar (name, _) => (name, [])
+ | CombApp _ => raise Fail "impossible \"CombApp\""
+ val t = ATerm (x, map fo_term_for_combtyp ty_args @
+ map (aux false) args)
+ in
+ if full_types then wrap_type (fo_term_for_combtyp (combtyp_of u)) t else t
+ end
+ in aux true end
+
+fun formula_for_combformula full_types =
+ let
+ fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
+ | aux (AConn (c, phis)) = AConn (c, map aux phis)
+ | aux (APred tm) = APred (fo_term_for_combterm full_types tm)
+ in aux end
+
+fun formula_for_axiom full_types (FOLFormula {combformula, ctypes_sorts, ...}) =
+ mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
+ (type_literals_for_types ctypes_sorts))
+ (formula_for_combformula full_types combformula)
+
+fun problem_line_for_axiom full_types
+ (formula as FOLFormula {formula_name, kind, ...}) =
+ Fof (axiom_prefix ^ ascii_of formula_name, kind,
+ formula_for_axiom full_types formula)
+
+fun problem_line_for_class_rel_clause
+ (ClassRelClause {axiom_name, subclass, superclass, ...}) =
+ let val ty_arg = ATerm (("T", "T"), []) in
+ Fof (ascii_of axiom_name, Axiom,
+ AConn (AImplies, [APred (ATerm (subclass, [ty_arg])),
+ APred (ATerm (superclass, [ty_arg]))]))
+ end
+
+fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =
+ (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
+ | fo_literal_for_arity_literal (TVarLit (c, sort)) =
+ (false, ATerm (c, [ATerm (sort, [])]))
+
+fun problem_line_for_arity_clause
+ (ArityClause {axiom_name, conclLit, premLits, ...}) =
+ Fof (arity_clause_prefix ^ ascii_of axiom_name, Axiom,
+ mk_ahorn (map (formula_for_fo_literal o apfst not
+ o fo_literal_for_arity_literal) premLits)
+ (formula_for_fo_literal
+ (fo_literal_for_arity_literal conclLit)))
+
+fun problem_line_for_conjecture full_types
+ (FOLFormula {formula_name, kind, combformula, ...}) =
+ Fof (conjecture_prefix ^ formula_name, kind,
+ formula_for_combformula full_types combformula)
+
+fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) =
+ map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)
+
+fun problem_line_for_free_type lit =
+ Fof (tfrees_name, Conjecture, mk_anot (formula_for_fo_literal lit))
+fun problem_lines_for_free_types conjectures =
+ let
+ val litss = map free_type_literals_for_conjecture conjectures
+ val lits = fold (union (op =)) litss []
+ in map problem_line_for_free_type lits end
+
+(** "hBOOL" and "hAPP" **)
+
+type const_info = {min_arity: int, max_arity: int, sub_level: bool}
+
+fun consider_term top_level (ATerm ((s, _), ts)) =
+ (if is_tptp_variable s then
+ I
+ else
+ let val n = length ts in
+ Symtab.map_default
+ (s, {min_arity = n, max_arity = 0, sub_level = false})
+ (fn {min_arity, max_arity, sub_level} =>
+ {min_arity = Int.min (n, min_arity),
+ max_arity = Int.max (n, max_arity),
+ sub_level = sub_level orelse not top_level})
+ end)
+ #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts
+fun consider_formula (AQuant (_, _, phi)) = consider_formula phi
+ | consider_formula (AConn (_, phis)) = fold consider_formula phis
+ | consider_formula (APred tm) = consider_term true tm
+
+fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi
+fun consider_problem problem = fold (fold consider_problem_line o snd) problem
+
+fun const_table_for_problem explicit_apply problem =
+ if explicit_apply then NONE
+ else SOME (Symtab.empty |> consider_problem problem)
+
+val tc_fun = make_fixed_type_const @{type_name fun}
+
+fun min_arity_of thy full_types NONE s =
+ (if s = "equal" orelse s = type_wrapper_name orelse
+ String.isPrefix type_const_prefix s orelse
+ String.isPrefix class_prefix s then
+ 16383 (* large number *)
+ else if full_types then
+ 0
+ else case strip_prefix_and_undo_ascii const_prefix s of
+ SOME s' => num_type_args thy (invert_const s')
+ | NONE => 0)
+ | min_arity_of _ _ (SOME the_const_tab) s =
+ case Symtab.lookup the_const_tab s of
+ SOME ({min_arity, ...} : const_info) => min_arity
+ | NONE => 0
+
+fun full_type_of (ATerm ((s, _), [ty, _])) =
+ if s = type_wrapper_name then ty else raise Fail "expected type wrapper"
+ | full_type_of _ = raise Fail "expected type wrapper"
+
+fun list_hAPP_rev _ t1 [] = t1
+ | list_hAPP_rev NONE t1 (t2 :: ts2) =
+ ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2])
+ | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) =
+ let val ty' = ATerm (`make_fixed_type_const @{type_name fun},
+ [full_type_of t2, ty]) in
+ ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2])
+ end
+
+fun repair_applications_in_term thy full_types const_tab =
+ let
+ fun aux opt_ty (ATerm (name as (s, _), ts)) =
+ if s = type_wrapper_name then
+ case ts of
+ [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2])
+ | _ => raise Fail "malformed type wrapper"
+ else
+ let
+ val ts = map (aux NONE) ts
+ val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts
+ in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end
+ in aux NONE end
+
+fun boolify t = ATerm (`I "hBOOL", [t])
+
+(* True if the constant ever appears outside of the top-level position in
+ literals, or if it appears with different arities (e.g., because of different
+ type instantiations). If false, the constant always receives all of its
+ arguments and is used as a predicate. *)
+fun is_predicate NONE s =
+ s = "equal" orelse String.isPrefix type_const_prefix s orelse
+ String.isPrefix class_prefix s
+ | is_predicate (SOME the_const_tab) s =
+ case Symtab.lookup the_const_tab s of
+ SOME {min_arity, max_arity, sub_level} =>
+ not sub_level andalso min_arity = max_arity
+ | NONE => false
+
+fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) =
+ if s = type_wrapper_name then
+ case ts of
+ [_, t' as ATerm ((s', _), _)] =>
+ if is_predicate const_tab s' then t' else boolify t
+ | _ => raise Fail "malformed type wrapper"
+ else
+ t |> not (is_predicate const_tab s) ? boolify
+
+fun close_universally phi =
+ let
+ fun term_vars bounds (ATerm (name as (s, _), tms)) =
+ (is_tptp_variable s andalso not (member (op =) bounds name))
+ ? insert (op =) name
+ #> fold (term_vars bounds) tms
+ fun formula_vars bounds (AQuant (q, xs, phi)) =
+ formula_vars (xs @ bounds) phi
+ | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
+ | formula_vars bounds (APred tm) = term_vars bounds tm
+ in
+ case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi)
+ end
+
+fun repair_formula thy explicit_forall full_types const_tab =
+ let
+ fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
+ | aux (AConn (c, phis)) = AConn (c, map aux phis)
+ | aux (APred tm) =
+ APred (tm |> repair_applications_in_term thy full_types const_tab
+ |> repair_predicates_in_term const_tab)
+ in aux #> explicit_forall ? close_universally end
+
+fun repair_problem_line thy explicit_forall full_types const_tab
+ (Fof (ident, kind, phi)) =
+ Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi)
+fun repair_problem_with_const_table thy =
+ map o apsnd o map ooo repair_problem_line thy
+
+fun repair_problem thy explicit_forall full_types explicit_apply problem =
+ repair_problem_with_const_table thy explicit_forall full_types
+ (const_table_for_problem explicit_apply problem) problem
+
+fun write_tptp_file thy readable_names explicit_forall full_types explicit_apply
+ file (conjectures, axiom_clauses, extra_clauses,
+ helper_clauses, class_rel_clauses, arity_clauses) =
+ let
+ val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses
+ val class_rel_lines =
+ map problem_line_for_class_rel_clause class_rel_clauses
+ val arity_lines = map problem_line_for_arity_clause arity_clauses
+ val helper_lines = map (problem_line_for_axiom full_types) helper_clauses
+ val conjecture_lines =
+ map (problem_line_for_conjecture full_types) conjectures
+ val tfree_lines = problem_lines_for_free_types conjectures
+ (* Reordering these might or might not confuse the proof reconstruction
+ code or the SPASS Flotter hack. *)
+ val problem =
+ [("Relevant facts", axiom_lines),
+ ("Class relationships", class_rel_lines),
+ ("Arity declarations", arity_lines),
+ ("Helper facts", helper_lines),
+ ("Conjectures", conjecture_lines),
+ ("Type variables", tfree_lines)]
+ |> repair_problem thy explicit_forall full_types explicit_apply
+ val (problem, pool) = nice_tptp_problem readable_names problem
+ val conjecture_offset =
+ length axiom_lines + length class_rel_lines + length arity_lines
+ + length helper_lines
+ val _ = File.write_list file (strings_for_tptp_problem problem)
+ in
+ (case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
+ conjecture_offset)
+ end
+
+fun extract_clause_sequence output =
+ let
+ val tokens_of = String.tokens (not o Char.isAlphaNum)
+ fun extract_num ("clause" :: (ss as _ :: _)) =
+ Int.fromString (List.last ss)
+ | extract_num _ = NONE
+ in output |> split_lines |> map_filter (extract_num o tokens_of) end
+
+val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation"
+
+val parse_clause_formula_pair =
+ $$ "(" |-- scan_integer --| $$ "," -- Symbol.scan_id --| $$ ")"
+ --| Scan.option ($$ ",")
+val parse_clause_formula_relation =
+ Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
+ |-- Scan.repeat parse_clause_formula_pair
+val extract_clause_formula_relation =
+ Substring.full
+ #> Substring.position set_ClauseFormulaRelationN
+ #> snd #> Substring.string #> strip_spaces #> explode
+ #> parse_clause_formula_relation #> fst
+
+fun repair_conjecture_shape_and_theorem_names output conjecture_shape
+ thm_names =
+ if String.isSubstring set_ClauseFormulaRelationN output then
+ (* This is a hack required for keeping track of axioms after they have been
+ clausified by SPASS's Flotter tool. The "SPASS_TPTP" script is also part
+ of this hack. *)
+ let
+ val j0 = hd conjecture_shape
+ val seq = extract_clause_sequence output
+ val name_map = extract_clause_formula_relation output
+ fun renumber_conjecture j =
+ AList.find (op =) name_map (conjecture_prefix ^ Int.toString (j - j0))
+ |> the_single
+ |> (fn s => find_index (curry (op =) s) seq + 1)
+ in
+ (conjecture_shape |> map renumber_conjecture,
+ seq |> map (the o AList.lookup (op =) name_map)
+ |> map (fn s => case try (unprefix axiom_prefix) s of
+ SOME s' => undo_ascii_of s'
+ | NONE => "")
+ |> Vector.fromList)
+ end
+ else
+ (conjecture_shape, thm_names)
+
+
+(* generic TPTP-based provers *)
+
+fun prover_fun name
+ {home_var, executable, arguments, proof_delims, known_failures,
+ max_new_relevant_facts_per_iter, prefers_theory_relevant,
+ explicit_forall}
+ ({debug, overlord, full_types, explicit_apply, relevance_threshold,
+ relevance_convergence, theory_relevant, defs_relevant, isar_proof,
+ isar_shrink_factor, ...} : params)
+ minimize_command timeout
+ ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
+ : problem) =
+ let
+ (* get clauses and prepare them for writing *)
+ val (ctxt, (_, th)) = goal;
+ val thy = ProofContext.theory_of ctxt
+ (* ### FIXME: (1) preprocessing for "if" etc. *)
+ val (params, hyp_ts, concl_t) = strip_subgoal th subgoal
+ val the_filtered_clauses =
+ case filtered_clauses of
+ SOME fcls => fcls
+ | NONE => relevant_facts full_types relevance_threshold
+ relevance_convergence defs_relevant
+ max_new_relevant_facts_per_iter
+ (the_default prefers_theory_relevant theory_relevant)
+ relevance_override goal hyp_ts concl_t
+ val the_axiom_clauses = axiom_clauses |> the_default the_filtered_clauses
+ val (internal_thm_names, clauses) =
+ prepare_clauses ctxt full_types hyp_ts concl_t the_axiom_clauses
+ the_filtered_clauses
+
+ (* path to unique problem file *)
+ val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
+ else Config.get ctxt dest_dir;
+ val the_problem_prefix = Config.get ctxt problem_prefix;
+ fun prob_pathname nr =
+ let
+ val probfile =
+ Path.basic ((if overlord then "prob_" ^ name
+ else the_problem_prefix ^ serial_string ())
+ ^ "_" ^ string_of_int nr)
+ in
+ if the_dest_dir = "" then File.tmp_path probfile
+ else if File.exists (Path.explode the_dest_dir)
+ then Path.append (Path.explode the_dest_dir) probfile
+ else error ("No such directory: " ^ the_dest_dir ^ ".")
+ end;
+
+ val home = getenv home_var
+ val command = Path.explode (home ^ "/" ^ executable)
+ (* write out problem file and call prover *)
+ fun command_line complete probfile =
+ let
+ val core = File.shell_path command ^ " " ^ arguments complete timeout ^
+ " " ^ File.shell_path probfile
+ in
+ (if Config.get ctxt measure_runtime then
+ "TIMEFORMAT='%3U'; { time " ^ core ^ " ; }"
+ else
+ "exec " ^ core) ^ " 2>&1"
+ end
+ fun split_time s =
+ let
+ val split = String.tokens (fn c => str c = "\n");
+ val (output, t) = s |> split |> split_last |> apfst cat_lines;
+ fun as_num f = f >> (fst o read_int);
+ val num = as_num (Scan.many1 Symbol.is_ascii_digit);
+ val digit = Scan.one Symbol.is_ascii_digit;
+ val num3 = as_num (digit ::: digit ::: (digit >> single));
+ val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b);
+ val as_time = the_default 0 o Scan.read Symbol.stopper time o explode;
+ in (output, as_time t) end;
+ fun run_on probfile =
+ if home = "" then
+ error ("The environment variable " ^ quote home_var ^ " is not set.")
+ else if File.exists command then
+ let
+ fun do_run complete =
+ let
+ val command = command_line complete probfile
+ val ((output, msecs), res_code) =
+ bash_output command
+ |>> (if overlord then
+ prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
+ else
+ I)
+ |>> (if Config.get ctxt measure_runtime then split_time
+ else rpair 0)
+ val (proof, outcome) =
+ extract_proof_and_outcome complete res_code proof_delims
+ known_failures output
+ in (output, msecs, proof, outcome) end
+ val readable_names = debug andalso overlord
+ val (pool, conjecture_offset) =
+ write_tptp_file thy readable_names explicit_forall full_types
+ explicit_apply probfile clauses
+ val conjecture_shape =
+ conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
+ val result =
+ do_run false
+ |> (fn (_, msecs0, _, SOME _) =>
+ do_run true
+ |> (fn (output, msecs, proof, outcome) =>
+ (output, msecs0 + msecs, proof, outcome))
+ | result => result)
+ in ((pool, conjecture_shape), result) end
+ else
+ error ("Bad executable: " ^ Path.implode command ^ ".");
+
+ (* If the problem file has not been exported, remove it; otherwise, export
+ the proof file too. *)
+ fun cleanup probfile =
+ if the_dest_dir = "" then try File.rm probfile else NONE
+ fun export probfile (_, (output, _, _, _)) =
+ if the_dest_dir = "" then
+ ()
+ else
+ File.write (Path.explode (Path.implode probfile ^ "_proof")) output
+
+ val ((pool, conjecture_shape), (output, msecs, proof, outcome)) =
+ with_path cleanup export run_on (prob_pathname subgoal)
+ val (conjecture_shape, internal_thm_names) =
+ repair_conjecture_shape_and_theorem_names output conjecture_shape
+ internal_thm_names
+
+ val (message, used_thm_names) =
+ case outcome of
+ NONE =>
+ proof_text isar_proof
+ (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
+ (full_types, minimize_command, proof, internal_thm_names, th,
+ subgoal)
+ | SOME failure => (string_for_failure failure ^ "\n", [])
+ in
+ {outcome = outcome, message = message, pool = pool,
+ used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs,
+ output = output, proof = proof, internal_thm_names = internal_thm_names,
+ conjecture_shape = conjecture_shape,
+ filtered_clauses = the_filtered_clauses}
+ end
+
+fun get_prover_fun thy name = prover_fun name (get_prover thy name)
+
+(* start prover thread *)
+fun start_prover_thread (params as {verbose, full_types, timeout, ...}) i n
+ relevance_override minimize_command proof_state name =
+ let
+ val thy = Proof.theory_of proof_state
+ val birth_time = Time.now ()
+ val death_time = Time.+ (birth_time, timeout)
+ val prover = get_prover_fun thy name
+ val {context = ctxt, facts, goal} = Proof.goal proof_state;
+ val desc =
+ "ATP " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
+ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));
+ in
+ Async_Manager.launch das_Tool verbose birth_time death_time desc
+ (fn () =>
+ let
+ val problem =
+ {subgoal = i, goal = (ctxt, (facts, goal)),
+ relevance_override = relevance_override, axiom_clauses = NONE,
+ filtered_clauses = NONE}
+ in
+ prover params (minimize_command name) timeout problem |> #message
+ handle ERROR message => "Error: " ^ message ^ "\n"
+ end)
+ end
+
+val setup =
+ dest_dir_setup
+ #> problem_prefix_setup
+ #> measure_runtime_setup
+
+end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Jul 27 17:10:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Jul 27 20:16:14 2010 +0200
@@ -1,5 +1,5 @@
(* Title: HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
- Author: Jia Meng, Cambridge University Computer Laboratory, NICTA
+ Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
Author: Jasmin Blanchette, TU Muenchen
*)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Tue Jul 27 17:10:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Tue Jul 27 20:16:14 2010 +0200
@@ -7,8 +7,8 @@
signature SLEDGEHAMMER_FACT_MINIMIZER =
sig
- type params = ATP_Manager.params
- type prover_result = ATP_Manager.prover_result
+ type params = Sledgehammer.params
+ type prover_result = Sledgehammer.prover_result
val minimize_theorems :
params -> int -> int -> Proof.state -> (string * thm list) list
@@ -21,19 +21,7 @@
open Metis_Clauses
open Sledgehammer_Util
open Sledgehammer_Proof_Reconstruct
-open ATP_Manager
-
-(* Linear minimization algorithm *)
-
-fun linear_minimize test s =
- let
- fun aux [] p = p
- | aux (x :: xs) (needed, result) =
- case test (xs @ needed) of
- SOME result => aux xs (needed, result)
- | NONE => aux xs (x :: needed, result)
- in aux s end
-
+open Sledgehammer
(* wrapper for calling external prover *)
@@ -52,8 +40,15 @@
let
val thy = Proof.theory_of state
val num_theorems = length name_thms_pairs
- val _ = priority ("Testing " ^ string_of_int num_theorems ^
- " theorem" ^ plural_s num_theorems ^ "...")
+ val _ =
+ priority ("Testing " ^ string_of_int num_theorems ^
+ " theorem" ^ plural_s num_theorems ^
+ (if num_theorems > 0 then
+ ": " ^ space_implode " "
+ (name_thms_pairs
+ |> map fst |> sort_distinct string_ord)
+ else
+ "") ^ "...")
val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
val {context = ctxt, facts, goal} = Proof.goal state
val problem =
@@ -69,62 +64,62 @@
(* minimalization of thms *)
+fun filter_used_facts used = filter (member (op =) used o fst)
+
+fun sublinear_minimize _ [] p = p
+ | sublinear_minimize test (x :: xs) (seen, result) =
+ case test (xs @ seen) of
+ result as {outcome = NONE, proof, used_thm_names, ...}
+ : prover_result =>
+ sublinear_minimize test (filter_used_facts used_thm_names xs)
+ (filter_used_facts used_thm_names seen, result)
+ | _ => sublinear_minimize test xs (x :: seen, result)
+
fun minimize_theorems (params as {debug, atps, full_types, minimize_timeout,
isar_proof, isar_shrink_factor, ...})
i n state name_thms_pairs =
let
val thy = Proof.theory_of state
val prover = case atps of
- [atp_name] => get_prover thy atp_name
+ [atp_name] => get_prover_fun thy atp_name
| _ => error "Expected a single ATP."
val msecs = Time.toMilliseconds minimize_timeout
val _ =
priority ("Sledgehammer minimizer: ATP " ^ quote (the_single atps) ^
" with a time limit of " ^ string_of_int msecs ^ " ms.")
- val test_thms_fun =
+ val test_facts =
sledgehammer_test_theorems params prover minimize_timeout i state
- fun test_thms filtered thms =
- case test_thms_fun filtered thms of
- (result as {outcome = NONE, ...}) => SOME result
- | _ => NONE
-
val {context = ctxt, goal, ...} = Proof.goal state;
in
(* try prove first to check result and get used theorems *)
- (case test_thms_fun NONE name_thms_pairs of
- result as {outcome = NONE, pool, internal_thm_names, conjecture_shape,
- filtered_clauses, ...} =>
- let
- val used = internal_thm_names |> Vector.foldr (op ::) []
- |> sort_distinct string_ord
- val to_use =
- if length used < length name_thms_pairs then
- filter (fn (name1, _) => exists (curry (op =) name1) used)
- name_thms_pairs
- else name_thms_pairs
- val (min_thms, {proof, internal_thm_names, ...}) =
- linear_minimize (test_thms (SOME filtered_clauses)) to_use
- ([], result)
- val m = length min_thms
- val _ = priority (cat_lines
- ["Minimized: " ^ string_of_int m ^ " theorem" ^ plural_s m] ^ ".")
- in
- (SOME min_thms,
- proof_text isar_proof
- (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
- (full_types, K "", proof, internal_thm_names, goal, i) |> fst)
- end
- | {outcome = SOME TimedOut, ...} =>
- (NONE, "Timeout: You can increase the time limit using the \"timeout\" \
- \option (e.g., \"timeout = " ^
- string_of_int (10 + msecs div 1000) ^ " s\").")
- | {outcome = SOME UnknownError, ...} =>
- (* Failure sometimes mean timeout, unfortunately. *)
- (NONE, "Failure: No proof was found with the current time limit. You \
- \can increase the time limit using the \"timeout\" \
- \option (e.g., \"timeout = " ^
- string_of_int (10 + msecs div 1000) ^ " s\").")
- | {message, ...} => (NONE, "ATP error: " ^ message))
+ (case test_facts NONE name_thms_pairs of
+ result as {outcome = NONE, pool, proof, used_thm_names,
+ conjecture_shape, filtered_clauses, ...} =>
+ let
+ val (min_thms, {proof, internal_thm_names, ...}) =
+ sublinear_minimize (test_facts (SOME filtered_clauses))
+ (filter_used_facts used_thm_names name_thms_pairs)
+ ([], result)
+ val m = length min_thms
+ val _ = priority (cat_lines
+ ["Minimized: " ^ string_of_int m ^ " theorem" ^ plural_s m] ^ ".")
+ in
+ (SOME min_thms,
+ proof_text isar_proof
+ (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
+ (full_types, K "", proof, internal_thm_names, goal, i) |> fst)
+ end
+ | {outcome = SOME TimedOut, ...} =>
+ (NONE, "Timeout: You can increase the time limit using the \"timeout\" \
+ \option (e.g., \"timeout = " ^
+ string_of_int (10 + msecs div 1000) ^ " s\").")
+ | {outcome = SOME UnknownError, ...} =>
+ (* Failure sometimes mean timeout, unfortunately. *)
+ (NONE, "Failure: No proof was found with the current time limit. You \
+ \can increase the time limit using the \"timeout\" \
+ \option (e.g., \"timeout = " ^
+ string_of_int (10 + msecs div 1000) ^ " s\").")
+ | {message, ...} => (NONE, "ATP error: " ^ message))
handle ERROR msg => (NONE, "Error: " ^ msg)
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Jul 27 17:10:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Jul 27 20:16:14 2010 +0200
@@ -6,7 +6,7 @@
signature SLEDGEHAMMER_ISAR =
sig
- type params = ATP_Manager.params
+ type params = Sledgehammer.params
val atps: string Unsynchronized.ref
val timeout: int Unsynchronized.ref
@@ -17,10 +17,10 @@
structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
struct
+open ATP_Systems
open Sledgehammer_Util
open Sledgehammer_Fact_Filter
-open ATP_Manager
-open ATP_Systems
+open Sledgehammer
open Sledgehammer_Fact_Minimizer
(** Sledgehammer commands **)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Jul 27 17:10:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Jul 27 20:16:14 2010 +0200
@@ -1,5 +1,6 @@
(* Title: HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
- Author: Lawrence C Paulson and Claire Quigley, Cambridge University Computer Laboratory
+ Author: Lawrence C. Paulson, Cambridge University Computer Laboratory
+ Author: Claire Quigley, Cambridge University Computer Laboratory
Author: Jasmin Blanchette, TU Muenchen
Transfer of proofs from external provers.
@@ -26,14 +27,34 @@
structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
struct
+open ATP_Problem
open Metis_Clauses
open Sledgehammer_Util
open Sledgehammer_Fact_Filter
-open Sledgehammer_TPTP_Format
type minimize_command = string list -> string
-fun mk_anot phi = AConn (ANot, [phi])
+(* Simple simplifications to ensure that sort annotations don't leave a trail of
+ spurious "True"s. *)
+fun s_not @{const False} = @{const True}
+ | s_not @{const True} = @{const False}
+ | s_not (@{const Not} $ t) = t
+ | s_not t = @{const Not} $ t
+fun s_conj (@{const True}, t2) = t2
+ | s_conj (t1, @{const True}) = t1
+ | s_conj p = HOLogic.mk_conj p
+fun s_disj (@{const False}, t2) = t2
+ | s_disj (t1, @{const False}) = t1
+ | s_disj p = HOLogic.mk_disj p
+fun s_imp (@{const True}, t2) = t2
+ | s_imp (t1, @{const False}) = s_not t1
+ | s_imp p = HOLogic.mk_imp p
+fun s_iff (@{const True}, t2) = t2
+ | s_iff (t1, @{const True}) = t1
+ | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
+
+fun mk_anot (AConn (ANot, [phi])) = phi
+ | mk_anot phi = AConn (ANot, [phi])
fun mk_aconn c (phi1, phi2) = AConn (c, [phi1, phi2])
val index_in_shape : int -> int list -> int = find_index o curry (op =)
@@ -220,6 +241,20 @@
Type_Infer.param 0 (a, HOLogic.typeS)
end
+(* Type class literal applied to a type. Returns triple of polarity, class,
+ type. *)
+fun type_constraint_from_term pos tfrees (u as ATerm (a, us)) =
+ case (strip_prefix_and_undo_ascii class_prefix a,
+ map (type_from_fo_term tfrees) us) of
+ (SOME b, [T]) => (pos, b, T)
+ | _ => raise FO_TERM [u]
+
+(** Accumulate type constraints in a clause: negative type literals **)
+fun add_var (key, z) = Vartab.map_default (key, []) (cons z)
+fun add_type_constraint (false, cl, TFree (a ,_)) = add_var ((a, ~1), cl)
+ | add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl)
+ | add_type_constraint _ = I
+
fun fix_atp_variable_name s =
let
fun subscript_name s n = s ^ nat_subscript n
@@ -238,8 +273,8 @@
end
(* First-order translation. No types are known for variables. "HOLogic.typeT"
- should allow them to be inferred.*)
-fun term_from_fo_term thy full_types tfrees opt_T =
+ should allow them to be inferred. *)
+fun raw_term_from_pred thy full_types tfrees =
let
fun aux opt_T extra_us u =
case u of
@@ -289,32 +324,19 @@
case strip_prefix_and_undo_ascii schematic_var_prefix a of
SOME b => Var ((b, 0), T)
| NONE =>
- (* Variable from the ATP, say "X1" *)
- Var ((fix_atp_variable_name a, 0), T)
+ if is_tptp_variable a then
+ Var ((fix_atp_variable_name a, 0), T)
+ else
+ raise Fail ("Unexpected constant: " ^ quote a)
in list_comb (t, ts) end
- in aux opt_T [] end
+ in aux (SOME HOLogic.boolT) [] end
-(* Type class literal applied to a type. Returns triple of polarity, class,
- type. *)
-fun type_constraint_from_formula pos tfrees (AConn (ANot, [u])) =
- type_constraint_from_formula (not pos) tfrees u
- | type_constraint_from_formula pos tfrees (phi as APred (ATerm (a, us))) =
- (case (strip_prefix_and_undo_ascii class_prefix a,
- map (type_from_fo_term tfrees) us) of
- (SOME b, [T]) => (pos, b, T)
- | _ => raise FORMULA [phi])
- | type_constraint_from_formula _ _ phi = raise FORMULA [phi]
-
-(** Accumulate type constraints in a clause: negative type literals **)
-
-fun add_var (key, z) = Vartab.map_default (key, []) (cons z)
-
-fun add_type_constraint (false, cl, TFree (a ,_)) = add_var ((a, ~1), cl)
- | add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl)
- | add_type_constraint _ = I
-
-fun is_positive_literal (@{const Not} $ _) = false
- | is_positive_literal _ = true
+fun term_from_pred thy full_types tfrees pos (u as ATerm (s, _)) =
+ if String.isPrefix class_prefix s then
+ add_type_constraint (type_constraint_from_term pos tfrees u)
+ #> pair @{const True}
+ else
+ pair (raw_term_from_pred thy full_types tfrees u)
val combinator_table =
[(@{const_name COMBI}, @{thm COMBI_def_raw}),
@@ -331,12 +353,9 @@
| NONE => t)
| uncombine_term t = t
-fun disjuncts (AConn (AOr, phis)) = maps disjuncts phis
- | disjuncts phi = [phi]
-
(* Update schematic type variables with detected sort constraints. It's not
totally clear when this code is necessary. *)
-fun repair_tvar_sorts (tvar_tab, t) =
+fun repair_tvar_sorts (t, tvar_tab) =
let
fun do_type (Type (a, Ts)) = Type (a, map do_type Ts)
| do_type (TVar (xi, s)) =
@@ -350,58 +369,39 @@
| do_term (t1 $ t2) = do_term t1 $ do_term t2
in t |> not (Vartab.is_empty tvar_tab) ? do_term end
-fun s_disj (t1, @{const False}) = t1
- | s_disj p = HOLogic.mk_disj p
-
fun quantify_over_free quant_s free_s body_t =
case Term.add_frees body_t [] |> filter (curry (op =) free_s o fst) of
[] => body_t
| frees as (_, free_T) :: _ =>
Abs (free_s, free_T, fold (curry abstract_over) (map Free frees) body_t)
- (* Interpret a list of syntax trees as a clause, given by "real" literals and
- sort constraints. Accumulates sort constraints in "tvar_tab", with "real"
- literals in "lits". *)
-fun prop_from_formula thy full_types tfrees =
- let
- val do_sort_constraint =
- add_type_constraint o type_constraint_from_formula true tfrees
- fun do_real_literal phi =
+(* Interpret a list of syntax trees as a clause, extracting sort constraints
+ as they appear in the formula. *)
+fun prop_from_formula thy full_types tfrees phi =
+ let
+ fun do_formula pos phi =
case phi of
- AQuant (_, [], phi) => do_real_literal phi
+ AQuant (_, [], phi) => do_formula pos phi
| AQuant (q, x :: xs, phi') =>
- let
- val body = do_real_literal (AQuant (q, xs, phi'))
- val quant_s = case q of
- AForall => @{const_name All}
- | AExists => @{const_name Ex}
- in quantify_over_free quant_s x body end
- | AConn (ANot, [phi']) => HOLogic.mk_not (do_real_literal phi')
+ do_formula pos (AQuant (q, xs, phi'))
+ #>> quantify_over_free (case q of
+ AForall => @{const_name All}
+ | AExists => @{const_name Ex}) x
+ | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
| AConn (c, [phi1, phi2]) =>
- (phi1, phi2)
- |> pairself do_real_literal
- |> (case c of
- AAnd => HOLogic.mk_conj
- | AOr => HOLogic.mk_disj
- | AImplies => HOLogic.mk_imp
- | AIff => (fn (t1, t2) => HOLogic.eq_const HOLogic.boolT $ t1 $ t2))
- | APred tm =>
- term_from_fo_term thy full_types tfrees (SOME @{typ bool}) tm
+ do_formula (pos |> c = AImplies ? not) phi1
+ ##>> do_formula pos phi2
+ #>> (case c of
+ AAnd => s_conj
+ | AOr => s_disj
+ | AImplies => s_imp
+ | AIff => s_iff)
+ | APred tm => term_from_pred thy full_types tfrees pos tm
| _ => raise FORMULA [phi]
- fun do_literals (tvar_tab, t) [] = (tvar_tab, t)
- | do_literals (tvar_tab, t) (u :: us) =
- (do_literals (tvar_tab |> do_sort_constraint u, t) us
- handle FO_TERM _ => raise SAME ()
- | FORMULA _ => raise SAME ())
- handle SAME () =>
- do_literals (tvar_tab, s_disj (do_real_literal u, t)) us
- in
- repair_tvar_sorts o do_literals (Vartab.empty, HOLogic.false_const)
- o disjuncts
- end
+ in repair_tvar_sorts (do_formula true phi Vartab.empty) end
fun check_formula ctxt =
- Type_Infer.constrain @{typ bool}
+ Type_Infer.constrain HOLogic.boolT
#> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
@@ -565,17 +565,18 @@
val unprefix_chained = perhaps (try (unprefix chained_prefix))
+fun used_facts thm_names =
+ extract_formula_numbers_in_atp_proof
+ #> filter (is_axiom_clause_number thm_names)
+ #> map (fn i => Vector.sub (thm_names, i - 1))
+ #> List.partition (String.isPrefix chained_prefix)
+ #>> map (unprefix chained_prefix)
+ #> pairself (sort_distinct string_ord)
+
fun metis_proof_text (full_types, minimize_command, atp_proof, thm_names, goal,
i) =
let
- val raw_lemmas =
- atp_proof |> extract_formula_numbers_in_atp_proof
- |> filter (is_axiom_clause_number thm_names)
- |> map (fn i => Vector.sub (thm_names, i - 1))
- val (chained_lemmas, other_lemmas) =
- raw_lemmas |> List.partition (String.isPrefix chained_prefix)
- |>> map (unprefix chained_prefix)
- |> pairself (sort_distinct string_ord)
+ val (chained_lemmas, other_lemmas) = used_facts thm_names atp_proof
val lemmas = other_lemmas @ chained_lemmas
val n = Logic.count_prems (prop_of goal)
in
@@ -937,8 +938,6 @@
(other_params as (full_types, _, atp_proof, thm_names, goal,
i)) =
let
- (* ### FIXME: avoid duplication with ATP_Systems -- and move strip_subgoal
- to ATP_Systems *)
val (params, hyp_ts, concl_t) = strip_subgoal goal i
val frees = fold Term.add_frees (concl_t :: hyp_ts) []
val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Tue Jul 27 17:10:27 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,429 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML
- Author: Jia Meng, NICTA
- Author: Jasmin Blanchette, TU Muenchen
-
-TPTP syntax.
-*)
-
-signature SLEDGEHAMMER_TPTP_FORMAT =
-sig
- type name = Metis_Clauses.name
- type kind = Metis_Clauses.kind
- type combterm = Metis_Clauses.combterm
- type class_rel_clause = Metis_Clauses.class_rel_clause
- type arity_clause = Metis_Clauses.arity_clause
-
- datatype 'a fo_term = ATerm of 'a * 'a fo_term list
- datatype quantifier = AForall | AExists
- datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
- datatype ('a, 'b) formula =
- AQuant of quantifier * 'a list * ('a, 'b) formula |
- AConn of connective * ('a, 'b) formula list |
- APred of 'b
-
- datatype fol_formula =
- FOLFormula of {formula_name: string,
- kind: kind,
- combformula: (name, combterm) formula,
- ctypes_sorts: typ list}
-
- val axiom_prefix : string
- val conjecture_prefix : string
- val write_tptp_file :
- theory -> bool -> bool -> bool -> bool -> Path.T
- -> fol_formula list * fol_formula list * fol_formula list * fol_formula list
- * class_rel_clause list * arity_clause list
- -> string Symtab.table * int
-end;
-
-structure Sledgehammer_TPTP_Format : SLEDGEHAMMER_TPTP_FORMAT =
-struct
-
-open Metis_Clauses
-open Sledgehammer_Util
-
-
-(** ATP problem **)
-
-datatype 'a fo_term = ATerm of 'a * 'a fo_term list
-datatype quantifier = AForall | AExists
-datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
-datatype ('a, 'b) formula =
- AQuant of quantifier * 'a list * ('a, 'b) formula |
- AConn of connective * ('a, 'b) formula list |
- APred of 'b
-
-fun mk_anot phi = AConn (ANot, [phi])
-fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
-fun mk_ahorn [] phi = phi
- | mk_ahorn (phi :: phis) psi =
- AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi])
-
-datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula
-type 'a problem = (string * 'a problem_line list) list
-
-fun string_for_term (ATerm (s, [])) = s
- | string_for_term (ATerm (s, ts)) =
- if s = "equal" then space_implode " = " (map string_for_term ts)
- else s ^ "(" ^ commas (map string_for_term ts) ^ ")"
-fun string_for_quantifier AForall = "!"
- | string_for_quantifier AExists = "?"
-fun string_for_connective ANot = "~"
- | string_for_connective AAnd = "&"
- | string_for_connective AOr = "|"
- | string_for_connective AImplies = "=>"
- | string_for_connective AIf = "<="
- | string_for_connective AIff = "<=>"
- | string_for_connective ANotIff = "<~>"
-fun string_for_formula (AQuant (q, xs, phi)) =
- string_for_quantifier q ^ "[" ^ commas xs ^ "]: " ^
- string_for_formula phi
- | string_for_formula (AConn (ANot, [APred (ATerm ("equal", ts))])) =
- space_implode " != " (map string_for_term ts)
- | string_for_formula (AConn (c, [phi])) =
- string_for_connective c ^ " " ^ string_for_formula phi
- | string_for_formula (AConn (c, phis)) =
- "(" ^ space_implode (" " ^ string_for_connective c ^ " ")
- (map string_for_formula phis) ^ ")"
- | string_for_formula (APred tm) = string_for_term tm
-
-fun string_for_problem_line (Fof (ident, kind, phi)) =
- "fof(" ^ ident ^ ", " ^
- (case kind of Axiom => "axiom" | Conjecture => "conjecture") ^ ",\n" ^
- " (" ^ string_for_formula phi ^ ")).\n"
-fun strings_for_problem problem =
- "% This file was generated by Isabelle (most likely Sledgehammer)\n\
- \% " ^ timestamp () ^ "\n" ::
- maps (fn (_, []) => []
- | (heading, lines) =>
- "\n% " ^ heading ^ " (" ^ Int.toString (length lines) ^ ")\n" ::
- map string_for_problem_line lines) problem
-
-
-(** Nice names **)
-
-fun empty_name_pool readable_names =
- if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE
-
-fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs
-fun pool_map f xs =
- pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs []
-
-(* "equal" is reserved by some ATPs. "op" is also reserved, to avoid the
- unreadable "op_1", "op_2", etc., in the problem files. *)
-val reserved_nice_names = ["equal", "op"]
-fun readable_name full_name s =
- if s = full_name then
- s
- else
- let
- val s = s |> Long_Name.base_name
- |> Name.desymbolize (Char.isUpper (String.sub (full_name, 0)))
- in if member (op =) reserved_nice_names s then full_name else s end
-
-fun nice_name (full_name, _) NONE = (full_name, NONE)
- | nice_name (full_name, desired_name) (SOME the_pool) =
- case Symtab.lookup (fst the_pool) full_name of
- SOME nice_name => (nice_name, SOME the_pool)
- | NONE =>
- let
- val nice_prefix = readable_name full_name desired_name
- fun add j =
- let
- val nice_name = nice_prefix ^
- (if j = 0 then "" else "_" ^ Int.toString j)
- in
- case Symtab.lookup (snd the_pool) nice_name of
- SOME full_name' =>
- if full_name = full_name' then (nice_name, the_pool)
- else add (j + 1)
- | NONE =>
- (nice_name,
- (Symtab.update_new (full_name, nice_name) (fst the_pool),
- Symtab.update_new (nice_name, full_name) (snd the_pool)))
- end
- in add 0 |> apsnd SOME end
-
-
-fun nice_term (ATerm (name, ts)) =
- nice_name name ##>> pool_map nice_term ts #>> ATerm
-fun nice_formula (AQuant (q, xs, phi)) =
- pool_map nice_name xs ##>> nice_formula phi
- #>> (fn (xs, phi) => AQuant (q, xs, phi))
- | nice_formula (AConn (c, phis)) =
- pool_map nice_formula phis #>> curry AConn c
- | nice_formula (APred tm) = nice_term tm #>> APred
-fun nice_problem_line (Fof (ident, kind, phi)) =
- nice_formula phi #>> (fn phi => Fof (ident, kind, phi))
-fun nice_problem problem =
- pool_map (fn (heading, lines) =>
- pool_map nice_problem_line lines #>> pair heading) problem
-
-
-(** Sledgehammer stuff **)
-
-datatype fol_formula =
- FOLFormula of {formula_name: string,
- kind: kind,
- combformula: (name, combterm) formula,
- ctypes_sorts: typ list}
-
-val axiom_prefix = "ax_"
-val conjecture_prefix = "conj_"
-val arity_clause_prefix = "clsarity_"
-val tfrees_name = "tfrees"
-
-fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
-
-fun fo_term_for_combtyp (CombTVar name) = ATerm (name, [])
- | fo_term_for_combtyp (CombTFree name) = ATerm (name, [])
- | fo_term_for_combtyp (CombType (name, tys)) =
- ATerm (name, map fo_term_for_combtyp tys)
-
-fun fo_literal_for_type_literal (TyLitVar (class, name)) =
- (true, ATerm (class, [ATerm (name, [])]))
- | fo_literal_for_type_literal (TyLitFree (class, name)) =
- (true, ATerm (class, [ATerm (name, [])]))
-
-fun formula_for_fo_literal (pos, t) = APred t |> not pos ? mk_anot
-
-fun fo_term_for_combterm full_types =
- let
- fun aux top_level u =
- let
- val (head, args) = strip_combterm_comb u
- val (x, ty_args) =
- case head of
- CombConst (name, _, ty_args) =>
- if fst name = "equal" then
- (if top_level andalso length args = 2 then name
- else ("c_fequal", @{const_name fequal}), [])
- else
- (name, if full_types then [] else ty_args)
- | CombVar (name, _) => (name, [])
- | CombApp _ => raise Fail "impossible \"CombApp\""
- val t = ATerm (x, map fo_term_for_combtyp ty_args @
- map (aux false) args)
- in
- if full_types then wrap_type (fo_term_for_combtyp (combtyp_of u)) t else t
- end
- in aux true end
-
-fun formula_for_combformula full_types =
- let
- fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
- | aux (AConn (c, phis)) = AConn (c, map aux phis)
- | aux (APred tm) = APred (fo_term_for_combterm full_types tm)
- in aux end
-
-fun formula_for_axiom full_types (FOLFormula {combformula, ctypes_sorts, ...}) =
- mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
- (type_literals_for_types ctypes_sorts))
- (formula_for_combformula full_types combformula)
-
-fun problem_line_for_axiom full_types
- (formula as FOLFormula {formula_name, kind, ...}) =
- Fof (axiom_prefix ^ ascii_of formula_name, kind,
- formula_for_axiom full_types formula)
-
-fun problem_line_for_class_rel_clause
- (ClassRelClause {axiom_name, subclass, superclass, ...}) =
- let val ty_arg = ATerm (("T", "T"), []) in
- Fof (ascii_of axiom_name, Axiom,
- AConn (AImplies, [APred (ATerm (subclass, [ty_arg])),
- APred (ATerm (superclass, [ty_arg]))]))
- end
-
-fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =
- (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
- | fo_literal_for_arity_literal (TVarLit (c, sort)) =
- (false, ATerm (c, [ATerm (sort, [])]))
-
-fun problem_line_for_arity_clause
- (ArityClause {axiom_name, conclLit, premLits, ...}) =
- Fof (arity_clause_prefix ^ ascii_of axiom_name, Axiom,
- mk_ahorn (map (formula_for_fo_literal o apfst not
- o fo_literal_for_arity_literal) premLits)
- (formula_for_fo_literal
- (fo_literal_for_arity_literal conclLit)))
-
-fun problem_line_for_conjecture full_types
- (FOLFormula {formula_name, kind, combformula, ...}) =
- Fof (conjecture_prefix ^ formula_name, kind,
- formula_for_combformula full_types combformula)
-
-fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) =
- map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)
-
-fun problem_line_for_free_type lit =
- Fof (tfrees_name, Conjecture, mk_anot (formula_for_fo_literal lit))
-fun problem_lines_for_free_types conjectures =
- let
- val litss = map free_type_literals_for_conjecture conjectures
- val lits = fold (union (op =)) litss []
- in map problem_line_for_free_type lits end
-
-(** "hBOOL" and "hAPP" **)
-
-type const_info = {min_arity: int, max_arity: int, sub_level: bool}
-
-fun is_variable s = Char.isUpper (String.sub (s, 0))
-
-fun consider_term top_level (ATerm ((s, _), ts)) =
- (if is_variable s then
- I
- else
- let val n = length ts in
- Symtab.map_default
- (s, {min_arity = n, max_arity = 0, sub_level = false})
- (fn {min_arity, max_arity, sub_level} =>
- {min_arity = Int.min (n, min_arity),
- max_arity = Int.max (n, max_arity),
- sub_level = sub_level orelse not top_level})
- end)
- #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts
-fun consider_formula (AQuant (_, _, phi)) = consider_formula phi
- | consider_formula (AConn (_, phis)) = fold consider_formula phis
- | consider_formula (APred tm) = consider_term true tm
-
-fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi
-fun consider_problem problem = fold (fold consider_problem_line o snd) problem
-
-fun const_table_for_problem explicit_apply problem =
- if explicit_apply then NONE
- else SOME (Symtab.empty |> consider_problem problem)
-
-val tc_fun = make_fixed_type_const @{type_name fun}
-
-fun min_arity_of thy full_types NONE s =
- (if s = "equal" orelse s = type_wrapper_name orelse
- String.isPrefix type_const_prefix s orelse
- String.isPrefix class_prefix s then
- 16383 (* large number *)
- else if full_types then
- 0
- else case strip_prefix_and_undo_ascii const_prefix s of
- SOME s' => num_type_args thy (invert_const s')
- | NONE => 0)
- | min_arity_of _ _ (SOME the_const_tab) s =
- case Symtab.lookup the_const_tab s of
- SOME ({min_arity, ...} : const_info) => min_arity
- | NONE => 0
-
-fun full_type_of (ATerm ((s, _), [ty, _])) =
- if s = type_wrapper_name then ty else raise Fail "expected type wrapper"
- | full_type_of _ = raise Fail "expected type wrapper"
-
-fun list_hAPP_rev _ t1 [] = t1
- | list_hAPP_rev NONE t1 (t2 :: ts2) =
- ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2])
- | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) =
- let val ty' = ATerm (`make_fixed_type_const @{type_name fun},
- [full_type_of t2, ty]) in
- ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2])
- end
-
-fun repair_applications_in_term thy full_types const_tab =
- let
- fun aux opt_ty (ATerm (name as (s, _), ts)) =
- if s = type_wrapper_name then
- case ts of
- [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2])
- | _ => raise Fail "malformed type wrapper"
- else
- let
- val ts = map (aux NONE) ts
- val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts
- in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end
- in aux NONE end
-
-fun boolify t = ATerm (`I "hBOOL", [t])
-
-(* True if the constant ever appears outside of the top-level position in
- literals, or if it appears with different arities (e.g., because of different
- type instantiations). If false, the constant always receives all of its
- arguments and is used as a predicate. *)
-fun is_predicate NONE s =
- s = "equal" orelse String.isPrefix type_const_prefix s orelse
- String.isPrefix class_prefix s
- | is_predicate (SOME the_const_tab) s =
- case Symtab.lookup the_const_tab s of
- SOME {min_arity, max_arity, sub_level} =>
- not sub_level andalso min_arity = max_arity
- | NONE => false
-
-fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) =
- if s = type_wrapper_name then
- case ts of
- [_, t' as ATerm ((s', _), _)] =>
- if is_predicate const_tab s' then t' else boolify t
- | _ => raise Fail "malformed type wrapper"
- else
- t |> not (is_predicate const_tab s) ? boolify
-
-fun close_universally phi =
- let
- fun term_vars bounds (ATerm (name as (s, _), tms)) =
- (is_variable s andalso not (member (op =) bounds name))
- ? insert (op =) name
- #> fold (term_vars bounds) tms
- fun formula_vars bounds (AQuant (q, xs, phi)) =
- formula_vars (xs @ bounds) phi
- | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
- | formula_vars bounds (APred tm) = term_vars bounds tm
- in
- case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi)
- end
-
-fun repair_formula thy explicit_forall full_types const_tab =
- let
- fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
- | aux (AConn (c, phis)) = AConn (c, map aux phis)
- | aux (APred tm) =
- APred (tm |> repair_applications_in_term thy full_types const_tab
- |> repair_predicates_in_term const_tab)
- in aux #> explicit_forall ? close_universally end
-
-fun repair_problem_line thy explicit_forall full_types const_tab
- (Fof (ident, kind, phi)) =
- Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi)
-fun repair_problem_with_const_table thy =
- map o apsnd o map ooo repair_problem_line thy
-
-fun repair_problem thy explicit_forall full_types explicit_apply problem =
- repair_problem_with_const_table thy explicit_forall full_types
- (const_table_for_problem explicit_apply problem) problem
-
-fun write_tptp_file thy readable_names explicit_forall full_types explicit_apply
- file (conjectures, axiom_clauses, extra_clauses,
- helper_clauses, class_rel_clauses, arity_clauses) =
- let
- val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses
- val class_rel_lines =
- map problem_line_for_class_rel_clause class_rel_clauses
- val arity_lines = map problem_line_for_arity_clause arity_clauses
- val helper_lines = map (problem_line_for_axiom full_types) helper_clauses
- val conjecture_lines =
- map (problem_line_for_conjecture full_types) conjectures
- val tfree_lines = problem_lines_for_free_types conjectures
- (* Reordering these might or might not confuse the proof reconstruction
- code or the SPASS Flotter hack. *)
- val problem =
- [("Relevant facts", axiom_lines),
- ("Class relationships", class_rel_lines),
- ("Arity declarations", arity_lines),
- ("Helper facts", helper_lines),
- ("Conjectures", conjecture_lines),
- ("Type variables", tfree_lines)]
- |> repair_problem thy explicit_forall full_types explicit_apply
- val (problem, pool) = nice_problem problem (empty_name_pool readable_names)
- val conjecture_offset =
- length axiom_lines + length class_rel_lines + length arity_lines
- + length helper_lines
- val _ = File.write_list file (strings_for_problem problem)
- in
- (case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
- conjecture_offset)
- end
-
-end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Jul 27 17:10:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Jul 27 20:16:14 2010 +0200
@@ -8,7 +8,6 @@
sig
val plural_s : int -> string
val serial_commas : string -> string list -> string list
- val timestamp : unit -> string
val strip_spaces : string -> string
val parse_bool_option : bool -> string -> string -> bool option
val parse_time_option : string -> string -> Time.time option
@@ -32,8 +31,6 @@
| serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
| serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
-val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
-
fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
fun strip_spaces_in_list [] = ""