# HG changeset patch # User blanchet # Date 1282917946 -7200 # Node ID c18e8f90f4dc39a00245c4e7bb0eb191bf7229d1 # Parent d0196406ee325d0276d037c9a334d59c6b25245e# Parent 91ad85f962c48e28c3c00dec54eb60e48cf0ef01 merged diff -r d0196406ee32 -r c18e8f90f4dc src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Aug 27 14:25:29 2010 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Aug 27 16:05:46 2010 +0200 @@ -357,15 +357,16 @@ case result of SH_OK (time_isa, time_atp, names) => let - fun get_thms (name, loc) = - ((name, loc), thms_of_name (Proof.context_of st) name) + fun get_thms (name, Sledgehammer_Fact_Filter.Chained) = NONE + | get_thms (name, loc) = + SOME ((name, loc), thms_of_name (Proof.context_of st) name) in change_data id inc_sh_success; change_data id (inc_sh_lemmas (length names)); change_data id (inc_sh_max_lems (length names)); change_data id (inc_sh_time_isa time_isa); change_data id (inc_sh_time_atp time_atp); - named_thms := SOME (map get_thms names); + named_thms := SOME (map_filter get_thms names); log (sh_tag id ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^ string_of_int time_atp ^ ") [" ^ prover_name ^ "]:\n" ^ msg) end diff -r d0196406ee32 -r c18e8f90f4dc src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Fri Aug 27 14:25:29 2010 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Aug 27 16:05:46 2010 +0200 @@ -293,7 +293,7 @@ (remotify_name name, remotify_config system_name system_versions config) val remote_e = remotify_prover e "EP" ["1.0", "1.1", "1.2"] -val remote_vampire = remotify_prover vampire "Vampire" ["9.9", "0.6", "1.0"] +val remote_vampire = remotify_prover vampire "Vampire" ["9.0", "1.0", "0.6"] val remote_sine_e = remote_prover "sine_e" "SInE" [] [] [(Unprovable, "says Unknown")] 1000 (* FUDGE *) false true diff -r d0196406ee32 -r c18e8f90f4dc src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Aug 27 14:25:29 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Aug 27 16:05:46 2010 +0200 @@ -38,7 +38,7 @@ atp_run_time_in_msecs: int, output: string, proof: string, - axiom_names: (string * locality) vector, + axiom_names: (string * locality) list vector, conjecture_shape: int list list} type prover = params -> minimize_command -> problem -> prover_result @@ -107,7 +107,7 @@ atp_run_time_in_msecs: int, output: string, proof: string, - axiom_names: (string * locality) vector, + axiom_names: (string * locality) list vector, conjecture_shape: int list list} type prover = params -> minimize_command -> problem -> prover_result @@ -175,6 +175,7 @@ #> snd #> Substring.string #> strip_spaces_except_between_ident_chars #> explode #> parse_clause_formula_relation #> fst +(* TODO: move to "Sledgehammer_Proof_Reconstruct.ML" *) fun repair_conjecture_shape_and_theorem_names output conjecture_shape axiom_names = if String.isSubstring set_ClauseFormulaRelationN output then @@ -189,19 +190,17 @@ conjecture_prefix ^ string_of_int (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 unascii_of - val loc = - case axioms of - [axiom] => find_first_in_vector axiom_names axiom General - | _ => General - in (axioms |> space_implode " ", loc) end + fun names_for_number j = + j |> AList.lookup (op =) name_map |> these + |> map_filter (try (unprefix axiom_prefix)) |> map unascii_of + |> map (fn name => + (name, name |> find_first_in_list_vector axiom_names + |> the) + handle Option.Option => + error ("No such fact: " ^ quote name ^ ".")) in (conjecture_shape |> map (maps renumber_conjecture), - seq |> map name_for_number |> Vector.fromList) + seq |> map names_for_number |> Vector.fromList) end else (conjecture_shape, axiom_names) @@ -253,7 +252,7 @@ if the_dest_dir = "" then File.tmp_path probfile else if File.exists (Path.explode the_dest_dir) then Path.append (Path.explode the_dest_dir) probfile - else error ("No such directory: " ^ the_dest_dir ^ ".") + else error ("No such directory: " ^ quote the_dest_dir ^ ".") end; val measure_run_time = verbose orelse Config.get ctxt measure_runtime diff -r d0196406ee32 -r c18e8f90f4dc src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Aug 27 14:25:29 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Aug 27 16:05:46 2010 +0200 @@ -13,6 +13,7 @@ only: bool} val trace : bool Unsynchronized.ref + val term_patterns : bool Unsynchronized.ref val name_thm_pairs_from_ref : Proof.context -> unit Symtab.table -> thm list -> Facts.ref -> ((string * locality) * thm) list @@ -30,6 +31,9 @@ val trace = Unsynchronized.ref false fun trace_msg msg = if !trace then tracing (msg ()) else () +(* experimental feature *) +val term_patterns = Unsynchronized.ref false + val respect_no_atp = true datatype locality = General | Theory | Local | Chained @@ -65,82 +69,92 @@ (*** constants with types ***) -(*An abstraction of Isabelle types*) -datatype pseudotype = PVar | PType of string * pseudotype list +(* An abstraction of Isabelle types and first-order terms *) +datatype pattern = PVar | PApp of string * pattern list -fun string_for_pseudotype PVar = "?" - | string_for_pseudotype (PType (s, Ts)) = - (case Ts of - [] => "" - | [T] => string_for_pseudotype T - | Ts => string_for_pseudotypes Ts ^ " ") ^ s -and string_for_pseudotypes Ts = - "(" ^ commas (map string_for_pseudotype Ts) ^ ")" +fun string_for_pattern PVar = "_" + | string_for_pattern (PApp (s, ps)) = + if null ps then s else s ^ string_for_patterns ps +and string_for_patterns ps = "(" ^ commas (map string_for_pattern ps) ^ ")" (*Is the second type an instance of the first one?*) -fun match_pseudotype (PType (a, T), PType (b, U)) = - a = b andalso match_pseudotypes (T, U) - | match_pseudotype (PVar, _) = true - | match_pseudotype (_, PVar) = false -and match_pseudotypes ([], []) = true - | match_pseudotypes (T :: Ts, U :: Us) = - match_pseudotype (T, U) andalso match_pseudotypes (Ts, Us) +fun match_pattern (PVar, _) = true + | match_pattern (PApp _, PVar) = false + | match_pattern (PApp (s, ps), PApp (t, qs)) = + s = t andalso match_patterns (ps, qs) +and match_patterns (_, []) = true + | match_patterns ([], _) = false + | match_patterns (p :: ps, q :: qs) = + match_pattern (p, q) andalso match_patterns (ps, qs) -(*Is there a unifiable constant?*) -fun pseudoconst_mem f const_tab (c, c_typ) = - exists (curry (match_pseudotypes o f) c_typ) - (these (Symtab.lookup const_tab c)) +(* Is there a unifiable constant? *) +fun pconst_mem f consts (s, ps) = + exists (curry (match_patterns o f) ps) + (map snd (filter (curry (op =) s o fst) consts)) +fun pconst_hyper_mem f const_tab (s, ps) = + exists (curry (match_patterns o f) ps) (these (Symtab.lookup const_tab s)) -fun pseudotype_for (Type (c,typs)) = PType (c, map pseudotype_for typs) - | pseudotype_for (TFree _) = PVar - | pseudotype_for (TVar _) = PVar -(* Pairs a constant with the list of its type instantiations. *) -fun pseudoconst_for thy (c, T) = - (c, map pseudotype_for (Sign.const_typargs thy (c, T))) - handle TYPE _ => (c, []) (* Variable (locale constant): monomorphic *) +fun ptype (Type (s, Ts)) = PApp (s, map ptype Ts) + | ptype (TFree (s, _)) = PApp (s, []) + | ptype (TVar _) = PVar -fun string_for_pseudoconst (s, []) = s - | string_for_pseudoconst (s, Ts) = s ^ string_for_pseudotypes Ts -fun string_for_super_pseudoconst (s, [[]]) = s - | string_for_super_pseudoconst (s, Tss) = - s ^ "{" ^ commas (map string_for_pseudotypes Tss) ^ "}" +fun pterm thy t = + case strip_comb t of + (Const x, ts) => PApp (pconst thy true x ts) + | (Free x, ts) => PApp (pconst thy false x ts) + | (Var x, []) => PVar + | _ => PApp ("?", []) (* equivalence class of higher-order constructs *) +(* Pairs a constant with the list of its type instantiations. *) +and pconst_args thy const (s, T) ts = + (if const then map ptype (these (try (Sign.const_typargs thy) (s, T))) + else []) @ + (if !term_patterns then map (pterm thy) ts else []) +and pconst thy const (s, T) ts = (s, pconst_args thy const (s, T) ts) -val abs_prefix = "Sledgehammer.abs" +fun string_for_hyper_pconst (s, pss) = + s ^ "{" ^ commas (map string_for_patterns pss) ^ "}" + +val abs_name = "Sledgehammer.abs" val skolem_prefix = "Sledgehammer.sko" -(* Add a pseudoconstant to the table, but a [] entry means a standard +(* These are typically simplified away by "Meson.presimplify". Equality is + handled specially via "fequal". *) +val boring_consts = + [@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let}, + @{const_name "op ="}] + +(* Add a pconstant to the table, but a [] entry means a standard connective, which we ignore.*) -fun add_pseudoconst_to_table also_skolem (c, ctyps) = - if also_skolem orelse not (String.isPrefix skolem_prefix c) then - Symtab.map_default (c, [ctyps]) - (fn [] => [] | ctypss => insert (op =) ctyps ctypss) +fun add_pconst_to_table also_skolem (c, ps) = + if member (op =) boring_consts c orelse + (not also_skolem andalso String.isPrefix skolem_prefix c) then + I else - I + Symtab.map_default (c, [ps]) (insert (op =) ps) fun is_formula_type T = (T = HOLogic.boolT orelse T = propT) -val flip = Option.map not -(* These are typically simplified away by "Meson.presimplify". *) -val boring_consts = - [@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let}] - -fun get_pseudoconsts thy also_skolems pos ts = +fun get_pconsts thy also_skolems pos ts = let + val flip = Option.map not (* We include free variables, as well as constants, to handle locales. For each quantifiers that must necessarily be skolemized by the ATP, we introduce a fresh constant to simulate the effect of Skolemization. *) - fun do_term t = - case t of - Const x => add_pseudoconst_to_table also_skolems (pseudoconst_for thy x) - | Free (s, _) => add_pseudoconst_to_table also_skolems (s, []) - | t1 $ t2 => fold do_term [t1, t2] - | Abs (_, _, t') => - do_term t' #> add_pseudoconst_to_table true (abs_prefix, []) - | _ => I + fun do_const const (s, T) ts = + add_pconst_to_table also_skolems (pconst thy const (s, T) ts) + #> fold do_term ts + and do_term t = + case strip_comb t of + (Const x, ts) => do_const true x ts + | (Free x, ts) => do_const false x ts + | (Abs (_, _, t'), ts) => + null ts ? add_pconst_to_table true (abs_name, []) + #> fold do_term (t' :: ts) + | (_, ts) => fold do_term ts fun do_quantifier will_surely_be_skolemized body_t = do_formula pos body_t #> (if also_skolems andalso will_surely_be_skolemized then - add_pseudoconst_to_table true (gensym skolem_prefix, []) + add_pconst_to_table true (gensym skolem_prefix, []) else I) and do_term_or_formula T = @@ -179,10 +193,7 @@ | (t0 as Const (_, @{typ bool})) $ t1 => do_term t0 #> do_formula pos t1 (* theory constant *) | _ => do_term t - in - Symtab.empty |> fold (Symtab.update o rpair []) boring_consts - |> fold (do_formula pos) ts - end + in Symtab.empty |> fold (do_formula pos) ts end (*Inserts a dummy "constant" referring to the theory name, so that relevance takes the given theory into account.*) @@ -199,43 +210,41 @@ (* A two-dimensional symbol table counts frequencies of constants. It's keyed first by constant name and second by its list of type instantiations. For the - latter, we need a linear ordering on "pseudotype list". *) + latter, we need a linear ordering on "pattern list". *) -fun pseudotype_ord p = +fun pattern_ord p = case p of (PVar, PVar) => EQUAL - | (PVar, PType _) => LESS - | (PType _, PVar) => GREATER - | (PType q1, PType q2) => - prod_ord fast_string_ord (dict_ord pseudotype_ord) (q1, q2) + | (PVar, PApp _) => LESS + | (PApp _, PVar) => GREATER + | (PApp q1, PApp q2) => + prod_ord fast_string_ord (dict_ord pattern_ord) (q1, q2) structure CTtab = - Table(type key = pseudotype list val ord = dict_ord pseudotype_ord) + Table(type key = pattern list val ord = dict_ord pattern_ord) -fun count_axiom_consts theory_relevant thy (_, th) = +fun count_axiom_consts theory_relevant thy = let - fun do_const (a, T) = - let val (c, cts) = pseudoconst_for thy (a, T) in - (* Two-dimensional table update. Constant maps to types maps to - count. *) - CTtab.map_default (cts, 0) (Integer.add 1) - |> Symtab.map_default (c, CTtab.empty) - end - fun do_term (Const x) = do_const x - | do_term (Free x) = do_const x - | do_term (t $ u) = do_term t #> do_term u - | do_term (Abs (_, _, t)) = do_term t - | do_term _ = I - in th |> theory_const_prop_of theory_relevant |> do_term end + fun do_const const (s, T) ts = + (* Two-dimensional table update. Constant maps to types maps to count. *) + CTtab.map_default (pconst_args thy const (s, T) ts, 0) (Integer.add 1) + |> Symtab.map_default (s, CTtab.empty) + #> fold do_term ts + and do_term t = + case strip_comb t of + (Const x, ts) => do_const true x ts + | (Free x, ts) => do_const false x ts + | (Abs (_, _, t'), ts) => fold do_term (t' :: ts) + | (_, ts) => fold do_term ts + in do_term o theory_const_prop_of theory_relevant o snd end (**** Actual Filtering Code ****) (*The frequency of a constant is the sum of those of all instances of its type.*) -fun pseudoconst_freq match const_tab (c, cts) = - CTtab.fold (fn (cts', m) => match (cts, cts') ? Integer.add m) +fun pconst_freq match const_tab (c, ps) = + CTtab.fold (fn (qs, m) => match (ps, qs) ? Integer.add m) (the (Symtab.lookup const_tab c)) 0 - handle Option.Option => 0 (* A surprising number of theorems contain only a few significant constants. @@ -244,24 +253,23 @@ (* "log" seems best in practice. A constant function of one ignores the constant frequencies. *) fun rel_log n = 1.0 + 2.0 / Math.ln (Real.fromInt n + 1.0) -(* TODO: experiment -fun irrel_log n = 0.5 + 1.0 / Math.ln (Real.fromInt n + 1.0) -*) fun irrel_log n = Math.ln (Real.fromInt n + 19.0) / 6.4 (* FUDGE *) -val skolem_weight = 1.0 -val abs_weight = 2.0 +val abs_rel_weight = 0.5 +val abs_irrel_weight = 2.0 +val skolem_rel_weight = 2.0 (* impossible *) +val skolem_irrel_weight = 0.5 (* Computes a constant's weight, as determined by its frequency. *) -val rel_weight = rel_log oo pseudoconst_freq match_pseudotypes -fun irrel_weight const_tab (c as (s, _)) = - if String.isPrefix skolem_prefix s then skolem_weight - else if String.isPrefix abs_prefix s then abs_weight - else irrel_log (pseudoconst_freq (match_pseudotypes o swap) const_tab c) -(* TODO: experiment -fun irrel_weight _ _ = 1.0 -*) +fun generic_weight abs_weight skolem_weight logx f const_tab (c as (s, _)) = + if s = abs_name then abs_weight + else if String.isPrefix skolem_prefix s then skolem_weight + else logx (pconst_freq (match_patterns o f) const_tab c) + +val rel_weight = generic_weight abs_rel_weight skolem_rel_weight rel_log I +val irrel_weight = generic_weight abs_irrel_weight skolem_irrel_weight irrel_log + swap (* FUDGE *) fun locality_multiplier General = 1.0 @@ -270,43 +278,33 @@ | locality_multiplier Chained = 2.0 fun axiom_weight loc const_tab relevant_consts axiom_consts = - case axiom_consts |> List.partition (pseudoconst_mem I relevant_consts) - ||> filter_out (pseudoconst_mem swap relevant_consts) of - ([], []) => 0.0 - | (_, []) => 1.0 + case axiom_consts |> List.partition (pconst_hyper_mem I relevant_consts) + ||> filter_out (pconst_hyper_mem swap relevant_consts) of + ([], _) => 0.0 | (rel, irrel) => - let - val rel_weight = fold (curry Real.+ o rel_weight const_tab) rel 0.0 - |> curry Real.* (locality_multiplier loc) - val irrel_weight = fold (curry Real.+ o irrel_weight const_tab) irrel 0.0 - val res = rel_weight / (rel_weight + irrel_weight) - in if Real.isFinite res then res else 0.0 end + case irrel |> filter_out (pconst_mem swap rel) of + [] => 1.0 + | irrel => + let + val rel_weight = + fold (curry Real.+ o rel_weight const_tab) rel 0.0 + |> curry Real.* (locality_multiplier loc) + val irrel_weight = + fold (curry Real.+ o irrel_weight const_tab) irrel 0.0 + val res = rel_weight / (rel_weight + irrel_weight) + in if Real.isFinite res then res else 0.0 end -(* TODO: experiment -fun debug_axiom_weight const_tab relevant_consts axiom_consts = - case axiom_consts |> List.partition (pseudoconst_mem I relevant_consts) - ||> filter_out (pseudoconst_mem swap relevant_consts) of - ([], []) => 0.0 - | (_, []) => 1.0 - | (rel, irrel) => - let -val _ = tracing (PolyML.makestring ("REL: ", rel)) -val _ = tracing (PolyML.makestring ("IRREL: ", irrel)) - val rel_weight = fold (curry Real.+ o rel_weight const_tab) rel 0.0 - val irrel_weight = fold (curry Real.+ o irrel_weight const_tab) irrel 0.0 - val res = rel_weight / (rel_weight + irrel_weight) - in if Real.isFinite res then res else 0.0 end -*) - -fun pseudoconsts_of_term thy t = - Symtab.fold (fn (x, ys) => fold (fn y => cons (x, y)) ys) - (get_pseudoconsts thy true (SOME true) [t]) [] +fun pconsts_in_axiom thy t = + Symtab.fold (fn (s, pss) => fold (cons o pair s) pss) + (get_pconsts thy true (SOME true) [t]) [] fun pair_consts_axiom theory_relevant thy axiom = - (axiom, axiom |> snd |> theory_const_prop_of theory_relevant - |> pseudoconsts_of_term thy) + case axiom |> snd |> theory_const_prop_of theory_relevant + |> pconsts_in_axiom thy of + [] => NONE + | consts => SOME ((axiom, consts), NONE) type annotated_thm = - (((unit -> string) * locality) * thm) * (string * pseudotype list) list + (((unit -> string) * locality) * thm) * (string * pattern list) list fun take_most_relevant max_max_imperfect max_relevant remaining_max (candidates : (annotated_thm * real) list) = @@ -321,18 +319,22 @@ val ((accepts, more_rejects), rejects) = chop max_imperfect imperfect |>> append perfect |>> chop remaining_max in - trace_msg (fn () => "Number of candidates: " ^ - string_of_int (length candidates)); - trace_msg (fn () => "Effective threshold: " ^ - Real.toString (#2 (hd accepts))); trace_msg (fn () => "Actually passed (" ^ Int.toString (length accepts) ^ - "): " ^ (accepts + " of " ^ Int.toString (length candidates) ^ "): " ^ (accepts |> map (fn ((((name, _), _), _), weight) => name () ^ " [" ^ Real.toString weight ^ "]") |> commas)); (accepts, more_rejects @ rejects) end +fun if_empty_replace_with_locality thy axioms loc tab = + if Symtab.is_empty tab then + get_pconsts thy false (SOME false) + (map_filter (fn ((_, loc'), th) => + if loc' = loc then SOME (prop_of th) else NONE) axioms) + else + tab + (* FUDGE *) val threshold_divisor = 2.0 val ridiculous_threshold = 0.1 @@ -342,8 +344,12 @@ ({add, del, ...} : relevance_override) axioms goal_ts = let val thy = ProofContext.theory_of ctxt - val const_tab = fold (count_axiom_consts theory_relevant thy) axioms - Symtab.empty + val const_tab = + fold (count_axiom_consts theory_relevant thy) axioms Symtab.empty + val goal_const_tab = + get_pconsts thy false (SOME false) goal_ts + |> fold (if_empty_replace_with_locality thy axioms) + [Chained, Local, Theory] val add_thms = maps (ProofContext.get_fact ctxt) add val del_thms = maps (ProofContext.get_fact ctxt) del val max_max_imperfect = @@ -373,7 +379,7 @@ candidates val rel_const_tab' = rel_const_tab - |> fold (add_pseudoconst_to_table false) + |> fold (add_pconst_to_table false) (maps (snd o fst) accepts) fun is_dirty (c, _) = Symtab.lookup rel_const_tab' c <> Symtab.lookup rel_const_tab c @@ -389,14 +395,14 @@ (ax, if exists is_dirty consts then NONE else SOME old_weight))) val threshold = - threshold + (1.0 - threshold) - * Math.pow (decay, Real.fromInt (length accepts)) + 1.0 - (1.0 - threshold) + * Math.pow (decay, Real.fromInt (length accepts)) val remaining_max = remaining_max - length accepts in trace_msg (fn () => "New or updated constants: " ^ commas (rel_const_tab' |> Symtab.dest - |> subtract (op =) (Symtab.dest rel_const_tab) - |> map string_for_super_pseudoconst)); + |> subtract (op =) (rel_const_tab |> Symtab.dest) + |> map string_for_hyper_pconst)); map (fst o fst) accepts @ (if remaining_max = 0 then game_over (hopeful_rejects @ map (apsnd SOME) hopeless_rejects) @@ -431,14 +437,13 @@ Real.toString threshold ^ ", constants: " ^ commas (rel_const_tab |> Symtab.dest |> filter (curry (op <>) [] o snd) - |> map string_for_super_pseudoconst)); + |> map string_for_hyper_pconst)); relevant [] [] hopeless hopeful end in axioms |> filter_out (member Thm.eq_thm del_thms o snd) - |> map (rpair NONE o pair_consts_axiom theory_relevant thy) - |> iter 0 max_relevant threshold0 - (get_pseudoconsts thy false (SOME false) goal_ts) [] + |> map_filter (pair_consts_axiom theory_relevant thy) + |> iter 0 max_relevant threshold0 goal_const_tab [] |> tap (fn res => trace_msg (fn () => "Total relevant: " ^ Int.toString (length res))) end @@ -503,12 +508,17 @@ val exists_sledgehammer_const = exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s) -fun is_strange_theorem th = +fun is_metastrange_theorem th = case head_of (concl_of th) of Const (a, _) => (a <> @{const_name Trueprop} andalso a <> @{const_name "=="}) | _ => false +fun is_that_fact th = + String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th) + andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN + | _ => false) (prop_of th) + val type_has_top_sort = exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false) @@ -578,7 +588,7 @@ let val t = prop_of thm in is_formula_too_complex t orelse exists_type type_has_top_sort t orelse is_dangerous_term full_types t orelse exists_sledgehammer_const t orelse - is_strange_theorem thm + is_metastrange_theorem thm orelse is_that_fact thm end fun all_name_thms_pairs ctxt reserved full_types add_thms chained_ths = @@ -589,15 +599,15 @@ val local_facts = ProofContext.facts_of ctxt val named_locals = local_facts |> Facts.dest_static [] val is_chained = member Thm.eq_thm chained_ths - (* Unnamed, not chained formulas with schematic variables are omitted, - because they are rejected by the backticks (`...`) parser for some - reason. *) + (* Unnamed nonchained formulas with schematic variables are omitted, because + they are rejected by the backticks (`...`) parser for some reason. *) fun is_good_unnamed_local th = + not (Thm.has_name_hint th) andalso + (not (exists_subterm is_Var (prop_of th)) orelse (is_chained th)) andalso forall (fn (_, ths) => not (member Thm.eq_thm ths th)) named_locals - andalso (not (exists_subterm is_Var (prop_of th)) orelse (is_chained th)) val unnamed_locals = - local_facts |> Facts.props |> filter is_good_unnamed_local - |> map (pair "" o single) + union Thm.eq_thm (Facts.props local_facts) chained_ths + |> filter is_good_unnamed_local |> map (pair "" o single) val full_space = Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts) fun add_facts global foldx facts = @@ -667,8 +677,8 @@ theory_relevant (relevance_override as {add, del, only}) (ctxt, (chained_ths, _)) hyp_ts concl_t = let - val decay = 1.0 - Math.pow ((1.0 - threshold1) / (1.0 - threshold0), - 1.0 / Real.fromInt (max_relevant + 1)) + val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0), + 1.0 / Real.fromInt (max_relevant + 1)) val add_thms = maps (ProofContext.get_fact ctxt) add val reserved = reserved_isar_keyword_table () val axioms = @@ -689,7 +699,7 @@ else relevance_filter ctxt threshold0 decay max_relevant theory_relevant relevance_override axioms (concl_t :: hyp_ts)) - |> map (apfst (apfst (fn f => f ()))) |> sort_wrt (fst o fst) + |> map (apfst (apfst (fn f => f ()))) end end; diff -r d0196406ee32 -r c18e8f90f4dc src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Aug 27 14:25:29 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Aug 27 16:05:46 2010 +0200 @@ -10,18 +10,16 @@ sig type locality = Sledgehammer_Fact_Filter.locality type minimize_command = string list -> string - - val metis_proof_text: - bool * minimize_command * string * (string * locality) vector * thm * int - -> string * (string * locality) list - val isar_proof_text: + type metis_params = + bool * minimize_command * string * (string * locality) list vector * thm + * int + type isar_params = string Symtab.table * bool * int * Proof.context * int list list - -> bool * minimize_command * string * (string * locality) vector * thm * int - -> string * (string * locality) list - val proof_text: - bool -> string Symtab.table * bool * int * Proof.context * int list list - -> bool * minimize_command * string * (string * locality) vector * thm * int - -> string * (string * locality) list + type text_result = string * (string * locality) list + + val metis_proof_text : metis_params -> text_result + val isar_proof_text : isar_params -> metis_params -> text_result + val proof_text : bool -> isar_params -> metis_params -> text_result end; structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT = @@ -34,6 +32,11 @@ open Sledgehammer_Translate type minimize_command = string list -> string +type metis_params = + bool * minimize_command * string * (string * locality) list vector * thm * int +type isar_params = + string Symtab.table * bool * int * Proof.context * int list list +type text_result = string * (string * locality) list (* Simple simplifications to ensure that sort annotations don't leave a trail of spurious "True"s. *) @@ -61,7 +64,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 - fst (Vector.sub (axiom_names, num - 1)) <> "" + not (null (Vector.sub (axiom_names, num - 1))) fun is_conjecture_number conjecture_shape num = index_in_shape num conjecture_shape >= 0 @@ -565,12 +568,10 @@ "108. ... [input]". *) fun used_facts_in_atp_proof axiom_names atp_proof = let - fun axiom_name_at_index num = + fun axiom_names_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)) - else - NONE + if is_axiom_number axiom_names j then Vector.sub (axiom_names, j - 1) + else [] end val tokens_of = String.tokens (fn c => not (Char.isAlphaNum c) andalso c <> #"_") @@ -579,17 +580,19 @@ (case strip_prefix_and_unascii axiom_prefix (List.last rest) of SOME name => if member (op =) rest "file" then - SOME (name, find_first_in_vector axiom_names name General) + ([(name, name |> find_first_in_list_vector axiom_names |> the)] + handle Option.Option => + error ("No such fact: " ^ quote name ^ ".")) else - axiom_name_at_index num - | NONE => axiom_name_at_index num) + axiom_names_at_index num + | NONE => axiom_names_at_index num) else - NONE - | do_line (num :: "0" :: "Inp" :: _) = axiom_name_at_index num + [] + | do_line (num :: "0" :: "Inp" :: _) = axiom_names_at_index num | do_line (num :: rest) = - (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 + (case List.last rest of "input" => axiom_names_at_index num | _ => []) + | do_line _ = [] + in atp_proof |> split_proof_lines |> maps (do_line o tokens_of) end val indent_size = 2 val no_label = ("", ~1) @@ -663,7 +666,7 @@ fun add_fact_from_dep axiom_names num = if is_axiom_number axiom_names num then - apsnd (insert (op =) (fst (Vector.sub (axiom_names, num - 1)))) + apsnd (union (op =) (map fst (Vector.sub (axiom_names, num - 1)))) else apfst (insert (op =) (raw_prefix, num)) diff -r d0196406ee32 -r c18e8f90f4dc src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Fri Aug 27 14:25:29 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Fri Aug 27 16:05:46 2010 +0200 @@ -19,7 +19,7 @@ val prepare_problem : Proof.context -> bool -> bool -> bool -> bool -> term list -> term -> ((string * 'a) * thm) list - -> string problem * string Symtab.table * int * (string * 'a) vector + -> string problem * string Symtab.table * int * (string * 'a) list vector end; structure Sledgehammer_Translate : SLEDGEHAMMER_TRANSLATE = @@ -271,7 +271,7 @@ val (supers', arity_clauses) = make_arity_clauses thy tycons supers val class_rel_clauses = make_class_rel_clauses thy subs supers' in - (Vector.fromList axiom_names, + (axiom_names |> map single |> Vector.fromList, (conjectures, axioms, helper_facts, class_rel_clauses, arity_clauses)) end diff -r d0196406ee32 -r c18e8f90f4dc src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Aug 27 14:25:29 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Aug 27 16:05:46 2010 +0200 @@ -6,7 +6,7 @@ signature SLEDGEHAMMER_UTIL = sig - val find_first_in_vector : (''a * 'b) vector -> ''a -> 'b -> 'b + val find_first_in_list_vector : (''a * 'b) list vector -> ''a -> 'b option val plural_s : int -> string val serial_commas : string -> string list -> string list val simplify_spaces : string -> string @@ -29,9 +29,9 @@ structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = struct -fun find_first_in_vector vec key default = - Vector.foldl (fn ((key', value'), value) => - if key' = key then value' else value) default vec +fun find_first_in_list_vector vec key = + Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key + | (_, value) => value) NONE vec fun plural_s n = if n = 1 then "" else "s"