1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jun 27 12:06:22 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jun 27 14:20:50 2014 +0200
     1.3 @@ -55,7 +55,7 @@
     1.4    val run_prover_for_mash : Proof.context -> params -> string -> string -> fact list -> thm ->
     1.5      prover_result
     1.6    val features_of : Proof.context -> theory -> int -> int Symtab.table -> stature -> term list ->
     1.7 -    (string * real) list
     1.8 +    string list
     1.9    val trim_dependencies : string list -> string list option
    1.10    val isar_dependencies_of : string Symtab.table * string Symtab.table -> thm -> string list option
    1.11    val prover_dependencies_of : Proof.context -> params -> string -> int -> raw_fact list ->
    1.12 @@ -896,12 +896,11 @@
    1.13        |> map snd |> take max_facts
    1.14      end
    1.15  
    1.16 -val default_weight = 1.0
    1.17 -fun free_feature_of s = ("f" ^ s, 40.0 (* FUDGE *))
    1.18 -fun thy_feature_of s = ("y" ^ s, 8.0 (* FUDGE *))
    1.19 -fun type_feature_of s = ("t" ^ s, 4.0 (* FUDGE *))
    1.20 -fun class_feature_of s = ("s" ^ s, 1.0 (* FUDGE *))
    1.21 -val local_feature = ("local", 16.0 (* FUDGE *))
    1.22 +fun free_feature_of s = "f" ^ s
    1.23 +fun thy_feature_of s = "y" ^ s
    1.24 +fun type_feature_of s = "t" ^ s
    1.25 +fun class_feature_of s = "s" ^ s
    1.26 +val local_feature = "local"
    1.27  
    1.28  fun crude_theory_ord p =
    1.29    if Theory.subthy p then
    1.30 @@ -982,7 +981,7 @@
    1.31            #> swap #> op ::
    1.32            #> subtract (op =) @{sort type} #> map massage_long_name
    1.33            #> map class_feature_of
    1.34 -          #> union (eq_fst (op =))) S
    1.35 +          #> union (op =)) S
    1.36  
    1.37      fun pattify_type 0 _ = []
    1.38        | pattify_type _ (Type (s, [])) =
    1.39 @@ -1001,11 +1000,10 @@
    1.40          maybe_singleton_str pat_tvar_prefix (crude_str_of_sort S)
    1.41  
    1.42      fun add_type_pat depth T =
    1.43 -      union (eq_fst (op =)) (map type_feature_of (pattify_type depth T))
    1.44 +      union (op =) (map type_feature_of (pattify_type depth T))
    1.45  
    1.46      fun add_type_pats 0 _ = I
    1.47 -      | add_type_pats depth t =
    1.48 -        add_type_pat depth t #> add_type_pats (depth - 1) t
    1.49 +      | add_type_pats depth t = add_type_pat depth t #> add_type_pats (depth - 1) t
    1.50  
    1.51      fun add_type T =
    1.52        add_type_pats type_max_depth T
    1.53 @@ -1014,44 +1012,28 @@
    1.54      fun add_subtypes (T as Type (_, Ts)) = add_type T #> fold add_subtypes Ts
    1.55        | add_subtypes T = add_type T
    1.56  
    1.57 -    val base_weight_of_const = 16.0 (* FUDGE *)
    1.58 -    val weight_of_const =
    1.59 -      (if num_facts = 0 orelse Symtab.is_empty const_tab then
    1.60 -         K base_weight_of_const
    1.61 -       else
    1.62 -         fn s =>
    1.63 -         let val count = Symtab.lookup const_tab s |> the_default 1 in
    1.64 -           base_weight_of_const + Real.fromInt num_facts / Real.fromInt count
    1.65 -         end)
    1.66 -
    1.67      fun pattify_term _ 0 _ = []
    1.68        | pattify_term _ _ (Const (s, _)) =
    1.69 -        if is_widely_irrelevant_const s then [] else [(massage_long_name s, weight_of_const s)]
    1.70 +        if is_widely_irrelevant_const s then [] else [massage_long_name s]
    1.71        | pattify_term _ _ (Free (s, T)) =
    1.72          maybe_singleton_str pat_var_prefix (crude_str_of_typ T)
    1.73 -        |> map (rpair 1.0)
    1.74          |> (if member (op =) fixes s then
    1.75 -              cons (free_feature_of (massage_long_name
    1.76 -                  (thy_name ^ Long_Name.separator ^ s)))
    1.77 +              cons (free_feature_of (massage_long_name (thy_name ^ Long_Name.separator ^ s)))
    1.78              else
    1.79                I)
    1.80 -      | pattify_term _ _ (Var (_, T)) =
    1.81 -        maybe_singleton_str pat_var_prefix (crude_str_of_typ T) |> map (rpair default_weight)
    1.82 +      | pattify_term _ _ (Var (_, T)) = maybe_singleton_str pat_var_prefix (crude_str_of_typ T)
    1.83        | pattify_term Ts _ (Bound j) =
    1.84          maybe_singleton_str pat_var_prefix (crude_str_of_typ (nth Ts j))
    1.85 -        |> map (rpair default_weight)
    1.86        | pattify_term Ts depth (t $ u) =
    1.87          let
    1.88            val ps = take max_pat_breadth (pattify_term Ts depth t)
    1.89 -          val qs = take max_pat_breadth (("", default_weight) :: pattify_term Ts (depth - 1) u)
    1.90 +          val qs = take max_pat_breadth ("" :: pattify_term Ts (depth - 1) u)
    1.91          in
    1.92 -          map_product (fn ppw as (p, pw) =>
    1.93 -            fn ("", _) => ppw
    1.94 -             | (q, qw) => (p ^ "(" ^ q ^ ")", pw + qw)) ps qs
    1.95 +          map_product (fn p => fn "" => p | q => p ^ "(" ^ q ^ ")") ps qs
    1.96          end
    1.97        | pattify_term _ _ _ = []
    1.98  
    1.99 -    fun add_term_pat Ts = union (eq_fst (op =)) oo pattify_term Ts
   1.100 +    fun add_term_pat Ts = union (op =) oo pattify_term Ts
   1.101  
   1.102      fun add_term_pats _ 0 _ = I
   1.103        | add_term_pats Ts depth t = add_term_pat Ts depth t #> add_term_pats Ts (depth - 1) t
   1.104 @@ -1062,8 +1044,7 @@
   1.105        (case strip_comb t of
   1.106          (Const (s, T), args) =>
   1.107          (not (is_widely_irrelevant_const s) ? add_term Ts t)
   1.108 -        #> add_subtypes T
   1.109 -        #> fold (add_subterms Ts) args
   1.110 +        #> add_subtypes T #> fold (add_subterms Ts) args
   1.111        | (head, args) =>
   1.112          (case head of
   1.113             Free (_, T) => add_term Ts t #> add_subtypes T
   1.114 @@ -1333,7 +1314,7 @@
   1.115      fun chained_or_extra_features_of factor (((_, stature), th), weight) =
   1.116        [prop_of th]
   1.117        |> features_of ctxt (theory_of_thm th) num_facts const_tab stature
   1.118 -      |> map (apsnd (fn r => weight * factor * r))
   1.119 +      |> map (rpair (weight * factor))
   1.120  
   1.121      fun query_args access_G =
   1.122        let
   1.123 @@ -1352,7 +1333,8 @@
   1.124            |> weight_facts_steeply
   1.125            |> map (chained_or_extra_features_of extra_feature_factor)
   1.126            |> rpair [] |-> fold (union (eq_fst (op =)))
   1.127 -        val feats = fold (union (eq_fst (op =))) [chained_feats, extra_feats] goal_feats
   1.128 +        val feats =
   1.129 +          fold (union (eq_fst (op =))) [chained_feats, extra_feats] (map (rpair 1.0) goal_feats)
   1.130            |> debug ? sort (Real.compare o swap o pairself snd)
   1.131        in
   1.132          (parents, feats)
   1.133 @@ -1453,7 +1435,7 @@
   1.134      launch_thread timeout (fn () =>
   1.135        let
   1.136          val thy = Proof_Context.theory_of ctxt
   1.137 -        val feats = map fst (features_of ctxt thy 0 Symtab.empty (Local, General) [t])
   1.138 +        val feats = features_of ctxt thy 0 Symtab.empty (Local, General) [t]
   1.139        in
   1.140          map_state ctxt overlord
   1.141            (fn state as {access_G, xtabs as ((num_facts0, _), _), ffds, freqs, dirty_facts} =>
   1.142 @@ -1572,8 +1554,7 @@
   1.143                (learns, (num_nontrivial, next_commit, _)) =
   1.144              let
   1.145                val name = nickname_of_thm th
   1.146 -              val feats =
   1.147 -                map fst (features_of ctxt (theory_of_thm th) 0 Symtab.empty stature [prop_of th])
   1.148 +              val feats = features_of ctxt (theory_of_thm th) 0 Symtab.empty stature [prop_of th]
   1.149                val deps = deps_of status th |> these
   1.150                val num_nontrivial = num_nontrivial |> not (null deps) ? Integer.add 1
   1.151                val learns = (name, parents, feats, deps) :: learns