--- a/doc-src/Sledgehammer/sledgehammer.tex Wed Jun 23 10:05:13 2010 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Wed Jun 23 10:20:54 2010 +0200
@@ -341,11 +341,6 @@
download page. Sledgehammer requires version 3.5 or above. See
\S\ref{installation} for details.
-\item[$\bullet$] \textbf{\textit{spass\_dfg}:} Same as the above, except that
-Sledgehammer communicates with SPASS using the native DFG syntax rather than the
-TPTP syntax. Sledgehammer requires version 3.0 or above. This ATP is provided
-for compatibility reasons.
-
\item[$\bullet$] \textbf{\textit{vampire}:} Vampire is an ATP developed by
Andrei Voronkov and his colleagues \cite{riazanov-voronkov-2002}. To use
Vampire, set the environment variable \texttt{VAMPIRE\_HOME} to the directory
--- a/src/HOL/IsaMakefile Wed Jun 23 10:05:13 2010 +0200
+++ b/src/HOL/IsaMakefile Wed Jun 23 10:20:54 2010 +0200
@@ -322,6 +322,7 @@
Tools/Sledgehammer/sledgehammer_hol_clause.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 Wed Jun 23 10:05:13 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Jun 23 10:20:54 2010 +0200
@@ -299,6 +299,7 @@
fun run_sh prover hard_timeout timeout dir st =
let
+ val _ = Sledgehammer_Fact_Filter.use_natural_form := true (* experimental *)
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)
@@ -324,7 +325,7 @@
NONE => (message, SH_OK (time_isa, time_atp, relevant_thm_names))
| SOME _ => (message, SH_FAIL (time_isa, time_atp))
end
- handle Sledgehammer_HOL_Clause.TRIVIAL => ("trivial", SH_OK (0, 0, []))
+ handle Sledgehammer_HOL_Clause.TRIVIAL () => ("trivial", SH_OK (0, 0, []))
| ERROR msg => ("error: " ^ msg, SH_ERROR)
| TimeLimit.TimeOut => ("timeout", SH_ERROR)
--- a/src/HOL/Nitpick_Examples/Mini_Nits.thy Wed Jun 23 10:05:13 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy Wed Jun 23 10:20:54 2010 +0200
@@ -14,14 +14,19 @@
ML {*
exception FAIL
-(* int -> term -> string *)
+val has_kodkodi = (getenv "KODKODI" <> "")
+
fun minipick n t =
map (fn k => Minipick.kodkod_problem_from_term @{context} (K k) t) (1 upto n)
|> Minipick.solve_any_kodkod_problem @{theory}
-(* int -> term -> bool *)
-fun none n t = (minipick n t = "none" orelse raise FAIL)
-fun genuine n t = (minipick n t = "genuine" orelse raise FAIL)
-fun unknown n t = (minipick n t = "unknown" orelse raise FAIL)
+fun minipick_expect expect n t =
+ if has_kodkodi then
+ if minipick n t = expect then () else raise FAIL
+ else
+ ()
+val none = minipick_expect "none"
+val genuine = minipick_expect "genuine"
+val unknown = minipick_expect "unknown"
*}
ML {* genuine 1 @{prop "x = Not"} *}
--- a/src/HOL/Nitpick_Examples/ROOT.ML Wed Jun 23 10:05:13 2010 +0200
+++ b/src/HOL/Nitpick_Examples/ROOT.ML Wed Jun 23 10:20:54 2010 +0200
@@ -5,8 +5,4 @@
Nitpick examples.
*)
-if getenv "KODKODI" = "" then
- ()
-else
- setmp_noncritical quick_and_dirty true use_thys
- ["Nitpick_Examples"];
+setmp_noncritical quick_and_dirty true use_thys ["Nitpick_Examples"];
--- a/src/HOL/Nitpick_Examples/Tests_Nits.thy Wed Jun 23 10:05:13 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Tests_Nits.thy Wed Jun 23 10:20:54 2010 +0200
@@ -11,6 +11,6 @@
imports Main
begin
-ML {* Nitpick_Tests.run_all_tests () *}
+ML {* () |> getenv "KODKODI" <> "" ? Nitpick_Tests.run_all_tests *}
end
--- a/src/HOL/Sledgehammer.thy Wed Jun 23 10:05:13 2010 +0200
+++ b/src/HOL/Sledgehammer.thy Wed Jun 23 10:20:54 2010 +0200
@@ -17,6 +17,7 @@
("Tools/Sledgehammer/sledgehammer_hol_clause.ML")
("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
("Tools/Sledgehammer/sledgehammer_fact_filter.ML")
+ ("Tools/Sledgehammer/sledgehammer_tptp_format.ML")
("Tools/ATP_Manager/atp_manager.ML")
("Tools/ATP_Manager/atp_systems.ML")
("Tools/Sledgehammer/sledgehammer_fact_minimizer.ML")
@@ -103,12 +104,12 @@
use "Tools/Sledgehammer/sledgehammer_hol_clause.ML"
use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
+use "Tools/Sledgehammer/sledgehammer_tptp_format.ML"
use "Tools/ATP_Manager/atp_manager.ML"
use "Tools/ATP_Manager/atp_systems.ML"
setup ATP_Systems.setup
use "Tools/Sledgehammer/sledgehammer_fact_minimizer.ML"
use "Tools/Sledgehammer/sledgehammer_isar.ML"
-setup Sledgehammer_Isar.setup
subsection {* The MESON prover *}
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Wed Jun 23 10:05:13 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Wed Jun 23 10:20:54 2010 +0200
@@ -8,7 +8,8 @@
signature ATP_MANAGER =
sig
- type name_pool = Sledgehammer_HOL_Clause.name_pool
+ type name_pool = Sledgehammer_FOL_Clause.name_pool
+ type cnf_thm = Sledgehammer_Fact_Preprocessor.cnf_thm
type relevance_override = Sledgehammer_Fact_Filter.relevance_override
type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
type params =
@@ -31,8 +32,8 @@
{subgoal: int,
goal: Proof.context * (thm list * thm),
relevance_override: relevance_override,
- axiom_clauses: (thm * (string * int)) list option,
- filtered_clauses: (thm * (string * int)) list option}
+ axiom_clauses: cnf_thm list option,
+ filtered_clauses: cnf_thm list option}
datatype failure =
Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass |
MalformedInput | MalformedOutput | UnknownError
@@ -46,7 +47,7 @@
proof: string,
internal_thm_names: string Vector.vector,
conjecture_shape: int list list,
- filtered_clauses: (thm * (string * int)) list}
+ filtered_clauses: cnf_thm list}
type prover =
params -> minimize_command -> Time.time -> problem -> prover_result
@@ -66,6 +67,7 @@
open Sledgehammer_Util
open Sledgehammer_Fact_Filter
+open Sledgehammer_HOL_Clause
open Sledgehammer_Proof_Reconstruct
(** problems, results, provers, etc. **)
@@ -91,8 +93,8 @@
{subgoal: int,
goal: Proof.context * (thm list * thm),
relevance_override: relevance_override,
- axiom_clauses: (thm * (string * int)) list option,
- filtered_clauses: (thm * (string * int)) list option};
+ axiom_clauses: cnf_thm list option,
+ filtered_clauses: cnf_thm list option}
datatype failure =
Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass |
@@ -108,7 +110,7 @@
proof: string,
internal_thm_names: string Vector.vector,
conjecture_shape: int list list,
- filtered_clauses: (thm * (string * int)) list};
+ filtered_clauses: cnf_thm list}
type prover =
params -> minimize_command -> Time.time -> problem -> prover_result
@@ -354,7 +356,7 @@
filtered_clauses = NONE}
val message =
#message (prover params (minimize_command name) timeout problem)
- handle Sledgehammer_HOL_Clause.TRIVIAL => metis_line full_types i n []
+ handle TRIVIAL () => metis_line full_types i n []
| ERROR message => "Error: " ^ message ^ "\n"
val _ = unregister params message (Thread.self ());
in () end)
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Wed Jun 23 10:05:13 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Wed Jun 23 10:20:54 2010 +0200
@@ -27,6 +27,7 @@
open Sledgehammer_HOL_Clause
open Sledgehammer_Fact_Filter
open Sledgehammer_Proof_Reconstruct
+open Sledgehammer_TPTP_Format
open ATP_Manager
(** generic ATP **)
@@ -110,33 +111,39 @@
fun shape_of_clauses _ [] = []
| shape_of_clauses j ([] :: clauses) = [] :: shape_of_clauses j clauses
- | shape_of_clauses j ((lit :: lits) :: clauses) =
+ | shape_of_clauses j ((_ :: lits) :: clauses) =
let val shape = shape_of_clauses (j + 1) (lits :: clauses) in
(j :: hd shape) :: tl shape
end
-fun generic_prover overlord get_facts prepare write_file home_var executable
- args proof_delims known_failures name
- ({debug, full_types, explicit_apply, isar_proof, isar_shrink_factor,
- ...} : params) minimize_command
+(* generic TPTP-based provers *)
+
+fun generic_tptp_prover
+ (name, {home_var, executable, arguments, proof_delims, known_failures,
+ max_axiom_clauses, prefers_theory_relevant})
+ ({debug, overlord, full_types, explicit_apply, respect_no_atp,
+ 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, (chained_ths, th)) = goal;
+ val (ctxt, (_, th)) = goal;
val thy = ProofContext.theory_of ctxt;
val goal_clss = #1 (neg_conjecture_clauses ctxt th subgoal)
val goal_cls = List.concat goal_clss
val the_filtered_clauses =
(case filtered_clauses of
- NONE => get_facts relevance_override goal goal_cls
+ NONE => relevant_facts full_types respect_no_atp relevance_threshold
+ relevance_convergence defs_relevant max_axiom_clauses
+ (the_default prefers_theory_relevant theory_relevant)
+ relevance_override goal goal_cls
| SOME fcls => fcls);
- val the_axiom_clauses =
- (case axiom_clauses of
- NONE => the_filtered_clauses
- | SOME axcls => axcls);
+ val the_axiom_clauses = axiom_clauses |> the_default the_filtered_clauses
val (internal_thm_names, clauses) =
- prepare goal_cls chained_ths the_axiom_clauses the_filtered_clauses thy;
+ prepare_clauses full_types goal_cls the_axiom_clauses the_filtered_clauses
+ thy
(* path to unique problem file *)
val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
@@ -161,10 +168,10 @@
fun command_line probfile =
(if Config.get ctxt measure_runtime then
"TIMEFORMAT='%3U'; { time " ^
- space_implode " " [File.shell_path command, args,
+ space_implode " " [File.shell_path command, arguments timeout,
File.shell_path probfile] ^ " ; } 2>&1"
else
- space_implode " " ["exec", File.shell_path command, args,
+ space_implode " " ["exec", File.shell_path command, arguments timeout,
File.shell_path probfile, "2>&1"]) ^
(if overlord then
" | sed 's/,/, /g' \
@@ -185,11 +192,12 @@
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 split_time' s =
- if Config.get ctxt measure_runtime then split_time s else (s, 0)
+ val split_time' =
+ if Config.get ctxt measure_runtime then split_time else rpair 0
fun run_on probfile =
if File.exists command then
- write_file full_types explicit_apply probfile clauses
+ write_tptp_file (debug andalso overlord) full_types explicit_apply
+ probfile clauses
|> pair (apfst split_time' (bash_output (command_line probfile)))
else if home = "" then
error ("The environment variable " ^ quote home_var ^ " is not set.")
@@ -233,58 +241,12 @@
proof = proof, internal_thm_names = internal_thm_names,
conjecture_shape = conjecture_shape,
filtered_clauses = the_filtered_clauses}
- end;
-
-
-(* generic TPTP-based provers *)
-
-fun generic_tptp_prover
- (name, {home_var, executable, arguments, proof_delims, known_failures,
- max_axiom_clauses, prefers_theory_relevant})
- (params as {debug, overlord, full_types, respect_no_atp,
- relevance_threshold, relevance_convergence, theory_relevant,
- defs_relevant, isar_proof, ...})
- minimize_command timeout =
- generic_prover overlord
- (relevant_facts full_types respect_no_atp relevance_threshold
- relevance_convergence defs_relevant max_axiom_clauses
- (the_default prefers_theory_relevant theory_relevant))
- (prepare_clauses false full_types)
- (write_tptp_file (debug andalso overlord)) home_var
- executable (arguments timeout) proof_delims known_failures name params
- minimize_command
+ end
fun tptp_prover name p = (name, generic_tptp_prover (name, p));
-
-(** common provers **)
-
fun to_generous_secs time = (Time.toMilliseconds time + 999) div 1000
-(* Vampire *)
-
-(* Vampire requires an explicit time limit. *)
-
-val vampire_config : prover_config =
- {home_var = "VAMPIRE_HOME",
- executable = "vampire",
- arguments = fn timeout =>
- "--output_syntax tptp --mode casc -t " ^
- string_of_int (to_generous_secs timeout),
- proof_delims =
- [("=========== Refutation ==========",
- "======= End of refutation ======="),
- ("% SZS output start Refutation", "% SZS output end Refutation")],
- known_failures =
- [(Unprovable, "UNPROVABLE"),
- (IncompleteUnprovable, "CANNOT PROVE"),
- (Unprovable, "Satisfiability detected"),
- (OutOfResources, "Refutation not found")],
- max_axiom_clauses = 60,
- prefers_theory_relevant = false}
-val vampire = tptp_prover "vampire" vampire_config
-
-
(* E prover *)
val tstp_proof_delims =
@@ -311,33 +273,14 @@
val e = tptp_prover "e" e_config
-(* SPASS *)
-
-fun generic_dfg_prover
- (name, {home_var, executable, arguments, proof_delims, known_failures,
- max_axiom_clauses, prefers_theory_relevant})
- (params as {overlord, full_types, respect_no_atp, relevance_threshold,
- relevance_convergence, theory_relevant, defs_relevant, ...})
- minimize_command timeout =
- generic_prover overlord
- (relevant_facts full_types respect_no_atp relevance_threshold
- relevance_convergence defs_relevant max_axiom_clauses
- (the_default prefers_theory_relevant theory_relevant))
- (prepare_clauses true full_types) write_dfg_file home_var executable
- (arguments timeout) proof_delims known_failures name params
- minimize_command
-
-fun dfg_prover name p = (name, generic_dfg_prover (name, p))
-
(* The "-VarWeight=3" option helps the higher-order problems, probably by
counteracting the presence of "hAPP". *)
-fun generic_spass_config dfg : prover_config =
+val spass_config : prover_config =
{home_var = "SPASS_HOME",
executable = "SPASS",
arguments = fn timeout =>
- "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
- \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout)
- |> not dfg ? prefix "-TPTP ",
+ "-TPTP -Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
+ \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout),
proof_delims = [("Here is a proof", "Formulae used in the proof")],
known_failures =
[(IncompleteUnprovable, "SPASS beiseite: Completion found"),
@@ -349,13 +292,30 @@
(OldSpass, "Unrecognized option TPTP")],
max_axiom_clauses = 40,
prefers_theory_relevant = true}
-val spass_dfg_config = generic_spass_config true
-val spass_dfg = dfg_prover "spass_dfg" spass_dfg_config
-
-val spass_config = generic_spass_config false
val spass = tptp_prover "spass" spass_config
-(* remote prover invocation via SystemOnTPTP *)
+(* Vampire *)
+
+val vampire_config : prover_config =
+ {home_var = "VAMPIRE_HOME",
+ executable = "vampire",
+ arguments = fn timeout =>
+ "--output_syntax tptp --mode casc -t " ^
+ string_of_int (to_generous_secs timeout),
+ proof_delims =
+ [("=========== Refutation ==========",
+ "======= End of refutation ======="),
+ ("% SZS output start Refutation", "% SZS output end Refutation")],
+ known_failures =
+ [(Unprovable, "UNPROVABLE"),
+ (IncompleteUnprovable, "CANNOT PROVE"),
+ (Unprovable, "Satisfiability detected"),
+ (OutOfResources, "Refutation not found")],
+ max_axiom_clauses = 60,
+ prefers_theory_relevant = false}
+val vampire = tptp_prover "vampire" vampire_config
+
+(* Remote prover invocation via SystemOnTPTP *)
val systems = Synchronized.var "atp_systems" ([]: string list);
@@ -366,7 +326,7 @@
error ("Failed to get available systems at SystemOnTPTP:\n" ^ answer)
fun refresh_systems_on_tptp () =
- Synchronized.change systems (fn _ => get_systems ());
+ Synchronized.change systems (fn _ => get_systems ())
fun get_system prefix = Synchronized.change_result systems (fn systems =>
(if null systems then get_systems () else systems)
@@ -374,15 +334,14 @@
fun the_system prefix =
(case get_system prefix of
- NONE => error ("System " ^ quote prefix ^
- " not available at SystemOnTPTP.")
+ NONE => error ("System " ^ quote prefix ^ " not available at SystemOnTPTP.")
| SOME sys => sys);
val remote_known_failures =
[(TimedOut, "says Timeout"),
(MalformedOutput, "Remote script could not extract proof")]
-fun remote_prover_config atp_prefix args
+fun remote_config atp_prefix args
({proof_delims, known_failures, max_axiom_clauses,
prefers_theory_relevant, ...} : prover_config) : prover_config =
{home_var = "ISABELLE_ATP_MANAGER",
@@ -395,17 +354,12 @@
max_axiom_clauses = max_axiom_clauses,
prefers_theory_relevant = prefers_theory_relevant}
-val remote_vampire =
- tptp_prover (remotify (fst vampire))
- (remote_prover_config "Vampire---9" "" vampire_config)
+fun remote_tptp_prover prover atp_prefix args config =
+ tptp_prover (remotify (fst prover)) (remote_config atp_prefix args config)
-val remote_e =
- tptp_prover (remotify (fst e))
- (remote_prover_config "EP---" "" e_config)
-
-val remote_spass =
- tptp_prover (remotify (fst spass))
- (remote_prover_config "SPASS---" "-x" spass_config)
+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 maybe_remote (name, _) ({home_var, ...} : prover_config) =
name |> getenv home_var = "" ? remotify
@@ -414,8 +368,7 @@
space_implode " " [maybe_remote e e_config, maybe_remote spass spass_config,
remotify (fst vampire)]
-val provers =
- [spass, spass_dfg, vampire, e, remote_vampire, remote_spass, remote_e]
+val provers = [e, spass, vampire, remote_e, remote_spass, remote_vampire]
val prover_setup = fold add_prover provers
val setup =
--- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Jun 23 10:05:13 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Wed Jun 23 10:20:54 2010 +0200
@@ -943,15 +943,15 @@
fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i n
step subst orig_assm_ts orig_t =
- let
- val warning_m = if auto then K () else warning
- val unknown_outcome = ("unknown", state)
- in
+ let val warning_m = if auto then K () else warning in
if getenv "KODKODI" = "" then
+ (* The "expect" argument is deliberately ignored if Kodkodi is missing so
+ that the "Nitpick_Examples" can be processed on any machine. *)
(warning_m (Pretty.string_of (plazy install_kodkodi_message));
- unknown_outcome)
+ ("no_kodkodi", state))
else
let
+ val unknown_outcome = ("unknown", state)
val deadline = Option.map (curry Time.+ (Time.now ())) timeout
val outcome as (outcome_code, _) =
time_limit (if debug then NONE else timeout)
--- a/src/HOL/Tools/Sledgehammer/meson_tactic.ML Wed Jun 23 10:05:13 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/meson_tactic.ML Wed Jun 23 10:20:54 2010 +0200
@@ -17,11 +17,11 @@
open Sledgehammer_Fact_Preprocessor
(*Expand all new definitions of abstraction or Skolem functions in a proof state.*)
-fun is_absko (Const (@{const_name "=="}, _) $ Free (a, _) $ u) =
+fun is_absko (Const (@{const_name "=="}, _) $ Free (a, _) $ _) =
String.isPrefix skolem_prefix a
| is_absko _ = false;
-fun is_okdef xs (Const (@{const_name "=="}, _) $ t $ u) = (*Definition of Free, not in certain terms*)
+fun is_okdef xs (Const (@{const_name "=="}, _) $ t $ _) = (*Definition of Free, not in certain terms*)
is_Free t andalso not (member (op aconv) xs t)
| is_okdef _ _ = false
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Wed Jun 23 10:05:13 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Wed Jun 23 10:20:54 2010 +0200
@@ -24,6 +24,7 @@
open Sledgehammer_HOL_Clause
open Sledgehammer_Proof_Reconstruct
open Sledgehammer_Fact_Filter
+open Sledgehammer_TPTP_Format
val trace = Unsynchronized.ref false;
fun trace_msg msg = if !trace then tracing (msg ()) else ();
@@ -58,7 +59,7 @@
(* Finding the relative location of an untyped term within a list of terms *)
fun get_index lit =
let val lit = Envir.eta_contract lit
- fun get n [] = raise Empty
+ fun get _ [] = raise Empty
| get n (x::xs) = if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x))
then n else get (n+1) xs
in get 1 end;
@@ -238,7 +239,7 @@
| NONE => raise Fail ("fol_type_to_isa: " ^ x));
fun reveal_skolem_somes skolem_somes =
- map_aterms (fn t as Const (s, T) =>
+ map_aterms (fn t as Const (s, _) =>
if String.isPrefix skolem_theory_name s then
AList.lookup (op =) skolem_somes s
|> the |> map_types Type_Infer.paramify_vars
@@ -348,8 +349,7 @@
| hol_term_from_fol _ = hol_term_from_fol_PT
fun hol_terms_from_fol ctxt mode skolem_somes fol_tms =
- let val thy = ProofContext.theory_of ctxt
- val ts = map (hol_term_from_fol mode ctxt) fol_tms
+ let val ts = map (hol_term_from_fol mode ctxt) fol_tms
val _ = trace_msg (fn () => " calling type inference:")
val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts
val ts' = ts |> map (reveal_skolem_somes skolem_somes) |> infer_types ctxt
@@ -694,11 +694,10 @@
tfrees = union (op =) tfree_lits tfrees,
skolem_somes = skolem_somes}
end;
- val lmap as {skolem_somes, ...} =
- {axioms = [], tfrees = init_tfrees ctxt, skolem_somes = []}
- |> fold (add_thm true) cls
- |> add_tfrees
- |> fold (add_thm false) ths
+ val lmap = {axioms = [], tfrees = init_tfrees ctxt, skolem_somes = []}
+ |> fold (add_thm true) cls
+ |> add_tfrees
+ |> fold (add_thm false) ths
val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
fun is_used c =
exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Jun 23 10:05:13 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Jun 23 10:20:54 2010 +0200
@@ -5,17 +5,17 @@
signature SLEDGEHAMMER_FACT_FILTER =
sig
+ type cnf_thm = Sledgehammer_Fact_Preprocessor.cnf_thm
type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
type arity_clause = Sledgehammer_FOL_Clause.arity_clause
- type axiom_name = Sledgehammer_HOL_Clause.axiom_name
type hol_clause = Sledgehammer_HOL_Clause.hol_clause
- type hol_clause_id = Sledgehammer_HOL_Clause.hol_clause_id
type relevance_override =
{add: Facts.ref list,
del: Facts.ref list,
only: bool}
+ val use_natural_form : bool Unsynchronized.ref
val name_thms_pair_from_ref :
Proof.context -> thm list -> Facts.ref -> string * thm list
val tvar_classes_of_terms : term list -> string list
@@ -24,15 +24,12 @@
val is_quasi_fol_term : theory -> term -> bool
val relevant_facts :
bool -> bool -> real -> real -> bool -> int -> bool -> relevance_override
- -> Proof.context * (thm list * 'a) -> thm list
- -> (thm * (string * int)) list
+ -> Proof.context * (thm list * 'a) -> thm list -> cnf_thm list
val prepare_clauses :
- bool -> bool -> thm list -> thm list
- -> (thm * (axiom_name * hol_clause_id)) list
- -> (thm * (axiom_name * hol_clause_id)) list -> theory
- -> axiom_name vector
- * (hol_clause list * hol_clause list * hol_clause list *
- hol_clause list * classrel_clause list * arity_clause list)
+ bool -> thm list -> cnf_thm list -> cnf_thm list -> theory
+ -> string vector
+ * (hol_clause list * hol_clause list * hol_clause list
+ * hol_clause list * classrel_clause list * arity_clause list)
end;
structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
@@ -42,6 +39,9 @@
open Sledgehammer_Fact_Preprocessor
open Sledgehammer_HOL_Clause
+(* Experimental feature: Filter theorems in natural form or in CNF? *)
+val use_natural_form = Unsynchronized.ref false
+
type relevance_override =
{add: Facts.ref list,
del: Facts.ref list,
@@ -54,36 +54,13 @@
fun strip_Trueprop (@{const Trueprop} $ t) = t
| strip_Trueprop t = t;
-(*A surprising number of theorems contain only a few significant constants.
- These include all induction rules, and other general theorems. Filtering
- theorems in clause form reveals these complexities in the form of Skolem
- functions. If we were instead to filter theorems in their natural form,
- some other method of measuring theorem complexity would become necessary.*)
-
-fun log_weight2 (x:real) = 1.0 + 2.0/Math.ln (x+1.0);
-
-(*The default seems best in practice. A constant function of one ignores
- the constant frequencies.*)
-val weight_fn = log_weight2;
-
-
-(*Including equality in this list might be expected to stop rules like subset_antisym from
- being chosen, but for some reason filtering works better with them listed. The
- logical signs All, Ex, &, and --> are omitted because any remaining occurrrences
- must be within comprehensions.*)
-val standard_consts =
- [@{const_name Trueprop}, @{const_name "==>"}, @{const_name all},
- @{const_name "=="}, @{const_name "op |"}, @{const_name Not},
- @{const_name "op ="}];
-
-
(*** constants with types ***)
(*An abstraction of Isabelle types*)
datatype const_typ = CTVar | CType of string * const_typ list
(*Is the second type an instance of the first one?*)
-fun match_type (CType(con1,args1)) (CType(con2,args2)) =
+fun match_type (CType(con1,args1)) (CType(con2,args2)) =
con1=con2 andalso match_types args1 args2
| match_type CTVar _ = true
| match_type _ CTVar = false
@@ -91,63 +68,85 @@
| match_types (a1::as1) (a2::as2) = match_type a1 a2 andalso match_types as1 as2;
(*Is there a unifiable constant?*)
-fun uni_mem gctab (c,c_typ) =
- case Symtab.lookup gctab c of
- NONE => false
- | SOME ctyps_list => exists (match_types c_typ) ctyps_list;
-
+fun uni_mem goal_const_tab (c, c_typ) =
+ exists (match_types c_typ) (these (Symtab.lookup goal_const_tab c))
+
(*Maps a "real" type to a const_typ*)
-fun const_typ_of (Type (c,typs)) = CType (c, map const_typ_of typs)
+fun const_typ_of (Type (c,typs)) = CType (c, map const_typ_of typs)
| const_typ_of (TFree _) = CTVar
| const_typ_of (TVar _) = CTVar
(*Pairs a constant with the list of its type instantiations (using const_typ)*)
-fun const_with_typ thy (c,typ) =
+fun const_with_typ thy (c,typ) =
let val tvars = Sign.const_typargs thy (c,typ)
in (c, map const_typ_of tvars) end
- handle TYPE _ => (c,[]); (*Variable (locale constant): monomorphic*)
+ handle TYPE _ => (c,[]); (*Variable (locale constant): monomorphic*)
(*Add a const/type pair to the table, but a [] entry means a standard connective,
which we ignore.*)
-fun add_const_typ_table ((c,ctyps), tab) =
- Symtab.map_default (c, [ctyps]) (fn [] => [] | ctyps_list => insert (op =) ctyps ctyps_list)
- tab;
+fun add_const_type_to_table (c, ctyps) =
+ Symtab.map_default (c, [ctyps])
+ (fn [] => [] | ctypss => insert (op =) ctyps ctypss)
+
+val fresh_Ex_prefix = "Sledgehammer.Ex."
-(*Free variables are included, as well as constants, to handle locales*)
-fun add_term_consts_typs_rm thy (Const(c, typ), tab) =
- add_const_typ_table (const_with_typ thy (c,typ), tab)
- | add_term_consts_typs_rm thy (Free(c, typ), tab) =
- add_const_typ_table (const_with_typ thy (c,typ), tab)
- | add_term_consts_typs_rm _ (Const (@{const_name skolem_id}, _) $ _, tab) =
- tab
- | add_term_consts_typs_rm thy (t $ u, tab) =
- add_term_consts_typs_rm thy (t, add_term_consts_typs_rm thy (u, tab))
- | add_term_consts_typs_rm thy (Abs(_,_,t), tab) = add_term_consts_typs_rm thy (t, tab)
- | add_term_consts_typs_rm _ (_, tab) = tab;
-
-(*The empty list here indicates that the constant is being ignored*)
-fun add_standard_const (s,tab) = Symtab.update (s,[]) tab;
-
-val null_const_tab : const_typ list list Symtab.table =
- List.foldl add_standard_const Symtab.empty standard_consts;
-
-fun get_goal_consts_typs thy = List.foldl (add_term_consts_typs_rm thy) null_const_tab;
+fun get_goal_consts_typs thy goals =
+ let
+ val use_natural_form = !use_natural_form
+ (* Free variables are included, as well as constants, to handle locales.
+ "skolem_id" is included to increase the complexity of theorems containing
+ Skolem functions. In non-CNF form, "Ex" is included but each occurrence
+ is considered fresh, to simulate the effect of Skolemization. *)
+ fun aux (Const (x as (s, _))) =
+ (if s = @{const_name Ex} andalso use_natural_form then
+ (gensym fresh_Ex_prefix, [])
+ else
+ (const_with_typ thy x))
+ |> add_const_type_to_table
+ | aux (Free x) = add_const_type_to_table (const_with_typ thy x)
+ | aux ((t as Const (@{const_name skolem_id}, _)) $ _) = aux t
+ | aux (t $ u) = aux t #> aux u
+ | aux (Abs (_, _, t)) = aux t
+ | aux _ = I
+ (* Including equality in this list might be expected to stop rules like
+ subset_antisym from being chosen, but for some reason filtering works better
+ with them listed. The logical signs All, Ex, &, and --> are omitted for CNF
+ because any remaining occurrences must be within comprehensions. *)
+ val standard_consts =
+ [@{const_name Trueprop}, @{const_name "==>"}, @{const_name all},
+ @{const_name "=="}, @{const_name "op |"}, @{const_name Not},
+ @{const_name "op ="}] @
+ (if use_natural_form then
+ [@{const_name All}, @{const_name Ex}, @{const_name "op &"},
+ @{const_name "op -->"}]
+ else
+ [])
+ in
+ Symtab.empty |> fold (Symtab.update o rpair []) standard_consts
+ |> fold aux goals
+ end
(*Inserts a dummy "constant" referring to the theory name, so that relevance
takes the given theory into account.*)
fun const_prop_of theory_relevant th =
- if theory_relevant then
- let val name = Context.theory_name (theory_of_thm th)
- val t = Const (name ^ ". 1", HOLogic.boolT)
- in t $ prop_of th end
- else prop_of th;
+ if theory_relevant then
+ let
+ val name = Context.theory_name (theory_of_thm th)
+ val t = Const (name ^ ". 1", @{typ bool})
+ in t $ prop_of th end
+ else
+ prop_of th
+
+fun appropriate_prop_of theory_relevant (cnf_thm, (_, orig_thm)) =
+ (if !use_natural_form then orig_thm else cnf_thm)
+ |> const_prop_of theory_relevant
(**** Constant / Type Frequencies ****)
(*A two-dimensional symbol table counts frequencies of constants. It's keyed first by
constant name and second by its list of type instantiations. For the latter, we need
a linear ordering on type const_typ list.*)
-
+
local
fun cons_nr CTVar = 0
@@ -165,137 +164,149 @@
structure CTtab = Table(type key = const_typ list val ord = dict_ord const_typ_ord);
-fun count_axiom_consts theory_relevant thy ((thm,_), tab) =
- let fun count_const (a, T, tab) =
- let val (c, cts) = const_with_typ thy (a,T)
- in (*Two-dimensional table update. Constant maps to types maps to count.*)
- Symtab.map_default (c, CTtab.empty)
- (CTtab.map_default (cts,0) (fn n => n+1)) tab
- end
- fun count_term_consts (Const(a,T), tab) = count_const(a,T,tab)
- | count_term_consts (Free(a,T), tab) = count_const(a,T,tab)
- | count_term_consts (t $ u, tab) =
- count_term_consts (t, count_term_consts (u, tab))
- | count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab)
- | count_term_consts (_, tab) = tab
- in count_term_consts (const_prop_of theory_relevant thm, tab) end;
+fun count_axiom_consts theory_relevant thy axiom =
+ let
+ fun do_const (a, T) =
+ let val (c, cts) = const_with_typ thy (a,T) in
+ (* Two-dimensional table update. Constant maps to types maps to
+ count. *)
+ CTtab.map_default (cts, 0) (Integer.add 1)
+ |> Symtab.map_default (c, CTtab.empty)
+ end
+ fun do_term (Const x) = do_const x
+ | do_term (Free x) = do_const x
+ | do_term (Const (@{const_name skolem_id}, _) $ _) = I
+ | do_term (t $ u) = do_term t #> do_term u
+ | do_term (Abs (_, _, t)) = do_term t
+ | do_term _ = I
+ in axiom |> appropriate_prop_of theory_relevant |> do_term end
(**** Actual Filtering Code ****)
(*The frequency of a constant is the sum of those of all instances of its type.*)
-fun const_frequency ctab (c, cts) =
+fun const_frequency const_tab (c, cts) =
CTtab.fold (fn (cts', m) => match_types cts cts' ? Integer.add m)
- (the (Symtab.lookup ctab c)) 0
+ (the (Symtab.lookup const_tab c)
+ handle Option.Option => raise Fail ("Const: " ^ c)) 0
-(*Add in a constant's weight, as determined by its frequency.*)
-fun add_ct_weight ctab ((c,T), w) =
- w + weight_fn (real (const_frequency ctab (c,T)));
+(*A surprising number of theorems contain only a few significant constants.
+ These include all induction rules, and other general theorems. Filtering
+ theorems in clause form reveals these complexities in the form of Skolem
+ functions. If we were instead to filter theorems in their natural form,
+ some other method of measuring theorem complexity would become necessary.*)
-(*Relevant constants are weighted according to frequency,
+(* "log" seems best in practice. A constant function of one ignores the constant
+ frequencies. *)
+fun log_weight2 (x:real) = 1.0 + 2.0 / Math.ln (x + 1.0)
+
+(* Computes a constant's weight, as determined by its frequency. *)
+val ct_weight = log_weight2 o real oo const_frequency
+
+(*Relevant constants are weighted according to frequency,
but irrelevant constants are simply counted. Otherwise, Skolem functions,
which are rare, would harm a clause's chances of being picked.*)
-fun clause_weight ctab gctyps consts_typs =
+fun clause_weight const_tab gctyps consts_typs =
let val rel = filter (uni_mem gctyps) consts_typs
- val rel_weight = List.foldl (add_ct_weight ctab) 0.0 rel
+ val rel_weight = fold (curry Real.+ o ct_weight const_tab) rel 0.0
in
rel_weight / (rel_weight + real (length consts_typs - length rel))
end;
-
+
(*Multiplies out to a list of pairs: 'a * 'b list -> ('a * 'b) list -> ('a * 'b) list*)
fun add_expand_pairs (x,ys) xys = List.foldl (fn (y,acc) => (x,y)::acc) xys ys;
-fun consts_typs_of_term thy t =
- let val tab = add_term_consts_typs_rm thy (t, null_const_tab)
- in Symtab.fold add_expand_pairs tab [] end;
+fun consts_typs_of_term thy t =
+ Symtab.fold add_expand_pairs (get_goal_consts_typs thy [t]) []
-fun pair_consts_typs_axiom theory_relevant thy (p as (thm, _)) =
- (p, (consts_typs_of_term thy (const_prop_of theory_relevant thm)));
+fun pair_consts_typs_axiom theory_relevant thy axiom =
+ (axiom, axiom |> appropriate_prop_of theory_relevant
+ |> consts_typs_of_term thy)
-exception ConstFree;
-fun dest_ConstFree (Const aT) = aT
- | dest_ConstFree (Free aT) = aT
- | dest_ConstFree _ = raise ConstFree;
+exception CONST_OR_FREE of unit
+
+fun dest_Const_or_Free (Const x) = x
+ | dest_Const_or_Free (Free x) = x
+ | dest_Const_or_Free _ = raise CONST_OR_FREE ()
(*Look for definitions of the form f ?x1 ... ?xn = t, but not reversed.*)
fun defines thy thm gctypes =
let val tm = prop_of thm
fun defs lhs rhs =
let val (rator,args) = strip_comb lhs
- val ct = const_with_typ thy (dest_ConstFree rator)
+ val ct = const_with_typ thy (dest_Const_or_Free rator)
in
forall is_Var args andalso uni_mem gctypes ct andalso
subset (op =) (Term.add_vars rhs [], Term.add_vars lhs [])
end
- handle ConstFree => false
- in
+ handle CONST_OR_FREE () => false
+ in
case tm of
- @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ lhs $ rhs) =>
- defs lhs rhs
+ @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ lhs $ rhs) =>
+ defs lhs rhs
| _ => false
end;
-type annotd_cls = (thm * (string * int)) * ((string * const_typ list) list);
-
+type annotated_clause = cnf_thm * ((string * const_typ list) list)
+
(*For a reverse sort, putting the largest values first.*)
-fun compare_pairs ((_,w1),(_,w2)) = Real.compare (w2,w1);
+fun compare_pairs ((_, w1), (_, w2)) = Real.compare (w2, w1)
(*Limit the number of new clauses, to prevent runaway acceptance.*)
-fun take_best max_new (newpairs : (annotd_cls*real) list) =
+fun take_best max_new (newpairs : (annotated_clause * real) list) =
let val nnew = length newpairs
in
if nnew <= max_new then (map #1 newpairs, [])
- else
+ else
let val cls = sort compare_pairs newpairs
val accepted = List.take (cls, max_new)
in
- trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^
+ trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^
", exceeds the limit of " ^ Int.toString (max_new)));
trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
trace_msg (fn () => "Actually passed: " ^
- space_implode ", " (map (fn (((_,(name,_)),_),_) => name) accepted));
+ space_implode ", " (map (fn (((_,((name,_), _)),_),_) => name) accepted));
(map #1 accepted, map #1 (List.drop (cls, max_new)))
end
end;
-fun cnf_for_facts ctxt =
- let val thy = ProofContext.theory_of ctxt in
- maps (maps (cnf_axiom thy) o ProofContext.get_fact ctxt)
- end
-
fun relevant_clauses ctxt relevance_convergence defs_relevant max_new
- (relevance_override as {add, del, only}) ctab =
+ ({add, del, ...} : relevance_override) const_tab =
let
val thy = ProofContext.theory_of ctxt
- val add_thms = cnf_for_facts ctxt add
- val del_thms = cnf_for_facts ctxt del
- fun iter threshold rel_consts =
+ val add_thms = maps (ProofContext.get_fact ctxt) add
+ val del_thms = maps (ProofContext.get_fact ctxt) del
+ fun iter threshold rel_const_tab =
let
fun relevant ([], _) [] = [] (* Nothing added this iteration *)
| relevant (newpairs, rejects) [] =
let
val (newrels, more_rejects) = take_best max_new newpairs
val new_consts = maps #2 newrels
- val rel_consts' = List.foldl add_const_typ_table rel_consts new_consts
+ val rel_const_tab =
+ rel_const_tab |> fold add_const_type_to_table new_consts
val threshold =
threshold + (1.0 - threshold) / relevance_convergence
in
trace_msg (fn () => "relevant this iteration: " ^
Int.toString (length newrels));
- map #1 newrels @ iter threshold rel_consts'
+ map #1 newrels @ iter threshold rel_const_tab
(more_rejects @ rejects)
end
| relevant (newrels, rejects)
- ((ax as (clsthm as (thm, (name, n)), consts_typs)) :: axs) =
+ ((ax as (clsthm as (_, ((name, n), orig_th)),
+ consts_typs)) :: axs) =
let
- val weight = if member Thm.eq_thm add_thms thm then 1.0
- else if member Thm.eq_thm del_thms thm then 0.0
- else clause_weight ctab rel_consts consts_typs
+ val weight =
+ if member Thm.eq_thm add_thms orig_th then 1.0
+ else if member Thm.eq_thm del_thms orig_th then 0.0
+ else clause_weight const_tab rel_const_tab consts_typs
in
if weight >= threshold orelse
- (defs_relevant andalso defines thy (#1 clsthm) rel_consts) then
- (trace_msg (fn () => name ^ " clause " ^ Int.toString n ^
+ (defs_relevant andalso
+ defines thy (#1 clsthm) rel_const_tab) then
+ (trace_msg (fn () => name ^ " clause " ^ Int.toString n ^
" passes: " ^ Real.toString weight);
relevant ((ax, weight) :: newrels, rejects) axs)
else
@@ -307,14 +318,14 @@
relevant ([], [])
end
in iter end
-
+
fun relevance_filter ctxt relevance_threshold relevance_convergence
defs_relevant max_new theory_relevant relevance_override
- thy axioms goals =
+ thy (axioms : cnf_thm list) goals =
if relevance_threshold > 0.0 then
let
- val const_tab = List.foldl (count_axiom_consts theory_relevant thy)
- Symtab.empty axioms
+ val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
+ Symtab.empty
val goal_const_tab = get_goal_consts_typs thy goals
val _ =
trace_msg (fn () => "Initial constants: " ^
@@ -398,7 +409,7 @@
fun multi_name a th (n, pairs) =
(n + 1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs);
-fun add_names (a, []) pairs = pairs
+fun add_names (_, []) pairs = pairs
| add_names (a, [th]) pairs = (a, th) :: pairs
| add_names (a, ths) pairs = #2 (fold (multi_name a) ths (1, pairs))
@@ -453,16 +464,16 @@
fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
| fold_type_consts _ _ x = x;
-val add_type_consts_in_type = fold_type_consts setinsert;
-
(*Type constructors used to instantiate overloaded constants are the only ones needed.*)
fun add_type_consts_in_term thy =
- let val const_typargs = Sign.const_typargs thy
- fun add_tcs (Const cT) x = fold add_type_consts_in_type (const_typargs cT) x
- | add_tcs (Abs (_, _, u)) x = add_tcs u x
- | add_tcs (t $ u) x = add_tcs t (add_tcs u x)
- | add_tcs _ x = x
- in add_tcs end
+ let
+ val const_typargs = Sign.const_typargs thy
+ fun aux (Const cT) = fold (fold_type_consts setinsert) (const_typargs cT)
+ | aux (Abs (_, _, u)) = aux u
+ | aux (Const (@{const_name skolem_id}, _) $ _) = I
+ | aux (t $ u) = aux t #> aux u
+ | aux _ = I
+ in aux end
fun type_consts_of_terms thy ts =
Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
@@ -478,7 +489,7 @@
(*Ensures that no higher-order theorems "leak out"*)
fun restrict_to_logic thy true cls =
filter (is_quasi_fol_term thy o prop_of o fst) cls
- | restrict_to_logic thy false cls = cls;
+ | restrict_to_logic _ false cls = cls
(**** Predicates to detect unwanted clauses (prolific or likely to cause
unsoundness) ****)
@@ -524,16 +535,14 @@
omitted. *)
fun is_dangerous_term _ @{prop True} = true
| is_dangerous_term full_types t =
- not full_types andalso
+ not full_types andalso
(has_typed_var dangerous_types t orelse
forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t)))
-fun is_dangerous_theorem full_types add_thms thm =
- not (member Thm.eq_thm add_thms thm) andalso
- is_dangerous_term full_types (prop_of thm)
-
fun remove_dangerous_clauses full_types add_thms =
- filter_out (is_dangerous_theorem full_types add_thms o fst)
+ filter_out (fn (cnf_th, (_, orig_th)) =>
+ not (member Thm.eq_thm add_thms orig_th) andalso
+ is_dangerous_term full_types (prop_of cnf_th))
fun is_fol_goal thy = forall (Meson.is_fol_term thy) o map prop_of
@@ -555,8 +564,11 @@
|> cnf_rules_pairs thy
|> not has_override ? make_unique
|> not only ? restrict_to_logic thy is_FO
- |> (if only then I
- else remove_dangerous_clauses full_types (cnf_for_facts ctxt add))
+ |> (if only then
+ I
+ else
+ remove_dangerous_clauses full_types
+ (maps (ProofContext.get_fact ctxt) add))
in
relevance_filter ctxt relevance_threshold relevance_convergence
defs_relevant max_new theory_relevant relevance_override
@@ -564,9 +576,50 @@
|> has_override ? make_unique
end
+(** Helper clauses **)
+
+fun count_combterm (CombConst ((c, _), _, _)) =
+ Symtab.map_entry c (Integer.add 1)
+ | count_combterm (CombVar _) = I
+ | count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2
+fun count_literal (Literal (_, t)) = count_combterm t
+fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
+
+val raw_cnf_rules_pairs = map (fn (name, thm) => (thm, ((name, 0), thm)))
+fun cnf_helper_thms thy raw =
+ map (`Thm.get_name_hint)
+ #> (if raw then raw_cnf_rules_pairs else cnf_rules_pairs thy)
+
+val optional_helpers =
+ [(["c_COMBI", "c_COMBK"], (false, @{thms COMBI_def COMBK_def})),
+ (["c_COMBB", "c_COMBC"], (false, @{thms COMBB_def COMBC_def})),
+ (["c_COMBS"], (false, @{thms COMBS_def}))]
+val optional_typed_helpers =
+ [(["c_True", "c_False"], (true, @{thms True_or_False})),
+ (["c_If"], (true, @{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 thy is_FO full_types conjectures axcls =
+ let
+ val axclauses = map snd (make_axiom_clauses thy axcls)
+ val ct = fold (fold count_clause) [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, (raw, ths)) =>
+ if exists is_needed ss then cnf_helper_thms thy raw ths
+ else []))
+ @ (if is_FO then [] else cnf_helper_thms thy false mandatory_helpers)
+ in map snd (make_axiom_clauses thy cnfs) end
+
(* prepare for passing to writer,
create additional clauses based on the information from extra_cls *)
-fun prepare_clauses dfg full_types goal_cls chained_ths axcls extra_cls thy =
+fun prepare_clauses full_types goal_cls axcls extra_cls thy =
let
val is_FO = is_fol_goal thy goal_cls
val ccls = subtract_cls extra_cls goal_cls
@@ -577,12 +630,12 @@
and supers = tvar_classes_of_terms axtms
and tycons = type_consts_of_terms thy (ccltms @ axtms)
(*TFrees in conjecture clauses; TVars in axiom clauses*)
- val conjectures = make_conjecture_clauses dfg thy ccls
- val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses dfg thy extra_cls)
- val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses dfg thy axcls)
+ val conjectures = make_conjecture_clauses thy ccls
+ val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses thy extra_cls)
+ val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses thy axcls)
val helper_clauses =
- get_helper_clauses dfg thy is_FO full_types conjectures extra_cls
- val (supers', arity_clauses) = make_arity_clauses_dfg dfg thy tycons supers
+ get_helper_clauses thy is_FO full_types conjectures extra_cls
+ val (supers', arity_clauses) = make_arity_clauses thy tycons supers
val classrel_clauses = make_classrel_clauses thy subs supers'
in
(Vector.fromList clnames,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Wed Jun 23 10:05:13 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Wed Jun 23 10:20:54 2010 +0200
@@ -20,6 +20,7 @@
open Sledgehammer_Util
open Sledgehammer_Fact_Preprocessor
+open Sledgehammer_HOL_Clause
open Sledgehammer_Proof_Reconstruct
open ATP_Manager
@@ -47,8 +48,8 @@
fun string_for_outcome NONE = "Success."
| string_for_outcome (SOME failure) = string_for_failure failure
-fun sledgehammer_test_theorems (params as {full_types, ...} : params) prover
- timeout subgoal state filtered_clauses name_thms_pairs =
+fun sledgehammer_test_theorems (params : params) prover timeout subgoal state
+ filtered_clauses name_thms_pairs =
let
val num_theorems = length name_thms_pairs
val _ = priority ("Testing " ^ string_of_int num_theorems ^
@@ -88,7 +89,7 @@
(result as {outcome = NONE, ...}) => SOME result
| _ => NONE
- val {context = ctxt, facts, goal} = Proof.goal state;
+ 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
@@ -125,8 +126,7 @@
\option (e.g., \"timeout = " ^
string_of_int (10 + msecs div 1000) ^ " s\").")
| {message, ...} => (NONE, "ATP error: " ^ message))
- handle Sledgehammer_HOL_Clause.TRIVIAL =>
- (SOME [], metis_line full_types i n [])
+ handle TRIVIAL () => (SOME [], metis_line full_types i n [])
| ERROR msg => (NONE, "Error: " ^ msg)
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Wed Jun 23 10:05:13 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Wed Jun 23 10:20:54 2010 +0200
@@ -7,6 +7,7 @@
signature SLEDGEHAMMER_FACT_PREPROCESSOR =
sig
+ type cnf_thm = thm * ((string * int) * thm)
val chained_prefix: string
val trace: bool Unsynchronized.ref
val trace_msg: (unit -> string) -> unit
@@ -18,15 +19,12 @@
val multi_base_blacklist: string list
val is_theorem_bad_for_atps: thm -> bool
val type_has_topsort: typ -> bool
- val cnf_rules_pairs:
- theory -> (string * thm) list -> (thm * (string * int)) list
- val use_skolem_cache: bool Unsynchronized.ref
- (* for emergency use where the Skolem cache causes problems *)
- val strip_subgoal : thm -> int -> (string * typ) list * term list * term
+ val cnf_rules_pairs : theory -> (string * thm) list -> cnf_thm list
+ val saturate_skolem_cache: theory -> theory option
+ val auto_saturate_skolem_cache: bool Unsynchronized.ref
val neg_clausify: thm -> thm list
val neg_conjecture_clauses:
Proof.context -> thm -> int -> thm list list * (string * typ) list
- val neg_clausify_tac: Proof.context -> int -> tactic
val setup: theory -> theory
end;
@@ -35,6 +33,8 @@
open Sledgehammer_FOL_Clause
+type cnf_thm = thm * ((string * int) * thm)
+
(* Used to label theorems chained into the goal. *)
val chained_prefix = "Sledgehammer.chained_"
@@ -132,14 +132,18 @@
| dec_sko (@{const "op &"} $ p $ q) thx = dec_sko q (dec_sko p thx)
| dec_sko (@{const "op |"} $ p $ q) thx = dec_sko q (dec_sko p thx)
| dec_sko (@{const Trueprop} $ p) thx = dec_sko p thx
- | dec_sko t thx = thx
+ | dec_sko _ thx = thx
in dec_sko (prop_of th) ([], thy) end
fun mk_skolem_id t =
let val T = fastype_of t in
- Const (@{const_name skolem_id}, T --> T) $ Envir.beta_norm t
+ Const (@{const_name skolem_id}, T --> T) $ t
end
+fun quasi_beta_eta_contract (Abs (s, T, t')) =
+ Abs (s, T, quasi_beta_eta_contract t')
+ | quasi_beta_eta_contract t = Envir.beta_eta_contract t
+
(*Traverse a theorem, accumulating Skolem function definitions.*)
fun assume_skolem_funs inline s th =
let
@@ -153,10 +157,12 @@
val cT = Ts ---> T (* FIXME: use "skolem_type_and_args" *)
val id = skolem_name s (Unsynchronized.inc skolem_count) s'
val c = Free (id, cT)
- val rhs = list_abs_free (map dest_Free args,
- HOLogic.choice_const T $ body)
- |> inline ? mk_skolem_id
- (*Forms a lambda-abstraction over the formal parameters*)
+ (* Forms a lambda-abstraction over the formal parameters *)
+ val rhs =
+ list_abs_free (map dest_Free args,
+ HOLogic.choice_const T
+ $ quasi_beta_eta_contract body)
+ |> inline ? mk_skolem_id
val def = Logic.mk_equals (c, rhs)
val comb = list_comb (if inline then rhs else c, args)
in dec_sko (subst_bound (comb, p)) (def :: defs) end
@@ -167,7 +173,7 @@
| dec_sko (@{const "op &"} $ p $ q) defs = dec_sko q (dec_sko p defs)
| dec_sko (@{const "op |"} $ p $ q) defs = dec_sko q (dec_sko p defs)
| dec_sko (@{const Trueprop} $ p) defs = dec_sko p defs
- | dec_sko t defs = defs (*Do nothing otherwise*)
+ | dec_sko _ defs = defs
in dec_sko (prop_of th) [] end;
@@ -409,7 +415,6 @@
val ctxt0 = Variable.global_thm_context th
val (nnfth, ctxt) = to_nnf th ctxt0
val inline = exists_type (exists_subtype (can dest_TFree)) (prop_of nnfth)
- val inline = false (* FIXME: temporary *)
val defs = skolem_theorems_of_assume inline s nnfth
val (cnfs, ctxt) = Meson.make_cnf defs nnfth ctxt
in
@@ -447,20 +452,20 @@
(**** Translate a set of theorems into CNF ****)
-fun pair_name_cls _ (_, []) = []
- | pair_name_cls k (n, cls::clss) = (cls, (n,k)) :: pair_name_cls (k+1) (n, clss)
-
(*The combination of rev and tail recursion preserves the original order*)
fun cnf_rules_pairs thy =
let
- fun aux pairs [] = pairs
- | aux pairs ((name, th) :: ths) =
+ fun do_one _ [] = []
+ | do_one ((name, k), th) (cls :: clss) =
+ (cls, ((name, k), th)) :: do_one ((name, k + 1), th) clss
+ fun do_all pairs [] = pairs
+ | do_all pairs ((name, th) :: ths) =
let
- val new_pairs = pair_name_cls 0 (name, cnf_axiom thy th)
+ val new_pairs = do_one ((name, 0), th) (cnf_axiom thy th)
handle THM _ => [] |
CLAUSE _ => []
- in aux (new_pairs @ pairs) ths end
- in aux [] o rev end
+ in do_all (new_pairs @ pairs) ths end
+ in do_all [] o rev end
(**** Convert all facts of the theory into FOL or HOL clauses ****)
@@ -520,22 +525,12 @@
end;
-val use_skolem_cache = Unsynchronized.ref true
-
-fun clause_cache_endtheory thy =
- if !use_skolem_cache then saturate_skolem_cache thy else NONE
-
+(* For emergency use where the Skolem cache causes problems. *)
+val auto_saturate_skolem_cache = Unsynchronized.ref true
-(* The cache can be kept smaller by inspecting the prop of each thm. Can ignore
- all that are quasi-lambda-free, but then the individual theory caches become
- much bigger. *)
+fun conditionally_saturate_skolem_cache thy =
+ if !auto_saturate_skolem_cache then saturate_skolem_cache thy else NONE
-fun strip_subgoal goal i =
- let
- val (t, frees) = Logic.goal_params (prop_of goal) i
- val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees)
- val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees
- in (rev (map dest_Free frees), hyp_ts, concl_t) end
(*** Converting a subgoal into negated conjecture clauses. ***)
@@ -556,25 +551,11 @@
Subgoal.focus (Variable.set_body false ctxt) n st
in (map neg_clausify prems, map (dest_Free o term_of o #2) params) end
-(*Conversion of a subgoal to conjecture clauses. Each clause has
- leading !!-bound universal variables, to express generality. *)
-fun neg_clausify_tac ctxt =
- neg_skolemize_tac ctxt THEN'
- SUBGOAL (fn (prop, i) =>
- let val ts = Logic.strip_assums_hyp prop in
- EVERY'
- [Subgoal.FOCUS
- (fn {prems, ...} =>
- (Method.insert_tac
- (map forall_intr_vars (maps neg_clausify prems)) i)) ctxt,
- REPEAT_DETERM_N (length ts) o etac thin_rl] i
- end);
-
(** setup **)
val setup =
- perhaps saturate_skolem_cache
- #> Theory.at_end clause_cache_endtheory
+ perhaps conditionally_saturate_skolem_cache
+ #> Theory.at_end conditionally_saturate_skolem_cache
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Wed Jun 23 10:05:13 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Wed Jun 23 10:20:54 2010 +0200
@@ -10,11 +10,11 @@
signature SLEDGEHAMMER_FOL_CLAUSE =
sig
+ val type_wrapper_name : string
val schematic_var_prefix: string
val fixed_var_prefix: string
val tvar_prefix: string
val tfree_prefix: string
- val clause_prefix: string
val const_prefix: string
val tconst_prefix: string
val class_prefix: string
@@ -23,13 +23,12 @@
val type_const_trans_table: string Symtab.table
val ascii_of: string -> string
val undo_ascii_of: string -> string
- val paren_pack : string list -> string
val make_schematic_var : string * int -> string
val make_fixed_var : string -> string
val make_schematic_type_var : string * int -> string
val make_fixed_type_var : string -> string
- val make_fixed_const : bool -> string -> string
- val make_fixed_type_const : bool -> string -> string
+ val make_fixed_const : string -> string
+ val make_fixed_type_const : string -> string
val make_type_class : string -> string
type name = string * string
type name_pool = string Symtab.table * string Symtab.table
@@ -37,56 +36,20 @@
val pool_map : ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
val nice_name : name -> name_pool option -> string * name_pool option
datatype kind = Axiom | Conjecture
- type axiom_name = string
- datatype fol_type =
- TyVar of name |
- TyFree of name |
- TyConstr of name * fol_type list
- val string_of_fol_type :
- fol_type -> name_pool option -> string * name_pool option
datatype type_literal =
TyLitVar of string * name |
TyLitFree of string * name
exception CLAUSE of string * term
val type_literals_for_types : typ list -> type_literal list
- val get_tvar_strs: typ list -> string list
datatype arLit =
TConsLit of class * string * string list
| TVarLit of class * string
datatype arity_clause = ArityClause of
- {axiom_name: axiom_name, conclLit: arLit, premLits: arLit list}
+ {axiom_name: string, conclLit: arLit, premLits: arLit list}
datatype classrel_clause = ClassrelClause of
- {axiom_name: axiom_name, subclass: class, superclass: class}
+ {axiom_name: string, subclass: class, superclass: class}
val make_classrel_clauses: theory -> class list -> class list -> classrel_clause list
- val make_arity_clauses_dfg: bool -> theory -> string list -> class list -> class list * arity_clause list
val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list
- val add_type_sort_preds: typ -> int Symtab.table -> int Symtab.table
- val add_classrel_clause_preds :
- classrel_clause -> int Symtab.table -> int Symtab.table
- val class_of_arityLit: arLit -> class
- val add_arity_clause_preds: arity_clause -> int Symtab.table -> int Symtab.table
- val add_fol_type_funcs: fol_type -> int Symtab.table -> int Symtab.table
- val add_arity_clause_funcs:
- arity_clause -> int Symtab.table -> int Symtab.table
- val init_functab: int Symtab.table
- val dfg_sign: bool -> string -> string
- val dfg_of_type_literal: bool -> type_literal -> string
- val gen_dfg_cls: int * string * kind * string list * string list * string list -> string
- val string_of_preds: (string * Int.int) list -> string
- val string_of_funcs: (string * int) list -> string
- val string_of_symbols: string -> string -> string
- val string_of_start: string -> string
- val string_of_descrip : string -> string
- val dfg_tfree_clause : string -> string
- val dfg_classrel_clause: classrel_clause -> string
- val dfg_arity_clause: arity_clause -> string
- val tptp_sign: bool -> string -> string
- val tptp_of_type_literal :
- bool -> type_literal -> name_pool option -> string * name_pool option
- val gen_tptp_cls : int * string * kind * string list * string list -> string
- val tptp_tfree_clause : string -> string
- val tptp_arity_clause : arity_clause -> string
- val tptp_classrel_clause : classrel_clause -> string
end
structure Sledgehammer_FOL_Clause : SLEDGEHAMMER_FOL_CLAUSE =
@@ -94,15 +57,15 @@
open Sledgehammer_Util
+val type_wrapper_name = "ti"
+
val schematic_var_prefix = "V_";
val fixed_var_prefix = "v_";
val tvar_prefix = "T_";
val tfree_prefix = "t_";
-val clause_prefix = "cls_";
-val arclause_prefix = "clsarity_"
-val clrelclause_prefix = "clsrel_";
+val classrel_clause_prefix = "clsrel_";
val const_prefix = "c_";
val tconst_prefix = "tc_";
@@ -175,12 +138,6 @@
val undo_ascii_of = undo_ascii_aux [] o String.explode;
-(* convert a list of strings into one single string; surrounded by brackets *)
-fun paren_pack [] = "" (*empty argument list*)
- | paren_pack strings = "(" ^ commas strings ^ ")";
-
-fun tptp_clause strings = "(" ^ space_implode " | " strings ^ ")"
-
(*Remove the initial ' character from a type variable, if it is present*)
fun trim_type_var s =
if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)
@@ -196,31 +153,21 @@
tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
-val max_dfg_symbol_length = 63
-
-(* HACK because SPASS 3.0 truncates identifiers to 63 characters. *)
-fun controlled_length dfg s =
- if dfg andalso size s > max_dfg_symbol_length then
- String.extract (s, 0, SOME (max_dfg_symbol_length div 2 - 1)) ^ "__" ^
- String.extract (s, size s - max_dfg_symbol_length div 2 + 1, NONE)
- else
- s
+fun lookup_const c =
+ case Symtab.lookup const_trans_table c of
+ SOME c' => c'
+ | NONE => ascii_of c
-fun lookup_const dfg c =
- case Symtab.lookup const_trans_table c of
- SOME c' => c'
- | NONE => controlled_length dfg (ascii_of c);
-
-fun lookup_type_const dfg c =
- case Symtab.lookup type_const_trans_table c of
- SOME c' => c'
- | NONE => controlled_length dfg (ascii_of c);
+fun lookup_type_const c =
+ case Symtab.lookup type_const_trans_table c of
+ SOME c' => c'
+ | NONE => ascii_of c
(* "op =" MUST BE "equal" because it's built into ATPs. *)
-fun make_fixed_const _ (@{const_name "op ="}) = "equal"
- | make_fixed_const dfg c = const_prefix ^ lookup_const dfg c;
+fun make_fixed_const @{const_name "op ="} = "equal"
+ | make_fixed_const c = const_prefix ^ lookup_const c
-fun make_fixed_type_const dfg c = tconst_prefix ^ lookup_type_const dfg c;
+fun make_fixed_type_const c = tconst_prefix ^ lookup_type_const c
fun make_type_class clas = class_prefix ^ ascii_of clas;
@@ -287,28 +234,12 @@
the_pool
|> apsnd SOME
-(**** Definitions and functions for FOL clauses, for conversion to TPTP or DFG
- format ****)
+(**** Definitions and functions for FOL clauses for TPTP format output ****)
datatype kind = Axiom | Conjecture;
-type axiom_name = string;
-
(**** Isabelle FOL clauses ****)
-datatype fol_type =
- TyVar of name |
- TyFree of name |
- TyConstr of name * fol_type list
-
-fun string_of_fol_type (TyVar sp) pool = nice_name sp pool
- | string_of_fol_type (TyFree sp) pool = nice_name sp pool
- | string_of_fol_type (TyConstr (sp, tys)) pool =
- let
- val (s, pool) = nice_name sp pool
- val (ss, pool) = pool_map string_of_fol_type tys pool
- in (s ^ paren_pack ss, pool) end
-
(* The first component is the type class; the second is a TVar or TFree. *)
datatype type_literal =
TyLitVar of string * name |
@@ -329,39 +260,19 @@
fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s)
| sorts_on_typs (TVar (v,s)) = sorts_on_typs_aux (v,s);
-fun pred_of_sort (TyLitVar (s, _)) = (s, 1)
- | pred_of_sort (TyLitFree (s, _)) = (s, 1)
-
(*Given a list of sorted type variables, return a list of type literals.*)
fun type_literals_for_types Ts =
fold (union (op =)) (map sorts_on_typs Ts) []
-(*The correct treatment of TFrees like 'a in lemmas (axiom clauses) is not clear.
- * Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a
- in a lemma has the same sort as 'a in the conjecture.
- * Deleting such clauses will lead to problems with locales in other use of local results
- where 'a is fixed. Probably we should delete clauses unless the sorts agree.
- * Currently we include a class constraint in the clause, exactly as with TVars.
-*)
-
(** make axiom and conjecture clauses. **)
-fun get_tvar_strs [] = []
- | get_tvar_strs ((TVar (indx,s))::Ts) =
- insert (op =) (make_schematic_type_var indx) (get_tvar_strs Ts)
- | get_tvar_strs((TFree _)::Ts) = get_tvar_strs Ts
-
-
-
(**** Isabelle arities ****)
datatype arLit = TConsLit of class * string * string list
| TVarLit of class * string;
datatype arity_clause =
- ArityClause of {axiom_name: axiom_name,
- conclLit: arLit,
- premLits: arLit list};
+ ArityClause of {axiom_name: string, conclLit: arLit, premLits: arLit list}
fun gen_TVars 0 = []
@@ -372,25 +283,23 @@
| pack_sort(tvar, cls::srt) = (cls, tvar) :: pack_sort(tvar, srt);
(*Arity of type constructor tcon :: (arg1,...,argN)res*)
-fun make_axiom_arity_clause dfg (tcons, axiom_name, (cls,args)) =
+fun make_axiom_arity_clause (tcons, axiom_name, (cls,args)) =
let val tvars = gen_TVars (length args)
val tvars_srts = ListPair.zip (tvars,args)
in
- ArityClause {axiom_name = axiom_name,
- conclLit = TConsLit (cls, make_fixed_type_const dfg tcons, tvars),
- premLits = map TVarLit (union_all(map pack_sort tvars_srts))}
+ ArityClause {axiom_name = axiom_name,
+ conclLit = TConsLit (cls, make_fixed_type_const tcons, tvars),
+ premLits = map TVarLit (union_all(map pack_sort tvars_srts))}
end;
(**** Isabelle class relations ****)
datatype classrel_clause =
- ClassrelClause of {axiom_name: axiom_name,
- subclass: class,
- superclass: class};
+ ClassrelClause of {axiom_name: string, subclass: class, superclass: class}
(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
-fun class_pairs thy [] supers = []
+fun class_pairs _ [] _ = []
| class_pairs thy subs supers =
let
val class_less = Sorts.class_less (Sign.classes_of thy)
@@ -399,7 +308,8 @@
in fold add_supers subs [] end
fun make_classrel_clause (sub,super) =
- ClassrelClause {axiom_name = clrelclause_prefix ^ ascii_of sub ^ "_" ^ ascii_of super,
+ ClassrelClause {axiom_name = classrel_clause_prefix ^ ascii_of sub ^ "_" ^
+ ascii_of super,
subclass = make_type_class sub,
superclass = make_type_class super};
@@ -409,20 +319,20 @@
(** Isabelle arities **)
-fun arity_clause dfg _ _ (tcons, []) = []
- | arity_clause dfg seen n (tcons, ("HOL.type",_)::ars) = (*ignore*)
- arity_clause dfg seen n (tcons,ars)
- | arity_clause dfg seen n (tcons, (ar as (class,_)) :: ars) =
+fun arity_clause _ _ (_, []) = []
+ | arity_clause seen n (tcons, ("HOL.type",_)::ars) = (*ignore*)
+ arity_clause seen n (tcons,ars)
+ | arity_clause seen n (tcons, (ar as (class,_)) :: ars) =
if member (op =) seen class then (*multiple arities for the same tycon, class pair*)
- make_axiom_arity_clause dfg (tcons, lookup_type_const dfg tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) ::
- arity_clause dfg seen (n+1) (tcons,ars)
+ make_axiom_arity_clause (tcons, lookup_type_const tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) ::
+ arity_clause seen (n+1) (tcons,ars)
else
- make_axiom_arity_clause dfg (tcons, lookup_type_const dfg tcons ^ "_" ^ class, ar) ::
- arity_clause dfg (class::seen) n (tcons,ars)
+ make_axiom_arity_clause (tcons, lookup_type_const tcons ^ "_" ^ class, ar) ::
+ arity_clause (class::seen) n (tcons,ars)
-fun multi_arity_clause dfg [] = []
- | multi_arity_clause dfg ((tcons, ars) :: tc_arlists) =
- arity_clause dfg [] 1 (tcons, ars) @ multi_arity_clause dfg tc_arlists
+fun multi_arity_clause [] = []
+ | multi_arity_clause ((tcons, ars) :: tc_arlists) =
+ arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy
provided its arguments have the corresponding sorts.*)
@@ -436,7 +346,7 @@
in map try_classes tycons end;
(*Proving one (tycon, class) membership may require proving others, so iterate.*)
-fun iter_type_class_pairs thy tycons [] = ([], [])
+fun iter_type_class_pairs _ _ [] = ([], [])
| iter_type_class_pairs thy tycons classes =
let val cpairs = type_class_pairs thy tycons classes
val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs)))
@@ -444,165 +354,8 @@
val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
in (union (op =) classes' classes, union (op =) cpairs' cpairs) end;
-fun make_arity_clauses_dfg dfg thy tycons classes =
+fun make_arity_clauses thy tycons classes =
let val (classes', cpairs) = iter_type_class_pairs thy tycons classes
- in (classes', multi_arity_clause dfg cpairs) end;
-val make_arity_clauses = make_arity_clauses_dfg false;
-
-(**** Find occurrences of predicates in clauses ****)
-
-(*FIXME: multiple-arity checking doesn't work, as update_new is the wrong
- function (it flags repeated declarations of a function, even with the same arity)*)
-
-fun update_many keypairs = fold Symtab.update keypairs
-
-val add_type_sort_preds = update_many o map pred_of_sort o sorts_on_typs
-
-fun add_classrel_clause_preds (ClassrelClause {subclass, superclass, ...}) =
- Symtab.update (subclass, 1) #> Symtab.update (superclass, 1)
-
-fun class_of_arityLit (TConsLit (tclass, _, _)) = tclass
- | class_of_arityLit (TVarLit (tclass, _)) = tclass;
-
-fun add_arity_clause_preds (ArityClause {conclLit, premLits, ...}) =
- let
- val classes = map (make_type_class o class_of_arityLit)
- (conclLit :: premLits)
- in fold (Symtab.update o rpair 1) classes end;
-
-(*** Find occurrences of functions in clauses ***)
-
-fun add_fol_type_funcs (TyVar _) = I
- | add_fol_type_funcs (TyFree (s, _)) = Symtab.update (s, 0)
- | add_fol_type_funcs (TyConstr ((s, _), tys)) =
- Symtab.update (s, length tys) #> fold add_fol_type_funcs tys
-
-(*TFrees are recorded as constants*)
-fun add_type_sort_funcs (TVar _, funcs) = funcs
- | add_type_sort_funcs (TFree (a, _), funcs) =
- Symtab.update (make_fixed_type_var a, 0) funcs
-
-fun add_arity_clause_funcs (ArityClause {conclLit,...}) funcs =
- let val TConsLit (_, tcons, tvars) = conclLit
- in Symtab.update (tcons, length tvars) funcs end;
-
-(*This type can be overlooked because it is built-in...*)
-val init_functab = Symtab.update ("tc_itself", 1) Symtab.empty;
-
-
-(**** String-oriented operations ****)
-
-fun string_of_clausename (cls_id,ax_name) =
- clause_prefix ^ ascii_of ax_name ^ "_" ^ Int.toString cls_id;
-
-fun string_of_type_clsname (cls_id,ax_name,idx) =
- string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx);
-
-
-(**** Producing DFG files ****)
-
-(*Attach sign in DFG syntax: false means negate.*)
-fun dfg_sign true s = s
- | dfg_sign false s = "not(" ^ s ^ ")"
-
-fun dfg_of_type_literal pos (TyLitVar (s, (s', _))) =
- dfg_sign pos (s ^ "(" ^ s' ^ ")")
- | dfg_of_type_literal pos (TyLitFree (s, (s', _))) =
- dfg_sign pos (s ^ "(" ^ s' ^ ")");
-
-(*Enclose the clause body by quantifiers, if necessary*)
-fun dfg_forall [] body = body
- | dfg_forall vars body = "forall([" ^ commas vars ^ "],\n" ^ body ^ ")"
-
-fun gen_dfg_cls (cls_id, ax_name, Axiom, lits, tylits, vars) =
- "clause( %(axiom)\n" ^
- dfg_forall vars ("or(" ^ commas (tylits@lits) ^ ")") ^ ",\n" ^
- string_of_clausename (cls_id,ax_name) ^ ").\n\n"
- | gen_dfg_cls (cls_id, ax_name, Conjecture, lits, _, vars) =
- "clause( %(negated_conjecture)\n" ^
- dfg_forall vars ("or(" ^ commas lits ^ ")") ^ ",\n" ^
- string_of_clausename (cls_id,ax_name) ^ ").\n\n";
-
-fun string_of_arity (name, arity) = "(" ^ name ^ ", " ^ Int.toString arity ^ ")"
-
-fun string_of_preds [] = ""
- | string_of_preds preds = "predicates[" ^ commas(map string_of_arity preds) ^ "].\n";
-
-fun string_of_funcs [] = ""
- | string_of_funcs funcs = "functions[" ^ commas(map string_of_arity funcs) ^ "].\n" ;
-
-fun string_of_symbols predstr funcstr =
- "list_of_symbols.\n" ^ predstr ^ funcstr ^ "end_of_list.\n\n";
-
-fun string_of_start name = "begin_problem(" ^ name ^ ").\n\n";
-
-fun string_of_descrip name =
- "list_of_descriptions.\nname({*" ^ name ^
- "*}).\nauthor({*Isabelle*}).\nstatus(unknown).\ndescription({*auto-generated*}).\nend_of_list.\n\n"
-
-fun dfg_tfree_clause tfree_lit =
- "clause( %(negated_conjecture)\n" ^ "or( " ^ tfree_lit ^ "),\n" ^ "tfree_tcs" ^ ").\n\n"
-
-fun dfg_of_arLit (TConsLit (c,t,args)) =
- dfg_sign true (make_type_class c ^ "(" ^ t ^ paren_pack args ^ ")")
- | dfg_of_arLit (TVarLit (c,str)) =
- dfg_sign false (make_type_class c ^ "(" ^ str ^ ")")
-
-fun dfg_classrelLits sub sup = "not(" ^ sub ^ "(T)), " ^ sup ^ "(T)";
-
-fun dfg_classrel_clause (ClassrelClause {axiom_name,subclass,superclass,...}) =
- "clause(forall([T],\nor( " ^ dfg_classrelLits subclass superclass ^ ")),\n" ^
- axiom_name ^ ").\n\n";
-
-fun string_of_ar axiom_name = arclause_prefix ^ ascii_of axiom_name;
-
-fun dfg_arity_clause (ArityClause{axiom_name,conclLit,premLits,...}) =
- let val TConsLit (_,_,tvars) = conclLit
- val lits = map dfg_of_arLit (conclLit :: premLits)
- in
- "clause( %(axiom)\n" ^
- dfg_forall tvars ("or( " ^ commas lits ^ ")") ^ ",\n" ^
- string_of_ar axiom_name ^ ").\n\n"
- end;
-
-
-(**** Produce TPTP files ****)
-
-fun tptp_sign true s = s
- | tptp_sign false s = "~ " ^ s
-
-fun tptp_of_type_literal pos (TyLitVar (s, name)) =
- nice_name name #>> (fn s' => tptp_sign pos (s ^ "(" ^ s' ^ ")"))
- | tptp_of_type_literal pos (TyLitFree (s, name)) =
- nice_name name #>> (fn s' => tptp_sign pos (s ^ "(" ^ s' ^ ")"))
-
-fun tptp_cnf name kind formula =
- "cnf(" ^ name ^ ", " ^ kind ^ ",\n " ^ formula ^ ").\n"
-
-fun gen_tptp_cls (cls_id, ax_name, Axiom, lits, tylits) =
- tptp_cnf (string_of_clausename (cls_id, ax_name)) "axiom"
- (tptp_clause (tylits @ lits))
- | gen_tptp_cls (cls_id, ax_name, Conjecture, lits, _) =
- tptp_cnf (string_of_clausename (cls_id, ax_name)) "negated_conjecture"
- (tptp_clause lits)
-
-fun tptp_tfree_clause tfree_lit =
- tptp_cnf "tfree_tcs" "negated_conjecture" (tptp_clause [tfree_lit])
-
-fun tptp_of_arLit (TConsLit (c,t,args)) =
- tptp_sign true (make_type_class c ^ "(" ^ t ^ paren_pack args ^ ")")
- | tptp_of_arLit (TVarLit (c,str)) =
- tptp_sign false (make_type_class c ^ "(" ^ str ^ ")")
-
-fun tptp_arity_clause (ArityClause{axiom_name,conclLit,premLits,...}) =
- tptp_cnf (string_of_ar axiom_name) "axiom"
- (tptp_clause (map tptp_of_arLit (conclLit :: premLits)))
-
-fun tptp_classrelLits sub sup =
- let val tvar = "(T)"
- in tptp_clause [tptp_sign false (sub^tvar), tptp_sign true (sup^tvar)] end;
-
-fun tptp_classrel_clause (ClassrelClause {axiom_name,subclass,superclass,...}) =
- tptp_cnf axiom_name "axiom" (tptp_classrelLits subclass superclass)
+ in (classes', multi_arity_clause cpairs) end;
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Wed Jun 23 10:05:13 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Wed Jun 23 10:20:54 2010 +0200
@@ -2,49 +2,40 @@
Author: Jia Meng, NICTA
Author: Jasmin Blanchette, TU Muenchen
-FOL clauses translated from HOL formulae.
+FOL clauses translated from HOL formulas.
*)
signature SLEDGEHAMMER_HOL_CLAUSE =
sig
+ type cnf_thm = Sledgehammer_Fact_Preprocessor.cnf_thm
type name = Sledgehammer_FOL_Clause.name
type name_pool = Sledgehammer_FOL_Clause.name_pool
type kind = Sledgehammer_FOL_Clause.kind
- type fol_type = Sledgehammer_FOL_Clause.fol_type
type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
type arity_clause = Sledgehammer_FOL_Clause.arity_clause
- type axiom_name = string
type polarity = bool
- type hol_clause_id = int
+ datatype combtyp =
+ TyVar of name |
+ TyFree of name |
+ TyConstr of name * combtyp list
datatype combterm =
- CombConst of name * fol_type * fol_type list (* Const and Free *) |
- CombVar of name * fol_type |
+ CombConst of name * combtyp * combtyp list (* Const and Free *) |
+ CombVar of name * combtyp |
CombApp of combterm * combterm
datatype literal = Literal of polarity * combterm
datatype hol_clause =
- HOLClause of {clause_id: hol_clause_id, axiom_name: axiom_name, th: thm,
- kind: kind, literals: literal list, ctypes_sorts: typ list}
+ HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
+ literals: literal list, ctypes_sorts: typ list}
- val type_of_combterm : combterm -> fol_type
+ val type_of_combterm : combterm -> combtyp
val strip_combterm_comb : combterm -> combterm * combterm list
val literals_of_term : theory -> term -> literal list * typ list
val conceal_skolem_somes :
int -> (string * term) list -> term -> (string * term) list * term
- exception TRIVIAL
- val make_conjecture_clauses : bool -> theory -> thm list -> hol_clause list
- val make_axiom_clauses : bool -> theory ->
- (thm * (axiom_name * hol_clause_id)) list -> (axiom_name * hol_clause) list
- val type_wrapper_name : string
- val get_helper_clauses :
- bool -> theory -> bool -> bool -> hol_clause list
- -> (thm * (axiom_name * hol_clause_id)) list -> hol_clause list
- val write_tptp_file : bool -> bool -> bool -> Path.T ->
- hol_clause list * hol_clause list * hol_clause list * hol_clause list *
- classrel_clause list * arity_clause list -> name_pool option * int
- val write_dfg_file : bool -> bool -> Path.T ->
- hol_clause list * hol_clause list * hol_clause list * hol_clause list *
- classrel_clause list * arity_clause list -> name_pool option * int
+ exception TRIVIAL of unit
+ val make_conjecture_clauses : theory -> thm list -> hol_clause list
+ val make_axiom_clauses : theory -> cnf_thm list -> (string * hol_clause) list
end
structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE =
@@ -54,39 +45,46 @@
open Sledgehammer_FOL_Clause
open Sledgehammer_Fact_Preprocessor
-fun min_arity_of const_min_arity c =
- the_default 0 (Symtab.lookup const_min_arity c)
-
-(*True if the constant ever appears outside of the top-level position in literals.
- If false, the constant always receives all of its arguments and is used as a predicate.*)
-fun needs_hBOOL explicit_apply const_needs_hBOOL c =
- explicit_apply orelse the_default false (Symtab.lookup const_needs_hBOOL c)
-
-
(******************************************************)
(* data types for typed combinator expressions *)
(******************************************************)
-type axiom_name = string;
-type polarity = bool;
-type hol_clause_id = int;
+type polarity = bool
+
+datatype combtyp =
+ TyVar of name |
+ TyFree of name |
+ TyConstr of name * combtyp list
datatype combterm =
- CombConst of name * fol_type * fol_type list (* Const and Free *) |
- CombVar of name * fol_type |
+ CombConst of name * combtyp * combtyp list (* Const and Free *) |
+ CombVar of name * combtyp |
CombApp of combterm * combterm
datatype literal = Literal of polarity * combterm;
datatype hol_clause =
- HOLClause of {clause_id: hol_clause_id, axiom_name: axiom_name, th: thm,
- kind: kind, literals: literal list, ctypes_sorts: typ list};
-
+ HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
+ literals: literal list, ctypes_sorts: typ list}
(*********************************************************************)
(* convert a clause with type Term.term to a clause with type clause *)
(*********************************************************************)
+(*Result of a function type; no need to check that the argument type matches.*)
+fun result_type (TyConstr (_, [_, tp2])) = tp2
+ | result_type _ = raise Fail "non-function type"
+
+fun type_of_combterm (CombConst (_, tp, _)) = tp
+ | type_of_combterm (CombVar (_, tp)) = tp
+ | type_of_combterm (CombApp (t1, _)) = result_type (type_of_combterm t1)
+
+(*gets the head of a combinator application, along with the list of arguments*)
+fun strip_combterm_comb u =
+ let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
+ | stripc x = x
+ in stripc(u,[]) end
+
fun isFalse (Literal (pol, CombConst ((c, _), _, _))) =
(pol andalso c = "c_False") orelse (not pol andalso c = "c_True")
| isFalse _ = false;
@@ -98,65 +96,65 @@
fun isTaut (HOLClause {literals,...}) = exists isTrue literals;
-fun type_of dfg (Type (a, Ts)) =
- let val (folTypes,ts) = types_of dfg Ts in
- (TyConstr (`(make_fixed_type_const dfg) a, folTypes), ts)
+fun type_of (Type (a, Ts)) =
+ let val (folTypes,ts) = types_of Ts in
+ (TyConstr (`make_fixed_type_const a, folTypes), ts)
end
- | type_of _ (tp as TFree (a, _)) = (TyFree (`make_fixed_type_var a), [tp])
- | type_of _ (tp as TVar (x, _)) =
+ | type_of (tp as TFree (a, _)) = (TyFree (`make_fixed_type_var a), [tp])
+ | type_of (tp as TVar (x, _)) =
(TyVar (make_schematic_type_var x, string_of_indexname x), [tp])
-and types_of dfg Ts =
- let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts)
- in (folTyps, union_all ts) end;
+and types_of Ts =
+ let val (folTyps, ts) = ListPair.unzip (map type_of Ts) in
+ (folTyps, union_all ts)
+ end
(* same as above, but no gathering of sort information *)
-fun simp_type_of dfg (Type (a, Ts)) =
- TyConstr (`(make_fixed_type_const dfg) a, map (simp_type_of dfg) Ts)
- | simp_type_of _ (TFree (a, _)) = TyFree (`make_fixed_type_var a)
- | simp_type_of _ (TVar (x, _)) =
- TyVar (make_schematic_type_var x, string_of_indexname x);
-
+fun simp_type_of (Type (a, Ts)) =
+ TyConstr (`make_fixed_type_const a, map simp_type_of Ts)
+ | simp_type_of (TFree (a, _)) = TyFree (`make_fixed_type_var a)
+ | simp_type_of (TVar (x, _)) =
+ TyVar (make_schematic_type_var x, string_of_indexname x)
(* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
-fun combterm_of dfg thy (Const (c, T)) =
+fun combterm_of thy (Const (c, T)) =
let
- val (tp, ts) = type_of dfg T
+ val (tp, ts) = type_of T
val tvar_list =
(if String.isPrefix skolem_theory_name c then
[] |> Term.add_tvarsT T |> map TVar
else
(c, T) |> Sign.const_typargs thy)
- |> map (simp_type_of dfg)
- val c' = CombConst (`(make_fixed_const dfg) c, tp, tvar_list)
+ |> map simp_type_of
+ val c' = CombConst (`make_fixed_const c, tp, tvar_list)
in (c',ts) end
- | combterm_of dfg _ (Free(v, T)) =
- let val (tp,ts) = type_of dfg T
+ | combterm_of _ (Free(v, T)) =
+ let val (tp,ts) = type_of T
val v' = CombConst (`make_fixed_var v, tp, [])
in (v',ts) end
- | combterm_of dfg _ (Var(v, T)) =
- let val (tp,ts) = type_of dfg T
+ | combterm_of _ (Var(v, T)) =
+ let val (tp,ts) = type_of T
val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp)
in (v',ts) end
- | combterm_of dfg thy (P $ Q) =
- let val (P',tsP) = combterm_of dfg thy P
- val (Q',tsQ) = combterm_of dfg thy Q
- in (CombApp(P',Q'), union (op =) tsP tsQ) end
- | combterm_of _ _ (t as Abs _) = raise CLAUSE ("HOL clause", t);
-
-fun predicate_of dfg thy ((@{const Not} $ P), polarity) = predicate_of dfg thy (P, not polarity)
- | predicate_of dfg thy (t,polarity) = (combterm_of dfg thy (Envir.eta_contract t), polarity);
+ | combterm_of thy (P $ Q) =
+ let val (P', tsP) = combterm_of thy P
+ val (Q', tsQ) = combterm_of thy Q
+ in (CombApp (P', Q'), union (op =) tsP tsQ) end
+ | combterm_of _ (t as Abs _) = raise CLAUSE ("HOL clause", t)
-fun literals_of_term1 dfg thy args (@{const Trueprop} $ P) = literals_of_term1 dfg thy args P
- | literals_of_term1 dfg thy args (@{const "op |"} $ P $ Q) =
- literals_of_term1 dfg thy (literals_of_term1 dfg thy args P) Q
- | literals_of_term1 dfg thy (lits,ts) P =
- let val ((pred,ts'),pol) = predicate_of dfg thy (P,true)
- in
- (Literal(pol,pred)::lits, union (op =) ts ts')
- end;
+fun predicate_of thy ((@{const Not} $ P), polarity) =
+ predicate_of thy (P, not polarity)
+ | predicate_of thy (t, polarity) =
+ (combterm_of thy (Envir.eta_contract t), polarity)
-fun literals_of_term_dfg dfg thy P = literals_of_term1 dfg thy ([],[]) P;
-val literals_of_term = literals_of_term_dfg false;
+fun literals_of_term1 args thy (@{const Trueprop} $ P) =
+ literals_of_term1 args thy P
+ | literals_of_term1 args thy (@{const "op |"} $ P $ Q) =
+ literals_of_term1 (literals_of_term1 args thy P) thy Q
+ | literals_of_term1 (lits, ts) thy P =
+ let val ((pred, ts'), pol) = predicate_of thy (P, true) in
+ (Literal (pol, pred) :: lits, union (op =) ts ts')
+ end
+val literals_of_term = literals_of_term1 ([], [])
fun skolem_name i j num_T_args =
skolem_prefix ^ (space_implode "_" (map Int.toString [i, j, num_T_args])) ^
@@ -195,438 +193,39 @@
(skolem_somes, t)
(* Trivial problem, which resolution cannot handle (empty clause) *)
-exception TRIVIAL;
+exception TRIVIAL of unit
(* making axiom and conjecture clauses *)
-fun make_clause dfg thy (clause_id, axiom_name, kind, th) skolem_somes =
+fun make_clause thy (clause_id, axiom_name, kind, th) skolem_somes =
let
val (skolem_somes, t) =
th |> prop_of |> conceal_skolem_somes clause_id skolem_somes
- val (lits, ctypes_sorts) = literals_of_term_dfg dfg thy t
+ val (lits, ctypes_sorts) = literals_of_term thy t
in
if forall isFalse lits then
- raise TRIVIAL
+ raise TRIVIAL ()
else
(skolem_somes,
HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,
kind = kind, literals = lits, ctypes_sorts = ctypes_sorts})
end
-fun add_axiom_clause dfg thy (th, (name, id)) (skolem_somes, clss) =
+fun add_axiom_clause thy (th, ((name, id), _ : thm)) (skolem_somes, clss) =
let
- val (skolem_somes, cls) =
- make_clause dfg thy (id, name, Axiom, th) skolem_somes
+ val (skolem_somes, cls) = make_clause thy (id, name, Axiom, th) skolem_somes
in (skolem_somes, clss |> not (isTaut cls) ? cons (name, cls)) end
-fun make_axiom_clauses dfg thy clauses =
- ([], []) |> fold (add_axiom_clause dfg thy) clauses |> snd
+fun make_axiom_clauses thy clauses =
+ ([], []) |> fold (add_axiom_clause thy) clauses |> snd
-fun make_conjecture_clauses dfg thy =
+fun make_conjecture_clauses thy =
let
fun aux _ _ [] = []
| aux n skolem_somes (th :: ths) =
let
val (skolem_somes, cls) =
- make_clause dfg thy (n, "conjecture", Conjecture, th) skolem_somes
+ make_clause thy (n, "conjecture", Conjecture, th) skolem_somes
in cls :: aux (n + 1) skolem_somes ths end
in aux 0 [] end
-(**********************************************************************)
-(* convert clause into ATP specific formats: *)
-(* TPTP used by Vampire and E *)
-(* DFG used by SPASS *)
-(**********************************************************************)
-
-(*Result of a function type; no need to check that the argument type matches.*)
-fun result_type (TyConstr (_, [_, tp2])) = tp2
- | result_type _ = raise Fail "non-function type"
-
-fun type_of_combterm (CombConst (_, tp, _)) = tp
- | type_of_combterm (CombVar (_, tp)) = tp
- | type_of_combterm (CombApp (t1, _)) = result_type (type_of_combterm t1);
-
-(*gets the head of a combinator application, along with the list of arguments*)
-fun strip_combterm_comb u =
- let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
- | stripc x = x
- in stripc(u,[]) end;
-
-val type_wrapper_name = "ti"
-
-fun head_needs_hBOOL explicit_apply const_needs_hBOOL
- (CombConst ((c, _), _, _)) =
- needs_hBOOL explicit_apply const_needs_hBOOL c
- | head_needs_hBOOL _ _ _ = true
-
-fun wrap_type full_types (s, ty) pool =
- if full_types then
- let val (s', pool) = string_of_fol_type ty pool in
- (type_wrapper_name ^ paren_pack [s, s'], pool)
- end
- else
- (s, pool)
-
-fun wrap_type_if full_types explicit_apply cnh (head, s, tp) =
- if head_needs_hBOOL explicit_apply cnh head then
- wrap_type full_types (s, tp)
- else
- pair s
-
-fun apply ss = "hAPP" ^ paren_pack ss;
-
-fun rev_apply (v, []) = v
- | rev_apply (v, arg::args) = apply [rev_apply (v, args), arg];
-
-fun string_apply (v, args) = rev_apply (v, rev args);
-
-(* Apply an operator to the argument strings, using either the "apply" operator
- or direct function application. *)
-fun string_of_application full_types cma (CombConst ((s, s'), _, tvars), args)
- pool =
- let
- val s = if s = "equal" then "c_fequal" else s
- val nargs = min_arity_of cma s
- val args1 = List.take (args, nargs)
- handle Subscript =>
- raise Fail (quote s ^ " has arity " ^ Int.toString nargs ^
- " but is applied to " ^ commas (map quote args))
- val args2 = List.drop (args, nargs)
- val (targs, pool) = if full_types then ([], pool)
- else pool_map string_of_fol_type tvars pool
- val (s, pool) = nice_name (s, s') pool
- in (string_apply (s ^ paren_pack (args1 @ targs), args2), pool) end
- | string_of_application _ _ (CombVar (name, _), args) pool =
- nice_name name pool |>> (fn s => string_apply (s, args))
-
-fun string_of_combterm (params as (full_types, explicit_apply, cma, cnh)) t
- pool =
- let
- val (head, args) = strip_combterm_comb t
- val (ss, pool) = pool_map (string_of_combterm params) args pool
- val (s, pool) = string_of_application full_types cma (head, ss) pool
- in
- wrap_type_if full_types explicit_apply cnh (head, s, type_of_combterm t)
- pool
- end
-
-(*Boolean-valued terms are here converted to literals.*)
-fun boolify params c =
- string_of_combterm params c #>> prefix "hBOOL" o paren_pack o single
-
-fun string_of_predicate (params as (_, explicit_apply, _, cnh)) t =
- case t of
- (CombApp (CombApp (CombConst (("equal", _), _, _), t1), t2)) =>
- (* DFG only: new TPTP prefers infix equality *)
- pool_map (string_of_combterm params) [t1, t2]
- #>> prefix "equal" o paren_pack
- | _ =>
- case #1 (strip_combterm_comb t) of
- CombConst ((s, _), _, _) =>
- (if needs_hBOOL explicit_apply cnh s then boolify else string_of_combterm)
- params t
- | _ => boolify params t
-
-
-(*** TPTP format ***)
-
-fun tptp_of_equality params pos (t1, t2) =
- pool_map (string_of_combterm params) [t1, t2]
- #>> space_implode (if pos then " = " else " != ")
-
-fun tptp_literal params
- (Literal (pos, CombApp (CombApp (CombConst (("equal", _), _, _), t1),
- t2))) =
- tptp_of_equality params pos (t1, t2)
- | tptp_literal params (Literal (pos, pred)) =
- string_of_predicate params pred #>> tptp_sign pos
-
-(* Given a clause, returns its literals paired with a list of literals
- concerning TFrees; the latter should only occur in conjecture clauses. *)
-fun tptp_type_literals params pos (HOLClause {literals, ctypes_sorts, ...})
- pool =
- let
- val (lits, pool) = pool_map (tptp_literal params) literals pool
- val (tylits, pool) = pool_map (tptp_of_type_literal pos)
- (type_literals_for_types ctypes_sorts) pool
- in ((lits, tylits), pool) end
-
-fun tptp_clause params (cls as HOLClause {axiom_name, clause_id, kind, ...})
- pool =
-let
- val ((lits, tylits), pool) =
- tptp_type_literals params (kind = Conjecture) cls pool
- in
- ((gen_tptp_cls (clause_id, axiom_name, kind, lits, tylits), tylits), pool)
- end
-
-
-(*** DFG format ***)
-
-fun dfg_literal params (Literal (pos, pred)) =
- string_of_predicate params pred #>> dfg_sign pos
-
-fun dfg_type_literals params pos (HOLClause {literals, ctypes_sorts, ...}) =
- pool_map (dfg_literal params) literals
- #>> rpair (map (dfg_of_type_literal pos)
- (type_literals_for_types ctypes_sorts))
-
-fun get_uvars (CombConst _) vars pool = (vars, pool)
- | get_uvars (CombVar (name, _)) vars pool =
- nice_name name pool |>> (fn var => var :: vars)
- | get_uvars (CombApp (P, Q)) vars pool =
- let val (vars, pool) = get_uvars P vars pool in get_uvars Q vars pool end
-
-fun get_uvars_l (Literal (_, c)) = get_uvars c [];
-
-fun dfg_vars (HOLClause {literals, ...}) =
- pool_map get_uvars_l literals #>> union_all
-
-fun dfg_clause params (cls as HOLClause {axiom_name, clause_id, kind,
- ctypes_sorts, ...}) pool =
- let
- val ((lits, tylits), pool) =
- dfg_type_literals params (kind = Conjecture) cls pool
- val (vars, pool) = dfg_vars cls pool
- val tvars = get_tvar_strs ctypes_sorts
- in
- ((gen_dfg_cls (clause_id, axiom_name, kind, lits, tylits, tvars @ vars),
- tylits), pool)
- end
-
-
-(** For DFG format: accumulate function and predicate declarations **)
-
-fun add_types tvars = fold add_fol_type_funcs tvars
-
-fun add_decls (full_types, explicit_apply, cma, cnh)
- (CombConst ((c, _), ctp, tvars)) (funcs, preds) =
- (if c = "equal" then
- (add_types tvars funcs, preds)
- else
- let val arity = min_arity_of cma c
- val ntys = if not full_types then length tvars else 0
- val addit = Symtab.update(c, arity + ntys)
- in
- if needs_hBOOL explicit_apply cnh c then
- (add_types tvars (addit funcs), preds)
- else
- (add_types tvars funcs, addit preds)
- end) |>> full_types ? add_fol_type_funcs ctp
- | add_decls _ (CombVar (_, ctp)) (funcs, preds) =
- (add_fol_type_funcs ctp funcs, preds)
- | add_decls params (CombApp (P, Q)) decls =
- decls |> add_decls params P |> add_decls params Q
-
-fun add_literal_decls params (Literal (_, c)) = add_decls params c
-
-fun add_clause_decls params (HOLClause {literals, ...}) decls =
- fold (add_literal_decls params) literals decls
- handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities")
-
-fun decls_of_clauses (params as (full_types, explicit_apply, _, _)) clauses
- arity_clauses =
- let
- val functab =
- init_functab
- |> fold Symtab.update [(type_wrapper_name, 2), ("hAPP", 2),
- ("tc_bool", 0)]
- val predtab = Symtab.empty |> Symtab.update ("hBOOL", 1)
- val (functab, predtab) =
- (functab, predtab) |> fold (add_clause_decls params) clauses
- |>> fold add_arity_clause_funcs arity_clauses
- in (Symtab.dest functab, Symtab.dest predtab) end
-
-fun add_clause_preds (HOLClause {ctypes_sorts, ...}) preds =
- fold add_type_sort_preds ctypes_sorts preds
- handle Symtab.DUP a => error ("predicate " ^ a ^ " has multiple arities")
-
-(*Higher-order clauses have only the predicates hBOOL and type classes.*)
-fun preds_of_clauses clauses clsrel_clauses arity_clauses =
- Symtab.empty
- |> fold add_clause_preds clauses
- |> fold add_arity_clause_preds arity_clauses
- |> fold add_classrel_clause_preds clsrel_clauses
- |> Symtab.dest
-
-(**********************************************************************)
-(* write clauses to files *)
-(**********************************************************************)
-
-fun count_combterm (CombConst ((c, _), _, _)) =
- Symtab.map_entry c (Integer.add 1)
- | count_combterm (CombVar _) = I
- | count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2
-
-fun count_literal (Literal (_, t)) = count_combterm t
-
-fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
-
-val raw_cnf_rules_pairs = map (fn (name, thm) => (thm, (name, 0)))
-fun cnf_helper_thms thy raw =
- map (`Thm.get_name_hint)
- #> (if raw then raw_cnf_rules_pairs else cnf_rules_pairs thy)
-
-val optional_helpers =
- [(["c_COMBI", "c_COMBK"], (false, @{thms COMBI_def COMBK_def})),
- (["c_COMBB", "c_COMBC"], (false, @{thms COMBB_def COMBC_def})),
- (["c_COMBS"], (false, @{thms COMBS_def}))]
-val optional_typed_helpers =
- [(["c_True", "c_False"], (true, @{thms True_or_False})),
- (["c_If"], (true, @{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 dfg thy is_FO full_types conjectures axcls =
- let
- val axclauses = map snd (make_axiom_clauses dfg thy axcls)
- val ct = fold (fold count_clause) [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, (raw, ths)) =>
- if exists is_needed ss then cnf_helper_thms thy raw ths
- else []))
- @ (if is_FO then [] else cnf_helper_thms thy false mandatory_helpers)
- in map snd (make_axiom_clauses dfg thy cnfs) end
-
-(*Find the minimal arity of each function mentioned in the term. Also, note which uses
- are not at top level, to see if hBOOL is needed.*)
-fun count_constants_term toplev t (const_min_arity, const_needs_hBOOL) =
- let val (head, args) = strip_combterm_comb t
- val n = length args
- val (const_min_arity, const_needs_hBOOL) =
- (const_min_arity, const_needs_hBOOL)
- |> fold (count_constants_term false) args
- in
- case head of
- CombConst ((a, _),_,_) => (*predicate or function version of "equal"?*)
- let val a = if a="equal" andalso not toplev then "c_fequal" else a
- in
- (const_min_arity |> Symtab.map_default (a, n) (Integer.min n),
- const_needs_hBOOL |> not toplev ? Symtab.update (a, true))
- end
- | _ => (const_min_arity, const_needs_hBOOL)
- end;
-
-(*A literal is a top-level term*)
-fun count_constants_lit (Literal (_,t)) (const_min_arity, const_needs_hBOOL) =
- count_constants_term true t (const_min_arity, const_needs_hBOOL);
-
-fun count_constants_clause (HOLClause {literals, ...})
- (const_min_arity, const_needs_hBOOL) =
- fold count_constants_lit literals (const_min_arity, const_needs_hBOOL);
-
-fun display_arity explicit_apply const_needs_hBOOL (c,n) =
- trace_msg (fn () => "Constant: " ^ c ^
- " arity:\t" ^ Int.toString n ^
- (if needs_hBOOL explicit_apply const_needs_hBOOL c then
- " needs hBOOL"
- else
- ""))
-
-fun count_constants explicit_apply
- (conjectures, _, extra_clauses, helper_clauses, _, _) =
- if not explicit_apply then
- let val (const_min_arity, const_needs_hBOOL) =
- fold count_constants_clause conjectures (Symtab.empty, Symtab.empty)
- |> fold count_constants_clause extra_clauses
- |> fold count_constants_clause helper_clauses
- val _ = app (display_arity explicit_apply const_needs_hBOOL)
- (Symtab.dest (const_min_arity))
- in (const_min_arity, const_needs_hBOOL) end
- else (Symtab.empty, Symtab.empty);
-
-fun header () =
- "% This file was generated by Isabelle (most likely Sledgehammer)\n" ^
- "% " ^ timestamp () ^ "\n"
-
-(* TPTP format *)
-
-fun write_tptp_file readable_names full_types explicit_apply file clauses =
- let
- fun section _ [] = []
- | section name ss =
- "\n% " ^ name ^ plural_s (length ss) ^ " (" ^ Int.toString (length ss) ^
- ")\n" :: ss
- val pool = empty_name_pool readable_names
- val (conjectures, axclauses, _, helper_clauses,
- classrel_clauses, arity_clauses) = clauses
- val (cma, cnh) = count_constants explicit_apply clauses
- val params = (full_types, explicit_apply, cma, cnh)
- val ((conjecture_clss, tfree_litss), pool) =
- pool_map (tptp_clause params) conjectures pool |>> ListPair.unzip
- val tfree_clss = map tptp_tfree_clause (fold (union (op =)) tfree_litss [])
- val (ax_clss, pool) = pool_map (apfst fst oo tptp_clause params) axclauses
- pool
- val classrel_clss = map tptp_classrel_clause classrel_clauses
- val arity_clss = map tptp_arity_clause arity_clauses
- val (helper_clss, pool) = pool_map (apfst fst oo tptp_clause params)
- helper_clauses pool
- val conjecture_offset =
- length ax_clss + length classrel_clss + length arity_clss
- + length helper_clss
- val _ =
- File.write_list file
- (header () ::
- section "Relevant fact" ax_clss @
- section "Class relationship" classrel_clss @
- section "Arity declaration" arity_clss @
- section "Helper fact" helper_clss @
- section "Conjecture" conjecture_clss @
- section "Type variable" tfree_clss)
- in (pool, conjecture_offset) end
-
-(* DFG format *)
-
-fun dfg_tfree_predicate s = (first_field "(" s |> the |> fst, 1)
-
-fun write_dfg_file full_types explicit_apply file clauses =
- let
- (* Some of the helper functions below are not name-pool-aware. However,
- there's no point in adding name pool support if the DFG format is on its
- way out anyway. *)
- val pool = NONE
- val (conjectures, axclauses, _, helper_clauses,
- classrel_clauses, arity_clauses) = clauses
- val (cma, cnh) = count_constants explicit_apply clauses
- val params = (full_types, explicit_apply, cma, cnh)
- val ((conjecture_clss, tfree_litss), pool) =
- pool_map (dfg_clause params) conjectures pool |>> ListPair.unzip
- val tfree_lits = union_all tfree_litss
- val problem_name = Path.implode (Path.base file)
- val (axstrs, pool) = pool_map (apfst fst oo dfg_clause params) axclauses pool
- val tfree_clss = map dfg_tfree_clause tfree_lits
- val tfree_preds = map dfg_tfree_predicate tfree_lits
- val (helper_clauses_strs, pool) =
- pool_map (apfst fst oo dfg_clause params) helper_clauses pool
- val (funcs, cl_preds) =
- decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
- val ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
- val preds = tfree_preds @ cl_preds @ ty_preds
- val conjecture_offset =
- length axclauses + length classrel_clauses + length arity_clauses
- + length helper_clauses
- val _ =
- File.write_list file
- (header () ::
- string_of_start problem_name ::
- string_of_descrip problem_name ::
- string_of_symbols (string_of_funcs funcs)
- (string_of_preds preds) ::
- "list_of_clauses(axioms, cnf).\n" ::
- axstrs @
- map dfg_classrel_clause classrel_clauses @
- map dfg_arity_clause arity_clauses @
- helper_clauses_strs @
- ["end_of_list.\n\nlist_of_clauses(conjectures, cnf).\n"] @
- conjecture_clss @
- tfree_clss @
- ["end_of_list.\n\n",
- "end_problem.\n"])
- in (pool, conjecture_offset) end
-
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jun 23 10:05:13 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jun 23 10:20:54 2010 +0200
@@ -12,7 +12,6 @@
val timeout: int Unsynchronized.ref
val full_types: bool Unsynchronized.ref
val default_params : theory -> (string * string) list -> params
- val setup: theory -> theory
end;
structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
@@ -25,31 +24,6 @@
open ATP_Systems
open Sledgehammer_Fact_Minimizer
-(** Proof method used in Isar proofs **)
-
-val neg_clausify_setup =
- Method.setup @{binding neg_clausify}
- (Scan.succeed (SIMPLE_METHOD' o neg_clausify_tac)
- o tap (fn _ => legacy_feature "Old 'neg_clausify' method -- \
- \rerun Sledgehammer to obtain a direct \
- \proof"))
- "conversion of goal to negated conjecture clauses (legacy)"
-
-(** Attribute for converting a theorem into clauses **)
-
-val parse_clausify_attribute : attribute context_parser =
- Scan.lift Parse.nat
- >> (fn i => Thm.rule_attribute (fn context => fn th =>
- let val thy = Context.theory_of context in
- Meson.make_meta_clause (nth (cnf_axiom thy th) i)
- end))
-
-val clausify_setup =
- Attrib.setup @{binding clausify}
- (parse_clausify_attribute
- o tap (fn _ => legacy_feature "Old 'clausify' attribute"))
- "conversion of theorem to clauses"
-
(** Sledgehammer commands **)
fun add_to_relevance_override ns : relevance_override =
@@ -58,7 +32,6 @@
{add = [], del = ns, only = false}
fun only_relevance_override ns : relevance_override =
{add = ns, del = [], only = true}
-val no_relevance_override = add_to_relevance_override []
fun merge_relevance_override_pairwise (r1 : relevance_override)
(r2 : relevance_override) =
{add = #add r1 @ #add r2, del = #del r1 @ #del r2,
@@ -166,7 +139,7 @@
val infinity_time_in_secs = 60 * 60 * 24 * 365
val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs)
-fun extract_params thy default_params override_params =
+fun extract_params default_params override_params =
let
val override_params = map unalias_raw_param override_params
val raw_params = rev override_params @ rev default_params
@@ -216,7 +189,7 @@
timeout = timeout, minimize_timeout = minimize_timeout}
end
-fun get_params thy = extract_params thy (default_raw_params thy)
+fun get_params thy = extract_params (default_raw_params thy)
fun default_params thy = get_params thy o map (apsnd single)
val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal
@@ -264,7 +237,6 @@
val running_atpsN = "running_atps"
val kill_atpsN = "kill_atps"
val refresh_tptpN = "refresh_tptp"
-val helpN = "help"
fun minimizize_raw_param_name "timeout" = "minimize_timeout"
| minimizize_raw_param_name name = name
@@ -359,8 +331,4 @@
"set and display the default parameters for Sledgehammer" Keyword.thy_decl
parse_sledgehammer_params_command
-val setup =
- neg_clausify_setup
- #> clausify_setup
-
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Jun 23 10:05:13 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Jun 23 10:20:54 2010 +0200
@@ -368,7 +368,7 @@
| add_type_constraint _ = I
fun is_positive_literal (@{const Not} $ _) = false
- | is_positive_literal t = true
+ | is_positive_literal _ = true
fun negate_term thy (Const (@{const_name All}, T) $ Abs (s, T', t')) =
Const (@{const_name Ex}, T) $ Abs (s, T', negate_term thy t')
@@ -551,11 +551,11 @@
(* Vampire is keen on producing these. *)
fun is_trivial_formula (@{const Not} $ (Const (@{const_name "op ="}, _)
$ t1 $ t2)) = (t1 aconv t2)
- | is_trivial_formula t = false
+ | is_trivial_formula _ = false
-fun add_desired_line _ _ _ _ _ (line as Definition (num, _, _)) (j, lines) =
+fun add_desired_line _ _ _ _ (line as Definition (num, _, _)) (j, lines) =
(j, line :: map (replace_deps_in_line (num, [])) lines)
- | add_desired_line ctxt isar_shrink_factor conjecture_shape thm_names frees
+ | add_desired_line isar_shrink_factor conjecture_shape thm_names frees
(Inference (num, t, deps)) (j, lines) =
(j + 1,
if is_axiom_clause_number thm_names num orelse
@@ -667,7 +667,7 @@
fun forall_vars t = fold_rev forall_of (map Var (Term.add_vars t [])) t
-fun step_for_line _ _ (Definition (num, t1, t2)) = Let (t1, t2)
+fun step_for_line _ _ (Definition (_, t1, t2)) = Let (t1, t2)
| step_for_line _ _ (Inference (num, t, [])) = Assume ((raw_prefix, num), t)
| step_for_line thm_names j (Inference (num, t, deps)) =
Have (if j = 1 then [Show] else [], (raw_prefix, num),
@@ -683,7 +683,7 @@
|> decode_lines ctxt full_types tfrees
|> rpair [] |-> fold_rev (add_line conjecture_shape thm_names)
|> rpair [] |-> fold_rev add_nontrivial_line
- |> rpair (0, []) |-> fold_rev (add_desired_line ctxt isar_shrink_factor
+ |> rpair (0, []) |-> fold_rev (add_desired_line isar_shrink_factor
conjecture_shape thm_names frees)
|> snd
in
@@ -722,7 +722,7 @@
else if forall (curry (op =) (hd proof1) o hd) (tl proofs) then
aux (hd proof1 :: proof_tail) (map tl proofs)
else case hd proof1 of
- Have ([], l, t, by) =>
+ Have ([], l, t, _) => (* FIXME: should we really ignore the "by"? *)
if forall (fn Have ([], l', t', _) :: _ => (l, t) = (l', t')
| _ => false) (tl proofs) andalso
not (exists (member (op =) (maps new_labels_of proofs))
@@ -755,7 +755,7 @@
first_pass (proof, contra) |>> cons step
| first_pass ((step as Let _) :: proof, contra) =
first_pass (proof, contra) |>> cons step
- | first_pass ((step as Assume (l as (_, num), t)) :: proof, contra) =
+ | first_pass ((step as Assume (l as (_, num), _)) :: proof, contra) =
if member (op =) concl_ls l then
first_pass (proof, contra ||> l = hd concl_ls ? cons step)
else
@@ -992,6 +992,13 @@
do_indent 0 ^ (if n <> 1 then "next" else "qed") ^ "\n"
in do_proof end
+fun strip_subgoal goal i =
+ let
+ val (t, frees) = Logic.goal_params (prop_of goal) i
+ val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees)
+ val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees
+ in (rev (map dest_Free frees), hyp_ts, concl_t) end
+
fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
(other_params as (full_types, _, atp_proof, thm_names, goal,
i)) =
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Wed Jun 23 10:20:54 2010 +0200
@@ -0,0 +1,255 @@
+(* 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_pool = Sledgehammer_FOL_Clause.name_pool
+ type type_literal = Sledgehammer_FOL_Clause.type_literal
+ type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
+ type arity_clause = Sledgehammer_FOL_Clause.arity_clause
+ type hol_clause = Sledgehammer_HOL_Clause.hol_clause
+
+ val tptp_of_type_literal :
+ bool -> type_literal -> name_pool option -> string * name_pool option
+ val write_tptp_file :
+ bool -> bool -> bool -> Path.T
+ -> hol_clause list * hol_clause list * hol_clause list * hol_clause list
+ * classrel_clause list * arity_clause list
+ -> name_pool option * int
+end;
+
+structure Sledgehammer_TPTP_Format : SLEDGEHAMMER_TPTP_FORMAT =
+struct
+
+open Sledgehammer_Util
+open Sledgehammer_FOL_Clause
+open Sledgehammer_HOL_Clause
+
+val clause_prefix = "cls_"
+val arity_clause_prefix = "clsarity_"
+
+fun paren_pack [] = ""
+ | paren_pack strings = "(" ^ commas strings ^ ")"
+
+fun string_of_fol_type (TyVar sp) pool = nice_name sp pool
+ | string_of_fol_type (TyFree sp) pool = nice_name sp pool
+ | string_of_fol_type (TyConstr (sp, tys)) pool =
+ let
+ val (s, pool) = nice_name sp pool
+ val (ss, pool) = pool_map string_of_fol_type tys pool
+ in (s ^ paren_pack ss, pool) end
+
+(* True if the constant ever appears outside of the top-level position in
+ literals. If false, the constant always receives all of its arguments and is
+ used as a predicate. *)
+fun needs_hBOOL explicit_apply const_needs_hBOOL c =
+ explicit_apply orelse the_default false (Symtab.lookup const_needs_hBOOL c)
+
+fun head_needs_hBOOL explicit_apply const_needs_hBOOL
+ (CombConst ((c, _), _, _)) =
+ needs_hBOOL explicit_apply const_needs_hBOOL c
+ | head_needs_hBOOL _ _ _ = true
+
+fun wrap_type full_types (s, ty) pool =
+ if full_types then
+ let val (s', pool) = string_of_fol_type ty pool in
+ (type_wrapper_name ^ paren_pack [s, s'], pool)
+ end
+ else
+ (s, pool)
+
+fun wrap_type_if full_types explicit_apply cnh (head, s, tp) =
+ if head_needs_hBOOL explicit_apply cnh head then
+ wrap_type full_types (s, tp)
+ else
+ pair s
+
+fun apply ss = "hAPP" ^ paren_pack ss;
+
+fun rev_apply (v, []) = v
+ | rev_apply (v, arg::args) = apply [rev_apply (v, args), arg];
+
+fun string_apply (v, args) = rev_apply (v, rev args)
+
+fun min_arity_of const_min_arity = the_default 0 o Symtab.lookup const_min_arity
+
+(* Apply an operator to the argument strings, using either the "apply" operator
+ or direct function application. *)
+fun string_of_application full_types cma (CombConst ((s, s'), _, tvars), args)
+ pool =
+ let
+ val s = if s = "equal" then "c_fequal" else s
+ val nargs = min_arity_of cma s
+ val args1 = List.take (args, nargs)
+ handle Subscript =>
+ raise Fail (quote s ^ " has arity " ^ Int.toString nargs ^
+ " but is applied to " ^ commas (map quote args))
+ val args2 = List.drop (args, nargs)
+ val (targs, pool) = if full_types then ([], pool)
+ else pool_map string_of_fol_type tvars pool
+ val (s, pool) = nice_name (s, s') pool
+ in (string_apply (s ^ paren_pack (args1 @ targs), args2), pool) end
+ | string_of_application _ _ (CombVar (name, _), args) pool =
+ nice_name name pool |>> (fn s => string_apply (s, args))
+
+fun string_of_combterm (params as (full_types, explicit_apply, cma, cnh)) t
+ pool =
+ let
+ val (head, args) = strip_combterm_comb t
+ val (ss, pool) = pool_map (string_of_combterm params) args pool
+ val (s, pool) = string_of_application full_types cma (head, ss) pool
+ in
+ wrap_type_if full_types explicit_apply cnh (head, s, type_of_combterm t)
+ pool
+ end
+
+(*Boolean-valued terms are here converted to literals.*)
+fun boolify params c =
+ string_of_combterm params c #>> prefix "hBOOL" o paren_pack o single
+
+fun string_of_predicate (params as (_, explicit_apply, _, cnh)) t =
+ case #1 (strip_combterm_comb t) of
+ CombConst ((s, _), _, _) =>
+ (if needs_hBOOL explicit_apply cnh s then boolify else string_of_combterm)
+ params t
+ | _ => boolify params t
+
+fun tptp_of_equality params pos (t1, t2) =
+ pool_map (string_of_combterm params) [t1, t2]
+ #>> space_implode (if pos then " = " else " != ")
+
+fun tptp_sign true s = s
+ | tptp_sign false s = "~ " ^ s
+
+fun tptp_literal params
+ (Literal (pos, CombApp (CombApp (CombConst (("equal", _), _, _), t1),
+ t2))) =
+ tptp_of_equality params pos (t1, t2)
+ | tptp_literal params (Literal (pos, pred)) =
+ string_of_predicate params pred #>> tptp_sign pos
+
+fun tptp_of_type_literal pos (TyLitVar (s, name)) =
+ nice_name name #>> (fn s' => tptp_sign pos (s ^ "(" ^ s' ^ ")"))
+ | tptp_of_type_literal pos (TyLitFree (s, name)) =
+ nice_name name #>> (fn s' => tptp_sign pos (s ^ "(" ^ s' ^ ")"))
+
+(* Given a clause, returns its literals paired with a list of literals
+ concerning TFrees; the latter should only occur in conjecture clauses. *)
+fun tptp_type_literals params pos (HOLClause {literals, ctypes_sorts, ...})
+ pool =
+ let
+ val (lits, pool) = pool_map (tptp_literal params) literals pool
+ val (tylits, pool) = pool_map (tptp_of_type_literal pos)
+ (type_literals_for_types ctypes_sorts) pool
+ in ((lits, tylits), pool) end
+
+fun tptp_cnf name kind formula =
+ "cnf(" ^ name ^ ", " ^ kind ^ ",\n " ^ formula ^ ").\n"
+
+fun tptp_raw_clause strings = "(" ^ space_implode " | " strings ^ ")"
+
+val tptp_tfree_clause =
+ tptp_cnf "tfree_tcs" "negated_conjecture" o tptp_raw_clause o single
+
+fun tptp_classrel_literals sub sup =
+ let val tvar = "(T)" in
+ tptp_raw_clause [tptp_sign false (sub ^ tvar), tptp_sign true (sup ^ tvar)]
+ end
+
+fun tptp_clause params (cls as HOLClause {axiom_name, clause_id, kind, ...})
+ pool =
+ let
+ val ((lits, tylits), pool) =
+ tptp_type_literals params (kind = Conjecture) cls pool
+ val name = clause_prefix ^ ascii_of axiom_name ^ "_" ^
+ Int.toString clause_id
+ val cnf =
+ case kind of
+ Axiom => tptp_cnf name "axiom" (tptp_raw_clause (tylits @ lits))
+ | Conjecture => tptp_cnf name "negated_conjecture" (tptp_raw_clause lits)
+ in ((cnf, tylits), pool) end
+
+fun tptp_classrel_clause (ClassrelClause {axiom_name, subclass, superclass,
+ ...}) =
+ tptp_cnf axiom_name "axiom" (tptp_classrel_literals subclass superclass)
+
+fun tptp_of_arity_literal (TConsLit (c, t, args)) =
+ tptp_sign true (make_type_class c ^ "(" ^ t ^ paren_pack args ^ ")")
+ | tptp_of_arity_literal (TVarLit (c, str)) =
+ tptp_sign false (make_type_class c ^ "(" ^ str ^ ")")
+
+fun tptp_arity_clause (ArityClause {axiom_name, conclLit, premLits, ...}) =
+ tptp_cnf (arity_clause_prefix ^ ascii_of axiom_name) "axiom"
+ (tptp_raw_clause (map tptp_of_arity_literal (conclLit :: premLits)))
+
+(*Find the minimal arity of each function mentioned in the term. Also, note which uses
+ are not at top level, to see if hBOOL is needed.*)
+fun count_constants_term toplev t (const_min_arity, const_needs_hBOOL) =
+ let
+ val (head, args) = strip_combterm_comb t
+ val n = length args
+ val (const_min_arity, const_needs_hBOOL) =
+ (const_min_arity, const_needs_hBOOL)
+ |> fold (count_constants_term false) args
+ in
+ case head of
+ CombConst ((a, _), _, _) => (*predicate or function version of "equal"?*)
+ let val a = if a="equal" andalso not toplev then "c_fequal" else a
+ in
+ (const_min_arity |> Symtab.map_default (a, n) (Integer.min n),
+ const_needs_hBOOL |> not toplev ? Symtab.update (a, true))
+ end
+ | _ => (const_min_arity, const_needs_hBOOL)
+ end
+fun count_constants_lit (Literal (_, t)) = count_constants_term true t
+fun count_constants_clause (HOLClause {literals, ...}) =
+ fold count_constants_lit literals
+fun count_constants explicit_apply
+ (conjectures, _, extra_clauses, helper_clauses, _, _) =
+ (Symtab.empty, Symtab.empty)
+ |> (if explicit_apply then
+ I
+ else
+ fold (fold count_constants_clause)
+ [conjectures, extra_clauses, helper_clauses])
+
+fun write_tptp_file readable_names full_types explicit_apply file clauses =
+ let
+ fun section _ [] = []
+ | section name ss =
+ "\n% " ^ name ^ plural_s (length ss) ^ " (" ^ Int.toString (length ss) ^
+ ")\n" :: ss
+ val pool = empty_name_pool readable_names
+ val (conjectures, axclauses, _, helper_clauses,
+ classrel_clauses, arity_clauses) = clauses
+ val (cma, cnh) = count_constants explicit_apply clauses
+ val params = (full_types, explicit_apply, cma, cnh)
+ val ((conjecture_clss, tfree_litss), pool) =
+ pool_map (tptp_clause params) conjectures pool |>> ListPair.unzip
+ val tfree_clss = map tptp_tfree_clause (fold (union (op =)) tfree_litss [])
+ val (ax_clss, pool) =
+ pool_map (apfst fst oo tptp_clause params) axclauses pool
+ val classrel_clss = map tptp_classrel_clause classrel_clauses
+ val arity_clss = map tptp_arity_clause arity_clauses
+ val (helper_clss, pool) = pool_map (apfst fst oo tptp_clause params)
+ helper_clauses pool
+ val conjecture_offset =
+ length ax_clss + length classrel_clss + length arity_clss
+ + length helper_clss
+ val _ =
+ File.write_list file
+ ("% This file was generated by Isabelle (most likely Sledgehammer)\n\
+ \% " ^ timestamp () ^ "\n" ::
+ section "Relevant fact" ax_clss @
+ section "Class relationship" classrel_clss @
+ section "Arity declaration" arity_clss @
+ section "Helper fact" helper_clss @
+ section "Conjecture" conjecture_clss @
+ section "Type variable" tfree_clss)
+ in (pool, conjecture_offset) end
+
+end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Jun 23 10:05:13 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Jun 23 10:20:54 2010 +0200
@@ -6,7 +6,6 @@
signature SLEDGEHAMMER_UTIL =
sig
- val pairf : ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c
val plural_s : int -> string
val serial_commas : string -> string list -> string list
val replace_all : string -> string -> string -> string
@@ -24,8 +23,6 @@
structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
struct
-fun pairf f g x = (f x, g x)
-
fun plural_s n = if n = 1 then "" else "s"
fun serial_commas _ [] = ["??"]