--- a/src/HOL/Tools/ATP_Manager/SystemOnTPTP Fri Apr 23 10:00:53 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/SystemOnTPTP Fri Apr 23 11:34:49 2010 +0200
@@ -123,7 +123,7 @@
$extract =~ s/\)\.cnf/\)\.\ncnf/g;
print "========== ~~/lib/scripts/SystemOnTPTP extracted proof: ==========\n";
- # orientation for res_reconstruct.ML
+ # orientation for "sledgehammer_proof_reconstruct.ML"
print "# SZS output start CNFRefutation.\n";
print "$extract\n";
print "# SZS output end CNFRefutation.\n";
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Apr 23 10:00:53 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Apr 23 11:34:49 2010 +0200
@@ -9,6 +9,7 @@
signature ATP_MANAGER =
sig
type relevance_override = Sledgehammer_Fact_Filter.relevance_override
+ type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
type params =
{debug: bool,
verbose: bool,
@@ -41,7 +42,8 @@
proof: string,
internal_thm_names: string Vector.vector,
filtered_clauses: (thm * (string * int)) list}
- type prover = params -> Time.time -> problem -> prover_result
+ type prover =
+ params -> minimize_command -> Time.time -> problem -> prover_result
val atps: string Unsynchronized.ref
val timeout: int Unsynchronized.ref
@@ -52,7 +54,9 @@
val add_prover: string * prover -> theory -> theory
val get_prover: theory -> string -> prover option
val available_atps: theory -> unit
- val sledgehammer: params -> int -> relevance_override -> Proof.state -> unit
+ val sledgehammer:
+ params -> int -> relevance_override -> (string -> minimize_command)
+ -> Proof.state -> unit
end;
structure ATP_Manager : ATP_MANAGER =
@@ -62,7 +66,7 @@
open Sledgehammer_Fact_Filter
open Sledgehammer_Proof_Reconstruct
-(** parameters, problems, results, and provers **)
+(** problems, results, provers, etc. **)
type params =
{debug: bool,
@@ -99,7 +103,8 @@
internal_thm_names: string Vector.vector,
filtered_clauses: (thm * (string * int)) list};
-type prover = params -> Time.time -> problem -> prover_result;
+type prover =
+ params -> minimize_command -> Time.time -> problem -> prover_result
(** preferences **)
@@ -107,7 +112,7 @@
val message_store_limit = 20;
val message_display_limit = 5;
-val atps = Unsynchronized.ref "e spass remote_vampire";
+val atps = Unsynchronized.ref ""; (* set in "ATP_Wrapper" *)
val timeout = Unsynchronized.ref 60;
val full_types = Unsynchronized.ref false;
@@ -323,12 +328,12 @@
val empty = Symtab.empty;
val extend = I;
fun merge data : T = Symtab.merge (eq_snd op =) data
- handle Symtab.DUP dup => err_dup_prover dup;
+ handle Symtab.DUP name => err_dup_prover name;
);
fun add_prover (name, prover) thy =
Provers.map (Symtab.update_new (name, (prover, stamp ()))) thy
- handle Symtab.DUP dup => err_dup_prover dup;
+ handle Symtab.DUP name => err_dup_prover name;
fun get_prover thy name =
Option.map #1 (Symtab.lookup (Provers.get thy) name);
@@ -341,7 +346,7 @@
(* start prover thread *)
fun start_prover (params as {timeout, ...}) birth_time death_time i
- relevance_override proof_state name =
+ relevance_override minimize_command proof_state name =
(case get_prover (Proof.theory_of proof_state) name of
NONE => warning ("Unknown ATP: " ^ quote name ^ ".")
| SOME prover =>
@@ -359,7 +364,8 @@
{subgoal = i, goal = (ctxt, (facts, goal)),
relevance_override = relevance_override, axiom_clauses = NONE,
filtered_clauses = NONE}
- val message = #message (prover params timeout problem)
+ val message =
+ #message (prover params (minimize_command name) timeout problem)
handle Sledgehammer_HOL_Clause.TRIVIAL =>
metis_line i n []
| ERROR msg => "Error: " ^ msg ^ ".\n";
@@ -371,14 +377,15 @@
(* Sledgehammer the given subgoal *)
fun sledgehammer (params as {atps, timeout, ...}) i relevance_override
- proof_state =
+ minimize_command proof_state =
let
val birth_time = Time.now ()
val death_time = Time.+ (birth_time, timeout)
val _ = kill_atps () (* RACE w.r.t. other invocations of Sledgehammer *)
val _ = priority "Sledgehammering..."
val _ = List.app (start_prover params birth_time death_time i
- relevance_override proof_state) atps
+ relevance_override minimize_command
+ proof_state) atps
in () end
end;
--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Fri Apr 23 10:00:53 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Fri Apr 23 11:34:49 2010 +0200
@@ -78,13 +78,13 @@
axiom_clauses = SOME axclauses,
filtered_clauses = SOME (the_default axclauses filtered_clauses)}
in
- `outcome_of_result (prover params timeout problem)
+ `outcome_of_result (prover params (K "") timeout problem)
|>> tap (priority o string_of_outcome)
end
(* minimalization of thms *)
-fun minimize_theorems (params as {minimize_timeout, isar_proof, modulus,
+fun minimize_theorems (params as {debug, minimize_timeout, isar_proof, modulus,
sorts, ...})
prover atp_name i state name_thms_pairs =
let
@@ -122,8 +122,8 @@
["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ ".")
in
(SOME min_thms,
- proof_text isar_proof true modulus sorts atp_name proof
- internal_thm_names ctxt goal i |> fst)
+ proof_text isar_proof debug modulus sorts ctxt
+ (K "", proof, internal_thm_names, goal, i) |> fst)
end
| (Timeout, _) =>
(NONE, "Timeout: You can increase the time limit using the \"timeout\" \
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Fri Apr 23 10:00:53 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Fri Apr 23 11:34:49 2010 +0200
@@ -43,13 +43,15 @@
(* prover configuration *)
+val remotify = prefix "remote_"
+
type prover_config =
- {command: Path.T,
+ {home: string,
+ executable: string,
arguments: Time.time -> string,
known_failures: (string list * string) list,
max_new_clauses: int,
- prefers_theory_relevant: bool,
- supports_isar_proofs: bool};
+ prefers_theory_relevant: bool};
(* basic template *)
@@ -71,8 +73,10 @@
else "Error: The ATP output is ill-formed."
| (message :: _) => message
-fun generic_prover overlord get_facts prepare write_file cmd args known_failures
- proof_text name ({debug, full_types, explicit_apply, ...} : params)
+fun generic_prover overlord get_facts prepare write_file home executable args
+ known_failures name
+ ({debug, full_types, explicit_apply, isar_proof, modulus, sorts, ...}
+ : params) minimize_command
({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
: problem) =
let
@@ -105,18 +109,29 @@
in
if destdir' = "" then File.tmp_path probfile
else if File.exists (Path.explode destdir')
- then Path.append (Path.explode destdir') probfile
+ then Path.append (Path.explode destdir') probfile
else error ("No such directory: " ^ destdir' ^ ".")
end;
+ val command = Path.explode (home ^ "/" ^ executable)
(* write out problem file and call prover *)
- fun cmd_line probfile =
- if Config.get ctxt measure_runtime then
- "TIMEFORMAT='%3U'; { time " ^ space_implode " " [File.shell_path cmd,
- args, File.shell_path probfile] ^ " ; } 2>&1"
- else
- space_implode " " ["exec", File.shell_path cmd, args,
- File.shell_path probfile, "2>&1"];
+ fun command_line probfile =
+ (if Config.get ctxt measure_runtime then
+ "TIMEFORMAT='%3U'; { time " ^
+ space_implode " " [File.shell_path command, args,
+ File.shell_path probfile] ^ " ; } 2>&1"
+ else
+ space_implode " " ["exec", File.shell_path command, args,
+ File.shell_path probfile, "2>&1"]) ^
+ (if overlord then
+ " | sed 's/,/, /g' \
+ \| sed 's/\\([^!=]\\)\\([=|]\\)\\([^=]\\)/\\1 \\2 \\3/g' \
+ \| sed 's/! =/ !=/g' \
+ \| sed 's/ / /g' | sed 's/| |/||/g' \
+ \| sed 's/ = = =/===/g' \
+ \| sed 's/= = /== /g'"
+ else
+ "")
fun split_time s =
let
val split = String.tokens (fn c => str c = "\n");
@@ -131,10 +146,10 @@
fun split_time' s =
if Config.get ctxt measure_runtime then split_time s else (s, 0)
fun run_on probfile =
- if File.exists cmd then
+ if File.exists command then
write_file full_types explicit_apply probfile clauses
- |> pair (apfst split_time' (bash_output (cmd_line probfile)))
- else error ("Bad executable: " ^ Path.implode cmd ^ ".");
+ |> pair (apfst split_time' (bash_output (command_line probfile)))
+ else error ("Bad executable: " ^ Path.implode command ^ ".");
(* If the problem file has not been exported, remove it; otherwise, export
the proof file too. *)
@@ -144,7 +159,11 @@
()
else
File.write (Path.explode (Path.implode probfile ^ "_proof"))
- ("% " ^ timestamp () ^ "\n" ^ proof)
+ ((if overlord then
+ "% " ^ command_line probfile ^ "\n% " ^ timestamp () ^
+ "\n"
+ else
+ "") ^ proof)
val (((proof, atp_run_time_in_msecs), rc), _) =
with_path cleanup export run_on (prob_pathname subgoal);
@@ -154,9 +173,10 @@
val success = rc = 0 andalso failure = "";
val (message, relevant_thm_names) =
if success then
- proof_text name proof internal_thm_names ctxt th subgoal
+ proof_text isar_proof debug modulus sorts ctxt
+ (minimize_command, proof, internal_thm_names, th, subgoal)
else if failure <> "" then
- (failure, [])
+ (failure ^ "\n", [])
else
("Unknown ATP error: " ^ proof ^ ".\n", [])
in
@@ -171,21 +191,19 @@
(* generic TPTP-based provers *)
fun generic_tptp_prover
- (name, {command, arguments, known_failures, max_new_clauses,
- prefers_theory_relevant, supports_isar_proofs})
+ (name, {home, executable, arguments, known_failures, max_new_clauses,
+ prefers_theory_relevant})
(params as {debug, overlord, respect_no_atp, relevance_threshold,
convergence, theory_relevant, higher_order, follow_defs,
- isar_proof, modulus, sorts, ...})
- timeout =
+ isar_proof, ...})
+ minimize_command timeout =
generic_prover overlord
(get_relevant_facts respect_no_atp relevance_threshold convergence
higher_order follow_defs max_new_clauses
(the_default prefers_theory_relevant theory_relevant))
(prepare_clauses higher_order false)
- (write_tptp_file (debug andalso overlord andalso not isar_proof)) command
- (arguments timeout) known_failures
- (proof_text (supports_isar_proofs andalso isar_proof) false modulus sorts)
- name params
+ (write_tptp_file (debug andalso overlord andalso not isar_proof)) home
+ executable (arguments timeout) known_failures name params minimize_command
fun tptp_prover name p = (name, generic_tptp_prover (name, p));
@@ -196,10 +214,11 @@
(* Vampire *)
-(* NB: Vampire does not work without explicit time limit. *)
+(* Vampire requires an explicit time limit. *)
val vampire_config : prover_config =
- {command = Path.explode "$VAMPIRE_HOME/vampire",
+ {home = getenv "VAMPIRE_HOME",
+ executable = "vampire",
arguments = (fn timeout => "--output_syntax tptp --mode casc -t " ^
string_of_int (generous_to_secs timeout)),
known_failures =
@@ -208,15 +227,15 @@
(["Refutation not found"],
"The ATP failed to determine the problem's status.")],
max_new_clauses = 60,
- prefers_theory_relevant = false,
- supports_isar_proofs = true}
+ prefers_theory_relevant = false}
val vampire = tptp_prover "vampire" vampire_config
(* E prover *)
val e_config : prover_config =
- {command = Path.explode "$E_HOME/eproof",
+ {home = getenv "E_HOME",
+ executable = "eproof",
arguments = (fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev \
\-tAutoDev --silent --cpu-limit=" ^
string_of_int (generous_to_secs timeout)),
@@ -228,44 +247,42 @@
(["# Cannot determine problem status"],
"The ATP failed to determine the problem's status.")],
max_new_clauses = 100,
- prefers_theory_relevant = false,
- supports_isar_proofs = true}
+ prefers_theory_relevant = false}
val e = tptp_prover "e" e_config
(* SPASS *)
fun generic_dfg_prover
- (name, ({command, arguments, known_failures, max_new_clauses,
- prefers_theory_relevant, ...} : prover_config))
+ (name, {home, executable, arguments, known_failures, max_new_clauses,
+ prefers_theory_relevant})
(params as {overlord, respect_no_atp, relevance_threshold, convergence,
theory_relevant, higher_order, follow_defs, ...})
- timeout =
+ minimize_command timeout =
generic_prover overlord
(get_relevant_facts respect_no_atp relevance_threshold convergence
higher_order follow_defs max_new_clauses
(the_default prefers_theory_relevant theory_relevant))
- (prepare_clauses higher_order true) write_dfg_file command
- (arguments timeout) known_failures (metis_proof_text false false)
- name params
+ (prepare_clauses higher_order true) write_dfg_file home executable
+ (arguments timeout) 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". *)
val spass_config : prover_config =
- {command = Path.explode "$SPASS_HOME/SPASS",
- arguments = (fn timeout => "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0" ^
- " -FullRed=0 -DocProof -VarWeight=3 -TimeLimit=" ^
- string_of_int (generous_to_secs timeout)),
- known_failures =
- [(["SPASS beiseite: Completion found."], "The ATP problem is unprovable."),
- (["SPASS beiseite: Ran out of time."], "The ATP timed out."),
- (["SPASS beiseite: Maximal number of loops exceeded."],
- "The ATP hit its loop limit.")],
- max_new_clauses = 40,
- prefers_theory_relevant = true,
- supports_isar_proofs = false}
+ {home = getenv "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 (generous_to_secs timeout)),
+ known_failures =
+ [(["SPASS beiseite: Completion found."], "The ATP problem is unprovable."),
+ (["SPASS beiseite: Ran out of time."], "The ATP timed out."),
+ (["SPASS beiseite: Maximal number of loops exceeded."],
+ "The ATP hit its loop limit.")],
+ max_new_clauses = 40,
+ prefers_theory_relevant = true}
val spass = dfg_prover "spass" spass_config
(* SPASS 3.7 supports both the DFG and the TPTP syntax, whereas SPASS 3.0
@@ -277,7 +294,8 @@
page once the package is there (around the Isabelle2010 release). *)
val spass_tptp_config =
- {command = #command spass_config,
+ {home = #home spass_config,
+ executable = #executable spass_config,
arguments = prefix "-TPTP " o #arguments spass_config,
known_failures =
#known_failures spass_config @
@@ -291,8 +309,7 @@
map Path.basic ["etc", "components"]))) ^
"\" on a line of its own.")],
max_new_clauses = #max_new_clauses spass_config,
- prefers_theory_relevant = #prefers_theory_relevant spass_config,
- supports_isar_proofs = #supports_isar_proofs spass_config}
+ prefers_theory_relevant = #prefers_theory_relevant spass_config}
val spass_tptp = tptp_prover "spass_tptp" spass_tptp_config
(* remote prover invocation via SystemOnTPTP *)
@@ -328,27 +345,29 @@
fun remote_prover_config prover_prefix args
({known_failures, max_new_clauses, prefers_theory_relevant, ...}
: prover_config) : prover_config =
- {command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP",
+ {home = getenv "ISABELLE_ATP_MANAGER",
+ executable = "SystemOnTPTP",
arguments = (fn timeout =>
args ^ " -t " ^ string_of_int (generous_to_secs timeout) ^ " -s " ^
the_system prover_prefix),
known_failures = remote_known_failures @ known_failures,
max_new_clauses = max_new_clauses,
- prefers_theory_relevant = prefers_theory_relevant,
- supports_isar_proofs = false}
+ prefers_theory_relevant = prefers_theory_relevant}
val remote_vampire =
- tptp_prover "remote_vampire"
+ tptp_prover (remotify (fst vampire))
(remote_prover_config "Vampire---9" "" vampire_config)
val remote_e =
- tptp_prover "remote_e" (remote_prover_config "EP---" "" e_config)
+ tptp_prover (remotify (fst e))
+ (remote_prover_config "EP---" "" e_config)
val remote_spass =
- tptp_prover "remote_spass" (remote_prover_config "SPASS---" "-x" spass_config)
+ tptp_prover (remotify (fst spass))
+ (remote_prover_config "SPASS---" "-x" spass_config)
-val provers = [spass, spass_tptp, vampire, e, remote_vampire, remote_spass,
- remote_e]
+val provers =
+ [spass, spass_tptp, vampire, e, remote_vampire, remote_spass, remote_e]
val prover_setup = fold add_prover provers
val setup =
@@ -357,4 +376,9 @@
#> measure_runtime_setup
#> prover_setup;
+fun maybe_remote (name, _) ({home, ...} : prover_config) =
+ name |> home = "" ? remotify
+
+val _ = atps := ([maybe_remote e e_config, maybe_remote spass spass_config,
+ remotify (fst vampire)] |> space_implode " ")
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Apr 23 10:00:53 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Apr 23 11:34:49 2010 +0200
@@ -68,6 +68,10 @@
("metis_proof", "isar_proof"),
("no_sorts", "sorts")]
+val params_for_minimize =
+ ["full_types", "explicit_apply", "higher_order", "isar_proof", "modulus",
+ "sorts", "minimize_timeout"]
+
val property_dependent_params = ["atps", "full_types", "timeout"]
fun is_known_raw_param s =
@@ -98,19 +102,11 @@
val extend = I
fun merge p : T = AList.merge (op =) (K true) p)
-(* Don't even try to start ATPs that are not installed.
- Hack: Should not rely on naming convention. *)
-val filter_atps =
- space_explode " "
- #> filter (fn s => String.isPrefix "remote_" s orelse
- getenv (String.map Char.toUpper s ^ "_HOME") <> "")
- #> space_implode " "
-
val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param
fun default_raw_params thy =
Data.get thy
|> fold (AList.default (op =))
- [("atps", [filter_atps (!atps)]),
+ [("atps", [!atps]),
("full_types", [if !full_types then "true" else "false"]),
("timeout", let val timeout = !timeout in
[if timeout <= 0 then "none"
@@ -219,18 +215,33 @@
val refresh_tptpN = "refresh_tptp"
val helpN = "help"
-
fun minimizize_raw_param_name "timeout" = "minimize_timeout"
| minimizize_raw_param_name name = name
+val is_raw_param_relevant_for_minimize =
+ member (op =) params_for_minimize o fst o unalias_raw_param
+fun string_for_raw_param (key, values) =
+ key ^ (case space_implode " " values of
+ "" => ""
+ | value => " = " ^ value)
+
+fun minimize_command override_params i atp_name facts =
+ "sledgehammer minimize [atp = " ^ atp_name ^
+ (override_params |> filter is_raw_param_relevant_for_minimize
+ |> implode o map (prefix ", " o string_for_raw_param)) ^
+ "] (" ^ space_implode " " facts ^ ")" ^
+ (if i = 1 then "" else " " ^ string_of_int i)
+
fun hammer_away override_params subcommand opt_i relevance_override state =
let
val thy = Proof.theory_of state
val _ = List.app check_raw_param override_params
in
if subcommand = runN then
- sledgehammer (get_params thy override_params) (the_default 1 opt_i)
- relevance_override state
+ let val i = the_default 1 opt_i in
+ sledgehammer (get_params thy override_params) i relevance_override
+ (minimize_command override_params i) state
+ end
else if subcommand = minimizeN then
minimize (map (apfst minimizize_raw_param_name) override_params) []
(the_default 1 opt_i) (#add relevance_override) state
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Apr 23 10:00:53 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Apr 23 11:34:49 2010 +0200
@@ -6,6 +6,8 @@
signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
sig
+ type minimize_command = string list -> string
+
val chained_hint: string
val invert_const: string -> string
val invert_type_const: string -> string
@@ -15,14 +17,16 @@
val is_proof_well_formed: string -> bool
val metis_line: int -> int -> string list -> string
val metis_proof_text:
- bool -> bool -> string -> string -> string vector -> Proof.context -> thm
- -> int -> string * string list
+ minimize_command * string * string vector * thm * int
+ -> string * string list
val isar_proof_text:
- bool -> int -> bool -> string -> string -> string vector -> Proof.context
- -> thm -> int -> string * string list
+ bool -> int -> bool -> Proof.context
+ -> minimize_command * string * string vector * thm * int
+ -> string * string list
val proof_text:
- bool -> bool -> int -> bool -> string -> string -> string vector
- -> Proof.context -> thm -> int -> string * string list
+ bool -> bool -> int -> bool -> Proof.context
+ -> minimize_command * string * string vector * thm * int
+ -> string * string list
end;
structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
@@ -31,6 +35,8 @@
open Sledgehammer_FOL_Clause
open Sledgehammer_Fact_Preprocessor
+type minimize_command = string list -> string
+
val trace_proof_path = Path.basic "atp_trace";
fun trace_proof_msg f =
@@ -38,9 +44,13 @@
fun string_of_thm ctxt = PrintMode.setmp [] (Display.string_of_thm ctxt);
+fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
+
+fun is_axiom thm_names line_no = line_no <= Vector.length thm_names
+
(**** PARSING OF TSTP FORMAT ****)
-(*Syntax trees, either termlist or formulae*)
+(* Syntax trees, either term list or formulae *)
datatype stree = Int of int | Br of string * stree list;
fun atom x = Br(x,[]);
@@ -49,48 +59,88 @@
val listof = List.foldl scons (atom "nil");
(*Strings enclosed in single quotes, e.g. filenames*)
-val quoted = $$"'" |-- Scan.repeat (~$$"'") --| $$"'" >> implode;
+val quoted = $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode;
(*Intended for $true and $false*)
fun tf s = "c_" ^ str (Char.toUpper (String.sub(s,0))) ^ String.extract(s,1,NONE);
-val truefalse = $$"$" |-- Symbol.scan_id >> (atom o tf);
+val truefalse = $$ "$" |-- Symbol.scan_id >> (atom o tf);
(*Integer constants, typically proof line numbers*)
fun is_digit s = Char.isDigit (String.sub(s,0));
val integer = Scan.many1 is_digit >> (the o Int.fromString o implode);
+(* needed for SPASS's nonstandard output format *)
+fun smart_Br ("equal", ts) = Br ("c_equal", rev ts)
+ | smart_Br p = Br p
+
(*Generalized FO terms, which include filenames, numbers, etc.*)
-fun termlist x = (term ::: Scan.repeat ($$"," |-- term)) x
-and term x = (quoted >> atom || integer>>Int || truefalse ||
- Symbol.scan_id -- Scan.optional ($$"(" |-- termlist --| $$")") [] >> Br ||
- $$"(" |-- term --| $$")" ||
- $$"[" |-- Scan.optional termlist [] --| $$"]" >> listof) x;
+fun term x = (quoted >> atom || integer >> Int || truefalse
+ || Symbol.scan_id
+ -- Scan.optional ($$ "(" |-- terms --| $$ ")") [] >> smart_Br
+ || $$ "(" |-- term --| $$ ")"
+ || $$ "[" |-- Scan.optional terms [] --| $$ "]" >> listof) x
+and terms x = (term ::: Scan.repeat ($$ "," |-- term)) x
-fun negate t = Br("c_Not", [t]);
-fun equate (t1,t2) = Br("c_equal", [t1,t2]);
+fun negate t = Br ("c_Not", [t])
+fun equate t1 t2 = Br ("c_equal", [t1, t2]);
(*Apply equal or not-equal to a term*)
fun syn_equal (t, NONE) = t
- | syn_equal (t1, SOME (NONE, t2)) = equate (t1,t2)
- | syn_equal (t1, SOME (SOME _, t2)) = negate (equate (t1,t2));
+ | syn_equal (t1, SOME (NONE, t2)) = equate t1 t2
+ | syn_equal (t1, SOME (SOME _, t2)) = negate (equate t1 t2)
(*Literals can involve negation, = and !=.*)
-fun literal x = ($$"~" |-- literal >> negate ||
- (term -- Scan.option (Scan.option ($$"!") --| $$"=" -- term) >> syn_equal)) x;
+fun literal x =
+ ($$ "~" |-- literal >> negate
+ || (term -- Scan.option (Scan.option ($$ "!") --| $$ "=" -- term)
+ >> syn_equal)) x
-val literals = literal ::: Scan.repeat ($$"|" |-- literal);
+val literals = literal ::: Scan.repeat ($$ "|" |-- literal);
(*Clause: a list of literals separated by the disjunction sign*)
-val clause = $$"(" |-- literals --| $$")" || Scan.single literal;
+val clause = $$ "(" |-- literals --| $$ ")" || Scan.single literal;
+
+fun ints_of_stree (Int n) = cons n
+ | ints_of_stree (Br (_, ts)) = fold ints_of_stree ts
+
+val tstp_annotations =
+ Scan.optional ($$ "," |-- term --| Scan.option ($$ "," |-- terms)
+ >> (fn source => ints_of_stree source [])) []
+
+fun retuple_tstp_line ((name, ts), deps) = (name, ts, deps)
-val annotations = $$"," |-- term -- Scan.option ($$"," |-- termlist);
+(* <cnf_annotated> ::= cnf(<name>, <formula_role>, <cnf_formula> <annotations>).
+ The <name> could be an identifier, but we assume integers. *)
+val parse_tstp_line =
+ (Scan.this_string "cnf" -- $$ "(") |-- integer --| $$ "," --| Symbol.scan_id
+ --| $$ "," -- clause -- tstp_annotations --| $$ ")" --| $$ "."
+ >> retuple_tstp_line
+
+(**** PARSING OF SPASS OUTPUT ****)
+
+val dot_name = integer --| $$ "." --| integer
-(*<cnf_annotated> ::= cnf(<name>,<formula_role>,<cnf_formula><annotations>).
- The <name> could be an identifier, but we assume integers.*)
-val tstp_line = (Scan.this_string "cnf" -- $$"(") |--
- integer --| $$"," -- Symbol.scan_id --| $$"," --
- clause -- Scan.option annotations --| $$ ")";
+val spass_annotations =
+ Scan.optional ($$ ":" |-- Scan.repeat (dot_name --| Scan.option ($$ ","))) []
+
+val starred_literal = literal --| Scan.repeat ($$ "*" || $$ " ")
+
+val horn_clause =
+ Scan.repeat starred_literal --| $$ "-" --| $$ ">"
+ -- Scan.repeat starred_literal
+ >> (fn ([], []) => [atom (tf "false")]
+ | (clauses1, clauses2) => map negate clauses1 @ clauses2)
+fun retuple_spass_proof_line ((name, deps), ts) = (name, ts, deps)
+
+(* Syntax: <name>[0:<inference><annotations>] || -> <cnf_formula> **. *)
+val parse_spass_proof_line =
+ integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
+ -- spass_annotations --| $$ "]" --| $$ "|" --| $$ "|" -- horn_clause
+ --| $$ "."
+ >> retuple_spass_proof_line
+
+val parse_proof_line = fst o (parse_tstp_line || parse_spass_proof_line)
(**** INTERPRETATION OF TSTP SYNTAX TREES ****)
@@ -111,7 +161,8 @@
SOME c' => c'
| NONE => c;
-fun make_tvar b = TVar(("'" ^ b, 0), HOLogic.typeS);
+fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS);
+fun make_tparam s = TypeInfer.param 0 (s, HOLogic.typeS)
fun make_var (b,T) = Var((b,0),T);
(*Type variables are given the basic sort, HOL.type. Some will later be constrained
@@ -132,7 +183,7 @@
| NONE =>
case strip_prefix tvar_prefix a of
SOME b => make_tvar b
- | NONE => make_tvar a (*Variable from the ATP, say X1*)
+ | NONE => make_tparam a (* Variable from the ATP, say "X1" *)
end;
(*Invert the table of translations between Isabelle and ATPs*)
@@ -178,7 +229,7 @@
| NONE =>
case strip_prefix schematic_var_prefix a of
SOME b => make_var (b,T)
- | NONE => make_var (a,T) (*Variable from the ATP, say X1*)
+ | NONE => make_var (a,T) (* Variable from the ATP, say "X1" *)
in list_comb (opr, List.map (term_of_stree [] thy) (ts@args)) end;
(*Type class literal applied to a type. Returns triple of polarity, class, type.*)
@@ -226,32 +277,21 @@
| tmsubst (t as Bound _) = t
| tmsubst (Abs (a, T, t)) = Abs (a, tysubst T, tmsubst t)
| tmsubst (t $ u) = tmsubst t $ tmsubst u;
- in fn t => if Vartab.is_empty vt then t else tmsubst t end;
+ in not (Vartab.is_empty vt) ? tmsubst end;
(*Interpret a list of syntax trees as a clause, given by "real" literals and sort constraints.
vt0 holds the initial sort constraints, from the conjecture clauses.*)
fun clause_of_strees ctxt vt0 ts =
let val (vt, dt) = lits_of_strees ctxt (vt0,[]) ts in
singleton (Syntax.check_terms ctxt) (TypeInfer.constrain HOLogic.boolT (fix_sorts vt dt))
- end;
+ end
fun gen_all_vars t = fold_rev Logic.all (OldTerm.term_vars t) t;
-fun ints_of_stree_aux (Int n, ns) = n::ns
- | ints_of_stree_aux (Br(_,ts), ns) = List.foldl ints_of_stree_aux ns ts;
-
-fun ints_of_stree t = ints_of_stree_aux (t, []);
-
-fun decode_tstp vt0 (name, role, ts, annots) ctxt =
- let val deps = case annots of NONE => [] | SOME (source,_) => ints_of_stree source
- val cl = clause_of_strees ctxt vt0 ts
- in ((name, role, cl, deps), fold Variable.declare_term (OldTerm.term_frees cl) ctxt) end;
-
-fun dest_tstp ((((name, role), ts), annots), chs) =
- case chs of
- "."::_ => (name, role, ts, annots)
- | _ => error ("TSTP line not terminated by \".\": " ^ implode chs);
-
+fun decode_proof_step vt0 (name, ts, deps) ctxt =
+ let val cl = clause_of_strees ctxt vt0 ts in
+ ((name, cl, deps), fold Variable.declare_term (OldTerm.term_frees cl) ctxt)
+ end
(** Global sort constraints on TFrees (from tfree_tcs) are positive unit clauses. **)
@@ -268,9 +308,10 @@
(**** Translation of TSTP files to Isar Proofs ****)
-fun decode_tstp_list ctxt tuples =
- let val vt0 = tfree_constraints_of_clauses Vartab.empty (map #3 tuples)
- in #1 (fold_map (decode_tstp vt0) tuples ctxt) end;
+fun decode_proof_steps ctxt tuples =
+ let val vt0 = tfree_constraints_of_clauses Vartab.empty (map #2 tuples) in
+ #1 (fold_map (decode_proof_step vt0) tuples ctxt)
+ end
(** Finding a matching assumption. The literals may be permuted, and variable names
may disagree. We have to try all combinations of literals (quadratic!) and
@@ -342,9 +383,10 @@
fun have_or_show "show" _ = " show \""
| have_or_show have lname = " " ^ have ^ " " ^ lname ^ ": \""
fun do_line _ (lname, t, []) =
- (* No deps: it's a conjecture clause, with no proof. *)
+ (* No depedencies: it's a conjecture clause, with no proof. *)
(case permuted_clause t ctms of
SOME u => " assume " ^ lname ^ ": \"" ^ string_of_term u ^ "\"\n"
+ | NONE => " assume? " ^ lname ^ ": \"" ^ string_of_term t ^ "\"\n"
| NONE => raise TERM ("Sledgehammer_Proof_Reconstruct.isar_proof_body",
[t]))
| do_line have (lname, t, deps) =
@@ -368,17 +410,21 @@
(*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ
only in type information.*)
-fun add_prfline ((lno, "axiom", t, []), lines) = (*axioms are not proof lines*)
- if eq_types t (*must be clsrel/clsarity: type information, so delete refs to it*)
- then map (replace_deps (lno, [])) lines
+fun add_proof_line thm_names (lno, t, []) lines =
+ (* No dependencies: axiom or conjecture clause *)
+ if is_axiom thm_names lno then
+ (* Axioms are not proof lines *)
+ if eq_types t then
+ (* Must be clsrel/clsarity: type information, so delete refs to it *)
+ map (replace_deps (lno, [])) lines
+ else
+ (case take_prefix (unequal t) lines of
+ (_,[]) => lines (*no repetition of proof line*)
+ | (pre, (lno', _, _) :: post) => (*repetition: replace later line by earlier one*)
+ pre @ map (replace_deps (lno', [lno])) post)
else
- (case take_prefix (unequal t) lines of
- (_,[]) => lines (*no repetition of proof line*)
- | (pre, (lno', _, _) :: post) => (*repetition: replace later line by earlier one*)
- pre @ map (replace_deps (lno', [lno])) post)
- | add_prfline ((lno, _, t, []), lines) = (*no deps: conjecture clause*)
- (lno, t, []) :: lines
- | add_prfline ((lno, _, t, deps), lines) =
+ (lno, t, []) :: lines
+ | add_proof_line _ (lno, t, deps) lines =
if eq_types t then (lno, t, deps) :: lines
(*Type information will be deleted later; skip repetition test.*)
else (*FIXME: Doesn't this code risk conflating proofs involving different types??*)
@@ -417,12 +463,12 @@
(*Replace numeric proof lines by strings, either from thm_names or sequential line numbers*)
fun stringify_deps thm_names deps_map [] = []
| stringify_deps thm_names deps_map ((lno, t, deps) :: lines) =
- if lno <= Vector.length thm_names (*axiom*)
- then (Vector.sub(thm_names,lno-1), t, []) :: stringify_deps thm_names deps_map lines
+ if is_axiom thm_names lno then
+ (Vector.sub(thm_names,lno-1), t, []) :: stringify_deps thm_names deps_map lines
else let val lname = Int.toString (length deps_map)
- fun fix lno = if lno <= Vector.length thm_names
+ fun fix lno = if is_axiom thm_names lno
then SOME(Vector.sub(thm_names,lno-1))
- else AList.lookup op= deps_map lno;
+ else AList.lookup (op =) deps_map lno;
in (lname, t, map_filter fix (distinct (op=) deps)) ::
stringify_deps thm_names ((lno,lname)::deps_map) lines
end;
@@ -435,14 +481,15 @@
fun isar_proof_end 1 = "qed"
| isar_proof_end _ = "next"
-fun isar_proof_from_tstp_file cnfs modulus sorts ctxt goal i thm_names =
+fun isar_proof_from_atp_proof cnfs modulus sorts ctxt goal i thm_names =
let
- val _ = trace_proof_msg (K "\nisar_proof_from_tstp_file: start\n")
- val tuples = map (dest_tstp o tstp_line o explode) cnfs
+ val _ = trace_proof_msg (K "\nisar_proof_from_atp_proof: start\n")
+ val tuples = map (parse_proof_line o explode) cnfs
val _ = trace_proof_msg (fn () =>
Int.toString (length tuples) ^ " tuples extracted\n")
val ctxt = ProofContext.set_mode ProofContext.mode_schematic ctxt
- val raw_lines = List.foldr add_prfline [] (decode_tstp_list ctxt tuples)
+ val raw_lines =
+ fold_rev (add_proof_line thm_names) (decode_proof_steps ctxt tuples) []
val _ = trace_proof_msg (fn () =>
Int.toString (length raw_lines) ^ " raw_lines extracted\n")
val nonnull_lines = List.foldr add_nonnull_prfline [] raw_lines
@@ -460,12 +507,12 @@
val body = isar_proof_body ctxt sorts (map prop_of ccls)
(stringify_deps thm_names [] lines)
val n = Logic.count_prems (prop_of goal)
- val _ = trace_proof_msg (K "\nisar_proof_from_tstp_file: finishing\n")
+ val _ = trace_proof_msg (K "\nisar_proof_from_atp_proof: finishing\n")
in
isar_proof_start i ^ isar_fixes (map #1 fixes) ^ implode body ^
isar_proof_end n ^ "\n"
end
- handle STREE _ => error "Could not extract proof (ATP output malformed?)";
+ handle STREE _ => raise Fail "Cannot parse ATP output";
(*=== EXTRACTING PROOF-TEXT === *)
@@ -479,23 +526,19 @@
"Formulae used in the proof"];
fun get_proof_extract proof =
- let
- (*splits to_split by the first possible of a list of splitters*)
- val (begin_string, end_string) =
- (find_first (fn s => String.isSubstring s proof) begin_proof_strs,
- find_first (fn s => String.isSubstring s proof) end_proof_strs)
- in
- if is_none begin_string orelse is_none end_string
- then error "Could not extract proof (no substring indicating a proof)"
- else proof |> first_field (the begin_string) |> the |> snd
- |> first_field (the end_string) |> the |> fst
- end;
+ (* Splits by the first possible of a list of splitters. *)
+ case pairself (find_first (fn s => String.isSubstring s proof))
+ (begin_proof_strs, end_proof_strs) of
+ (SOME begin_string, SOME end_string) =>
+ proof |> first_field begin_string |> the |> snd
+ |> first_field end_string |> the |> fst
+ | _ => raise Fail "Cannot extract proof"
(* ==== CHECK IF PROOF WAS SUCCESSFUL === *)
fun is_proof_well_formed proof =
- exists (fn s => String.isSubstring s proof) begin_proof_strs andalso
- exists (fn s => String.isSubstring s proof) end_proof_strs
+ forall (exists (fn s => String.isSubstring s proof))
+ [begin_proof_strs, end_proof_strs]
(* === EXTRACTING LEMMAS === *)
(* A list consisting of the first number in each line is returned.
@@ -505,11 +548,11 @@
extracted. *)
fun get_step_nums proof_extract =
let
- val toks = String.tokens (not o Char.isAlphaNum)
+ val toks = String.tokens (not o is_ident_char)
fun inputno ("cnf" :: ntok :: "axiom" :: _) = Int.fromString ntok
- | inputno ("cnf" :: ntok :: "negated" :: "conjecture" :: _) =
+ | inputno ("cnf" :: ntok :: "negated_conjecture" :: _) =
Int.fromString ntok
- | inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok (* DFG *)
+ | inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok (* DFG format *)
| inputno _ = NONE
val lines = split_lines proof_extract
in map_filter (inputno o toks) lines end
@@ -528,55 +571,76 @@
fun metis_line i n xs =
"Try this command: " ^
Markup.markup Markup.sendback (metis_command i n xs) ^ ".\n"
-fun minimize_line _ _ [] = ""
- | minimize_line isar_proof atp_name xs =
+fun minimize_line _ [] = ""
+ | minimize_line minimize_command facts =
+ case minimize_command facts of
+ "" => ""
+ | command =>
"To minimize the number of lemmas, try this command: " ^
- Markup.markup Markup.sendback
- ("sledgehammer minimize [atp = " ^ atp_name ^
- (if isar_proof then ", isar_proof" else "") ^ "] (" ^
- space_implode " " xs ^ ")") ^ ".\n"
+ Markup.markup Markup.sendback command ^ ".\n"
-fun metis_proof_text isar_proof minimal atp_name proof thm_names
- (_ : Proof.context) goal i =
+fun metis_proof_text (minimize_command, proof, thm_names, goal, i) =
let
val lemmas =
proof |> get_proof_extract
|> get_step_nums
- |> filter (fn i => i <= Vector.length thm_names)
+ |> filter (is_axiom thm_names)
|> map (fn i => Vector.sub (thm_names, i - 1))
|> filter (fn x => x <> "??.unknown")
|> sort_distinct string_ord
val n = Logic.count_prems (prop_of goal)
val xs = kill_chained lemmas
in
- (metis_line i n xs ^
- (if minimal then "" else minimize_line isar_proof atp_name xs),
- kill_chained lemmas)
+ (metis_line i n xs ^ minimize_line minimize_command xs, kill_chained lemmas)
end
-fun isar_proof_text minimal modulus sorts atp_name proof thm_names ctxt goal i =
+val is_proof_line = String.isPrefix "cnf(" orf String.isSubstring "||"
+
+fun do_space c = if Char.isSpace c then "" else str c
+
+fun strip_spaces_in_list [] = ""
+ | strip_spaces_in_list [c1] = do_space c1
+ | strip_spaces_in_list [c1, c2] = do_space c1 ^ do_space c2
+ | strip_spaces_in_list (c1 :: c2 :: c3 :: cs) =
+ if Char.isSpace c1 then
+ strip_spaces_in_list (c2 :: c3 :: cs)
+ else if Char.isSpace c2 then
+ if Char.isSpace c3 then
+ strip_spaces_in_list (c1 :: c3 :: cs)
+ else
+ str c1 ^
+ (if is_ident_char c1 andalso is_ident_char c3 then " " else "") ^
+ strip_spaces_in_list (c3 :: cs)
+ else
+ str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs)
+
+val strip_spaces = strip_spaces_in_list o String.explode
+
+fun isar_proof_text debug modulus sorts ctxt
+ (minimize_command, proof, thm_names, goal, i) =
let
- (* We could use "split_lines", but it can return blank lines. *)
- val lines = String.tokens (equal #"\n");
- val kill_spaces =
- String.translate (fn c => if Char.isSpace c then "" else str c)
- val extract = get_proof_extract proof
- val cnfs = filter (String.isPrefix "cnf(") (map kill_spaces (lines extract))
+ val cnfs = proof |> get_proof_extract |> split_lines |> map strip_spaces
+ |> filter is_proof_line
val (one_line_proof, lemma_names) =
- metis_proof_text true minimal atp_name proof thm_names ctxt goal i
+ metis_proof_text (minimize_command, proof, thm_names, goal, i)
val tokens = String.tokens (fn c => c = #" ") one_line_proof
+ fun isar_proof_for () =
+ case isar_proof_from_atp_proof cnfs modulus sorts ctxt goal i thm_names of
+ "" => ""
+ | isar_proof =>
+ "\nStructured proof:\n" ^ Markup.markup Markup.sendback isar_proof
val isar_proof =
- if member (op =) tokens chained_hint then ""
- else isar_proof_from_tstp_file cnfs modulus sorts ctxt goal i thm_names
- in
- (one_line_proof ^
- (if isar_proof = "" then ""
- else "\nStructured proof:\n" ^ Markup.markup Markup.sendback isar_proof),
- lemma_names)
- end
+ if member (op =) tokens chained_hint then
+ ""
+ else if debug then
+ isar_proof_for ()
+ else
+ try isar_proof_for ()
+ |> the_default "Warning: The Isar proof construction failed.\n"
+ in (one_line_proof ^ isar_proof, lemma_names) end
-fun proof_text isar_proof minimal modulus sorts =
- if isar_proof then isar_proof_text minimal modulus sorts
- else metis_proof_text isar_proof minimal
+fun proof_text isar_proof debug modulus sorts ctxt =
+ if isar_proof then isar_proof_text debug modulus sorts ctxt
+ else metis_proof_text
end;