# HG changeset patch # User blanchet # Date 1271682921 -7200 # Node ID 217ca1273786c862b749f15a40c3f738c3c7dc19 # Parent 0e3e49bd658d0fab81aa3f83a26b1a6c18e2ae33 make Sledgehammer's minimizer also minimize Isar proofs diff -r 0e3e49bd658d -r 217ca1273786 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Apr 19 11:54:07 2010 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Apr 19 15:15:21 2010 +0200 @@ -391,7 +391,7 @@ |> Option.map (fst o read_int o explode) |> the_default 5 val params = default_params thy [("minimize_timeout", Int.toString timeout)] - val minimize = minimize_theorems params linear_minimize prover prover_name 1 + val minimize = minimize_theorems params prover prover_name 1 val _ = log separator in case minimize st (these (!named_thms)) of diff -r 0e3e49bd658d -r 217ca1273786 src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Apr 19 11:54:07 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Apr 19 15:15:21 2010 +0200 @@ -35,6 +35,7 @@ type prover_result = {success: bool, message: string, + conjecture_pos: int * int, relevant_thm_names: string list, atp_run_time_in_msecs: int, proof: string, @@ -90,6 +91,7 @@ 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 0e3e49bd658d -r 217ca1273786 src/HOL/Tools/ATP_Manager/atp_minimal.ML --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Mon Apr 19 11:54:07 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Mon Apr 19 15:15:21 2010 +0200 @@ -9,13 +9,9 @@ type params = ATP_Manager.params type prover = ATP_Manager.prover type prover_result = ATP_Manager.prover_result - type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list - val linear_minimize : 'a minimize_fun - val binary_minimize : 'a minimize_fun val minimize_theorems : - params -> (string * thm list) minimize_fun -> prover -> string -> int - -> Proof.state -> (string * thm list) list + params -> prover -> string -> int -> Proof.state -> (string * thm list) list -> (string * thm list) list option * string end; @@ -27,62 +23,24 @@ open Sledgehammer_Proof_Reconstruct open ATP_Manager -type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list - (* Linear minimization algorithm *) -fun linear_minimize p s = +fun linear_minimize test s = let - fun aux [] needed = needed - | aux (x :: xs) needed = aux xs (needed |> not (p (xs @ needed)) ? cons x) - in aux s [] end; - -(* Binary minimalization *) - -local - fun isplit (l, r) [] = (l, r) - | isplit (l, r) [h] = (h :: l, r) - | isplit (l, r) (h1 :: h2 :: t) = isplit (h1 :: l, h2 :: r) t -in - fun split lst = isplit ([], []) lst -end - -local - fun min _ _ [] = raise Empty - | min _ _ [s0] = [s0] - | min p sup s = - let - val (l0, r0) = split s - in - if p (sup @ l0) then - min p sup l0 - else if p (sup @ r0) then - min p sup r0 - else - let - val l = min p (sup @ r0) l0 - val r = min p (sup @ l) r0 - in l @ r end - end -in - (* return a minimal subset v of s that satisfies p - @pre p(s) & ~p([]) & monotone(p) - @post v subset s & p(v) & - forall e in v. ~p(v \ e) - *) - fun binary_minimize p s = - case min p [] s of - [x] => if p [] then [] else [x] - | m => m -end + fun aux [] p = p + | aux (x :: xs) (needed, result) = + case test (xs @ needed) of + SOME result => aux xs (needed, result) + | NONE => aux xs (x :: needed, result) + in aux s end (* failure check and producing answer *) -datatype 'a prove_result = Success of 'a | Failure | Timeout | Error +datatype outcome = Success | Failure | Timeout | Error -val string_of_result = - fn Success _ => "Success" +val string_of_outcome = + fn Success => "Success" | Failure => "Failure" | Timeout => "Timeout" | Error => "Error" @@ -94,26 +52,19 @@ ("# Cannot determine problem status within resource limit", Timeout), ("Error", Error)] -fun produce_answer ({success, proof, internal_thm_names, filtered_clauses, ...} - : prover_result) = +fun outcome_of_result (result as {success, proof, ...} : prover_result) = if success then - (Success (Vector.foldr (op ::) [] internal_thm_names, filtered_clauses), - proof) - else - let - val failure = failure_strings |> get_first (fn (s, t) => - if String.isSubstring s proof then SOME (t, proof) else NONE) - in - (case failure of - SOME res => res - | NONE => (Failure, proof)) - end - + Success + else case get_first (fn (s, outcome) => + if String.isSubstring s proof then SOME outcome + else NONE) failure_strings of + SOME outcome => outcome + | NONE => Failure (* wrapper for calling external prover *) fun sledgehammer_test_theorems (params as {full_types, ...} : params) prover - timeout subgoal state filtered name_thms_pairs = + timeout subgoal state filtered_clauses name_thms_pairs = let val num_theorems = length name_thms_pairs val _ = priority ("Testing " ^ string_of_int num_theorems ^ @@ -124,50 +75,61 @@ val problem = {subgoal = subgoal, goal = (ctxt, (facts, goal)), relevance_override = {add = [], del = [], only = false}, - axiom_clauses = SOME axclauses, filtered_clauses = filtered} - val (result, proof) = produce_answer (prover params timeout problem) - val _ = priority (string_of_result result) - in (result, proof) end - + axiom_clauses = SOME axclauses, filtered_clauses = filtered_clauses} + in + `outcome_of_result (prover params timeout problem) + |>> tap (priority o string_of_outcome) + end (* minimalization of thms *) -fun minimize_theorems (params as {minimize_timeout, ...}) gen_min prover - prover_name i state name_thms_pairs = +fun minimize_theorems (params as {minimize_timeout, isar_proof, modulus, + sorts, ...}) + prover atp_name i state name_thms_pairs = let val msecs = Time.toMilliseconds minimize_timeout val _ = priority ("Minimize called with " ^ string_of_int (length name_thms_pairs) ^ - " theorems, ATP: " ^ prover_name ^ + " theorems, ATP: " ^ atp_name ^ ", time limit: " ^ string_of_int msecs ^ " ms") val test_thms_fun = sledgehammer_test_theorems params prover minimize_timeout i state fun test_thms filtered thms = - case test_thms_fun filtered thms of (Success _, _) => true | _ => false - val n = state |> Proof.raw_goal |> #goal |> prop_of |> Logic.count_prems + case test_thms_fun filtered thms of + (Success, result) => SOME result + | _ => NONE + + val {context = ctxt, facts, goal} = Proof.goal state; + val n = Logic.count_prems (prop_of goal) in (* try prove first to check result and get used theorems *) (case test_thms_fun NONE name_thms_pairs of - (Success (used, filtered), _) => + (Success, result as {internal_thm_names, filtered_clauses, + ...}) => let - val ordered_used = sort_distinct string_ord used + val used = internal_thm_names |> Vector.foldr (op ::) [] + |> sort_distinct string_ord val to_use = - if length ordered_used < length name_thms_pairs then - filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs + if length used < length name_thms_pairs then + filter (fn (name1, _) => List.exists (curry (op =) name1) used) + name_thms_pairs else name_thms_pairs - val min_thms = - if null to_use then [] - else gen_min (test_thms (SOME filtered)) to_use - val min_names = sort_distinct string_ord (map fst min_thms) + val (min_thms, {conjecture_pos, proof, internal_thm_names, ...}) = + linear_minimize (test_thms (SOME filtered_clauses)) to_use + ([], result) val _ = priority (cat_lines ["Minimal " ^ string_of_int (length min_thms) ^ " theorems"]) - in (SOME min_thms, metis_line i n min_names) end + in + (SOME min_thms, + proof_text isar_proof true modulus sorts atp_name + (proof, internal_thm_names, conjecture_pos, ctxt, goal, i) + |> fst) + end | (Timeout, _) => (NONE, "Timeout: You can increase the time limit using the \"timeout\" \ \option (e.g., \"timeout = " ^ string_of_int (10 + msecs div 1000) ^ " s\").") - | (Error, msg) => - (NONE, "Error in prover: " ^ msg) + | (Error, {message, ...}) => (NONE, "ATP error: " ^ message) | (Failure, _) => (* Failure sometimes mean timeout, unfortunately. *) (NONE, "Failure: No proof was found with the current time limit. You \ diff -r 0e3e49bd658d -r 217ca1273786 src/HOL/Tools/ATP_Manager/atp_wrapper.ML --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Mon Apr 19 11:54:07 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Mon Apr 19 15:15:21 2010 +0200 @@ -67,7 +67,7 @@ | (failure :: _) => SOME failure fun generic_prover overlord get_facts prepare write_file cmd args failure_strs - produce_answer name ({debug, full_types, ...} : params) + proof_text name ({debug, full_types, ...} : params) ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses} : problem) = let @@ -142,20 +142,22 @@ File.write (Path.explode (Path.implode probfile ^ "_proof")) ("% " ^ timestamp () ^ "\n" ^ proof) - val (((proof, atp_run_time_in_msecs), rc), conj_pos) = + val (((proof, atp_run_time_in_msecs), rc), conjecture_pos) = 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", []) + if is_some failure then + ("ATP failed to find a proof.\n", []) + else if rc <> 0 then + ("ATP error: " ^ proof ^ ".\n", []) else - (produce_answer name (proof, internal_thm_names, conj_pos, ctxt, th, - subgoal)); + proof_text name (proof, internal_thm_names, conjecture_pos, ctxt, th, + subgoal) in - {success = success, message = message, + {success = success, message = message, conjecture_pos = conjecture_pos, relevant_thm_names = relevant_thm_names, atp_run_time_in_msecs = atp_run_time_in_msecs, proof = proof, internal_thm_names = internal_thm_names, @@ -179,10 +181,8 @@ (prepare_clauses higher_order false) (write_tptp_file (overlord andalso not isar_proof)) command (arguments timeout) failure_strs - (if supports_isar_proofs andalso isar_proof then - structured_isar_proof modulus sorts - else - metis_lemma_list false) name params; + (proof_text (supports_isar_proofs andalso isar_proof) false modulus sorts) + name params fun tptp_prover name p = (name, generic_tptp_prover (name, p)); @@ -237,7 +237,8 @@ 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) failure_strs (metis_lemma_list true) name params; + (arguments timeout) failure_strs (metis_proof_text false false) + name params fun dfg_prover (name, p) = (name, generic_dfg_prover (name, p)); diff -r 0e3e49bd658d -r 217ca1273786 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Apr 19 11:54:07 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Apr 19 15:15:21 2010 +0200 @@ -183,27 +183,27 @@ fun get_time_limit_arg s = (case Int.fromString s of SOME t => Time.fromSeconds t - | NONE => error ("Invalid time limit: " ^ quote s)) + | NONE => error ("Invalid time limit: " ^ quote s ^ ".")) fun get_opt (name, a) (p, t) = (case name of "time" => (p, get_time_limit_arg a) | "atp" => (a, t) - | n => error ("Invalid argument: " ^ n)) + | n => error ("Invalid argument: " ^ n ^ ".")) val {atps, minimize_timeout, ...} = get_params thy override_params val (atp, timeout) = fold get_opt old_style_args (hd atps, minimize_timeout) val params = get_params thy - [("atps", [atp]), - ("minimize_timeout", - [string_of_int (Time.toMilliseconds timeout) ^ " ms"])] + (override_params @ + [("atps", [atp]), + ("minimize_timeout", + [string_of_int (Time.toMilliseconds timeout) ^ " ms"])]) val prover = (case get_prover thy atp of SOME prover => prover - | NONE => error ("Unknown ATP: " ^ quote atp)) + | NONE => error ("Unknown ATP: " ^ quote atp ^ ".")) val name_thms_pairs = theorems_from_refs ctxt fact_refs in - writeln (#2 (minimize_theorems params linear_minimize prover atp i state - name_thms_pairs)) + priority (#2 (minimize_theorems params prover atp i state name_thms_pairs)) end val runN = "run" diff -r 0e3e49bd658d -r 217ca1273786 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Apr 19 11:54:07 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Apr 19 15:15:21 2010 +0200 @@ -14,10 +14,18 @@ val strip_prefix: string -> string -> string option val is_proof_well_formed: string -> bool val metis_line: int -> int -> string list -> string - val metis_lemma_list: bool -> string -> - string * string vector * (int * int) * Proof.context * thm * int -> string * string list - val structured_isar_proof: int -> bool -> string -> - string * string vector * (int * int) * Proof.context * thm * int -> string * string list + val metis_proof_text: + bool -> bool -> string + -> string * string vector * (int * int) * 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 + val proof_text: + bool -> bool -> int -> bool -> string + -> string * string vector * (int * int) * Proof.context * thm * int + -> string * string list end; structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT = @@ -493,26 +501,21 @@ exists (fn s => String.isSubstring s proof) end_proof_strs (* === EXTRACTING LEMMAS === *) -(* lines have the form "cnf(108, axiom, ...", -the number (108) has to be extracted)*) -fun get_step_nums false extract = +(* A list consisting of the first number in each line is returned. + TPTP: Interesting lines have the form "cnf(108, axiom, ...)", where the + number (108) is extracted. + DFG: Lines have the form "108[0:Inp] ...", where the first number (108) is + extracted. *) +fun get_step_nums proof_extract = let val toks = String.tokens (not o Char.isAlphaNum) fun inputno ("cnf" :: ntok :: "axiom" :: _) = Int.fromString ntok | inputno ("cnf" :: ntok :: "negated" :: "conjecture" :: _) = Int.fromString ntok + | inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok (* DFG *) | inputno _ = NONE - val lines = split_lines extract + val lines = split_lines proof_extract in map_filter (inputno o toks) lines end -(*String contains multiple lines. We want those of the form - "253[0:Inp] et cetera..." - A list consisting of the first number in each line is returned. *) -| get_step_nums true proofextract = - let val toks = String.tokens (not o Char.isAlphaNum) - fun inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok - | inputno _ = NONE - val lines = split_lines proofextract - 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, conj_count, _, _, _) = @@ -546,28 +549,31 @@ fun metis_line i n xs = "Try this command: " ^ Markup.markup Markup.sendback (metis_command i n xs) ^ ".\n" -fun minimize_line _ [] = "" - | minimize_line name xs = +fun minimize_line _ _ [] = "" + | minimize_line isar_proof atp_name xs = "To minimize the number of lemmas, try this command: " ^ Markup.markup Markup.sendback - ("sledgehammer minimize [atp = " ^ name ^ "] (" ^ + ("sledgehammer minimize [atp = " ^ atp_name ^ + (if isar_proof then ", isar_proof" else "") ^ "] (" ^ space_implode " " xs ^ ")") ^ ".\n" -fun metis_lemma_list dfg name (result as (_, _, _, _, goal, i)) = +fun metis_proof_text isar_proof minimal atp_name + (result as (_, _, _, _, goal, i)) = let - val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result + val (lemmas, used_conj) = extract_lemmas get_step_nums result val n = Logic.count_prems (prop_of goal) val xs = kill_chained lemmas in - (metis_line i n xs ^ minimize_line name xs ^ + (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."), kill_chained lemmas) - end; + end -fun structured_isar_proof modulus sorts name +fun isar_proof_text minimal modulus sorts atp_name (result as (proof, thm_names, conj_count, ctxt, goal, i)) = let (* We could use "split_lines", but it can return blank lines. *) @@ -576,7 +582,8 @@ 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 (one_line_proof, lemma_names) = metis_lemma_list false name result + val (one_line_proof, lemma_names) = + metis_proof_text true minimal atp_name result val tokens = String.tokens (fn c => c = #" ") one_line_proof val isar_proof = if member (op =) tokens chained_hint then "" @@ -588,4 +595,8 @@ 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 + end;