# HG changeset patch # User blanchet # Date 1314784323 -7200 # Node ID 4a1132815a70b3c7076b11153f032bb3ed2011b0 # Parent b82085db501fa5a8dcd35a7d7478aaa175300d22 more tuning diff -r b82085db501f -r 4a1132815a70 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Aug 31 11:23:16 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Aug 31 11:52:03 2011 +0200 @@ -416,12 +416,12 @@ let val _ = if is_appropriate_prop concl_t then () else raise Fail "inappropriate" - val is_ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover_name + val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover_name val facts = - Sledgehammer_Filter.nearly_all_facts ctxt is_ho_atp - relevance_override chained_ths hyp_ts concl_t + Sledgehammer_Filter.nearly_all_facts ctxt ho_atp relevance_override + chained_ths hyp_ts concl_t |> filter (is_appropriate_prop o prop_of o snd) - |> Sledgehammer_Filter.relevant_facts ctxt is_ho_atp relevance_thresholds + |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds (the_default default_max_relevant max_relevant) is_built_in_const relevance_fudge relevance_override chained_ths hyp_ts concl_t diff -r b82085db501f -r 4a1132815a70 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Wed Aug 31 11:23:16 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Wed Aug 31 11:52:03 2011 +0200 @@ -129,12 +129,12 @@ val relevance_override = {add = [], del = [], only = false} val subgoal = 1 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal subgoal - val is_ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover + val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover val facts = - Sledgehammer_Filter.nearly_all_facts ctxt is_ho_atp relevance_override + Sledgehammer_Filter.nearly_all_facts ctxt ho_atp relevance_override chained_ths hyp_ts concl_t |> filter (is_appropriate_prop o prop_of o snd) - |> Sledgehammer_Filter.relevant_facts ctxt is_ho_atp relevance_thresholds + |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds (the_default default_max_relevant max_relevant) is_built_in_const relevance_fudge relevance_override chained_ths hyp_ts concl_t diff -r b82085db501f -r 4a1132815a70 src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Wed Aug 31 11:23:16 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Aug 31 11:52:03 2011 +0200 @@ -367,17 +367,17 @@ (** Isabelle arities **) -type arity_literal = name * name * name list +type arity_atom = name * name * name list val type_class = the_single @{sort type} -fun add_packed_sort tvar = - fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar, [])) - type arity_clause = {name : string, - prem_lits : arity_literal list, - concl_lit : arity_literal} + prem_atoms : arity_atom list, + concl_atom : arity_atom} + +fun add_prem_atom tvar = + fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar, [])) (* Arity of type constructor "tcon :: (arg1, ..., argN) res" *) fun make_axiom_arity_clause (tcons, name, (cls, args)) = @@ -386,9 +386,9 @@ val tvars_srts = ListPair.zip (tvars, args) in {name = name, - prem_lits = [] |> fold (uncurry add_packed_sort) tvars_srts, - concl_lit = (`make_type_class cls, `make_fixed_type_const tcons, - tvars ~~ tvars)} + prem_atoms = [] |> fold (uncurry add_prem_atom) tvars_srts, + concl_atom = (`make_type_class cls, `make_fixed_type_const tcons, + tvars ~~ tvars)} end fun arity_clause _ _ (_, []) = [] @@ -715,7 +715,7 @@ Explicit_Type_Args) end -(* Make literals for sorted type variables. *) +(* Make atoms for sorted type variables. *) fun generic_add_sorts_on_type (_, []) = I | generic_add_sorts_on_type ((x, i), s :: ss) = generic_add_sorts_on_type ((x, i), ss) @@ -731,8 +731,24 @@ fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z | add_sorts_on_tvar _ = I -fun type_literals_for_types type_enc add_sorts_on_typ Ts = +val tvar_a_str = "'a" +val tvar_a = TVar ((tvar_a_str, 0), HOLogic.typeS) +val tvar_a_name = (make_schematic_type_var (tvar_a_str, 0), tvar_a_str) +val itself_name = `make_fixed_type_const @{type_name itself} +val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE} +val tvar_a_atype = AType (tvar_a_name, []) +val a_itself_atype = AType (itself_name, [tvar_a_atype]) + +fun type_class_formula type_enc class arg = + AAtom (ATerm (class, arg :: + (case type_enc of + Simple_Types (_, Polymorphic, _) => + if exploit_tff1_dummy_type_vars then [] else [ATerm (TYPE_name, [arg])] + | _ => []))) +fun formulas_for_types type_enc add_sorts_on_typ Ts = [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts + |> map (fn (class, name) => + type_class_formula type_enc class (ATerm (name, []))) fun mk_aconns c phis = let val (phis', phi') = split_last phis in @@ -1273,14 +1289,6 @@ K (add_iterm_syms_to_table ctxt explicit_apply) |> formula_fold NONE |> fact_lift -val tvar_a_str = "'a" -val tvar_a = TVar ((tvar_a_str, 0), HOLogic.typeS) -val tvar_a_name = (make_schematic_type_var (tvar_a_str, 0), tvar_a_str) -val itself_name = `make_fixed_type_const @{type_name itself} -val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE} -val tvar_a_atype = AType (tvar_a_name, []) -val a_itself_atype = AType (itself_name, [tvar_a_atype]) - val default_sym_tab_entries : (string * sym_info) list = (prefixed_predicator_name, {pred_sym = true, min_ary = 1, max_ary = 1, types = []}) @@ -1453,22 +1461,8 @@ (("If", true), @{thms if_True if_False True_or_False})] |> map (apsnd (map zero_var_indexes)) -fun type_class_aterm type_enc class arg = - case type_enc of - Simple_Types (_, Polymorphic, _) => - if exploit_tff1_dummy_type_vars then ATerm (class, [arg]) - else ATerm (class, [arg, ATerm (TYPE_name, [arg])]) - | _ => ATerm (class, [arg]) - -fun fo_literal_from_type_literal type_enc (class, name) = - (true, type_class_aterm type_enc class (ATerm (name, []))) - -fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot - -fun bound_tvars type_enc Ts = - mk_ahorn (map (formula_from_fo_literal - o fo_literal_from_type_literal type_enc) - (type_literals_for_types type_enc add_sorts_on_tvar Ts)) +fun bound_tvars type_enc = + mk_ahorn o formulas_for_types type_enc add_sorts_on_tvar fun eq_formula type_enc atomic_Ts pred_sym tm1 tm2 = (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2]) @@ -1750,22 +1744,20 @@ let val ty_arg = ATerm (tvar_a_name, []) in Formula (class_rel_clause_prefix ^ ascii_of name, Axiom, AConn (AImplies, - [AAtom (type_class_aterm type_enc subclass ty_arg), - AAtom (type_class_aterm type_enc superclass ty_arg)]) + [type_class_formula type_enc subclass ty_arg, + type_class_formula type_enc superclass ty_arg]) |> close_formula_universally type_enc, isabelle_info introN, NONE) end -fun fo_literal_from_arity_literal type_enc (class, t, args) = - (true, type_class_aterm type_enc class - (ATerm (t, map (fn arg => ATerm (arg, [])) args))) +fun formula_from_arity_atom type_enc (class, t, args) = + ATerm (t, map (fn arg => ATerm (arg, [])) args) + |> type_class_formula type_enc class fun formula_line_for_arity_clause type_enc - ({name, prem_lits, concl_lit, ...} : arity_clause) = + ({name, prem_atoms, concl_atom, ...} : arity_clause) = Formula (arity_clause_prefix ^ name, Axiom, - mk_ahorn (map (formula_from_fo_literal - o fo_literal_from_arity_literal type_enc) prem_lits) - (formula_from_fo_literal - (fo_literal_from_arity_literal type_enc concl_lit)) + mk_ahorn (map (formula_from_arity_atom type_enc) prem_atoms) + (formula_from_arity_atom type_enc concl_atom) |> close_formula_universally type_enc, isabelle_info introN, NONE) fun formula_line_for_conjecture ctxt format mono type_enc @@ -1777,18 +1769,14 @@ |> bound_tvars type_enc atomic_types |> close_formula_universally type_enc, NONE, NONE) -fun free_type_literals type_enc ({atomic_types, ...} : translated_formula) = - atomic_types |> type_literals_for_types type_enc add_sorts_on_tfree - |> map (fo_literal_from_type_literal type_enc) - -fun formula_line_for_free_type j lit = - Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, - formula_from_fo_literal lit, NONE, NONE) +fun formula_line_for_free_type j phi = + Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, NONE) fun formula_lines_for_free_types type_enc facts = let - val litss = map (free_type_literals type_enc) facts - val lits = fold (union (op =)) litss [] - in map2 formula_line_for_free_type (0 upto length lits - 1) lits end + val phis = + fold (union (op =)) (map #atomic_types facts) [] + |> formulas_for_types type_enc add_sorts_on_tfree + in map2 formula_line_for_free_type (0 upto length phis - 1) phis end (** Symbol declarations **) diff -r b82085db501f -r 4a1132815a70 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Aug 31 11:23:16 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Aug 31 11:52:03 2011 +0200 @@ -52,7 +52,7 @@ Proof.context -> bool -> relevance_override -> thm list -> term list -> term -> (((unit -> string) * locality) * thm) list val relevant_facts : - Proof.context -> bool -> real * real -> int + Proof.context -> real * real -> int -> (string * typ -> term list -> bool * term list) -> relevance_fudge -> relevance_override -> thm list -> term list -> term -> (((unit -> string) * locality) * thm) list @@ -586,7 +586,7 @@ facts are included. *) val special_fact_index = 75 -fun relevance_filter ctxt ho_atp threshold0 decay max_relevant is_built_in_const +fun relevance_filter ctxt threshold0 decay max_relevant is_built_in_const (fudge as {threshold_divisor, ridiculous_threshold, ...}) ({add, del, ...} : relevance_override) facts chained_ts hyp_ts concl_t = let @@ -938,9 +938,9 @@ |> uniquify end -fun relevant_facts ctxt ho_atp (threshold0, threshold1) max_relevant - is_built_in_const fudge (override as {only, ...}) chained_ths - hyp_ts concl_t facts = +fun relevant_facts ctxt (threshold0, threshold1) max_relevant is_built_in_const + fudge (override as {only, ...}) chained_ths hyp_ts concl_t + facts = let val thy = Proof_Context.theory_of ctxt val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0), @@ -954,9 +954,9 @@ max_relevant = 0 then [] else - relevance_filter ctxt ho_atp threshold0 decay max_relevant - is_built_in_const fudge override facts (chained_ths |> map prop_of) - hyp_ts (concl_t |> theory_constify fudge (Context.theory_name thy))) + relevance_filter ctxt threshold0 decay max_relevant is_built_in_const + fudge override facts (chained_ths |> map prop_of) hyp_ts + (concl_t |> theory_constify fudge (Context.theory_name thy))) |> map (apfst (apfst (fn f => f ()))) end diff -r b82085db501f -r 4a1132815a70 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Aug 31 11:23:16 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Aug 31 11:52:03 2011 +0200 @@ -269,9 +269,10 @@ val {facts = chained_ths, goal, ...} = Proof.goal state val chained_ths = chained_ths |> normalize_chained_theorems val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i - val is_ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers - val facts = nearly_all_facts ctxt is_ho_atp relevance_override - chained_ths hyp_ts concl_t + val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers + val facts = + nearly_all_facts ctxt ho_atp relevance_override chained_ths hyp_ts + concl_t val _ = () |> not blocking ? kill_provers val _ = case find_first (not o is_prover_supported ctxt) provers of SOME name => error ("No such prover: " ^ name ^ ".") @@ -323,9 +324,9 @@ |> (case is_appropriate_prop of SOME is_app => filter (is_app o prop_of o snd) | NONE => I) - |> relevant_facts ctxt is_ho_atp relevance_thresholds - max_max_relevant is_built_in_const relevance_fudge - relevance_override chained_ths hyp_ts concl_t + |> relevant_facts ctxt relevance_thresholds max_max_relevant + is_built_in_const relevance_fudge relevance_override + chained_ths hyp_ts concl_t |> tap (fn facts => if debug then label ^ plural_s (length provers) ^ ": " ^ diff -r b82085db501f -r 4a1132815a70 src/HOL/ex/sledgehammer_tactics.ML --- a/src/HOL/ex/sledgehammer_tactics.ML Wed Aug 31 11:23:16 2011 +0200 +++ b/src/HOL/ex/sledgehammer_tactics.ML Wed Aug 31 11:52:03 2011 +0200 @@ -37,13 +37,11 @@ val relevance_fudge = Sledgehammer_Provers.relevance_fudge_for_prover ctxt name val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i - val is_ho_atp = - exists (Sledgehammer_Provers.is_ho_atp ctxt) - provers(*FIXME: duplicated from sledgehammer_run.ML*) + val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers val facts = - Sledgehammer_Filter.nearly_all_facts ctxt is_ho_atp relevance_override + Sledgehammer_Filter.nearly_all_facts ctxt ho_atp relevance_override chained_ths hyp_ts concl_t - |> Sledgehammer_Filter.relevant_facts ctxt is_ho_atp relevance_thresholds + |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds (the_default default_max_relevant max_relevant) is_built_in_const relevance_fudge relevance_override chained_ths hyp_ts concl_t val problem =