support readable names even when Isar proof reconstruction is enabled -- useful for debugging
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Sun Apr 25 10:22:31 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Sun Apr 25 11:38:46 2010 +0200
@@ -8,6 +8,7 @@
signature ATP_MANAGER =
sig
+ type name_pool = Sledgehammer_HOL_Clause.name_pool
type relevance_override = Sledgehammer_Fact_Filter.relevance_override
type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
type params =
@@ -40,6 +41,7 @@
type prover_result =
{outcome: failure option,
message: string,
+ pool: name_pool option,
relevant_thm_names: string list,
atp_run_time_in_msecs: int,
output: string,
@@ -102,6 +104,7 @@
type prover_result =
{outcome: failure option,
message: string,
+ pool: name_pool option,
relevant_thm_names: string list,
atp_run_time_in_msecs: int,
output: string,
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Sun Apr 25 10:22:31 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Sun Apr 25 11:38:46 2010 +0200
@@ -88,6 +88,8 @@
| string_for_failure TimedOut = "Timed out."
| string_for_failure OutOfResources = "The ATP ran out of resources."
| string_for_failure OldSpass =
+ (* FIXME: Change the error message below to point to the Isabelle download
+ page once the package is there (around the Isabelle2010 release). *)
"Warning: Sledgehammer requires a more recent version of SPASS with \
\support for the TPTP syntax. To install it, download and untar the \
\package \"http://isabelle.in.tum.de/~blanchet/spass-3.7.tgz\" and add the \
@@ -193,7 +195,7 @@
else
"") ^ output)
- val (((output, atp_run_time_in_msecs), res_code), _) =
+ val (((output, atp_run_time_in_msecs), res_code), pool) =
with_path cleanup export run_on (prob_pathname subgoal);
(* Check for success and print out some information on failure. *)
@@ -201,12 +203,12 @@
extract_proof_and_outcome res_code proof_delims known_failures output
val (message, relevant_thm_names) =
case outcome of
- NONE => proof_text isar_proof debug modulus sorts ctxt
+ NONE => proof_text isar_proof pool debug modulus sorts ctxt
(minimize_command, proof, internal_thm_names, th,
subgoal)
| SOME failure => (string_for_failure failure ^ "\n", [])
in
- {outcome = outcome, message = message,
+ {outcome = outcome, message = message, pool = pool,
relevant_thm_names = relevant_thm_names,
atp_run_time_in_msecs = atp_run_time_in_msecs, output = output,
proof = proof, internal_thm_names = internal_thm_names,
@@ -228,7 +230,7 @@
higher_order follow_defs max_axiom_clauses
(the_default prefers_theory_relevant theory_relevant))
(prepare_clauses higher_order false)
- (write_tptp_file (debug andalso overlord andalso not isar_proof)) home
+ (write_tptp_file (debug andalso overlord)) home
executable (arguments timeout) proof_delims known_failures name params
minimize_command
@@ -326,9 +328,6 @@
users have upgraded to 3.7, we can kill "spass" (and all DFG support in
Sledgehammer) and rename "spass_tptp" "spass". *)
-(* FIXME: Change the error message below to point to the Isabelle download
- page once the package is there (around the Isabelle2010 release). *)
-
val spass_tptp_config =
{home = #home spass_config,
executable = #executable spass_config,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Sun Apr 25 10:22:31 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Sun Apr 25 11:38:46 2010 +0200
@@ -1,5 +1,6 @@
(* Title: HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
Author: Jia Meng, Cambridge University Computer Laboratory, NICTA
+ Author: Jasmin Blanchette, TU Muenchen
*)
signature SLEDGEHAMMER_FACT_FILTER =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Sun Apr 25 10:22:31 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Sun Apr 25 11:38:46 2010 +0200
@@ -92,13 +92,14 @@
in
(* try prove first to check result and get used theorems *)
(case test_thms_fun NONE name_thms_pairs of
- result as {outcome = NONE, internal_thm_names, filtered_clauses, ...} =>
+ result as {outcome = NONE, pool, internal_thm_names, filtered_clauses,
+ ...} =>
let
val used = internal_thm_names |> Vector.foldr (op ::) []
|> sort_distinct string_ord
val to_use =
if length used < length name_thms_pairs then
- filter (fn (name1, _) => List.exists (curry (op =) name1) used)
+ filter (fn (name1, _) => exists (curry (op =) name1) used)
name_thms_pairs
else name_thms_pairs
val (min_thms, {proof, internal_thm_names, ...}) =
@@ -109,7 +110,7 @@
["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ ".")
in
(SOME min_thms,
- proof_text isar_proof debug modulus sorts ctxt
+ proof_text isar_proof pool debug modulus sorts ctxt
(K "", proof, internal_thm_names, goal, i) |> fst)
end
| {outcome = SOME TimedOut, ...} =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Sun Apr 25 10:22:31 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Sun Apr 25 11:38:46 2010 +0200
@@ -1,5 +1,6 @@
(* Title: HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
Author: Jia Meng, Cambridge University Computer Laboratory
+ Author: Jasmin Blanchette, TU Muenchen
Transformation of axiom rules (elim/intro/etc) into CNF forms.
*)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Sun Apr 25 10:22:31 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Sun Apr 25 11:38:46 2010 +0200
@@ -1,5 +1,6 @@
(* Title: HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
Author: Jia Meng, Cambridge University Computer Laboratory
+ Author: Jasmin Blanchette, TU Muenchen
Storing/printing FOL clauses and arity clauses. Typed equality is
treated differently.
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Sun Apr 25 10:22:31 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Sun Apr 25 11:38:46 2010 +0200
@@ -8,6 +8,7 @@
signature SLEDGEHAMMER_HOL_CLAUSE =
sig
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
@@ -37,10 +38,10 @@
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 -> unit
+ classrel_clause list * arity_clause list -> name_pool option
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 -> unit
+ classrel_clause list * arity_clause list -> name_pool option
end
structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE =
@@ -500,7 +501,9 @@
fun write_tptp_file readable_names full_types explicit_apply file clauses =
let
fun section _ [] = []
- | section name ss = "\n% " ^ name ^ plural_s (length ss) ^ "\n" :: ss
+ | 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
@@ -515,16 +518,16 @@
val arity_clss = map tptp_arity_clause arity_clauses
val (helper_clss, pool) = pool_map (apfst fst oo tptp_clause params)
helper_clauses pool
- in
- File.write_list file
- (header () ::
- section "Relevant fact" ax_clss @
- section "Type variable" tfree_clss @
- section "Conjecture" conjecture_clss @
- section "Class relationship" classrel_clss @
- section "Arity declaration" arity_clss @
- section "Helper fact" helper_clss)
- end
+ val _ =
+ File.write_list file
+ (header () ::
+ section "Relevant fact" ax_clss @
+ section "Helper fact" helper_clss @
+ section "Type variable" tfree_clss @
+ section "Conjecture" conjecture_clss @
+ section "Class relationship" classrel_clss @
+ section "Arity declaration" arity_clss)
+ in pool end
(* DFG format *)
@@ -541,30 +544,30 @@
val params = (full_types, explicit_apply, cma, cnh)
val ((conjecture_clss, tfree_litss), pool) =
pool_map (dfg_clause params) conjectures pool |>> ListPair.unzip
- and probname = Path.implode (Path.base file)
+ and 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 (union_all tfree_litss)
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
and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
- in
- File.write_list file
- (header () ::
- string_of_start probname ::
- string_of_descrip probname ::
- string_of_symbols (string_of_funcs funcs)
- (string_of_preds (cl_preds @ ty_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"] @
- tfree_clss @
- conjecture_clss @
- ["end_of_list.\n\n",
- "end_problem.\n"])
- end
+ 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 (cl_preds @ ty_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"] @
+ tfree_clss @
+ conjecture_clss @
+ ["end_of_list.\n\n",
+ "end_problem.\n"])
+ in pool end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Sun Apr 25 10:22:31 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Sun Apr 25 11:38:46 2010 +0200
@@ -8,6 +8,7 @@
signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
sig
type minimize_command = string list -> string
+ type name_pool = Sledgehammer_FOL_Clause.name_pool
val chained_hint: string
val invert_const: string -> string
@@ -20,11 +21,11 @@
minimize_command * string * string vector * thm * int
-> string * string list
val isar_proof_text:
- bool -> int -> bool -> Proof.context
+ name_pool option -> bool -> int -> bool -> Proof.context
-> minimize_command * string * string vector * thm * int
-> string * string list
val proof_text:
- bool -> bool -> int -> bool -> Proof.context
+ bool -> name_pool option -> bool -> int -> bool -> Proof.context
-> minimize_command * string * string vector * thm * int
-> string * string list
end;
@@ -37,18 +38,23 @@
type minimize_command = string list -> string
-val trace_proof_path = Path.basic "sledgehammer_trace_proof"
-
-fun trace_proof_msg f =
- if !trace then File.append (File.tmp_path trace_proof_path) (f ()) else ();
-
-fun string_of_thm ctxt = PrintMode.setmp [] (Display.string_of_thm ctxt);
-
fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
fun is_head_digit s = Char.isDigit (String.sub (s, 0))
fun is_axiom thm_names line_no = line_no <= Vector.length thm_names
+fun ugly_name NONE s = s
+ | ugly_name (SOME the_pool) s =
+ case Symtab.lookup (snd the_pool) s of
+ SOME s' => s'
+ | NONE => s
+
+val trace_path = Path.basic "sledgehammer_proof_trace"
+fun trace_proof_msg f =
+ if !trace then File.append (File.tmp_path trace_path) (f ()) else ();
+
+val string_of_thm = PrintMode.setmp [] o Display.string_of_thm
+
(**** PARSING OF TSTP FORMAT ****)
(* Syntax trees, either term list or formulae *)
@@ -66,52 +72,60 @@
val parse_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
(* needed for SPASS's output format *)
-fun fix_bool_literal "true" = "c_True"
- | fix_bool_literal "false" = "c_False"
-fun fix_symbol "equal" = "c_equal"
- | fix_symbol s = s
+fun repair_bool_literal "true" = "c_True"
+ | repair_bool_literal "false" = "c_False"
+fun repair_name pool "equal" = "c_equal"
+ | repair_name pool s = ugly_name pool s
(* Generalized first-order terms, which include file names, numbers, etc. *)
-fun parse_term x =
+(* The "x" argument is not strictly necessary, but without it Poly/ML loops
+ forever at compile time. *)
+fun parse_term pool x =
(parse_quoted >> atom
|| parse_integer >> SInt
- || $$ "$" |-- Symbol.scan_id >> (atom o fix_bool_literal)
- || (Symbol.scan_id >> fix_symbol)
- -- Scan.optional ($$ "(" |-- parse_terms --| $$ ")") [] >> SBranch
- || $$ "(" |-- parse_term --| $$ ")"
- || $$ "[" |-- Scan.optional parse_terms [] --| $$ "]" >> slist_of) x
-and parse_terms x = (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x
+ || $$ "$" |-- Symbol.scan_id >> (atom o repair_bool_literal)
+ || (Symbol.scan_id >> repair_name pool)
+ -- Scan.optional ($$ "(" |-- parse_terms pool --| $$ ")") [] >> SBranch
+ || $$ "(" |-- parse_term pool --| $$ ")"
+ || $$ "[" |-- Scan.optional (parse_terms pool) [] --| $$ "]" >> slist_of) x
+and parse_terms pool x =
+ (parse_term pool ::: Scan.repeat ($$ "," |-- parse_term pool)) x
fun negate_stree t = SBranch ("c_Not", [t])
fun equate_strees t1 t2 = SBranch ("c_equal", [t1, t2]);
(* Apply equal or not-equal to a term. *)
-fun do_equal (t, NONE) = t
- | do_equal (t1, SOME (NONE, t2)) = equate_strees t1 t2
- | do_equal (t1, SOME (SOME _, t2)) = negate_stree (equate_strees t1 t2)
+fun repair_predicate_term (t, NONE) = t
+ | repair_predicate_term (t1, SOME (NONE, t2)) = equate_strees t1 t2
+ | repair_predicate_term (t1, SOME (SOME _, t2)) =
+ negate_stree (equate_strees t1 t2)
+fun parse_predicate_term pool =
+ parse_term pool -- Scan.option (Scan.option ($$ "!") --| $$ "="
+ -- parse_term pool)
+ >> repair_predicate_term
(*Literals can involve negation, = and !=.*)
-fun parse_literal x =
- ($$ "~" |-- parse_literal >> negate_stree
- || (parse_term -- Scan.option (Scan.option ($$ "!") --| $$ "=" -- parse_term)
- >> do_equal)) x
+fun parse_literal pool x =
+ ($$ "~" |-- parse_literal pool >> negate_stree || parse_predicate_term pool) x
-val parse_literals = parse_literal ::: Scan.repeat ($$ "|" |-- parse_literal)
+fun parse_literals pool =
+ parse_literal pool ::: Scan.repeat ($$ "|" |-- parse_literal pool)
(*Clause: a list of literals separated by the disjunction sign*)
-val parse_clause =
- $$ "(" |-- parse_literals --| $$ ")" || Scan.single parse_literal
+fun parse_clause pool =
+ $$ "(" |-- parse_literals pool --| $$ ")" || Scan.single (parse_literal pool)
fun ints_of_stree (SInt n) = cons n
| ints_of_stree (SBranch (_, ts)) = fold ints_of_stree ts
val parse_tstp_annotations =
- Scan.optional ($$ "," |-- parse_term --| Scan.option ($$ "," |-- parse_terms)
+ Scan.optional ($$ "," |-- parse_term NONE
+ --| Scan.option ($$ "," |-- parse_terms NONE)
>> (fn source => ints_of_stree source [])) []
(* <cnf_annotated> ::= cnf(<name>, <formula_role>, <cnf_formula> <annotations>).
The <name> could be an identifier, but we assume integers. *)
fun retuple_tstp_line ((name, ts), deps) = (name, ts, deps)
-val parse_tstp_line =
+fun parse_tstp_line pool =
(Scan.this_string "cnf" -- $$ "(") |-- parse_integer --| $$ ","
- --| Symbol.scan_id --| $$ "," -- parse_clause -- parse_tstp_annotations
+ --| Symbol.scan_id --| $$ "," -- parse_clause pool -- parse_tstp_annotations
--| $$ ")" --| $$ "."
>> retuple_tstp_line
@@ -127,23 +141,26 @@
(* It is not clear why some literals are followed by sequences of stars. We
ignore them. *)
-val parse_starred_literal = parse_literal --| Scan.repeat ($$ "*" || $$ " ")
+fun parse_starred_predicate_term pool =
+ parse_predicate_term pool --| Scan.repeat ($$ "*" || $$ " ")
-val parse_horn_clause =
- Scan.repeat parse_starred_literal --| $$ "-" --| $$ ">"
- -- Scan.repeat parse_starred_literal
+fun parse_horn_clause pool =
+ Scan.repeat (parse_starred_predicate_term pool) --| $$ "-" --| $$ ">"
+ -- Scan.repeat (parse_starred_predicate_term pool)
>> (fn ([], []) => [atom "c_False"]
| (clauses1, clauses2) => map negate_stree clauses1 @ clauses2)
-(* Syntax: <name>[0:<inference><annotations>] || -> <cnf_formula>. *)
+(* Syntax: <name>[0:<inference><annotations>] ||
+ <cnf_formulas> -> <cnf_formulas>. *)
fun retuple_spass_proof_line ((name, deps), ts) = (name, ts, deps)
-val parse_spass_proof_line =
+fun parse_spass_proof_line pool =
parse_integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
-- parse_spass_annotations --| $$ "]" --| $$ "|" --| $$ "|"
- -- parse_horn_clause --| $$ "."
+ -- parse_horn_clause pool --| $$ "."
>> retuple_spass_proof_line
-val parse_proof_line = fst o (parse_tstp_line || parse_spass_proof_line)
+fun parse_proof_line pool =
+ fst o (parse_tstp_line pool || parse_spass_proof_line pool)
(**** INTERPRETATION OF TSTP SYNTAX TREES ****)
@@ -271,7 +288,7 @@
lits_of_strees ctxt (vt, term_of_stree [] (ProofContext.theory_of ctxt) t :: lits) ts;
(*Update TVars/TFrees with detected sort constraints.*)
-fun fix_sorts vt =
+fun repair_sorts vt =
let fun tysubst (Type (a, Ts)) = Type (a, map tysubst Ts)
| tysubst (TVar (xi, s)) = TVar (xi, the_default s (Vartab.lookup vt xi))
| tysubst (TFree (x, s)) = TFree (x, the_default s (Vartab.lookup vt (x, ~1)))
@@ -285,9 +302,10 @@
(*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))
+fun clause_of_strees ctxt vt ts =
+ let val (vt, dt) = lits_of_strees ctxt (vt, []) ts in
+ dt |> repair_sorts vt |> TypeInfer.constrain HOLogic.boolT
+ |> Syntax.check_term ctxt
end
fun gen_all_vars t = fold_rev Logic.all (OldTerm.term_vars t) t;
@@ -491,10 +509,10 @@
fun isar_proof_end 1 = "qed"
| isar_proof_end _ = "next"
-fun isar_proof_from_atp_proof cnfs modulus sorts ctxt goal i thm_names =
+fun isar_proof_from_atp_proof pool modulus sorts ctxt cnfs thm_names goal i =
let
val _ = trace_proof_msg (K "\nisar_proof_from_atp_proof: start\n")
- val tuples = map (parse_proof_line o explode) cnfs
+ val tuples = map (parse_proof_line pool o explode) cnfs
val _ = trace_proof_msg (fn () =>
Int.toString (length tuples) ^ " tuples extracted\n")
val ctxt = ProofContext.set_mode ProofContext.mode_schematic ctxt
@@ -600,7 +618,7 @@
val strip_spaces = strip_spaces_in_list o String.explode
-fun isar_proof_text debug modulus sorts ctxt
+fun isar_proof_text pool debug modulus sorts ctxt
(minimize_command, proof, thm_names, goal, i) =
let
val cnfs = proof |> split_lines |> map strip_spaces |> filter is_proof_line
@@ -608,7 +626,8 @@
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
+ case isar_proof_from_atp_proof pool modulus sorts ctxt cnfs thm_names goal
+ i of
"" => ""
| isar_proof =>
"\nStructured proof:\n" ^ Markup.markup Markup.sendback isar_proof
@@ -622,8 +641,8 @@
|> the_default "Warning: The Isar proof construction failed.\n"
in (one_line_proof ^ isar_proof, lemma_names) end
-fun proof_text isar_proof debug modulus sorts ctxt =
- if isar_proof then isar_proof_text debug modulus sorts ctxt
+fun proof_text isar_proof pool debug modulus sorts ctxt =
+ if isar_proof then isar_proof_text pool debug modulus sorts ctxt
else metis_proof_text
end;