# HG changeset patch # User blanchet # Date 1282665823 -7200 # Node ID d19c3a7ce38b7253374a4a5c87c4465ee80122a0 # Parent 9bbd5141d0a154a9a11de5183a6d1128e7d795a6 clean handling of whether a fact is chained or not; more elegant and reliable than encoding it in the name diff -r 9bbd5141d0a1 -r d19c3a7ce38b src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Aug 24 16:43:52 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Aug 24 18:03:43 2010 +0200 @@ -30,16 +30,16 @@ {subgoal: int, goal: Proof.context * (thm list * thm), relevance_override: relevance_override, - axioms: (string * thm) list option} + axioms: ((string * bool) * thm) list option} type prover_result = {outcome: failure option, message: string, pool: string Symtab.table, - used_thm_names: string list, + used_thm_names: (string * bool) list, atp_run_time_in_msecs: int, output: string, proof: string, - axiom_names: string Vector.vector, + axiom_names: (string * bool) vector, conjecture_shape: int list list} type prover = params -> minimize_command -> problem -> prover_result @@ -100,17 +100,17 @@ {subgoal: int, goal: Proof.context * (thm list * thm), relevance_override: relevance_override, - axioms: (string * thm) list option} + axioms: ((string * bool) * thm) list option} type prover_result = {outcome: failure option, message: string, pool: string Symtab.table, - used_thm_names: string list, + used_thm_names: (string * bool) list, atp_run_time_in_msecs: int, output: string, proof: string, - axiom_names: string Vector.vector, + axiom_names: (string * bool) vector, conjecture_shape: int list list} type prover = params -> minimize_command -> problem -> prover_result @@ -180,11 +180,11 @@ #> parse_clause_formula_relation #> fst fun repair_conjecture_shape_and_theorem_names output conjecture_shape - thm_names = + axiom_names = if String.isSubstring set_ClauseFormulaRelationN output then (* This is a hack required for keeping track of axioms after they have been - clausified by SPASS's Flotter tool. The "ATP/scripts/spass" script is also - part of this hack. *) + clausified by SPASS's Flotter tool. The "ATP/scripts/spass" script is + also part of this hack. *) let val j0 = hd (hd conjecture_shape) val seq = extract_clause_sequence output @@ -193,15 +193,20 @@ conjecture_prefix ^ Int.toString (j - j0) |> AList.find (fn (s, ss) => member (op =) ss s) name_map |> map (fn s => find_index (curry (op =) s) seq + 1) + fun name_for_number j = + let + val axioms = + j |> AList.lookup (op =) name_map + |> these |> map_filter (try (unprefix axiom_prefix)) + |> map undo_ascii_of + val chained = forall (is_true_for axiom_names) axioms + in (axioms |> space_implode " ", chained) end in (conjecture_shape |> map (maps renumber_conjecture), - seq |> map (AList.lookup (op =) name_map #> these - #> map_filter (try (unprefix axiom_prefix)) - #> map undo_ascii_of #> space_implode " ") - |> Vector.fromList) + seq |> map name_for_number |> Vector.fromList) end else - (conjecture_shape, thm_names) + (conjecture_shape, axiom_names) (* generic TPTP-based provers *) diff -r 9bbd5141d0a1 -r d19c3a7ce38b src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Aug 24 16:43:52 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Aug 24 18:03:43 2010 +0200 @@ -11,14 +11,13 @@ only: bool} val trace : bool Unsynchronized.ref - val chained_prefix : string val name_thms_pair_from_ref : Proof.context -> unit Symtab.table -> thm list -> Facts.ref - -> string * thm list + -> (string * bool) * thm list val relevant_facts : bool -> real -> real -> bool -> int -> bool -> relevance_override -> Proof.context * (thm list * 'a) -> term list -> term - -> (string * thm) list + -> ((string * bool) * thm) list end; structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER = @@ -37,17 +36,14 @@ only: bool} val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator -(* Used to label theorems chained into the goal. *) -val chained_prefix = sledgehammer_prefix ^ "chained_" fun name_thms_pair_from_ref ctxt reserved chained_ths xref = let val ths = ProofContext.get_fact ctxt xref val name = Facts.string_of_ref xref val name = name |> Symtab.defined reserved name ? quote - |> forall (member Thm.eq_thm chained_ths) ths - ? prefix chained_prefix - in (name, ths) end + val chained = forall (member Thm.eq_thm chained_ths) ths + in ((name, chained), ths) end (***************************************************************) @@ -282,7 +278,7 @@ | _ => false end; -type annotated_thm = (string * thm) * (string * const_typ list) list +type annotated_thm = ((string * bool) * thm) * (string * const_typ list) list (*For a reverse sort, putting the largest values first.*) fun compare_pairs ((_, w1), (_, w2)) = Real.compare (w2, w1) @@ -301,7 +297,7 @@ ", exceeds the limit of " ^ Int.toString max_new)); trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted)))); trace_msg (fn () => "Actually passed: " ^ - space_implode ", " (map (fst o fst o fst) accepted)); + space_implode ", " (map (fst o fst o fst o fst) accepted)); (map #1 accepted, List.drop (new_pairs, max_new)) end end; @@ -343,7 +339,7 @@ if null add_thms then [] else - map_filter (fn ((p as (name, th), _), _) => + map_filter (fn ((p as ((name, _), th), _), _) => if member Thm.eq_thm add_thms th then SOME p else NONE) rejects | relevant (new_pairs, rejects) [] = @@ -367,8 +363,8 @@ map #1 new_rels @ iter (j + 1) threshold rel_const_tab' rejects end | relevant (new_rels, rejects) - (((ax as ((name, th), axiom_consts)), cached_weight) - :: rest) = + (((ax as (((name, chained), th), axiom_consts)), + cached_weight) :: rest) = let val weight = case cached_weight of @@ -537,15 +533,15 @@ fun all_name_thms_pairs ctxt reserved full_types add_thms chained_ths = let val is_chained = member Thm.eq_thm chained_ths - fun is_bad_unnamed_local th = - exists (fn (_, ths) => member Thm.eq_thm ths th) named_locals orelse - (exists_subterm is_Var (prop_of th) andalso not (is_chained th)) val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt) val local_facts = ProofContext.facts_of ctxt val named_locals = local_facts |> Facts.dest_static [] (* Unnamed, not chained formulas with schematic variables are omitted, because they are rejected by the backticks (`...`) parser for some reason. *) + fun is_bad_unnamed_local th = + exists (fn (_, ths) => member Thm.eq_thm ths th) named_locals orelse + (exists_subterm is_Var (prop_of th) andalso not (is_chained th)) val unnamed_locals = local_facts |> Facts.props |> filter_out is_bad_unnamed_local |> map (pair "" o single) @@ -579,25 +575,22 @@ SOME name' => name' |> Symtab.defined reserved name' ? quote | NONE => ths |> map_filter (try backquotify) |> space_implode " " in - if name' = "" then - I - else - cons (name' |> forall is_chained ths0 ? prefix chained_prefix, - ths) + if name' = "" then I + else cons ((name', forall is_chained ths0), ths) end) in [] |> add_valid_facts fold local_facts (unnamed_locals @ named_locals) |> add_valid_facts Facts.fold_static global_facts global_facts end -fun multi_name a th (n, pairs) = - (n + 1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs); - +fun multi_name (name, chained) th (n, pairs) = + (n + 1, ((name ^ "(" ^ Int.toString n ^ ")", chained), th) :: pairs) fun add_names (_, []) pairs = pairs - | add_names (a, [th]) pairs = (a, th) :: pairs - | add_names (a, ths) pairs = #2 (fold (multi_name a) ths (1, pairs)) + | add_names (p, [th]) pairs = (p, th) :: pairs + | add_names (p, ths) pairs = #2 (fold (multi_name p) ths (1, pairs)) -fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a; +fun is_multi ((name, _), ths) = + length ths > 1 orelse String.isSuffix ".axioms" name (* The single-name theorems go after the multiple-name ones, so that single names are preferred when both are available. *) @@ -629,7 +622,7 @@ relevance_filter ctxt relevance_threshold relevance_convergence defs_relevant max_new theory_relevant relevance_override axioms (concl_t :: hyp_ts) - |> sort_wrt fst + |> sort_wrt (fst o fst) end end; diff -r 9bbd5141d0a1 -r d19c3a7ce38b src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Tue Aug 24 16:43:52 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Tue Aug 24 18:03:43 2010 +0200 @@ -10,8 +10,8 @@ type params = Sledgehammer.params val minimize_theorems : - params -> int -> int -> Proof.state -> (string * thm list) list - -> (string * thm list) list option * string + params -> int -> int -> Proof.state -> ((string * bool) * thm list) list + -> ((string * bool) * thm list) list option * string val run_minimize : params -> int -> Facts.ref list -> Proof.state -> unit end; @@ -30,14 +30,12 @@ | string_for_failure TimedOut = "Timed out." | string_for_failure _ = "Unknown error." -fun n_theorems name_thms_pairs = - let val n = length name_thms_pairs in +fun n_theorems names = + let val n = length names in string_of_int n ^ " theorem" ^ plural_s n ^ (if n > 0 then - ": " ^ space_implode " " - (name_thms_pairs - |> map (perhaps (try (unprefix chained_prefix))) - |> sort_distinct string_ord) + ": " ^ (names |> map fst + |> sort_distinct string_ord |> space_implode " ") else "") end @@ -65,8 +63,7 @@ {subgoal = subgoal, goal = (ctxt, (facts, goal)), relevance_override = {add = [], del = [], only = false}, axioms = SOME axioms} - val result as {outcome, used_thm_names, ...} = - prover params (K "") problem + val result as {outcome, used_thm_names, ...} = prover params (K "") problem in priority (case outcome of NONE => @@ -80,8 +77,7 @@ (* minimalization of thms *) -fun filter_used_facts used = - filter (member (op =) used o perhaps (try (unprefix chained_prefix)) o fst) +fun filter_used_facts used = filter (member (op =) used o fst) fun sublinear_minimize _ [] p = p | sublinear_minimize test (x :: xs) (seen, result) = @@ -130,10 +126,9 @@ val n = length min_thms val _ = priority (cat_lines ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ - (case filter (String.isPrefix chained_prefix o fst) min_thms of - [] => "" - | chained => " (including " ^ Int.toString (length chained) ^ - " chained)") ^ ".") + (case length (filter (snd o fst) min_thms) of + 0 => "" + | n => " (including " ^ Int.toString n ^ " chained)") ^ ".") in (SOME min_thms, proof_text isar_proof diff -r 9bbd5141d0a1 -r d19c3a7ce38b src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Aug 24 16:43:52 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Aug 24 18:03:43 2010 +0200 @@ -11,16 +11,16 @@ type minimize_command = string list -> string val metis_proof_text: - bool * minimize_command * string * string vector * thm * int - -> string * string list + bool * minimize_command * string * (string * bool) vector * thm * int + -> string * (string * bool) list val isar_proof_text: string Symtab.table * bool * int * Proof.context * int list list - -> bool * minimize_command * string * string vector * thm * int - -> string * string list + -> bool * minimize_command * string * (string * bool) vector * thm * int + -> string * (string * bool) list val proof_text: bool -> string Symtab.table * bool * int * Proof.context * int list list - -> bool * minimize_command * string * string vector * thm * int - -> string * string list + -> bool * minimize_command * string * (string * bool) vector * thm * int + -> string * (string * bool) list end; structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT = @@ -60,7 +60,7 @@ fun index_in_shape x = find_index (exists (curry (op =) x)) fun is_axiom_number axiom_names num = num > 0 andalso num <= Vector.length axiom_names andalso - Vector.sub (axiom_names, num - 1) <> "" + fst (Vector.sub (axiom_names, num - 1)) <> "" fun is_conjecture_number conjecture_shape num = index_in_shape num conjecture_shape >= 0 @@ -564,7 +564,7 @@ "108. ... [input]". *) fun used_facts_in_atp_proof axiom_names atp_proof = let - fun axiom_name num = + fun axiom_name_at_index num = let val j = Int.fromString num |> the_default ~1 in if is_axiom_number axiom_names j then SOME (Vector.sub (axiom_names, j - 1)) @@ -573,18 +573,20 @@ end val tokens_of = String.tokens (fn c => not (Char.isAlphaNum c) andalso c <> #"_") - val thm_name_list = Vector.foldr (op ::) [] axiom_names fun do_line (tag :: num :: "axiom" :: (rest as _ :: _)) = if tag = "cnf" orelse tag = "fof" then (case strip_prefix_and_undo_ascii axiom_prefix (List.last rest) of SOME name => - if member (op =) rest "file" then SOME name else axiom_name num - | NONE => axiom_name num) + if member (op =) rest "file" then + SOME (name, is_true_for axiom_names name) + else + axiom_name_at_index num + | NONE => axiom_name_at_index num) else NONE - | do_line (num :: "0" :: "Inp" :: _) = axiom_name num + | do_line (num :: "0" :: "Inp" :: _) = axiom_name_at_index num | do_line (num :: rest) = - (case List.last rest of "input" => axiom_name num | _ => NONE) + (case List.last rest of "input" => axiom_name_at_index num | _ => NONE) | do_line _ = NONE in atp_proof |> split_proof_lines |> map_filter (do_line o tokens_of) end @@ -620,23 +622,20 @@ "\nTo minimize the number of lemmas, try this: " ^ Markup.markup Markup.sendback command ^ "." -val unprefix_chained = perhaps (try (unprefix chained_prefix)) - fun used_facts axiom_names = used_facts_in_atp_proof axiom_names - #> List.partition (String.isPrefix chained_prefix) - #>> map (unprefix chained_prefix) - #> pairself (sort_distinct string_ord) + #> List.partition snd + #> pairself (sort_distinct (string_ord) o map fst) fun metis_proof_text (full_types, minimize_command, atp_proof, axiom_names, goal, i) = let val (chained_lemmas, other_lemmas) = used_facts axiom_names atp_proof - val lemmas = other_lemmas @ chained_lemmas val n = Logic.count_prems (prop_of goal) in (metis_line full_types i n other_lemmas ^ - minimize_line minimize_command lemmas, lemmas) + minimize_line minimize_command (other_lemmas @ chained_lemmas), + map (rpair false) other_lemmas @ map (rpair true) chained_lemmas) end (** Isar proof construction and manipulation **) @@ -663,7 +662,7 @@ fun add_fact_from_dep axiom_names num = if is_axiom_number axiom_names num then - apsnd (insert (op =) (Vector.sub (axiom_names, num - 1))) + apsnd (insert (op =) (fst (Vector.sub (axiom_names, num - 1)))) else apfst (insert (op =) (raw_prefix, num)) @@ -964,10 +963,9 @@ if member (op =) qs Show then "show" else "have") val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt) fun do_facts (ls, ss) = - let - val ls = ls |> sort_distinct (prod_ord string_ord int_ord) - val ss = ss |> map unprefix_chained |> sort_distinct string_ord - in metis_command full_types 1 1 (ls, ss) end + metis_command full_types 1 1 + (ls |> sort_distinct (prod_ord string_ord int_ord), + ss |> sort_distinct string_ord) and do_step ind (Fix xs) = do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n" | do_step ind (Let (t1, t2)) = diff -r 9bbd5141d0a1 -r d19c3a7ce38b src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Tue Aug 24 16:43:52 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Tue Aug 24 18:03:43 2010 +0200 @@ -18,8 +18,8 @@ val tfrees_name : string val prepare_problem : Proof.context -> bool -> bool -> bool -> bool -> term list -> term - -> (string * thm) list - -> string problem * string Symtab.table * int * string Vector.vector + -> ((string * bool) * thm) list + -> string problem * string Symtab.table * int * (string * bool) vector end; structure Sledgehammer_Translate : SLEDGEHAMMER_TRANSLATE = @@ -194,11 +194,11 @@ ctypes_sorts = ctypes_sorts} end -fun make_axiom ctxt presimp (name, th) = +fun make_axiom ctxt presimp ((name, chained), th) = case make_formula ctxt presimp name Axiom (prop_of th) of FOLFormula {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} => NONE - | formula => SOME (name, formula) + | formula => SOME ((name, chained), formula) fun make_conjecture ctxt ts = let val last = length ts - 1 in map2 (fn j => make_formula ctxt true (Int.toString j) @@ -235,20 +235,20 @@ let val ct = fold (fold count_fol_formula) [conjectures, axioms] init_counters fun is_needed c = the (Symtab.lookup ct c) > 0 + fun baptize th = ((Thm.get_name_hint th, false), th) in (optional_helpers |> full_types ? append optional_typed_helpers |> maps (fn (ss, ths) => - if exists is_needed ss then map (`Thm.get_name_hint) ths - else [])) @ - (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers) + if exists is_needed ss then map baptize ths else [])) @ + (if is_FO then [] else map baptize mandatory_helpers) |> map_filter (Option.map snd o make_axiom ctxt false) end -fun prepare_formulas ctxt full_types hyp_ts concl_t axioms = +fun prepare_formulas ctxt full_types hyp_ts concl_t axiom_pairs = let val thy = ProofContext.theory_of ctxt - val axiom_ts = map (prop_of o snd) axioms + val axiom_ts = map (prop_of o snd) axiom_pairs val hyp_ts = if null hyp_ts then [] @@ -267,7 +267,7 @@ (* TFrees in the conjecture; TVars in the axioms *) val conjectures = make_conjecture ctxt (hyp_ts @ [concl_t]) val (axiom_names, axioms) = - ListPair.unzip (map_filter (make_axiom ctxt true) axioms) + ListPair.unzip (map_filter (make_axiom ctxt true) axiom_pairs) val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms val (supers', arity_clauses) = make_arity_clauses thy tycons supers val class_rel_clauses = make_class_rel_clauses thy subs supers' @@ -500,12 +500,12 @@ (const_table_for_problem explicit_apply problem) problem fun prepare_problem ctxt readable_names explicit_forall full_types - explicit_apply hyp_ts concl_t axiom_ts = + explicit_apply hyp_ts concl_t axiom_pairs = let val thy = ProofContext.theory_of ctxt val (axiom_names, (conjectures, axioms, helper_facts, class_rel_clauses, arity_clauses)) = - prepare_formulas ctxt full_types hyp_ts concl_t axiom_ts + prepare_formulas ctxt full_types hyp_ts concl_t axiom_pairs val axiom_lines = map (problem_line_for_fact axiom_prefix full_types) axioms val helper_lines = map (problem_line_for_fact helper_prefix full_types) helper_facts diff -r 9bbd5141d0a1 -r d19c3a7ce38b src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Aug 24 16:43:52 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Aug 24 18:03:43 2010 +0200 @@ -6,6 +6,7 @@ signature SLEDGEHAMMER_UTIL = sig + val is_true_for : (string * bool) vector -> string -> bool val plural_s : int -> string val serial_commas : string -> string list -> string list val strip_spaces : string -> string @@ -27,6 +28,9 @@ structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = struct +fun is_true_for v s = + Vector.foldl (fn ((s', b'), b) => if s' = s then b' else b) false v + fun plural_s n = if n = 1 then "" else "s" fun serial_commas _ [] = ["??"]