more tuning
authorblanchet
Wed Aug 31 11:52:03 2011 +0200 (2011-08-31)
changeset 446254a1132815a70
parent 44624 b82085db501f
child 44626 a40b713232c8
more tuning
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
src/HOL/Tools/ATP/atp_translate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
src/HOL/ex/sledgehammer_tactics.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Aug 31 11:23:16 2011 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Aug 31 11:52:03 2011 +0200
     1.3 @@ -416,12 +416,12 @@
     1.4        let
     1.5          val _ = if is_appropriate_prop concl_t then ()
     1.6                  else raise Fail "inappropriate"
     1.7 -        val is_ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover_name
     1.8 +        val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover_name
     1.9          val facts =
    1.10 -          Sledgehammer_Filter.nearly_all_facts ctxt is_ho_atp
    1.11 -                          relevance_override chained_ths hyp_ts concl_t
    1.12 +          Sledgehammer_Filter.nearly_all_facts ctxt ho_atp relevance_override
    1.13 +            chained_ths hyp_ts concl_t
    1.14            |> filter (is_appropriate_prop o prop_of o snd)
    1.15 -          |> Sledgehammer_Filter.relevant_facts ctxt is_ho_atp relevance_thresholds
    1.16 +          |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
    1.17                   (the_default default_max_relevant max_relevant)
    1.18                   is_built_in_const relevance_fudge relevance_override
    1.19                   chained_ths hyp_ts concl_t
     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Wed Aug 31 11:23:16 2011 +0200
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Wed Aug 31 11:52:03 2011 +0200
     2.3 @@ -129,12 +129,12 @@
     2.4           val relevance_override = {add = [], del = [], only = false}
     2.5           val subgoal = 1
     2.6           val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal subgoal
     2.7 -         val is_ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
     2.8 +         val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
     2.9           val facts =
    2.10 -          Sledgehammer_Filter.nearly_all_facts ctxt is_ho_atp relevance_override
    2.11 +          Sledgehammer_Filter.nearly_all_facts ctxt ho_atp relevance_override
    2.12                                                 chained_ths hyp_ts concl_t
    2.13            |> filter (is_appropriate_prop o prop_of o snd)
    2.14 -          |> Sledgehammer_Filter.relevant_facts ctxt is_ho_atp relevance_thresholds
    2.15 +          |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
    2.16                   (the_default default_max_relevant max_relevant)
    2.17                   is_built_in_const relevance_fudge relevance_override
    2.18                   chained_ths hyp_ts concl_t
     3.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Aug 31 11:23:16 2011 +0200
     3.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Aug 31 11:52:03 2011 +0200
     3.3 @@ -367,17 +367,17 @@
     3.4  
     3.5  (** Isabelle arities **)
     3.6  
     3.7 -type arity_literal = name * name * name list
     3.8 +type arity_atom = name * name * name list
     3.9  
    3.10  val type_class = the_single @{sort type}
    3.11  
    3.12 -fun add_packed_sort tvar =
    3.13 -  fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar, []))
    3.14 -
    3.15  type arity_clause =
    3.16    {name : string,
    3.17 -   prem_lits : arity_literal list,
    3.18 -   concl_lit : arity_literal}
    3.19 +   prem_atoms : arity_atom list,
    3.20 +   concl_atom : arity_atom}
    3.21 +
    3.22 +fun add_prem_atom tvar =
    3.23 +  fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar, []))
    3.24  
    3.25  (* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)
    3.26  fun make_axiom_arity_clause (tcons, name, (cls, args)) =
    3.27 @@ -386,9 +386,9 @@
    3.28      val tvars_srts = ListPair.zip (tvars, args)
    3.29    in
    3.30      {name = name,
    3.31 -     prem_lits = [] |> fold (uncurry add_packed_sort) tvars_srts,
    3.32 -     concl_lit = (`make_type_class cls, `make_fixed_type_const tcons,
    3.33 -                  tvars ~~ tvars)}
    3.34 +     prem_atoms = [] |> fold (uncurry add_prem_atom) tvars_srts,
    3.35 +     concl_atom = (`make_type_class cls, `make_fixed_type_const tcons,
    3.36 +                   tvars ~~ tvars)}
    3.37    end
    3.38  
    3.39  fun arity_clause _ _ (_, []) = []
    3.40 @@ -715,7 +715,7 @@
    3.41                Explicit_Type_Args)
    3.42      end
    3.43  
    3.44 -(* Make literals for sorted type variables. *)
    3.45 +(* Make atoms for sorted type variables. *)
    3.46  fun generic_add_sorts_on_type (_, []) = I
    3.47    | generic_add_sorts_on_type ((x, i), s :: ss) =
    3.48      generic_add_sorts_on_type ((x, i), ss)
    3.49 @@ -731,8 +731,24 @@
    3.50  fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z
    3.51    | add_sorts_on_tvar _ = I
    3.52  
    3.53 -fun type_literals_for_types type_enc add_sorts_on_typ Ts =
    3.54 +val tvar_a_str = "'a"
    3.55 +val tvar_a = TVar ((tvar_a_str, 0), HOLogic.typeS)
    3.56 +val tvar_a_name = (make_schematic_type_var (tvar_a_str, 0), tvar_a_str)
    3.57 +val itself_name = `make_fixed_type_const @{type_name itself}
    3.58 +val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE}
    3.59 +val tvar_a_atype = AType (tvar_a_name, [])
    3.60 +val a_itself_atype = AType (itself_name, [tvar_a_atype])
    3.61 +
    3.62 +fun type_class_formula type_enc class arg =
    3.63 +  AAtom (ATerm (class, arg ::
    3.64 +      (case type_enc of
    3.65 +         Simple_Types (_, Polymorphic, _) =>
    3.66 +         if exploit_tff1_dummy_type_vars then [] else [ATerm (TYPE_name, [arg])]
    3.67 +       | _ => [])))
    3.68 +fun formulas_for_types type_enc add_sorts_on_typ Ts =
    3.69    [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
    3.70 +     |> map (fn (class, name) =>
    3.71 +                type_class_formula type_enc class (ATerm (name, [])))
    3.72  
    3.73  fun mk_aconns c phis =
    3.74    let val (phis', phi') = split_last phis in
    3.75 @@ -1273,14 +1289,6 @@
    3.76    K (add_iterm_syms_to_table ctxt explicit_apply)
    3.77    |> formula_fold NONE |> fact_lift
    3.78  
    3.79 -val tvar_a_str = "'a"
    3.80 -val tvar_a = TVar ((tvar_a_str, 0), HOLogic.typeS)
    3.81 -val tvar_a_name = (make_schematic_type_var (tvar_a_str, 0), tvar_a_str)
    3.82 -val itself_name = `make_fixed_type_const @{type_name itself}
    3.83 -val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE}
    3.84 -val tvar_a_atype = AType (tvar_a_name, [])
    3.85 -val a_itself_atype = AType (itself_name, [tvar_a_atype])
    3.86 -
    3.87  val default_sym_tab_entries : (string * sym_info) list =
    3.88    (prefixed_predicator_name,
    3.89     {pred_sym = true, min_ary = 1, max_ary = 1, types = []})
    3.90 @@ -1453,22 +1461,8 @@
    3.91     (("If", true), @{thms if_True if_False True_or_False})]
    3.92    |> map (apsnd (map zero_var_indexes))
    3.93  
    3.94 -fun type_class_aterm type_enc class arg =
    3.95 -  case type_enc of
    3.96 -    Simple_Types (_, Polymorphic, _) =>
    3.97 -    if exploit_tff1_dummy_type_vars then ATerm (class, [arg])
    3.98 -    else ATerm (class, [arg, ATerm (TYPE_name, [arg])])
    3.99 -  | _ => ATerm (class, [arg])
   3.100 -
   3.101 -fun fo_literal_from_type_literal type_enc (class, name) =
   3.102 -  (true, type_class_aterm type_enc class (ATerm (name, [])))
   3.103 -
   3.104 -fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
   3.105 -
   3.106 -fun bound_tvars type_enc Ts =
   3.107 -  mk_ahorn (map (formula_from_fo_literal
   3.108 -                 o fo_literal_from_type_literal type_enc)
   3.109 -                (type_literals_for_types type_enc add_sorts_on_tvar Ts))
   3.110 +fun bound_tvars type_enc =
   3.111 +  mk_ahorn o formulas_for_types type_enc add_sorts_on_tvar
   3.112  
   3.113  fun eq_formula type_enc atomic_Ts pred_sym tm1 tm2 =
   3.114    (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])
   3.115 @@ -1750,22 +1744,20 @@
   3.116    let val ty_arg = ATerm (tvar_a_name, []) in
   3.117      Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
   3.118               AConn (AImplies,
   3.119 -                    [AAtom (type_class_aterm type_enc subclass ty_arg),
   3.120 -                     AAtom (type_class_aterm type_enc superclass ty_arg)])
   3.121 +                    [type_class_formula type_enc subclass ty_arg,
   3.122 +                     type_class_formula type_enc superclass ty_arg])
   3.123               |> close_formula_universally type_enc, isabelle_info introN, NONE)
   3.124    end
   3.125  
   3.126 -fun fo_literal_from_arity_literal type_enc (class, t, args) =
   3.127 -  (true, type_class_aterm type_enc class
   3.128 -                          (ATerm (t, map (fn arg => ATerm (arg, [])) args)))
   3.129 +fun formula_from_arity_atom type_enc (class, t, args) =
   3.130 +  ATerm (t, map (fn arg => ATerm (arg, [])) args)
   3.131 +  |> type_class_formula type_enc class
   3.132  
   3.133  fun formula_line_for_arity_clause type_enc
   3.134 -        ({name, prem_lits, concl_lit, ...} : arity_clause) =
   3.135 +        ({name, prem_atoms, concl_atom, ...} : arity_clause) =
   3.136    Formula (arity_clause_prefix ^ name, Axiom,
   3.137 -           mk_ahorn (map (formula_from_fo_literal
   3.138 -                          o fo_literal_from_arity_literal type_enc) prem_lits)
   3.139 -                    (formula_from_fo_literal
   3.140 -                         (fo_literal_from_arity_literal type_enc concl_lit))
   3.141 +           mk_ahorn (map (formula_from_arity_atom type_enc) prem_atoms)
   3.142 +                    (formula_from_arity_atom type_enc concl_atom)
   3.143             |> close_formula_universally type_enc, isabelle_info introN, NONE)
   3.144  
   3.145  fun formula_line_for_conjecture ctxt format mono type_enc
   3.146 @@ -1777,18 +1769,14 @@
   3.147             |> bound_tvars type_enc atomic_types
   3.148             |> close_formula_universally type_enc, NONE, NONE)
   3.149  
   3.150 -fun free_type_literals type_enc ({atomic_types, ...} : translated_formula) =
   3.151 -  atomic_types |> type_literals_for_types type_enc add_sorts_on_tfree
   3.152 -               |> map (fo_literal_from_type_literal type_enc)
   3.153 -
   3.154 -fun formula_line_for_free_type j lit =
   3.155 -  Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis,
   3.156 -           formula_from_fo_literal lit, NONE, NONE)
   3.157 +fun formula_line_for_free_type j phi =
   3.158 +  Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, NONE)
   3.159  fun formula_lines_for_free_types type_enc facts =
   3.160    let
   3.161 -    val litss = map (free_type_literals type_enc) facts
   3.162 -    val lits = fold (union (op =)) litss []
   3.163 -  in map2 formula_line_for_free_type (0 upto length lits - 1) lits end
   3.164 +    val phis =
   3.165 +      fold (union (op =)) (map #atomic_types facts) []
   3.166 +      |> formulas_for_types type_enc add_sorts_on_tfree
   3.167 +  in map2 formula_line_for_free_type (0 upto length phis - 1) phis end
   3.168  
   3.169  (** Symbol declarations **)
   3.170  
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Aug 31 11:23:16 2011 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Aug 31 11:52:03 2011 +0200
     4.3 @@ -52,7 +52,7 @@
     4.4      Proof.context -> bool -> relevance_override -> thm list -> term list -> term
     4.5      -> (((unit -> string) * locality) * thm) list
     4.6    val relevant_facts :
     4.7 -    Proof.context -> bool -> real * real -> int
     4.8 +    Proof.context -> real * real -> int
     4.9      -> (string * typ -> term list -> bool * term list) -> relevance_fudge
    4.10      -> relevance_override -> thm list -> term list -> term
    4.11      -> (((unit -> string) * locality) * thm) list
    4.12 @@ -586,7 +586,7 @@
    4.13     facts are included. *)
    4.14  val special_fact_index = 75
    4.15  
    4.16 -fun relevance_filter ctxt ho_atp threshold0 decay max_relevant is_built_in_const
    4.17 +fun relevance_filter ctxt threshold0 decay max_relevant is_built_in_const
    4.18          (fudge as {threshold_divisor, ridiculous_threshold, ...})
    4.19          ({add, del, ...} : relevance_override) facts chained_ts hyp_ts concl_t =
    4.20    let
    4.21 @@ -938,9 +938,9 @@
    4.22      |> uniquify
    4.23    end
    4.24  
    4.25 -fun relevant_facts ctxt ho_atp (threshold0, threshold1) max_relevant
    4.26 -                   is_built_in_const fudge (override as {only, ...}) chained_ths
    4.27 -                   hyp_ts concl_t facts =
    4.28 +fun relevant_facts ctxt (threshold0, threshold1) max_relevant is_built_in_const
    4.29 +                   fudge (override as {only, ...}) chained_ths hyp_ts concl_t
    4.30 +                   facts =
    4.31    let
    4.32      val thy = Proof_Context.theory_of ctxt
    4.33      val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
    4.34 @@ -954,9 +954,9 @@
    4.35               max_relevant = 0 then
    4.36         []
    4.37       else
    4.38 -       relevance_filter ctxt ho_atp threshold0 decay max_relevant
    4.39 -           is_built_in_const fudge override facts (chained_ths |> map prop_of)
    4.40 -           hyp_ts (concl_t |> theory_constify fudge (Context.theory_name thy)))
    4.41 +       relevance_filter ctxt threshold0 decay max_relevant is_built_in_const
    4.42 +           fudge override facts (chained_ths |> map prop_of) hyp_ts
    4.43 +           (concl_t |> theory_constify fudge (Context.theory_name thy)))
    4.44      |> map (apfst (apfst (fn f => f ())))
    4.45    end
    4.46  
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Aug 31 11:23:16 2011 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Aug 31 11:52:03 2011 +0200
     5.3 @@ -269,9 +269,10 @@
     5.4        val {facts = chained_ths, goal, ...} = Proof.goal state
     5.5        val chained_ths = chained_ths |> normalize_chained_theorems
     5.6        val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i
     5.7 -      val is_ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
     5.8 -      val facts = nearly_all_facts ctxt is_ho_atp relevance_override
     5.9 -                                   chained_ths hyp_ts concl_t
    5.10 +      val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
    5.11 +      val facts =
    5.12 +        nearly_all_facts ctxt ho_atp relevance_override chained_ths hyp_ts
    5.13 +                         concl_t
    5.14        val _ = () |> not blocking ? kill_provers
    5.15        val _ = case find_first (not o is_prover_supported ctxt) provers of
    5.16                  SOME name => error ("No such prover: " ^ name ^ ".")
    5.17 @@ -323,9 +324,9 @@
    5.18            |> (case is_appropriate_prop of
    5.19                  SOME is_app => filter (is_app o prop_of o snd)
    5.20                | NONE => I)
    5.21 -          |> relevant_facts ctxt is_ho_atp relevance_thresholds
    5.22 -                            max_max_relevant is_built_in_const relevance_fudge
    5.23 -                            relevance_override chained_ths hyp_ts concl_t
    5.24 +          |> relevant_facts ctxt relevance_thresholds max_max_relevant
    5.25 +                            is_built_in_const relevance_fudge relevance_override
    5.26 +                            chained_ths hyp_ts concl_t
    5.27            |> tap (fn facts =>
    5.28                       if debug then
    5.29                         label ^ plural_s (length provers) ^ ": " ^
     6.1 --- a/src/HOL/ex/sledgehammer_tactics.ML	Wed Aug 31 11:23:16 2011 +0200
     6.2 +++ b/src/HOL/ex/sledgehammer_tactics.ML	Wed Aug 31 11:52:03 2011 +0200
     6.3 @@ -37,13 +37,11 @@
     6.4      val relevance_fudge =
     6.5        Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
     6.6      val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
     6.7 -    val is_ho_atp =
     6.8 -      exists (Sledgehammer_Provers.is_ho_atp ctxt)
     6.9 -        provers(*FIXME: duplicated from sledgehammer_run.ML*)
    6.10 +    val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
    6.11      val facts =
    6.12 -      Sledgehammer_Filter.nearly_all_facts ctxt is_ho_atp relevance_override
    6.13 +      Sledgehammer_Filter.nearly_all_facts ctxt ho_atp relevance_override
    6.14                                             chained_ths hyp_ts concl_t
    6.15 -      |> Sledgehammer_Filter.relevant_facts ctxt is_ho_atp relevance_thresholds
    6.16 +      |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
    6.17               (the_default default_max_relevant max_relevant) is_built_in_const
    6.18               relevance_fudge relevance_override chained_ths hyp_ts concl_t
    6.19      val problem =