# HG changeset patch # User blanchet # Date 1271695452 -7200 # Node ID bede2d49ba3b2ddb6dd5a753cbbb2edaabf80c1a # Parent 43d10a494c913197ddd6ccf1cf1cc6d374adb77c get rid of "conjecture_pos", which is no longer necessary now that it's Metis's job, not Sledgehammer's, to report inconsistent contexts diff -r 43d10a494c91 -r bede2d49ba3b src/HOL/Tools/ATP_Manager/atp_manager.ML --- 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, diff -r 43d10a494c91 -r bede2d49ba3b src/HOL/Tools/ATP_Manager/atp_minimal.ML --- 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\" \ diff -r 43d10a494c91 -r bede2d49ba3b src/HOL/Tools/ATP_Manager/atp_wrapper.ML --- 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, diff -r 43d10a494c91 -r bede2d49ba3b src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML --- 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; diff -r 43d10a494c91 -r bede2d49ba3b src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- 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 ""