src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
changeset 50382 cb564ff43c28
parent 50053 fea589c8583e
child 50383 4274b25ff4e7
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Wed Dec 05 11:05:34 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Wed Dec 05 13:25:06 2012 +0100
     1.3 @@ -18,10 +18,10 @@
     1.4    val const_names_in_fact :
     1.5      theory -> (string * typ -> term list -> bool * term list) -> term
     1.6      -> string list
     1.7 +  val weight_mepo_facts : ('a * thm) list -> (('a * thm) * real) list
     1.8    val mepo_suggested_facts :
     1.9      Proof.context -> params -> string -> int -> relevance_fudge option
    1.10      -> term list -> term -> fact list -> fact list
    1.11 -  val weight_mepo_facts : ('a * thm) list -> (('a * thm) * real) list
    1.12  end;
    1.13  
    1.14  structure Sledgehammer_MePo : SLEDGEHAMMER_MEPO =
    1.15 @@ -509,6 +509,12 @@
    1.16                        "Total relevant: " ^ string_of_int (length accepts)))
    1.17    end
    1.18  
    1.19 +(* Ad hoc score function roughly based on Blanchette's Ringberg 2011 data. *)
    1.20 +fun weight_of_fact rank = Math.pow (1.5, 15.5 - 0.05 * Real.fromInt rank) + 15.0
    1.21 +
    1.22 +fun weight_mepo_facts facts =
    1.23 +  facts ~~ map weight_of_fact (0 upto length facts - 1)
    1.24 +
    1.25  fun mepo_suggested_facts ctxt
    1.26          ({fact_thresholds = (thres0, thres1), ...} : params) prover
    1.27          max_facts fudge hyp_ts concl_t facts =
    1.28 @@ -535,10 +541,4 @@
    1.29             (concl_t |> theory_constify fudge (Context.theory_name thy)))
    1.30    end
    1.31  
    1.32 -(* Ad hoc score function roughly based on Blanchette's Ringberg 2011 data. *)
    1.33 -fun weight_of_fact rank = Math.pow (1.5, 15.5 - 0.05 * Real.fromInt rank) + 15.0
    1.34 -
    1.35 -fun weight_mepo_facts facts =
    1.36 -  facts ~~ map weight_of_fact (0 upto length facts - 1)
    1.37 -
    1.38  end;