1.1 --- a/src/HOL/TPTP/mash_eval.ML	Wed Jul 18 08:44:04 2012 +0200
     1.2 +++ b/src/HOL/TPTP/mash_eval.ML	Wed Jul 18 08:44:04 2012 +0200
     1.3 @@ -81,8 +81,8 @@
     1.4          val iter_facts =
     1.5            Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
     1.6                prover slack_max_facts NONE hyp_ts concl_t facts
     1.7 -        val mash_facts = suggested_facts suggs facts
     1.8 -        val mess = [(iter_facts, SOME (length iter_facts)), (mash_facts, NONE)]
     1.9 +        val mash_facts = facts |> suggested_facts suggs
    1.10 +        val mess = [(iter_facts, []), (mash_facts, [])]
    1.11          val mesh_facts = mesh_facts slack_max_facts mess
    1.12          fun prove ok heading facts =
    1.13            let

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:04 2012 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:04 2012 +0200
     2.3 @@ -26,7 +26,7 @@
     2.4    val unescape_metas : string -> string list
     2.5    val extract_query : string -> string * string list
     2.6    val suggested_facts : string list -> fact list -> fact list
     2.7 -  val mesh_facts : int -> (fact list * int option) list -> fact list
     2.8 +  val mesh_facts : int -> (fact list * fact list) list -> fact list
     2.9    val is_likely_tautology : Proof.context -> string -> thm -> bool
    2.10    val is_too_meta : thm -> bool
    2.11    val theory_ord : theory * theory -> order
    2.12 @@ -51,7 +51,7 @@
    2.13    val mash_can_suggest_facts : unit -> bool
    2.14    val mash_suggest_facts :
    2.15      Proof.context -> params -> string -> int -> term list -> term -> fact list
    2.16 -    -> fact list
    2.17 +    -> fact list * fact list
    2.18    val mash_learn_thy :
    2.19      Proof.context -> params -> theory -> Time.time -> fact list -> string
    2.20    val mash_learn_proof :
    2.21 @@ -125,20 +125,24 @@
    2.22    find_first (fn (_, th) => Thm.get_name_hint th = sugg) facts
    2.23  fun suggested_facts suggs facts = map_filter (find_suggested facts) suggs
    2.24  
    2.25 -fun sum_avg n xs =
    2.26 -  fold (Integer.add o Integer.mult n) xs 0 div (length xs)
    2.27 +fun sum_avg _ [] = 1000000000 (* big number *)
    2.28 +  | sum_avg n xs = fold (Integer.add o Integer.mult n) xs 0 div (length xs)
    2.29  
    2.30 -fun mesh_facts max_facts [(facts, _)] = facts |> take max_facts
    2.31 +fun mesh_facts max_facts [(selected, unknown)] =
    2.32 +    take max_facts selected @ take (max_facts - length selected) unknown
    2.33    | mesh_facts max_facts mess =
    2.34      let
    2.35 +      val mess = mess |> map (apfst (`length))
    2.36        val n = length mess
    2.37        val fact_eq = Thm.eq_thm o pairself snd
    2.38 -      fun score_in fact (facts, def) =
    2.39 -        case find_index (curry fact_eq fact) facts of
    2.40 -          ~1 => def
    2.41 +      fun score_in fact ((sel_len, sels), unks) =
    2.42 +        case find_index (curry fact_eq fact) sels of
    2.43 +          ~1 => (case find_index (curry fact_eq fact) unks of
    2.44 +                   ~1 => SOME sel_len
    2.45 +                 | _ => NONE)
    2.46          | j => SOME j
    2.47        fun score_of fact = mess |> map_filter (score_in fact) |> sum_avg n
    2.48 -      val facts = fold (union fact_eq o take max_facts o fst) mess []
    2.49 +      val facts = fold (union fact_eq o take max_facts o snd o fst) mess []
    2.50      in
    2.51        facts |> map (`score_of) |> sort (int_ord o pairself fst) |> map snd
    2.52              |> take max_facts
    2.53 @@ -482,6 +486,9 @@
    2.54     slack. *)
    2.55  fun max_suggs_of max_facts = max_facts + Int.min (200, max_facts)
    2.56  
    2.57 +fun is_fact_in_graph fact_graph (_, th) =
    2.58 +  can (Graph.get_node fact_graph) (Thm.get_name_hint th)
    2.59 +
    2.60  fun mash_suggest_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
    2.61                         concl_t facts =
    2.62    let
    2.63 @@ -490,8 +497,11 @@
    2.64      val parents = parents_wrt_facts facts fact_graph
    2.65      val feats = features_of ctxt prover thy General (concl_t :: hyp_ts)
    2.66      val suggs =
    2.67 -      mash_QUERY ctxt overlord (max_suggs_of max_facts) (parents, feats)
    2.68 -  in suggested_facts suggs facts end
    2.69 +      if Graph.is_empty fact_graph then []
    2.70 +      else mash_QUERY ctxt overlord (max_suggs_of max_facts) (parents, feats)
    2.71 +    val selected = facts |> suggested_facts suggs
    2.72 +    val unknown = facts |> filter_out (is_fact_in_graph fact_graph)
    2.73 +  in (selected, unknown) end
    2.74  
    2.75  fun add_thys_for thy =
    2.76    let fun add comp thy = Symtab.update (Context.theory_name thy, comp) in
    2.77 @@ -523,8 +533,9 @@
    2.78      fun timed_out frac =
    2.79        Time.> (Timer.checkRealTimer timer, time_mult frac timeout)
    2.80      val {fact_graph, ...} = mash_get ()
    2.81 -    fun is_old (_, th) = can (Graph.get_node fact_graph) (Thm.get_name_hint th)
    2.82 -    val new_facts = facts |> filter_out is_old |> sort (thm_ord o pairself snd)
    2.83 +    val new_facts =
    2.84 +      facts |> filter_out (is_fact_in_graph fact_graph)
    2.85 +            |> sort (thm_ord o pairself snd)
    2.86    in
    2.87      if null new_facts then
    2.88        ""
    2.89 @@ -645,12 +656,10 @@
    2.90        fun iter () =
    2.91          iterative_relevant_facts ctxt params prover max_facts NONE hyp_ts
    2.92                                   concl_t facts
    2.93 -        |> (fn facts => (facts, SOME (length facts)))
    2.94        fun mash () =
    2.95 -        (mash_suggest_facts ctxt params prover max_facts hyp_ts concl_t facts,
    2.96 -         NONE)
    2.97 +        mash_suggest_facts ctxt params prover max_facts hyp_ts concl_t facts
    2.98        val mess =
    2.99 -        [] |> (if fact_filter <> mashN then cons (iter ()) else I)
   2.100 +        [] |> (if fact_filter <> mashN then cons (iter (), []) else I)
   2.101             |> (if fact_filter <> iterN then cons (mash ()) else I)
   2.102      in
   2.103        mesh_facts max_facts mess