# HG changeset patch # User blanchet # Date 1282673370 -7200 # Node ID 20ff5600bd150d285cf5784c5987c1fe6b27824d # Parent 9db37e912ee40fd132f4f6392827fd3b232685c3# Parent fcb0fe4c2f27d3ac53ea9622bf5c2e47b796f99c merged diff -r 9db37e912ee4 -r 20ff5600bd15 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Aug 24 22:38:45 2010 +0800 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Aug 24 20:09:30 2010 +0200 @@ -293,7 +293,7 @@ local datatype sh_result = - SH_OK of int * int * string list | + SH_OK of int * int * (string * bool) list | SH_FAIL of int * int | SH_ERROR @@ -354,7 +354,9 @@ in case result of SH_OK (time_isa, time_atp, names) => - let fun get_thms name = (name, thms_of_name (Proof.context_of st) name) + let + fun get_thms (name, chained) = + ((name, chained), thms_of_name (Proof.context_of st) name) in change_data id inc_sh_success; change_data id (inc_sh_lemmas (length names)); @@ -442,7 +444,8 @@ if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal then () else let - val named_thms = Unsynchronized.ref (NONE : (string * thm list) list option) + val named_thms = + Unsynchronized.ref (NONE : ((string * bool) * thm list) list option) val minimize = AList.defined (op =) args minimizeK val metis_ft = AList.defined (op =) args metis_ftK diff -r 9db37e912ee4 -r 20ff5600bd15 src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Aug 24 22:38:45 2010 +0800 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Aug 24 20:09:30 2010 +0200 @@ -22,8 +22,6 @@ open Metis_Clauses -exception METIS of string * string - val trace = Unsynchronized.ref false; fun trace_msg msg = if !trace then tracing (msg ()) else (); @@ -88,7 +86,7 @@ val args = map hol_term_to_fol_FO tms in Metis.Term.Fn (c, tyargs @ args) end | (CombVar ((v, _), _), []) => Metis.Term.Var v - | _ => raise METIS ("hol_term_to_fol_FO", "non first-order combterm") + | _ => raise Fail "non-first-order combterm" fun hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) = Metis.Term.Fn (fn_isa_to_met_sublevel a, map metis_term_from_combtyp tylist) @@ -429,8 +427,8 @@ Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^ Syntax.string_of_term ctxt (term_of y))))); in cterm_instantiate substs' i_th end - handle THM (msg, _, _) => raise METIS ("inst_inf", msg) - | ERROR msg => raise METIS ("inst_inf", msg) + handle THM (msg, _, _) => + error ("Cannot replay Metis proof in Isabelle:\n" ^ msg) (* INFERENCE RULE: RESOLVE *) @@ -446,7 +444,6 @@ [th] => th | _ => raise THM ("resolve_inc_tyvars: unique result expected", i, [tha,thb]) end - handle TERM (msg, _) => raise METIS ("resolve_inc_tyvars", msg) fun resolve_inf ctxt mode skolems thpairs atm th1 th2 = let @@ -501,8 +498,11 @@ val adjustment = get_ty_arg_size thy tm1 val p' = if adjustment > p then p else p-adjustment val tm_p = List.nth(args,p') - handle Subscript => raise METIS ("equality_inf", Int.toString p ^ " adj " ^ - Int.toString adjustment ^ " term " ^ Syntax.string_of_term ctxt tm) + handle Subscript => + error ("Cannot replay Metis proof in Isabelle:\n" ^ + "equality_inf: " ^ Int.toString p ^ " adj " ^ + Int.toString adjustment ^ " term " ^ + Syntax.string_of_term ctxt tm) val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^ " " ^ Syntax.string_of_term ctxt tm_p) val (r,t) = path_finder_FO tm_p ps @@ -590,9 +590,8 @@ val _ = trace_msg (fn () => "=============================================") val n_metis_lits = length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th))) - val _ = - if nprems_of th = n_metis_lits then () - else raise METIS ("translate", "Proof reconstruction has gone wrong.") + val _ = if nprems_of th = n_metis_lits then () + else error "Cannot replay Metis proof in Isabelle." in (fol_th, th) :: thpairs end (*Determining which axiom clauses are actually used*) @@ -805,14 +804,7 @@ Meson.MESON (maps neg_clausify) (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i st0 - handle ERROR msg => raise METIS ("generic_metis_tac", msg) end - handle METIS (loc, msg) => - if mode = HO then - (warning ("Metis: Falling back on \"metisFT\"."); - generic_metis_tac FT ctxt ths i st0) - else - Seq.empty val metis_tac = generic_metis_tac HO val metisF_tac = generic_metis_tac FO diff -r 9db37e912ee4 -r 20ff5600bd15 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Aug 24 22:38:45 2010 +0800 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Aug 24 20:09:30 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 9db37e912ee4 -r 20ff5600bd15 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Aug 24 22:38:45 2010 +0800 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Aug 24 20:09:30 2010 +0200 @@ -11,13 +11,13 @@ only: bool} val trace : bool Unsynchronized.ref - val chained_prefix : string val name_thms_pair_from_ref : - Proof.context -> thm list -> Facts.ref -> string * thm list + Proof.context -> unit Symtab.table -> thm list -> Facts.ref + -> (unit -> 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 = @@ -36,17 +36,15 @@ 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 chained_ths xref = - let - val ths = ProofContext.get_fact ctxt xref - val name = Facts.string_of_ref xref - |> forall (member Thm.eq_thm chained_ths) ths - ? prefix chained_prefix - in (name, ths) end - +fun name_thms_pair_from_ref ctxt reserved chained_ths xref = + let val ths = ProofContext.get_fact ctxt xref in + (fn () => let + val name = Facts.string_of_ref xref + val name = name |> Symtab.defined reserved name ? quote + val chained = forall (member Thm.eq_thm chained_ths) ths + in (name, chained) end, ths) + end (***************************************************************) (* Relevance Filtering *) @@ -280,7 +278,8 @@ | _ => false end; -type annotated_thm = (string * thm) * (string * const_typ list) list +type annotated_thm = + ((unit -> 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) @@ -299,7 +298,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 (fn f => f ()) o fst o fst o fst) accepted)); (map #1 accepted, List.drop (new_pairs, max_new)) end end; @@ -341,7 +340,7 @@ if null add_thms then [] else - map_filter (fn ((p as (name, th), _), _) => + map_filter (fn ((p as (_, th), _), _) => if member Thm.eq_thm add_thms th then SOME p else NONE) rejects | relevant (new_pairs, rejects) [] = @@ -376,7 +375,7 @@ if weight >= threshold orelse (defs_relevant andalso defines thy th rel_const_tab) then (trace_msg (fn () => - name ^ " passes: " ^ Real.toString weight + fst (name ()) ^ " passes: " ^ Real.toString weight ^ " consts: " ^ commas (map fst axiom_consts)); relevant ((ax, weight) :: new_rels, rejects) rest) else @@ -532,72 +531,82 @@ is_strange_theorem thm end -fun all_name_thms_pairs ctxt full_types add_thms chained_ths = +fun all_name_thms_pairs ctxt reserved full_types add_thms chained_ths = let - val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt); + val is_chained = member Thm.eq_thm chained_ths + 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 (fn th => exists (fn (_, ths) => member Thm.eq_thm ths th) - named_locals) - |> map (pair "" o single) + local_facts |> Facts.props |> filter_out is_bad_unnamed_local + |> map (pair "" o single) val full_space = Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts); - fun add_valid_facts xfold facts = - xfold (fn (name, ths0) => - if name <> "" andalso - forall (not o member Thm.eq_thm add_thms) ths0 andalso - (Facts.is_concealed facts name orelse - (respect_no_atp andalso is_package_def name) orelse - exists (fn s => String.isSuffix s name) multi_base_blacklist orelse - String.isSuffix "_def_raw" (* FIXME: crude hack *) name) then + fun add_valid_facts foldx facts = + foldx (fn (name0, ths) => + if name0 <> "" andalso + forall (not o member Thm.eq_thm add_thms) ths andalso + (Facts.is_concealed facts name0 orelse + (respect_no_atp andalso is_package_def name0) orelse + exists (fn s => String.isSuffix s name0) multi_base_blacklist orelse + String.isSuffix "_def_raw" (* FIXME: crude hack *) name0) then I else let + val multi = length ths > 1 + fun backquotify th = + "`" ^ Print_Mode.setmp [Print_Mode.input] + (Syntax.string_of_term ctxt) (prop_of th) ^ "`" fun check_thms a = - (case try (ProofContext.get_thms ctxt) a of + case try (ProofContext.get_thms ctxt) a of NONE => false - | SOME ths1 => Thm.eq_thms (ths0, ths1)) - val name1 = Facts.extern facts name; - val name2 = Name_Space.extern full_space name; - val ths = - ths0 |> filter ((not o is_theorem_bad_for_atps full_types) orf - member Thm.eq_thm add_thms) - val name' = - case find_first check_thms [name1, name2, name] of - SOME name' => name' - | NONE => - ths |> map (fn th => - "`" ^ Print_Mode.setmp [Print_Mode.input] - (Syntax.string_of_term ctxt) - (prop_of th) ^ "`") - |> space_implode " " + | SOME ths' => Thm.eq_thms (ths, ths') in - cons (name' |> forall (member Thm.eq_thm chained_ths) ths0 - ? prefix chained_prefix, ths) + pair 1 + #> fold (fn th => fn (j, rest) => + (j + 1, + if is_theorem_bad_for_atps full_types th andalso + not (member Thm.eq_thm add_thms th) then + rest + else + (fn () => + (if name0 = "" then + th |> backquotify + else + let + val name1 = Facts.extern facts name0 + val name2 = Name_Space.extern full_space name0 + in + case find_first check_thms [name1, name2, name0] of + SOME name => + let + val name = + name |> Symtab.defined reserved name ? quote + in + if multi then name ^ "(" ^ Int.toString j ^ ")" + else name + end + | NONE => "" + end, is_chained th), (multi, th)) :: rest)) ths + #> snd 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 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)) - -fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a; - (* The single-name theorems go after the multiple-name ones, so that single names are preferred when both are available. *) -fun name_thm_pairs ctxt respect_no_atp name_thms_pairs = - let - val (mults, singles) = List.partition is_multi name_thms_pairs - val ps = [] |> fold add_names singles |> fold add_names mults - in ps |> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd) end; +fun name_thm_pairs ctxt respect_no_atp = + List.partition (fst o snd) #> op @ + #> map (apsnd snd) + #> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd) (***************************************************************) (* ATP invocation methods setup *) @@ -609,9 +618,13 @@ (ctxt, (chained_ths, _)) hyp_ts concl_t = let val add_thms = maps (ProofContext.get_fact ctxt) add + val reserved = reserved_isar_keyword_table () val axioms = - (if only then map (name_thms_pair_from_ref ctxt chained_ths) add - else all_name_thms_pairs ctxt full_types add_thms chained_ths) + (if only then + maps ((fn (n, ths) => map (pair n o pair false) ths) + o name_thms_pair_from_ref ctxt reserved chained_ths) add + else + all_name_thms_pairs ctxt reserved full_types add_thms chained_ths) |> name_thm_pairs ctxt (respect_no_atp andalso not only) |> make_unique in @@ -620,7 +633,8 @@ relevance_filter ctxt relevance_threshold relevance_convergence defs_relevant max_new theory_relevant relevance_override axioms (concl_t :: hyp_ts) - |> sort_wrt fst + |> map (apfst (fn f => f ())) + |> sort_wrt (fst o fst) end end; diff -r 9db37e912ee4 -r 20ff5600bd15 src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Tue Aug 24 22:38:45 2010 +0800 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Tue Aug 24 20:09:30 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 @@ -157,8 +152,11 @@ fun run_minimize params i refs state = let val ctxt = Proof.context_of state + val reserved = reserved_isar_keyword_table () val chained_ths = #facts (Proof.goal state) - val name_thms_pairs = map (name_thms_pair_from_ref ctxt chained_ths) refs + val name_thms_pairs = + map (apfst (fn f => f ()) + o name_thms_pair_from_ref ctxt reserved chained_ths) refs in case subgoal_count state of 0 => priority "No subgoal!" diff -r 9db37e912ee4 -r 20ff5600bd15 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Aug 24 22:38:45 2010 +0800 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Aug 24 20:09:30 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 @@ -613,30 +615,27 @@ "Try this command: " ^ Markup.markup Markup.sendback (metis_command full_types i n ([], ss)) ^ "." fun minimize_line _ [] = "" - | minimize_line minimize_command facts = - case minimize_command facts of + | minimize_line minimize_command ss = + case minimize_command ss of "" => "" | command => "\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 9db37e912ee4 -r 20ff5600bd15 src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Tue Aug 24 22:38:45 2010 +0800 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Tue Aug 24 20:09:30 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 9db37e912ee4 -r 20ff5600bd15 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Aug 24 22:38:45 2010 +0800 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Aug 24 20:09:30 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 @@ -21,11 +22,15 @@ val specialize_type : theory -> (string * typ) -> term -> term val subgoal_count : Proof.state -> int val strip_subgoal : thm -> int -> (string * typ) list * term list * term + val reserved_isar_keyword_table : unit -> unit Symtab.table end; 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 _ [] = ["??"] @@ -155,4 +160,8 @@ val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees in (rev (map dest_Free frees), hyp_ts, concl_t) end +fun reserved_isar_keyword_table () = + union (op =) (Keyword.dest_keywords ()) (Keyword.dest_commands ()) + |> map (rpair ()) |> Symtab.make + end;