honor suggested MaSh weights
authorblanchet
Fri Jul 20 22:19:46 2012 +0200 (2012-07-20 ago)
changeset 48406b002cc16aa99
parent 48405 7682bc885e8a
child 48407 47fe0ca12fc2
honor suggested MaSh weights
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
src/HOL/TPTP/atp_theory_export.ML
src/HOL/TPTP/mash_eval.ML
src/HOL/TPTP/mash_export.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Fri Jul 20 22:19:46 2012 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Fri Jul 20 22:19:46 2012 +0200
     1.3 @@ -133,7 +133,7 @@
     1.4                 Sledgehammer_Fact.no_fact_override reserved css_table chained_ths
     1.5                 hyp_ts concl_t
     1.6             |> filter (is_appropriate_prop o prop_of o snd)
     1.7 -           |> Sledgehammer_MePo.iterative_relevant_facts ctxt params
     1.8 +           |> Sledgehammer_MePo.mepo_suggested_facts ctxt params
     1.9                    default_prover (the_default default_max_facts max_facts)
    1.10                    (SOME relevance_fudge) hyp_ts concl_t
    1.11              |> map ((fn name => name ()) o fst o fst)
     2.1 --- a/src/HOL/TPTP/atp_theory_export.ML	Fri Jul 20 22:19:46 2012 +0200
     2.2 +++ b/src/HOL/TPTP/atp_theory_export.ML	Fri Jul 20 22:19:46 2012 +0200
     2.3 @@ -115,7 +115,7 @@
     2.4  
     2.5  fun all_non_tautological_facts_of thy css_table =
     2.6    Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table
     2.7 -  |> filter_out (Sledgehammer_MaSh.is_likely_tautology_or_too_meta o snd)
     2.8 +  |> filter_out (Sledgehammer_Fact.is_likely_tautology_or_too_meta o snd)
     2.9  
    2.10  fun generate_atp_inference_file_for_theory ctxt thy format type_enc file_name =
    2.11    let
     3.1 --- a/src/HOL/TPTP/mash_eval.ML	Fri Jul 20 22:19:46 2012 +0200
     3.2 +++ b/src/HOL/TPTP/mash_eval.ML	Fri Jul 20 22:19:46 2012 +0200
     3.3 @@ -78,26 +78,28 @@
     3.4          val isar_deps = isar_dependencies_of all_names th |> these
     3.5          val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
     3.6          val mepo_facts =
     3.7 -          Sledgehammer_MePo.iterative_relevant_facts ctxt params prover
     3.8 +          Sledgehammer_MePo.mepo_suggested_facts ctxt params prover
     3.9                slack_max_facts NONE hyp_ts concl_t facts
    3.10 -        val mash_facts = facts |> suggested_facts suggs
    3.11 +          |> Sledgehammer_MePo.weight_mepo_facts
    3.12 +        val mash_facts = suggested_facts suggs facts
    3.13          val mess = [(mepo_facts, []), (mash_facts, [])]
    3.14          val mesh_facts = mesh_facts slack_max_facts mess
    3.15 -        val isar_facts = suggested_facts isar_deps facts
    3.16 -        fun prove ok heading facts =
    3.17 +        val isar_facts = suggested_facts (map (rpair 1.0) isar_deps) facts
    3.18 +        fun prove ok heading get facts =
    3.19            let
    3.20              val facts =
    3.21 -              facts
    3.22 -              |> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t
    3.23 -              |> take (the max_facts)
    3.24 +              facts |> map get
    3.25 +                    |> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts
    3.26 +                                                                   concl_t
    3.27 +                    |> take (the max_facts)
    3.28              val res as {outcome, ...} =
    3.29                run_prover_for_mash ctxt params prover facts goal
    3.30              val _ = if is_none outcome then ok := !ok + 1 else ()
    3.31            in str_of_res heading facts res end
    3.32 -        val mepo_s = prove mepo_ok MePoN mepo_facts
    3.33 -        val mash_s = prove mash_ok MaShN mash_facts
    3.34 -        val mesh_s = prove mesh_ok MeshN mesh_facts
    3.35 -        val isar_s = prove isar_ok IsarN isar_facts
    3.36 +        val mepo_s = prove mepo_ok MePoN fst mepo_facts
    3.37 +        val mash_s = prove mash_ok MaShN fst mash_facts
    3.38 +        val mesh_s = prove mesh_ok MeshN I mesh_facts
    3.39 +        val isar_s = prove isar_ok IsarN fst isar_facts
    3.40        in
    3.41          ["Goal " ^ string_of_int j ^ ": " ^ name, mepo_s, mash_s, mesh_s,
    3.42           isar_s]
     4.1 --- a/src/HOL/TPTP/mash_export.ML	Fri Jul 20 22:19:46 2012 +0200
     4.2 +++ b/src/HOL/TPTP/mash_export.ML	Fri Jul 20 22:19:46 2012 +0200
     4.3 @@ -179,7 +179,7 @@
     4.4              let
     4.5                val suggs =
     4.6                  old_facts
     4.7 -                |> Sledgehammer_MePo.iterative_relevant_facts ctxt params prover
     4.8 +                |> Sledgehammer_MePo.mepo_suggested_facts ctxt params prover
     4.9                         max_relevant NONE hyp_ts concl_t
    4.10                  |> map (fn ((name, _), _) => name ())
    4.11                val s = escape_meta name ^ ": " ^ escape_metas suggs ^ "\n"
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Jul 20 22:19:46 2012 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Jul 20 22:19:46 2012 +0200
     5.3 @@ -23,6 +23,7 @@
     5.4    val fact_from_ref :
     5.5      Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
     5.6      -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
     5.7 +  val is_likely_tautology_or_too_meta : thm -> bool
     5.8    val backquote_thm : thm -> string
     5.9    val clasimpset_rule_table_of : Proof.context -> status Termtab.table
    5.10    val maybe_instantiate_inducts :
    5.11 @@ -210,6 +211,24 @@
    5.12      is_that_fact thm
    5.13    end
    5.14  
    5.15 +fun is_likely_tautology_or_too_meta th =
    5.16 +  let
    5.17 +    val is_boring_const = member (op =) atp_widely_irrelevant_consts
    5.18 +    fun is_boring_bool t =
    5.19 +      not (exists_Const (not o is_boring_const o fst) t) orelse
    5.20 +      exists_type (exists_subtype (curry (op =) @{typ prop})) t
    5.21 +    fun is_boring_prop (@{const Trueprop} $ t) = is_boring_bool t
    5.22 +      | is_boring_prop (@{const "==>"} $ t $ u) =
    5.23 +        is_boring_prop t andalso is_boring_prop u
    5.24 +      | is_boring_prop (Const (@{const_name all}, _) $ (Abs (_, _, t)) $ u) =
    5.25 +        is_boring_prop t andalso is_boring_prop u
    5.26 +      | is_boring_prop (Const (@{const_name "=="}, _) $ t $ u) =
    5.27 +        is_boring_bool t andalso is_boring_bool u
    5.28 +      | is_boring_prop _ = true
    5.29 +  in
    5.30 +    is_boring_prop (prop_of th) andalso not (Thm.eq_thm_prop (@{thm ext}, th))
    5.31 +  end
    5.32 +
    5.33  fun hackish_string_for_term thy t =
    5.34    Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
    5.35                     (print_mode_value ())) (Syntax.string_of_term_global thy) t
    5.36 @@ -439,6 +458,7 @@
    5.37         else
    5.38           let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in
    5.39             all_facts ctxt ho_atp reserved add chained css
    5.40 +           |> filter_out (is_likely_tautology_or_too_meta o snd)
    5.41             |> filter_out (member Thm.eq_thm_prop del o snd)
    5.42             |> maybe_filter_no_atps ctxt
    5.43             |> uniquify
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:46 2012 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:46 2012 +0200
     6.3 @@ -218,7 +218,7 @@
     6.4        val max_local_and_remote =
     6.5          max_local_and_remote
     6.6          |> (if String.isPrefix remote_prefix prover then apsnd else apfst)
     6.7 -              (Integer.add ~1)
     6.8 +               (Integer.add ~1)
     6.9      in prover :: avoid_too_many_threads ctxt max_local_and_remote provers end
    6.10  
    6.11  val max_default_remote_threads = 4
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
     7.3 @@ -28,12 +28,12 @@
     7.4    val escape_metas : string list -> string
     7.5    val unescape_meta : string -> string
     7.6    val unescape_metas : string -> string list
     7.7 -  val extract_query : string -> string * string list
     7.8 +  val extract_query : string -> string * (string * real) list
     7.9    val nickname_of : thm -> string
    7.10 -  val suggested_facts : string list -> ('a * thm) list -> ('a * thm) list
    7.11 +  val suggested_facts :
    7.12 +    (string * 'a) list -> ('b * thm) list -> (('b * thm) * 'a) list
    7.13    val mesh_facts :
    7.14 -    int -> (('a * thm) list * ('a * thm) list) list -> ('a * thm) list
    7.15 -  val is_likely_tautology_or_too_meta : thm -> bool
    7.16 +    int -> ((('a * thm) * real) list * ('a * thm) list) list -> ('a * thm) list
    7.17    val theory_ord : theory * theory -> order
    7.18    val thm_ord : thm * thm -> order
    7.19    val goal_of_thm : theory -> thm -> thm
    7.20 @@ -52,13 +52,14 @@
    7.21    val mash_REPROVE :
    7.22      Proof.context -> bool -> (string * string list) list -> unit
    7.23    val mash_QUERY :
    7.24 -    Proof.context -> bool -> int -> string list * string list -> string list
    7.25 +    Proof.context -> bool -> int -> string list * string list
    7.26 +    -> (string * real) list
    7.27    val mash_unlearn : Proof.context -> unit
    7.28    val mash_could_suggest_facts : unit -> bool
    7.29    val mash_can_suggest_facts : Proof.context -> bool
    7.30 -  val mash_suggest_facts :
    7.31 +  val mash_suggested_facts :
    7.32      Proof.context -> params -> string -> int -> term list -> term
    7.33 -    -> ('a * thm) list -> ('a * thm) list * ('a * thm) list
    7.34 +    -> ('a * thm) list -> (('a * thm) * real) list * ('a * thm) list
    7.35    val mash_learn_proof :
    7.36      Proof.context -> params -> string -> term -> ('a * thm) list -> thm list
    7.37      -> unit
    7.38 @@ -132,9 +133,22 @@
    7.39  val unescape_metas =
    7.40    space_explode " " #> filter_out (curry (op =) "") #> map unescape_meta
    7.41  
    7.42 +fun extract_node line =
    7.43 +  case space_explode ":" line of
    7.44 +    [name, parents] => (unescape_meta name, unescape_metas parents)
    7.45 +  | _ => ("", [])
    7.46 +
    7.47 +fun extract_suggestion sugg =
    7.48 +  case space_explode "=" sugg of
    7.49 +    [name, weight] =>
    7.50 +    SOME (unescape_meta name, Real.fromString weight |> the_default 0.0)
    7.51 +  | _ => NONE
    7.52 +
    7.53  fun extract_query line =
    7.54    case space_explode ":" line of
    7.55 -    [goal_name, suggs] => (unescape_meta goal_name, unescape_metas suggs)
    7.56 +    [goal, suggs] =>
    7.57 +    (unescape_meta goal,
    7.58 +     map_filter extract_suggestion (space_explode " " suggs))
    7.59    | _ => ("", [])
    7.60  
    7.61  fun parent_of_local_thm th =
    7.62 @@ -165,31 +179,35 @@
    7.63    let
    7.64      fun add_fact (fact as (_, th)) = Symtab.default (nickname_of th, fact)
    7.65      val tab = Symtab.empty |> fold add_fact facts
    7.66 -  in map_filter (Symtab.lookup tab) suggs end
    7.67 +    fun find_sugg (name, weight) =
    7.68 +      Symtab.lookup tab name |> Option.map (rpair weight)
    7.69 +  in map_filter find_sugg suggs end
    7.70  
    7.71 -(* Ad hoc score function roughly based on Blanchette's Ringberg 2011 data. *)
    7.72 -fun score x = Math.pow (1.5, 15.5 - 0.05 * Real.fromInt x) + 15.0
    7.73 +fun sum_avg [] = 0
    7.74 +  | sum_avg xs = Real.ceil (100000.0 * fold (curry (op +)) xs 0.0) div length xs
    7.75  
    7.76 -fun sum_sq_avg [] = 0
    7.77 -  | sum_sq_avg xs =
    7.78 -    Real.ceil (100000.0 * fold (curry (op +) o score) xs 0.0) div length xs
    7.79 +fun normalize_scores [] = []
    7.80 +  | normalize_scores ((fact, score) :: tail) =
    7.81 +    (fact, 1.0) :: map (apsnd (curry Real.* (1.0 / score))) tail
    7.82  
    7.83 -fun mesh_facts max_facts [(selected, unknown)] =
    7.84 -    take max_facts selected @ take (max_facts - length selected) unknown
    7.85 +fun mesh_facts max_facts [(sels, unks)] =
    7.86 +    map fst (take max_facts sels) @ take (max_facts - length sels) unks
    7.87    | mesh_facts max_facts mess =
    7.88      let
    7.89 -      val mess = mess |> map (apfst (`length))
    7.90 +      val mess = mess |> map (apfst (normalize_scores #> `length))
    7.91        val fact_eq = Thm.eq_thm o pairself snd
    7.92 +      fun score_at sels = try (nth sels) #> Option.map snd
    7.93        fun score_in fact ((sel_len, sels), unks) =
    7.94 -        case find_index (curry fact_eq fact) sels of
    7.95 +        case find_index (curry fact_eq fact o fst) sels of
    7.96            ~1 => (case find_index (curry fact_eq fact) unks of
    7.97 -                   ~1 => SOME sel_len
    7.98 +                   ~1 => score_at sels sel_len
    7.99                   | _ => NONE)
   7.100 -        | j => SOME j
   7.101 -      fun score_of fact = mess |> map_filter (score_in fact) |> sum_sq_avg
   7.102 -      val facts = fold (union fact_eq o take max_facts o snd o fst) mess []
   7.103 +        | rank => score_at sels rank
   7.104 +      fun weight_of fact = mess |> map_filter (score_in fact) |> sum_avg
   7.105 +      val facts =
   7.106 +        fold (union fact_eq o map fst o take max_facts o snd o fst) mess []
   7.107      in
   7.108 -      facts |> map (`score_of) |> sort (int_ord o swap o pairself fst)
   7.109 +      facts |> map (`weight_of) |> sort (int_ord o swap o pairself fst)
   7.110              |> map snd |> take max_facts
   7.111      end
   7.112  
   7.113 @@ -198,24 +216,6 @@
   7.114  val type_name_of = prefix "t"
   7.115  val class_name_of = prefix "s"
   7.116  
   7.117 -fun is_likely_tautology_or_too_meta th =
   7.118 -  let
   7.119 -    val is_boring_const = member (op =) atp_widely_irrelevant_consts
   7.120 -    fun is_boring_bool t =
   7.121 -      not (exists_Const (not o is_boring_const o fst) t) orelse
   7.122 -      exists_type (exists_subtype (curry (op =) @{typ prop})) t
   7.123 -    fun is_boring_prop (@{const Trueprop} $ t) = is_boring_bool t
   7.124 -      | is_boring_prop (@{const "==>"} $ t $ u) =
   7.125 -        is_boring_prop t andalso is_boring_prop u
   7.126 -      | is_boring_prop (Const (@{const_name all}, _) $ (Abs (_, _, t)) $ u) =
   7.127 -        is_boring_prop t andalso is_boring_prop u
   7.128 -      | is_boring_prop (Const (@{const_name "=="}, _) $ t $ u) =
   7.129 -        is_boring_bool t andalso is_boring_bool u
   7.130 -      | is_boring_prop _ = true
   7.131 -  in
   7.132 -    is_boring_prop (prop_of th) andalso not (Thm.eq_thm_prop (@{thm ext}, th))
   7.133 -  end
   7.134 -
   7.135  fun theory_ord p =
   7.136    if Theory.eq_thy p then
   7.137      EQUAL
   7.138 @@ -280,10 +280,11 @@
   7.139            if is_bad_const x args then ""
   7.140            else mk_app (const_name_of s) (map (patternify (depth - 1)) args)
   7.141          | _ => ""
   7.142 +    fun add_pattern depth t =
   7.143 +      case patternify depth t of "" => I | s => insert (op =) s
   7.144      fun add_term_patterns ~1 _ = I
   7.145        | add_term_patterns depth t =
   7.146 -        insert (op =) (patternify depth t)
   7.147 -        #> add_term_patterns (depth - 1) t
   7.148 +        add_pattern depth t #> add_term_patterns (depth - 1) t
   7.149      val add_term = add_term_patterns term_max_depth
   7.150      fun add_patterns t =
   7.151        let val (head, args) = strip_comb t in
   7.152 @@ -327,8 +328,8 @@
   7.153  fun trim_dependencies deps =
   7.154    if length deps <= max_dependencies then SOME deps else NONE
   7.155  
   7.156 -fun isar_dependencies_of all_facts =
   7.157 -  thms_in_proof (SOME all_facts) #> trim_dependencies
   7.158 +fun isar_dependencies_of all_names =
   7.159 +  thms_in_proof (SOME all_names) #> trim_dependencies
   7.160  
   7.161  fun atp_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover
   7.162                          auto_level facts all_names th =
   7.163 @@ -349,7 +350,7 @@
   7.164            SOME ((name, status), th) => accum @ [((name, status), th)]
   7.165          | NONE => accum (* shouldn't happen *)
   7.166        val facts =
   7.167 -        facts |> iterative_relevant_facts ctxt params prover
   7.168 +        facts |> mepo_suggested_facts ctxt params prover
   7.169                       (max_facts |> the_default atp_dependency_default_max_fact)
   7.170                       NONE hyp_ts concl_t
   7.171                |> fold (add_isar_dep facts) (these isar_deps)
   7.172 @@ -432,7 +433,7 @@
   7.173    "p " ^ escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
   7.174  
   7.175  fun str_of_query (parents, feats) =
   7.176 -  "? " ^ escape_metas parents ^ "; " ^ escape_metas feats
   7.177 +  "? " ^ escape_metas parents ^ "; " ^ escape_metas feats ^ "\n"
   7.178  
   7.179  fun mash_CLEAR ctxt =
   7.180    let val path = mash_model_dir () |> Path.explode in
   7.181 @@ -487,6 +488,13 @@
   7.182                  "Internal error when " ^ when ^ ":\n" ^
   7.183                  ML_Compiler.exn_message exn); def)
   7.184  
   7.185 +fun graph_info G =
   7.186 +  string_of_int (length (Graph.keys G)) ^ " node(s), " ^
   7.187 +  string_of_int (fold (Integer.add o length o snd) (Graph.dest G) 0) ^
   7.188 +  " edge(s), " ^
   7.189 +  string_of_int (length (Graph.minimals G)) ^ " minimal, " ^
   7.190 +  string_of_int (length (Graph.maximals G)) ^ " maximal"
   7.191 +
   7.192  type mash_state = {fact_G : unit Graph.T}
   7.193  
   7.194  val empty_state = {fact_G = Graph.empty}
   7.195 @@ -500,26 +508,27 @@
   7.196      let val path = mash_state_path () in
   7.197        (true,
   7.198         case try File.read_lines path of
   7.199 -         SOME (version' :: fact_lines) =>
   7.200 +         SOME (version' :: node_lines) =>
   7.201           let
   7.202             fun add_edge_to name parent =
   7.203 -             Graph.default_node (parent, ())
   7.204 -             #> Graph.add_edge (parent, name)
   7.205 -           fun add_fact_line line =
   7.206 -             case extract_query line of
   7.207 +             Graph.default_node (parent, ()) #> Graph.add_edge (parent, name)
   7.208 +           fun add_node line =
   7.209 +             case extract_node line of
   7.210                 ("", _) => I (* shouldn't happen *)
   7.211               | (name, parents) =>
   7.212 -               Graph.default_node (name, ())
   7.213 -               #> fold (add_edge_to name) parents
   7.214 +               Graph.default_node (name, ()) #> fold (add_edge_to name) parents
   7.215             val fact_G =
   7.216               try_graph ctxt "loading state" Graph.empty (fn () =>
   7.217 -                 Graph.empty |> version' = version
   7.218 -                                ? fold add_fact_line fact_lines)
   7.219 -         in {fact_G = fact_G} end
   7.220 +                 Graph.empty |> version' = version ? fold add_node node_lines)
   7.221 +         in
   7.222 +           trace_msg ctxt (fn () =>
   7.223 +               "Loaded fact graph (" ^ graph_info fact_G ^ ")");
   7.224 +           {fact_G = fact_G}
   7.225 +         end
   7.226         | _ => empty_state)
   7.227      end
   7.228  
   7.229 -fun save {fact_G} =
   7.230 +fun save ctxt {fact_G} =
   7.231    let
   7.232      val path = mash_state_path ()
   7.233      fun fact_line_for name parents =
   7.234 @@ -529,7 +538,8 @@
   7.235        append_fact name (Graph.Keys.dest parents)
   7.236    in
   7.237      File.write path (version ^ "\n");
   7.238 -    Graph.fold append_entry fact_G ()
   7.239 +    Graph.fold append_entry fact_G ();
   7.240 +    trace_msg ctxt (fn () => "Saved fact graph (" ^ graph_info fact_G ^ ")")
   7.241    end
   7.242  
   7.243  val global_state =
   7.244 @@ -538,7 +548,7 @@
   7.245  in
   7.246  
   7.247  fun mash_map ctxt f =
   7.248 -  Synchronized.change global_state (load ctxt ##> (f #> tap save))
   7.249 +  Synchronized.change global_state (load ctxt ##> (f #> tap (save ctxt)))
   7.250  
   7.251  fun mash_get ctxt =
   7.252    Synchronized.change_result global_state (load ctxt #> `snd)
   7.253 @@ -567,9 +577,11 @@
   7.254          if Symtab.defined tab name then
   7.255            let
   7.256              val new = (Graph.all_preds fact_G [name], name)
   7.257 -            fun not_ancestor (_, x) (yp, _) = not (member (op =) yp x)
   7.258 -            val maxs = maxs |> filter (fn max => not_ancestor max new)
   7.259 -            val maxs = maxs |> forall (not_ancestor new) maxs ? cons new
   7.260 +            fun is_ancestor (_, x) (yp, _) = member (op =) yp x
   7.261 +            val maxs = maxs |> filter (fn max => not (is_ancestor max new))
   7.262 +            val maxs =
   7.263 +              if exists (is_ancestor new) maxs then maxs
   7.264 +              else new :: filter_out (fn max => is_ancestor max new) maxs
   7.265            in find_maxes (name :: seen) maxs names end
   7.266          else
   7.267            find_maxes (name :: seen) maxs
   7.268 @@ -585,8 +597,8 @@
   7.269  fun is_fact_in_graph fact_G (_, th) =
   7.270    can (Graph.get_node fact_G) (nickname_of th)
   7.271  
   7.272 -fun mash_suggest_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
   7.273 -                       concl_t facts =
   7.274 +fun mash_suggested_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
   7.275 +                         concl_t facts =
   7.276    let
   7.277      val thy = Proof_Context.theory_of ctxt
   7.278      val fact_G = #fact_G (mash_get ctxt)
   7.279 @@ -756,13 +768,13 @@
   7.280              n
   7.281            else
   7.282              let
   7.283 -              fun score_of (_, th) =
   7.284 +              fun priority_of (_, th) =
   7.285                  random_range 0 (1000 * max_dependencies)
   7.286                  - 500 * (th |> isar_dependencies_of all_names
   7.287                              |> Option.map length
   7.288                              |> the_default max_dependencies)
   7.289                val old_facts =
   7.290 -                old_facts |> map (`score_of)
   7.291 +                old_facts |> map (`priority_of)
   7.292                            |> sort (int_ord o pairself fst)
   7.293                            |> map snd
   7.294                val (reps, (n, _, _)) =
   7.295 @@ -850,13 +862,14 @@
   7.296          ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @
   7.297           (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)))
   7.298          |> take max_facts
   7.299 -      fun iter () =
   7.300 -        iterative_relevant_facts ctxt params prover max_facts NONE hyp_ts
   7.301 -                                 concl_t facts
   7.302 +      fun mepo () =
   7.303 +        facts |> mepo_suggested_facts ctxt params prover max_facts NONE hyp_ts
   7.304 +                                      concl_t
   7.305 +              |> weight_mepo_facts
   7.306        fun mash () =
   7.307 -        mash_suggest_facts ctxt params prover max_facts hyp_ts concl_t facts
   7.308 +        mash_suggested_facts ctxt params prover max_facts hyp_ts concl_t facts
   7.309        val mess =
   7.310 -        [] |> (if fact_filter <> mashN then cons (iter (), []) else I)
   7.311 +        [] |> (if fact_filter <> mashN then cons (mepo (), []) else I)
   7.312             |> (if fact_filter <> mepoN then cons (mash ()) else I)
   7.313      in
   7.314        mesh_facts max_facts mess
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Fri Jul 20 22:19:46 2012 +0200
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Fri Jul 20 22:19:46 2012 +0200
     8.3 @@ -18,9 +18,10 @@
     8.4    val const_names_in_fact :
     8.5      theory -> (string * typ -> term list -> bool * term list) -> term
     8.6      -> string list
     8.7 -  val iterative_relevant_facts :
     8.8 +  val mepo_suggested_facts :
     8.9      Proof.context -> params -> string -> int -> relevance_fudge option
    8.10      -> term list -> term -> fact list -> fact list
    8.11 +  val weight_mepo_facts : fact list -> (fact * real) list
    8.12  end;
    8.13  
    8.14  structure Sledgehammer_MePo : SLEDGEHAMMER_MEPO =
    8.15 @@ -508,7 +509,7 @@
    8.16                        "Total relevant: " ^ string_of_int (length accepts)))
    8.17    end
    8.18  
    8.19 -fun iterative_relevant_facts ctxt
    8.20 +fun mepo_suggested_facts ctxt
    8.21          ({fact_thresholds = (thres0, thres1), ...} : params) prover
    8.22          max_facts fudge hyp_ts concl_t facts =
    8.23    let
    8.24 @@ -534,4 +535,11 @@
    8.25             (concl_t |> theory_constify fudge (Context.theory_name thy)))
    8.26    end
    8.27  
    8.28 +(* Ad hoc score function roughly based on Blanchette's Ringberg 2011 data. *)
    8.29 +fun weight_of_fact rank =
    8.30 +  Math.pow (1.5, 15.5 - 0.05 * Real.fromInt rank) + 15.0
    8.31 +
    8.32 +fun weight_mepo_facts facts =
    8.33 +  facts ~~ map weight_of_fact (0 upto length facts - 1)
    8.34 +
    8.35  end;