src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
changeset 50383 4274b25ff4e7
parent 50382 cb564ff43c28
child 50389 ad0ac9112d2c
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Dec 05 13:25:06 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Dec 05 13:25:06 2012 +0100
     1.3 @@ -44,7 +44,8 @@
     1.4    val suggested_facts :
     1.5      (string * 'a) list -> ('b * thm) list -> (('b * thm) * 'a) list
     1.6    val mesh_facts :
     1.7 -    int -> ((('a * thm) * real) list * ('a * thm) list) list -> ('a * thm) list
     1.8 +    int -> (real * ((('a * thm) * real) list * ('a * thm) list)) list
     1.9 +    -> ('a * thm) list
    1.10    val theory_ord : theory * theory -> order
    1.11    val thm_ord : thm * thm -> order
    1.12    val goal_of_thm : theory -> thm -> thm
    1.13 @@ -59,8 +60,8 @@
    1.14      -> thm -> bool * string list option
    1.15    val weight_mash_facts : ('a * thm) list -> (('a * thm) * real) list
    1.16    val mash_suggested_facts :
    1.17 -    Proof.context -> params -> string -> int -> term list -> term
    1.18 -    -> fact list -> fact list * fact list
    1.19 +    Proof.context -> params -> string -> int -> term list -> term -> fact list
    1.20 +    -> fact list
    1.21    val mash_learn_proof :
    1.22      Proof.context -> params -> string -> term -> ('a * thm) list -> thm list
    1.23      -> unit
    1.24 @@ -298,7 +299,7 @@
    1.25  
    1.26  local
    1.27  
    1.28 -val version = "*** MaSh version 20121204a ***"
    1.29 +val version = "*** MaSh version 20121205a ***"
    1.30  
    1.31  exception Too_New of unit
    1.32  
    1.33 @@ -425,30 +426,43 @@
    1.34        Symtab.lookup tab name |> Option.map (rpair weight)
    1.35    in map_filter find_sugg suggs end
    1.36  
    1.37 -fun sum_avg [] = 0
    1.38 -  | sum_avg xs =
    1.39 +fun scaled_avg [] = 0
    1.40 +  | scaled_avg xs =
    1.41      Real.ceil (100000000.0 * fold (curry (op +)) xs 0.0) div length xs
    1.42  
    1.43 -fun normalize_scores [] = []
    1.44 -  | normalize_scores ((fact, score) :: tail) =
    1.45 -    (fact, 1.0) :: map (apsnd (curry Real.* (1.0 / score))) tail
    1.46 +fun avg [] = 0.0
    1.47 +  | avg xs = fold (curry (op +)) xs 0.0 / Real.fromInt (length xs)
    1.48  
    1.49 -fun mesh_facts max_facts [(sels, unks)] =
    1.50 +fun normalize_scores _ [] = []
    1.51 +  | normalize_scores max_facts xs =
    1.52 +    let val avg = avg (map snd (take max_facts xs)) in
    1.53 +      map (apsnd (curry Real.* (1.0 / avg))) xs
    1.54 +    end
    1.55 +
    1.56 +fun mesh_facts max_facts [(_, (sels, unks))] =
    1.57      map fst (take max_facts sels) @ take (max_facts - length sels) unks
    1.58    | mesh_facts max_facts mess =
    1.59      let
    1.60 -      val mess = mess |> map (apfst (normalize_scores #> `length))
    1.61 +      val mess =
    1.62 +        mess |> map (apsnd (apfst (normalize_scores max_facts #> `length)))
    1.63        val fact_eq = Thm.eq_thm o pairself snd
    1.64 -      fun score_at sels = try (nth sels) #> Option.map snd
    1.65 -      fun score_in fact ((sel_len, sels), unks) =
    1.66 -        case find_index (curry fact_eq fact o fst) sels of
    1.67 -          ~1 => (case find_index (curry fact_eq fact) unks of
    1.68 -                   ~1 => score_at sels sel_len
    1.69 -                 | _ => NONE)
    1.70 -        | rank => score_at sels rank
    1.71 -      fun weight_of fact = mess |> map_filter (score_in fact) |> sum_avg
    1.72 +      fun score_in fact (global_weight, ((sel_len, sels), unks)) =
    1.73 +        let
    1.74 +          fun score_at j =
    1.75 +            case try (nth sels) j of
    1.76 +              SOME (_, score) => SOME (global_weight * score)
    1.77 +            | NONE => NONE
    1.78 +        in
    1.79 +          case find_index (curry fact_eq fact o fst) sels of
    1.80 +            ~1 => (case find_index (curry fact_eq fact) unks of
    1.81 +                     ~1 => score_at sel_len
    1.82 +                   | _ => NONE)
    1.83 +          | rank => score_at rank
    1.84 +        end
    1.85 +      fun weight_of fact = mess |> map_filter (score_in fact) |> scaled_avg
    1.86        val facts =
    1.87 -        fold (union fact_eq o map fst o take max_facts o snd o fst) mess []
    1.88 +        fold (union fact_eq o map fst o take max_facts o snd o fst o snd) mess
    1.89 +             []
    1.90      in
    1.91        facts |> map (`weight_of) |> sort (int_ord o swap o pairself fst)
    1.92              |> map snd |> take max_facts
    1.93 @@ -459,7 +473,7 @@
    1.94  fun type_feature_of s = ("t" ^ s, 1.0 (* FUDGE *))
    1.95  fun class_feature_of s = ("s" ^ s, 1.0 (* FUDGE *))
    1.96  fun status_feature_of status = (string_of_status status, 1.0 (* FUDGE *))
    1.97 -val local_feature = ("local", 20.0 (* FUDGE *))
    1.98 +val local_feature = ("local", 1.0 (* FUDGE *))
    1.99  val lams_feature = ("lams", 1.0 (* FUDGE *))
   1.100  val skos_feature = ("skos", 1.0 (* FUDGE *))
   1.101  
   1.102 @@ -531,7 +545,7 @@
   1.103          let
   1.104            val ps = patternify_term (u :: args) depth t
   1.105            val qs = "" :: patternify_term [] (depth - 1) u
   1.106 -        in map_product (fn p => fn "" => p | q => "(" ^ q ^ ")") ps qs end
   1.107 +        in map_product (fn p => fn "" => p | q => p ^ "(" ^ q ^ ")") ps qs end
   1.108        | patternify_term _ _ _ = []
   1.109      val add_term_pattern =
   1.110        union (op = o pairself fst) o map term_feature_of oo patternify_term []
   1.111 @@ -692,24 +706,22 @@
   1.112                                        (Graph.imm_preds fact_G new) news))
   1.113    in find_maxes Symtab.empty ([], Graph.maximals fact_G) end
   1.114  
   1.115 -(* Generate more suggestions than requested, because some might be thrown out
   1.116 -   later for various reasons and "meshing" gives better results with some
   1.117 -   slack. *)
   1.118 -fun max_suggs_of max_facts = max_facts + Int.min (50, max_facts)
   1.119 -
   1.120  fun is_fact_in_graph fact_G (_, th) =
   1.121    can (Graph.get_node fact_G) (nickname_of th)
   1.122  
   1.123 -fun interleave 0 _ _ = []
   1.124 -  | interleave n [] ys = take n ys
   1.125 -  | interleave n xs [] = take n xs
   1.126 -  | interleave 1 (x :: _) _ = [x]
   1.127 -  | interleave n (x :: xs) (y :: ys) = x :: y :: interleave (n - 2) xs ys
   1.128 -
   1.129  (* factor that controls whether unknown global facts should be included *)
   1.130  val include_unk_global_factor = 15
   1.131  
   1.132 -val weight_mash_facts = weight_mepo_facts (* use MePo weights for now *)
   1.133 +(* use MePo weights for now *)
   1.134 +val weight_raw_mash_facts = weight_mepo_facts
   1.135 +val weight_mash_facts = weight_raw_mash_facts
   1.136 +
   1.137 +(* FUDGE *)
   1.138 +fun weight_of_proximity_fact rank =
   1.139 +  Math.pow (1.3, 15.5 - 0.05 * Real.fromInt rank) + 15.0
   1.140 +
   1.141 +fun weight_proximity_facts facts =
   1.142 +  facts ~~ map weight_of_proximity_fact (0 upto length facts - 1)
   1.143  
   1.144  fun mash_suggested_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
   1.145                           concl_t facts =
   1.146 @@ -725,27 +737,23 @@
   1.147                val feats =
   1.148                  features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts)
   1.149              in
   1.150 -              (fact_G, mash_QUERY ctxt overlord (max_suggs_of max_facts)
   1.151 -                                  (parents, feats))
   1.152 +              (fact_G, mash_QUERY ctxt overlord max_facts (parents, feats))
   1.153              end)
   1.154      val (chained, unchained) =
   1.155        List.partition (fn ((_, (scope, _)), _) => scope = Chained) facts
   1.156 -    val sels =
   1.157 +    val raw_mash =
   1.158        facts |> suggested_facts suggs
   1.159              (* The weights currently returned by "mash.py" are too spaced out to
   1.160                 make any sense. *)
   1.161              |> map fst
   1.162 -            |> filter_out (member (Thm.eq_thm_prop o pairself snd) chained)
   1.163 -    val (unk_global, unk_local) =
   1.164 -      unchained |> filter_out (is_fact_in_graph fact_G)
   1.165 -                |> List.partition (fn ((_, (scope, _)), _) => scope = Global)
   1.166 -    val (small_unk_global, big_unk_global) =
   1.167 -      ([], unk_global)
   1.168 -      |> include_unk_global_factor * length unk_global <= max_facts ? swap
   1.169 -  in
   1.170 -    (interleave max_facts (chained @ unk_local @ small_unk_global) sels,
   1.171 -     big_unk_global)
   1.172 -  end
   1.173 +    val proximity =
   1.174 +      chained @ (facts |> subtract (Thm.eq_thm_prop o pairself snd) chained
   1.175 +                       |> sort (thm_ord o pairself snd o swap))
   1.176 +    val unknown = facts |> filter_out (is_fact_in_graph fact_G)
   1.177 +    val mess =
   1.178 +      [(0.667 (* FUDGE *), (weight_raw_mash_facts raw_mash, unknown)),
   1.179 +       (0.333 (* FUDGE *), (weight_proximity_facts proximity, []))]
   1.180 +  in mesh_facts max_facts mess end
   1.181  
   1.182  fun add_wrt_fact_graph ctxt (name, parents, feats, deps) (adds, graph) =
   1.183    let
   1.184 @@ -995,6 +1003,10 @@
   1.185  fun is_mash_enabled () = (getenv "MASH" = "yes")
   1.186  fun mash_can_suggest_facts ctxt = not (Graph.is_empty (#fact_G (mash_get ctxt)))
   1.187  
   1.188 +(* Generate more suggestions than requested, because some might be thrown out
   1.189 +   later for various reasons. *)
   1.190 +fun generous_max_facts max_facts = max_facts + Int.min (50, max_facts)
   1.191 +
   1.192  (* The threshold should be large enough so that MaSh doesn't kick in for Auto
   1.193     Sledgehammer and Try. *)
   1.194  val min_secs_for_learning = 15
   1.195 @@ -1040,11 +1052,12 @@
   1.196                               facts
   1.197          |> weight_mepo_facts
   1.198        fun mash () =
   1.199 -        mash_suggested_facts ctxt params prover max_facts hyp_ts concl_t facts
   1.200 -        |>> weight_mash_facts
   1.201 +        mash_suggested_facts ctxt params prover (generous_max_facts max_facts)
   1.202 +            hyp_ts concl_t facts
   1.203 +        |> weight_mash_facts
   1.204        val mess =
   1.205 -        [] |> (if fact_filter <> mashN then cons (mepo (), []) else I)
   1.206 -           |> (if fact_filter <> mepoN then cons (mash ()) else I)
   1.207 +        [] |> (if fact_filter <> mashN then cons (0.5, (mepo (), [])) else I)
   1.208 +           |> (if fact_filter <> mepoN then cons (0.5, (mash (), [])) else I)
   1.209      in
   1.210        mesh_facts max_facts mess
   1.211        |> not (null add_ths) ? prepend_facts add_ths