get rid of "conjecture_pos", which is no longer necessary now that it's Metis's job, not Sledgehammer's, to report inconsistent contexts
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Apr 19 18:14:45 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Apr 19 18:44:12 2010 +0200
@@ -35,7 +35,6 @@
type prover_result =
{success: bool,
message: string,
- conjecture_pos: int * int,
relevant_thm_names: string list,
atp_run_time_in_msecs: int,
proof: string,
@@ -92,7 +91,6 @@
type prover_result =
{success: bool,
message: string,
- conjecture_pos: int * int,
relevant_thm_names: string list,
atp_run_time_in_msecs: int,
proof: string,
--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Mon Apr 19 18:14:45 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Mon Apr 19 18:44:12 2010 +0200
@@ -113,7 +113,7 @@
filter (fn (name1, _) => List.exists (curry (op =) name1) used)
name_thms_pairs
else name_thms_pairs
- val (min_thms, {conjecture_pos, proof, internal_thm_names, ...}) =
+ val (min_thms, {proof, internal_thm_names, ...}) =
linear_minimize (test_thms (SOME filtered_clauses)) to_use
([], result)
val n = length min_thms
@@ -121,9 +121,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, conjecture_pos, ctxt, goal, i)
- |> fst)
+ proof_text isar_proof true modulus sorts atp_name proof
+ internal_thm_names ctxt 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 Mon Apr 19 18:14:45 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Mon Apr 19 18:44:12 2010 +0200
@@ -142,22 +142,18 @@
File.write (Path.explode (Path.implode probfile ^ "_proof"))
("% " ^ timestamp () ^ "\n" ^ proof)
- val (((proof, atp_run_time_in_msecs), rc), conjecture_pos) =
+ val (((proof, atp_run_time_in_msecs), rc), _) =
with_path cleanup export run_on (prob_pathname subgoal);
(* Check for success and print out some information on failure. *)
val failure = find_failure failure_strs proof;
val success = rc = 0 andalso is_none failure;
val (message, relevant_thm_names) =
- if is_some failure then
- ("ATP failed to find a proof.\n", [])
- else if rc <> 0 then
- ("ATP error: " ^ proof ^ ".\n", [])
- else
- proof_text name (proof, internal_thm_names, conjecture_pos, ctxt, th,
- subgoal)
+ if is_some failure then ("ATP failed to find a proof.\n", [])
+ else if rc <> 0 then ("ATP error: " ^ proof ^ ".\n", [])
+ else proof_text name proof internal_thm_names ctxt th subgoal
in
- {success = success, message = message, conjecture_pos = conjecture_pos,
+ {success = success, message = message,
relevant_thm_names = relevant_thm_names,
atp_run_time_in_msecs = atp_run_time_in_msecs, proof = proof,
internal_thm_names = internal_thm_names,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Mon Apr 19 18:14:45 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Mon Apr 19 18:44:12 2010 +0200
@@ -36,11 +36,10 @@
hol_clause list
val write_tptp_file : bool -> bool -> Path.T ->
hol_clause list * hol_clause list * hol_clause list * hol_clause list *
- classrel_clause list * arity_clause list ->
- int * int
+ classrel_clause list * arity_clause list -> unit
val write_dfg_file : bool -> Path.T ->
hol_clause list * hol_clause list * hol_clause list * hol_clause list *
- classrel_clause list * arity_clause list -> int * int
+ classrel_clause list * arity_clause list -> unit
end
structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE =
@@ -497,17 +496,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
- val _ =
- 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)
- in (length axclauses + 1, length tfree_clss + length conjecture_clss)
- end;
+ 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
(* DFG format *)
@@ -531,27 +529,23 @@
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
- val _ =
- 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"])
-
in
- (length axclauses + length classrel_clauses + length arity_clauses +
- length helper_clauses + 1, length tfree_clss + length conjecture_clss)
+ 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
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Apr 19 18:14:45 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Apr 19 18:44:12 2010 +0200
@@ -15,17 +15,14 @@
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 * (int * int) * Proof.context * thm * int
- -> string * string list
+ bool -> bool -> string -> string -> string vector -> Proof.context -> thm
+ -> int -> string * string list
val isar_proof_text:
- bool -> int -> bool -> string
- -> string * string vector * (int * int) * Proof.context * thm * int
- -> string * string list
+ bool -> int -> bool -> string -> string -> string vector -> Proof.context
+ -> thm -> int -> string * string list
val proof_text:
- bool -> bool -> int -> bool -> string
- -> string * string vector * (int * int) * Proof.context * thm * int
- -> string * string list
+ bool -> bool -> int -> bool -> string -> string -> string vector
+ -> Proof.context -> thm -> int -> string * string list
end;
structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
@@ -517,24 +514,6 @@
val lines = split_lines proof_extract
in map_filter (inputno o toks) lines end
-(* Extracting lemmas from TSTP output between the lines from above. *)
-fun extract_lemmas get_step_nums (proof, thm_names, conjecture_pos, _, _, _) =
- let
- (* get the names of axioms from their numbers*)
- fun get_axiom_names thm_names step_nums =
- let
- val last_axiom = Vector.length thm_names
- fun is_axiom n = n <= last_axiom
- fun is_conj n = n >= fst conjecture_pos andalso
- n < fst conjecture_pos + snd conjecture_pos
- fun name_at i = Vector.sub (thm_names, i - 1)
- in
- (sort_distinct string_ord (filter (fn x => x <> "??.unknown")
- (map name_at (filter is_axiom step_nums))),
- exists is_conj step_nums)
- end
- in get_axiom_names thm_names (get_step_nums (get_proof_extract proof)) end;
-
(*Used to label theorems chained into the sledgehammer call*)
val chained_hint = "CHAINED";
val kill_chained = filter_out (curry (op =) chained_hint)
@@ -557,24 +536,25 @@
(if isar_proof then ", isar_proof" else "") ^ "] (" ^
space_implode " " xs ^ ")") ^ ".\n"
-fun metis_proof_text isar_proof minimal atp_name
- (result as (_, _, _, _, goal, i)) =
+fun metis_proof_text isar_proof minimal atp_name proof thm_names
+ (_ : Proof.context) goal i =
let
- val (lemmas, used_conj) = extract_lemmas get_step_nums result
+ val lemmas =
+ proof |> get_proof_extract
+ |> get_step_nums
+ |> filter (fn i => i <= Vector.length 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) ^
- (if used_conj then
- ""
- else
- "\nWarning: The goal is provable because the context is inconsistent."),
+ (if minimal then "" else minimize_line isar_proof atp_name xs),
kill_chained lemmas)
end
-fun isar_proof_text minimal modulus sorts atp_name
- (result as (proof, thm_names, _, ctxt, goal, i)) =
+fun isar_proof_text minimal modulus sorts atp_name proof thm_names ctxt goal i =
let
(* We could use "split_lines", but it can return blank lines. *)
val lines = String.tokens (equal #"\n");
@@ -583,7 +563,7 @@
val extract = get_proof_extract proof
val cnfs = filter (String.isPrefix "cnf(") (map kill_spaces (lines extract))
val (one_line_proof, lemma_names) =
- metis_proof_text true minimal atp_name result
+ metis_proof_text true minimal atp_name proof thm_names ctxt goal i
val tokens = String.tokens (fn c => c = #" ") one_line_proof
val isar_proof =
if member (op =) tokens chained_hint then ""