renamed ML files
authorblanchet
Fri Jul 20 22:19:45 2012 +0200 (2012-07-20)
changeset 48380d4b7c7be3116
parent 48379 2b5ad61e2ccc
child 48381 1b7d798460bb
renamed ML files
src/HOL/IsaMakefile
src/HOL/Sledgehammer.thy
src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
     1.1 --- a/src/HOL/IsaMakefile	Fri Jul 20 22:19:45 2012 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Jul 20 22:19:45 2012 +0200
     1.3 @@ -371,8 +371,8 @@
     1.4    Tools/semiring_normalizer.ML \
     1.5    Tools/Sledgehammer/async_manager.ML \
     1.6    Tools/Sledgehammer/sledgehammer_fact.ML \
     1.7 -  Tools/Sledgehammer/sledgehammer_filter_iter.ML \
     1.8 -  Tools/Sledgehammer/sledgehammer_filter_mash.ML \
     1.9 +  Tools/Sledgehammer/sledgehammer_mash.ML \
    1.10 +  Tools/Sledgehammer/sledgehammer_mepo.ML \
    1.11    Tools/Sledgehammer/sledgehammer_minimize.ML \
    1.12    Tools/Sledgehammer/sledgehammer_isar.ML \
    1.13    Tools/Sledgehammer/sledgehammer_provers.ML \
     2.1 --- a/src/HOL/Sledgehammer.thy	Fri Jul 20 22:19:45 2012 +0200
     2.2 +++ b/src/HOL/Sledgehammer.thy	Fri Jul 20 22:19:45 2012 +0200
     2.3 @@ -14,8 +14,8 @@
     2.4       "Tools/Sledgehammer/sledgehammer_fact.ML"
     2.5       "Tools/Sledgehammer/sledgehammer_provers.ML"
     2.6       "Tools/Sledgehammer/sledgehammer_minimize.ML"
     2.7 -     "Tools/Sledgehammer/sledgehammer_filter_iter.ML"
     2.8 -     "Tools/Sledgehammer/sledgehammer_filter_mash.ML"
     2.9 +     "Tools/Sledgehammer/sledgehammer_mepo.ML"
    2.10 +     "Tools/Sledgehammer/sledgehammer_mash.ML"
    2.11       "Tools/Sledgehammer/sledgehammer_run.ML"
    2.12       "Tools/Sledgehammer/sledgehammer_isar.ML"
    2.13  begin
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML	Fri Jul 20 22:19:45 2012 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,537 +0,0 @@
     3.4 -(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML
     3.5 -    Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     3.6 -    Author:     Jasmin Blanchette, TU Muenchen
     3.7 -
     3.8 -Sledgehammer's iterative relevance filter.
     3.9 -*)
    3.10 -
    3.11 -signature SLEDGEHAMMER_FILTER_ITER =
    3.12 -sig
    3.13 -  type stature = ATP_Problem_Generate.stature
    3.14 -  type fact = Sledgehammer_Fact.fact
    3.15 -  type params = Sledgehammer_Provers.params
    3.16 -  type relevance_fudge = Sledgehammer_Provers.relevance_fudge
    3.17 -
    3.18 -  val trace : bool Config.T
    3.19 -  val pseudo_abs_name : string
    3.20 -  val pseudo_skolem_prefix : string
    3.21 -  val const_names_in_fact :
    3.22 -    theory -> (string * typ -> term list -> bool * term list) -> term
    3.23 -    -> string list
    3.24 -  val iterative_relevant_facts :
    3.25 -    Proof.context -> params -> string -> int -> relevance_fudge option
    3.26 -    -> term list -> term -> fact list -> fact list
    3.27 -end;
    3.28 -
    3.29 -structure Sledgehammer_Filter_Iter : SLEDGEHAMMER_FILTER_ITER =
    3.30 -struct
    3.31 -
    3.32 -open ATP_Problem_Generate
    3.33 -open Sledgehammer_Fact
    3.34 -open Sledgehammer_Provers
    3.35 -
    3.36 -val trace =
    3.37 -  Attrib.setup_config_bool @{binding sledgehammer_filter_iter_trace} (K false)
    3.38 -fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
    3.39 -
    3.40 -val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
    3.41 -val pseudo_abs_name = sledgehammer_prefix ^ "abs"
    3.42 -val pseudo_skolem_prefix = sledgehammer_prefix ^ "sko"
    3.43 -val theory_const_suffix = Long_Name.separator ^ " 1"
    3.44 -
    3.45 -fun order_of_type (Type (@{type_name fun}, [T1, T2])) =
    3.46 -    Int.max (order_of_type T1 + 1, order_of_type T2)
    3.47 -  | order_of_type (Type (_, Ts)) = fold (Integer.max o order_of_type) Ts 0
    3.48 -  | order_of_type _ = 0
    3.49 -
    3.50 -(* An abstraction of Isabelle types and first-order terms *)
    3.51 -datatype pattern = PVar | PApp of string * pattern list
    3.52 -datatype ptype = PType of int * pattern list
    3.53 -
    3.54 -fun string_for_pattern PVar = "_"
    3.55 -  | string_for_pattern (PApp (s, ps)) =
    3.56 -    if null ps then s else s ^ string_for_patterns ps
    3.57 -and string_for_patterns ps = "(" ^ commas (map string_for_pattern ps) ^ ")"
    3.58 -fun string_for_ptype (PType (_, ps)) = string_for_patterns ps
    3.59 -
    3.60 -(*Is the second type an instance of the first one?*)
    3.61 -fun match_pattern (PVar, _) = true
    3.62 -  | match_pattern (PApp _, PVar) = false
    3.63 -  | match_pattern (PApp (s, ps), PApp (t, qs)) =
    3.64 -    s = t andalso match_patterns (ps, qs)
    3.65 -and match_patterns (_, []) = true
    3.66 -  | match_patterns ([], _) = false
    3.67 -  | match_patterns (p :: ps, q :: qs) =
    3.68 -    match_pattern (p, q) andalso match_patterns (ps, qs)
    3.69 -fun match_ptype (PType (_, ps), PType (_, qs)) = match_patterns (ps, qs)
    3.70 -
    3.71 -(* Is there a unifiable constant? *)
    3.72 -fun pconst_mem f consts (s, ps) =
    3.73 -  exists (curry (match_ptype o f) ps)
    3.74 -         (map snd (filter (curry (op =) s o fst) consts))
    3.75 -fun pconst_hyper_mem f const_tab (s, ps) =
    3.76 -  exists (curry (match_ptype o f) ps) (these (Symtab.lookup const_tab s))
    3.77 -
    3.78 -fun pattern_for_type (Type (s, Ts)) = PApp (s, map pattern_for_type Ts)
    3.79 -  | pattern_for_type (TFree (s, _)) = PApp (s, [])
    3.80 -  | pattern_for_type (TVar _) = PVar
    3.81 -
    3.82 -(* Pairs a constant with the list of its type instantiations. *)
    3.83 -fun ptype thy const x =
    3.84 -  (if const then map pattern_for_type (these (try (Sign.const_typargs thy) x))
    3.85 -   else [])
    3.86 -fun rich_ptype thy const (s, T) =
    3.87 -  PType (order_of_type T, ptype thy const (s, T))
    3.88 -fun rich_pconst thy const (s, T) = (s, rich_ptype thy const (s, T))
    3.89 -
    3.90 -fun string_for_hyper_pconst (s, ps) =
    3.91 -  s ^ "{" ^ commas (map string_for_ptype ps) ^ "}"
    3.92 -
    3.93 -(* Add a pconstant to the table, but a [] entry means a standard
    3.94 -   connective, which we ignore.*)
    3.95 -fun add_pconst_to_table also_skolem (s, p) =
    3.96 -  if (not also_skolem andalso String.isPrefix pseudo_skolem_prefix s) then I
    3.97 -  else Symtab.map_default (s, [p]) (insert (op =) p)
    3.98 -
    3.99 -(* Set constants tend to pull in too many irrelevant facts. We limit the damage
   3.100 -   by treating them more or less as if they were built-in but add their
   3.101 -   axiomatization at the end. *)
   3.102 -val set_consts = [@{const_name Collect}, @{const_name Set.member}]
   3.103 -val set_thms = @{thms Collect_mem_eq mem_Collect_eq Collect_cong}
   3.104 -
   3.105 -fun add_pconsts_in_term thy is_built_in_const also_skolems pos =
   3.106 -  let
   3.107 -    val flip = Option.map not
   3.108 -    (* We include free variables, as well as constants, to handle locales. For
   3.109 -       each quantifiers that must necessarily be skolemized by the automatic
   3.110 -       prover, we introduce a fresh constant to simulate the effect of
   3.111 -       Skolemization. *)
   3.112 -    fun do_const const ext_arg (x as (s, _)) ts =
   3.113 -      let val (built_in, ts) = is_built_in_const x ts in
   3.114 -        if member (op =) set_consts s then
   3.115 -          fold (do_term ext_arg) ts
   3.116 -        else
   3.117 -          (not built_in
   3.118 -           ? add_pconst_to_table also_skolems (rich_pconst thy const x))
   3.119 -          #> fold (do_term false) ts
   3.120 -      end
   3.121 -    and do_term ext_arg t =
   3.122 -      case strip_comb t of
   3.123 -        (Const x, ts) => do_const true ext_arg x ts
   3.124 -      | (Free x, ts) => do_const false ext_arg x ts
   3.125 -      | (Abs (_, T, t'), ts) =>
   3.126 -        ((null ts andalso not ext_arg)
   3.127 -         (* Since lambdas on the right-hand side of equalities are usually
   3.128 -            extensionalized later by "abs_extensionalize_term", we don't
   3.129 -            penalize them here. *)
   3.130 -         ? add_pconst_to_table true (pseudo_abs_name,
   3.131 -                                     PType (order_of_type T + 1, [])))
   3.132 -        #> fold (do_term false) (t' :: ts)
   3.133 -      | (_, ts) => fold (do_term false) ts
   3.134 -    fun do_quantifier will_surely_be_skolemized abs_T body_t =
   3.135 -      do_formula pos body_t
   3.136 -      #> (if also_skolems andalso will_surely_be_skolemized then
   3.137 -            add_pconst_to_table true (pseudo_skolem_prefix ^ serial_string (),
   3.138 -                                      PType (order_of_type abs_T, []))
   3.139 -          else
   3.140 -            I)
   3.141 -    and do_term_or_formula ext_arg T =
   3.142 -      if T = HOLogic.boolT then do_formula NONE else do_term ext_arg
   3.143 -    and do_formula pos t =
   3.144 -      case t of
   3.145 -        Const (@{const_name all}, _) $ Abs (_, T, t') =>
   3.146 -        do_quantifier (pos = SOME false) T t'
   3.147 -      | @{const "==>"} $ t1 $ t2 =>
   3.148 -        do_formula (flip pos) t1 #> do_formula pos t2
   3.149 -      | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
   3.150 -        do_term_or_formula false T t1 #> do_term_or_formula true T t2
   3.151 -      | @{const Trueprop} $ t1 => do_formula pos t1
   3.152 -      | @{const False} => I
   3.153 -      | @{const True} => I
   3.154 -      | @{const Not} $ t1 => do_formula (flip pos) t1
   3.155 -      | Const (@{const_name All}, _) $ Abs (_, T, t') =>
   3.156 -        do_quantifier (pos = SOME false) T t'
   3.157 -      | Const (@{const_name Ex}, _) $ Abs (_, T, t') =>
   3.158 -        do_quantifier (pos = SOME true) T t'
   3.159 -      | @{const HOL.conj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
   3.160 -      | @{const HOL.disj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
   3.161 -      | @{const HOL.implies} $ t1 $ t2 =>
   3.162 -        do_formula (flip pos) t1 #> do_formula pos t2
   3.163 -      | Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2 =>
   3.164 -        do_term_or_formula false T t1 #> do_term_or_formula true T t2
   3.165 -      | Const (@{const_name If}, Type (_, [_, Type (_, [T, _])]))
   3.166 -        $ t1 $ t2 $ t3 =>
   3.167 -        do_formula NONE t1 #> fold (do_term_or_formula false T) [t2, t3]
   3.168 -      | Const (@{const_name Ex1}, _) $ Abs (_, T, t') =>
   3.169 -        do_quantifier (is_some pos) T t'
   3.170 -      | Const (@{const_name Ball}, _) $ t1 $ Abs (_, T, t') =>
   3.171 -        do_quantifier (pos = SOME false) T
   3.172 -                      (HOLogic.mk_imp (incr_boundvars 1 t1 $ Bound 0, t'))
   3.173 -      | Const (@{const_name Bex}, _) $ t1 $ Abs (_, T, t') =>
   3.174 -        do_quantifier (pos = SOME true) T
   3.175 -                      (HOLogic.mk_conj (incr_boundvars 1 t1 $ Bound 0, t'))
   3.176 -      | (t0 as Const (_, @{typ bool})) $ t1 =>
   3.177 -        do_term false t0 #> do_formula pos t1  (* theory constant *)
   3.178 -      | _ => do_term false t
   3.179 -  in do_formula pos end
   3.180 -
   3.181 -fun pconsts_in_fact thy is_built_in_const t =
   3.182 -  Symtab.fold (fn (s, pss) => fold (cons o pair s) pss)
   3.183 -              (Symtab.empty |> add_pconsts_in_term thy is_built_in_const true
   3.184 -                                                   (SOME true) t) []
   3.185 -
   3.186 -val const_names_in_fact = map fst ooo pconsts_in_fact
   3.187 -
   3.188 -(* Inserts a dummy "constant" referring to the theory name, so that relevance
   3.189 -   takes the given theory into account. *)
   3.190 -fun theory_constify ({theory_const_rel_weight, theory_const_irrel_weight, ...}
   3.191 -                     : relevance_fudge) thy_name t =
   3.192 -  if exists (curry (op <) 0.0) [theory_const_rel_weight,
   3.193 -                                theory_const_irrel_weight] then
   3.194 -    Const (thy_name ^ theory_const_suffix, @{typ bool}) $ t
   3.195 -  else
   3.196 -    t
   3.197 -
   3.198 -fun theory_const_prop_of fudge th =
   3.199 -  theory_constify fudge (Context.theory_name (theory_of_thm th)) (prop_of th)
   3.200 -
   3.201 -fun pair_consts_fact thy is_built_in_const fudge fact =
   3.202 -  case fact |> snd |> theory_const_prop_of fudge
   3.203 -            |> pconsts_in_fact thy is_built_in_const of
   3.204 -    [] => NONE
   3.205 -  | consts => SOME ((fact, consts), NONE)
   3.206 -
   3.207 -(* A two-dimensional symbol table counts frequencies of constants. It's keyed
   3.208 -   first by constant name and second by its list of type instantiations. For the
   3.209 -   latter, we need a linear ordering on "pattern list". *)
   3.210 -
   3.211 -fun pattern_ord p =
   3.212 -  case p of
   3.213 -    (PVar, PVar) => EQUAL
   3.214 -  | (PVar, PApp _) => LESS
   3.215 -  | (PApp _, PVar) => GREATER
   3.216 -  | (PApp q1, PApp q2) =>
   3.217 -    prod_ord fast_string_ord (dict_ord pattern_ord) (q1, q2)
   3.218 -fun ptype_ord (PType p, PType q) =
   3.219 -  prod_ord (dict_ord pattern_ord) int_ord (swap p, swap q)
   3.220 -
   3.221 -structure PType_Tab = Table(type key = ptype val ord = ptype_ord)
   3.222 -
   3.223 -fun count_fact_consts thy fudge =
   3.224 -  let
   3.225 -    fun do_const const (s, T) ts =
   3.226 -      (* Two-dimensional table update. Constant maps to types maps to count. *)
   3.227 -      PType_Tab.map_default (rich_ptype thy const (s, T), 0) (Integer.add 1)
   3.228 -      |> Symtab.map_default (s, PType_Tab.empty)
   3.229 -      #> fold do_term ts
   3.230 -    and do_term t =
   3.231 -      case strip_comb t of
   3.232 -        (Const x, ts) => do_const true x ts
   3.233 -      | (Free x, ts) => do_const false x ts
   3.234 -      | (Abs (_, _, t'), ts) => fold do_term (t' :: ts)
   3.235 -      | (_, ts) => fold do_term ts
   3.236 -  in do_term o theory_const_prop_of fudge o snd end
   3.237 -
   3.238 -fun pow_int _ 0 = 1.0
   3.239 -  | pow_int x 1 = x
   3.240 -  | pow_int x n = if n > 0 then x * pow_int x (n - 1) else pow_int x (n + 1) / x
   3.241 -
   3.242 -(*The frequency of a constant is the sum of those of all instances of its type.*)
   3.243 -fun pconst_freq match const_tab (c, ps) =
   3.244 -  PType_Tab.fold (fn (qs, m) => match (ps, qs) ? Integer.add m)
   3.245 -                 (the (Symtab.lookup const_tab c)) 0
   3.246 -
   3.247 -
   3.248 -(* A surprising number of theorems contain only a few significant constants.
   3.249 -   These include all induction rules, and other general theorems. *)
   3.250 -
   3.251 -(* "log" seems best in practice. A constant function of one ignores the constant
   3.252 -   frequencies. Rare constants give more points if they are relevant than less
   3.253 -   rare ones. *)
   3.254 -fun rel_weight_for _ freq = 1.0 + 2.0 / Math.ln (Real.fromInt freq + 1.0)
   3.255 -
   3.256 -(* Irrelevant constants are treated differently. We associate lower penalties to
   3.257 -   very rare constants and very common ones -- the former because they can't
   3.258 -   lead to the inclusion of too many new facts, and the latter because they are
   3.259 -   so common as to be of little interest. *)
   3.260 -fun irrel_weight_for ({worse_irrel_freq, higher_order_irrel_weight, ...}
   3.261 -                      : relevance_fudge) order freq =
   3.262 -  let val (k, x) = worse_irrel_freq |> `Real.ceil in
   3.263 -    (if freq < k then Math.ln (Real.fromInt (freq + 1)) / Math.ln x
   3.264 -     else rel_weight_for order freq / rel_weight_for order k)
   3.265 -    * pow_int higher_order_irrel_weight (order - 1)
   3.266 -  end
   3.267 -
   3.268 -fun multiplier_for_const_name local_const_multiplier s =
   3.269 -  if String.isSubstring "." s then 1.0 else local_const_multiplier
   3.270 -
   3.271 -(* Computes a constant's weight, as determined by its frequency. *)
   3.272 -fun generic_pconst_weight local_const_multiplier abs_weight skolem_weight
   3.273 -                          theory_const_weight chained_const_weight weight_for f
   3.274 -                          const_tab chained_const_tab (c as (s, PType (m, _))) =
   3.275 -  if s = pseudo_abs_name then
   3.276 -    abs_weight
   3.277 -  else if String.isPrefix pseudo_skolem_prefix s then
   3.278 -    skolem_weight
   3.279 -  else if String.isSuffix theory_const_suffix s then
   3.280 -    theory_const_weight
   3.281 -  else
   3.282 -    multiplier_for_const_name local_const_multiplier s
   3.283 -    * weight_for m (pconst_freq (match_ptype o f) const_tab c)
   3.284 -    |> (if chained_const_weight < 1.0 andalso
   3.285 -           pconst_hyper_mem I chained_const_tab c then
   3.286 -          curry (op *) chained_const_weight
   3.287 -        else
   3.288 -          I)
   3.289 -
   3.290 -fun rel_pconst_weight ({local_const_multiplier, abs_rel_weight,
   3.291 -                        theory_const_rel_weight, ...} : relevance_fudge)
   3.292 -                      const_tab =
   3.293 -  generic_pconst_weight local_const_multiplier abs_rel_weight 0.0
   3.294 -                        theory_const_rel_weight 0.0 rel_weight_for I const_tab
   3.295 -                        Symtab.empty
   3.296 -
   3.297 -fun irrel_pconst_weight (fudge as {local_const_multiplier, abs_irrel_weight,
   3.298 -                                   skolem_irrel_weight,
   3.299 -                                   theory_const_irrel_weight,
   3.300 -                                   chained_const_irrel_weight, ...})
   3.301 -                        const_tab chained_const_tab =
   3.302 -  generic_pconst_weight local_const_multiplier abs_irrel_weight
   3.303 -                        skolem_irrel_weight theory_const_irrel_weight
   3.304 -                        chained_const_irrel_weight (irrel_weight_for fudge) swap
   3.305 -                        const_tab chained_const_tab
   3.306 -
   3.307 -fun stature_bonus ({intro_bonus, ...} : relevance_fudge) (_, Intro) =
   3.308 -    intro_bonus
   3.309 -  | stature_bonus {elim_bonus, ...} (_, Elim) = elim_bonus
   3.310 -  | stature_bonus {simp_bonus, ...} (_, Simp) = simp_bonus
   3.311 -  | stature_bonus {local_bonus, ...} (Local, _) = local_bonus
   3.312 -  | stature_bonus {assum_bonus, ...} (Assum, _) = assum_bonus
   3.313 -  | stature_bonus {chained_bonus, ...} (Chained, _) = chained_bonus
   3.314 -  | stature_bonus _ _ = 0.0
   3.315 -
   3.316 -fun is_odd_const_name s =
   3.317 -  s = pseudo_abs_name orelse String.isPrefix pseudo_skolem_prefix s orelse
   3.318 -  String.isSuffix theory_const_suffix s
   3.319 -
   3.320 -fun fact_weight fudge stature const_tab relevant_consts chained_consts
   3.321 -                fact_consts =
   3.322 -  case fact_consts |> List.partition (pconst_hyper_mem I relevant_consts)
   3.323 -                   ||> filter_out (pconst_hyper_mem swap relevant_consts) of
   3.324 -    ([], _) => 0.0
   3.325 -  | (rel, irrel) =>
   3.326 -    if forall (forall (is_odd_const_name o fst)) [rel, irrel] then
   3.327 -      0.0
   3.328 -    else
   3.329 -      let
   3.330 -        val irrel = irrel |> filter_out (pconst_mem swap rel)
   3.331 -        val rel_weight =
   3.332 -          0.0 |> fold (curry (op +) o rel_pconst_weight fudge const_tab) rel
   3.333 -        val irrel_weight =
   3.334 -          ~ (stature_bonus fudge stature)
   3.335 -          |> fold (curry (op +)
   3.336 -                   o irrel_pconst_weight fudge const_tab chained_consts) irrel
   3.337 -        val res = rel_weight / (rel_weight + irrel_weight)
   3.338 -      in if Real.isFinite res then res else 0.0 end
   3.339 -
   3.340 -fun take_most_relevant ctxt max_facts remaining_max
   3.341 -        ({max_imperfect, max_imperfect_exp, ...} : relevance_fudge)
   3.342 -        (candidates : ((fact * (string * ptype) list) * real) list) =
   3.343 -  let
   3.344 -    val max_imperfect =
   3.345 -      Real.ceil (Math.pow (max_imperfect,
   3.346 -                    Math.pow (Real.fromInt remaining_max
   3.347 -                              / Real.fromInt max_facts, max_imperfect_exp)))
   3.348 -    val (perfect, imperfect) =
   3.349 -      candidates |> sort (Real.compare o swap o pairself snd)
   3.350 -                 |> take_prefix (fn (_, w) => w > 0.99999)
   3.351 -    val ((accepts, more_rejects), rejects) =
   3.352 -      chop max_imperfect imperfect |>> append perfect |>> chop remaining_max
   3.353 -  in
   3.354 -    trace_msg ctxt (fn () =>
   3.355 -        "Actually passed (" ^ string_of_int (length accepts) ^ " of " ^
   3.356 -        string_of_int (length candidates) ^ "): " ^
   3.357 -        (accepts |> map (fn ((((name, _), _), _), weight) =>
   3.358 -                            name () ^ " [" ^ Real.toString weight ^ "]")
   3.359 -                 |> commas));
   3.360 -    (accepts, more_rejects @ rejects)
   3.361 -  end
   3.362 -
   3.363 -fun if_empty_replace_with_scope thy is_built_in_const facts sc tab =
   3.364 -  if Symtab.is_empty tab then
   3.365 -    Symtab.empty
   3.366 -    |> fold (add_pconsts_in_term thy is_built_in_const false (SOME false))
   3.367 -            (map_filter (fn ((_, (sc', _)), th) =>
   3.368 -                            if sc' = sc then SOME (prop_of th) else NONE) facts)
   3.369 -  else
   3.370 -    tab
   3.371 -
   3.372 -fun consider_arities is_built_in_const th =
   3.373 -  let
   3.374 -    fun aux _ _ NONE = NONE
   3.375 -      | aux t args (SOME tab) =
   3.376 -        case t of
   3.377 -          t1 $ t2 => SOME tab |> aux t1 (t2 :: args) |> aux t2 []
   3.378 -        | Const (x as (s, _)) =>
   3.379 -          (if is_built_in_const x args |> fst then
   3.380 -             SOME tab
   3.381 -           else case Symtab.lookup tab s of
   3.382 -             NONE => SOME (Symtab.update (s, length args) tab)
   3.383 -           | SOME n => if n = length args then SOME tab else NONE)
   3.384 -        | _ => SOME tab
   3.385 -  in aux (prop_of th) [] end
   3.386 -
   3.387 -(* FIXME: This is currently only useful for polymorphic type encodings. *)
   3.388 -fun could_benefit_from_ext is_built_in_const facts =
   3.389 -  fold (consider_arities is_built_in_const o snd) facts (SOME Symtab.empty)
   3.390 -  |> is_none
   3.391 -
   3.392 -(* High enough so that it isn't wrongly considered as very relevant (e.g., for E
   3.393 -   weights), but low enough so that it is unlikely to be truncated away if few
   3.394 -   facts are included. *)
   3.395 -val special_fact_index = 75
   3.396 -
   3.397 -fun relevance_filter ctxt thres0 decay max_facts is_built_in_const
   3.398 -        (fudge as {threshold_divisor, ridiculous_threshold, ...}) facts hyp_ts
   3.399 -        concl_t =
   3.400 -  let
   3.401 -    val thy = Proof_Context.theory_of ctxt
   3.402 -    val const_tab = fold (count_fact_consts thy fudge) facts Symtab.empty
   3.403 -    val add_pconsts = add_pconsts_in_term thy is_built_in_const false o SOME
   3.404 -    val chained_ts =
   3.405 -      facts |> map_filter (fn ((_, (Chained, _)), th) => SOME (prop_of th)
   3.406 -                            | _ => NONE)
   3.407 -    val chained_const_tab = Symtab.empty |> fold (add_pconsts true) chained_ts
   3.408 -    val goal_const_tab =
   3.409 -      Symtab.empty |> fold (add_pconsts true) hyp_ts
   3.410 -                   |> add_pconsts false concl_t
   3.411 -      |> (fn tab => if Symtab.is_empty tab then chained_const_tab else tab)
   3.412 -      |> fold (if_empty_replace_with_scope thy is_built_in_const facts)
   3.413 -              [Chained, Assum, Local]
   3.414 -    fun iter j remaining_max thres rel_const_tab hopeless hopeful =
   3.415 -      let
   3.416 -        fun relevant [] _ [] =
   3.417 -            (* Nothing has been added this iteration. *)
   3.418 -            if j = 0 andalso thres >= ridiculous_threshold then
   3.419 -              (* First iteration? Try again. *)
   3.420 -              iter 0 max_facts (thres / threshold_divisor) rel_const_tab
   3.421 -                   hopeless hopeful
   3.422 -            else
   3.423 -              []
   3.424 -          | relevant candidates rejects [] =
   3.425 -            let
   3.426 -              val (accepts, more_rejects) =
   3.427 -                take_most_relevant ctxt max_facts remaining_max fudge candidates
   3.428 -              val rel_const_tab' =
   3.429 -                rel_const_tab
   3.430 -                |> fold (add_pconst_to_table false) (maps (snd o fst) accepts)
   3.431 -              fun is_dirty (c, _) =
   3.432 -                Symtab.lookup rel_const_tab' c <> Symtab.lookup rel_const_tab c
   3.433 -              val (hopeful_rejects, hopeless_rejects) =
   3.434 -                 (rejects @ hopeless, ([], []))
   3.435 -                 |-> fold (fn (ax as (_, consts), old_weight) =>
   3.436 -                              if exists is_dirty consts then
   3.437 -                                apfst (cons (ax, NONE))
   3.438 -                              else
   3.439 -                                apsnd (cons (ax, old_weight)))
   3.440 -                 |>> append (more_rejects
   3.441 -                             |> map (fn (ax as (_, consts), old_weight) =>
   3.442 -                                        (ax, if exists is_dirty consts then NONE
   3.443 -                                             else SOME old_weight)))
   3.444 -              val thres =
   3.445 -                1.0 - (1.0 - thres)
   3.446 -                      * Math.pow (decay, Real.fromInt (length accepts))
   3.447 -              val remaining_max = remaining_max - length accepts
   3.448 -            in
   3.449 -              trace_msg ctxt (fn () => "New or updated constants: " ^
   3.450 -                  commas (rel_const_tab' |> Symtab.dest
   3.451 -                          |> subtract (op =) (rel_const_tab |> Symtab.dest)
   3.452 -                          |> map string_for_hyper_pconst));
   3.453 -              map (fst o fst) accepts @
   3.454 -              (if remaining_max = 0 then
   3.455 -                 []
   3.456 -               else
   3.457 -                 iter (j + 1) remaining_max thres rel_const_tab'
   3.458 -                      hopeless_rejects hopeful_rejects)
   3.459 -            end
   3.460 -          | relevant candidates rejects
   3.461 -                     (((ax as (((_, stature), _), fact_consts)), cached_weight)
   3.462 -                      :: hopeful) =
   3.463 -            let
   3.464 -              val weight =
   3.465 -                case cached_weight of
   3.466 -                  SOME w => w
   3.467 -                | NONE => fact_weight fudge stature const_tab rel_const_tab
   3.468 -                                      chained_const_tab fact_consts
   3.469 -            in
   3.470 -              if weight >= thres then
   3.471 -                relevant ((ax, weight) :: candidates) rejects hopeful
   3.472 -              else
   3.473 -                relevant candidates ((ax, weight) :: rejects) hopeful
   3.474 -            end
   3.475 -        in
   3.476 -          trace_msg ctxt (fn () =>
   3.477 -              "ITERATION " ^ string_of_int j ^ ": current threshold: " ^
   3.478 -              Real.toString thres ^ ", constants: " ^
   3.479 -              commas (rel_const_tab |> Symtab.dest
   3.480 -                      |> filter (curry (op <>) [] o snd)
   3.481 -                      |> map string_for_hyper_pconst));
   3.482 -          relevant [] [] hopeful
   3.483 -        end
   3.484 -    fun uses_const s t =
   3.485 -      fold_aterms (curry (fn (Const (s', _), false) => s' = s | (_, b) => b)) t
   3.486 -                  false
   3.487 -    fun uses_const_anywhere accepts s =
   3.488 -      exists (uses_const s o prop_of o snd) accepts orelse
   3.489 -      exists (uses_const s) (concl_t :: hyp_ts)
   3.490 -    fun add_set_const_thms accepts =
   3.491 -      exists (uses_const_anywhere accepts) set_consts ? append set_thms
   3.492 -    fun insert_into_facts accepts [] = accepts
   3.493 -      | insert_into_facts accepts ths =
   3.494 -        let
   3.495 -          val add = facts |> filter (member Thm.eq_thm_prop ths o snd)
   3.496 -          val (bef, after) =
   3.497 -            accepts |> filter_out (member Thm.eq_thm_prop ths o snd)
   3.498 -                    |> take (max_facts - length add)
   3.499 -                    |> chop special_fact_index
   3.500 -        in bef @ add @ after end
   3.501 -    fun insert_special_facts accepts =
   3.502 -       (* FIXME: get rid of "ext" here once it is treated as a helper *)
   3.503 -       [] |> could_benefit_from_ext is_built_in_const accepts ? cons @{thm ext}
   3.504 -          |> add_set_const_thms accepts
   3.505 -          |> insert_into_facts accepts
   3.506 -  in
   3.507 -    facts |> map_filter (pair_consts_fact thy is_built_in_const fudge)
   3.508 -          |> iter 0 max_facts thres0 goal_const_tab []
   3.509 -          |> insert_special_facts
   3.510 -          |> tap (fn accepts => trace_msg ctxt (fn () =>
   3.511 -                      "Total relevant: " ^ string_of_int (length accepts)))
   3.512 -  end
   3.513 -
   3.514 -fun iterative_relevant_facts ctxt
   3.515 -        ({fact_thresholds = (thres0, thres1), ...} : params) prover
   3.516 -        max_facts fudge hyp_ts concl_t facts =
   3.517 -  let
   3.518 -    val thy = Proof_Context.theory_of ctxt
   3.519 -    val is_built_in_const =
   3.520 -      Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover
   3.521 -    val fudge =
   3.522 -      case fudge of
   3.523 -        SOME fudge => fudge
   3.524 -      | NONE => Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover
   3.525 -    val decay = Math.pow ((1.0 - thres1) / (1.0 - thres0),
   3.526 -                          1.0 / Real.fromInt (max_facts + 1))
   3.527 -  in
   3.528 -    trace_msg ctxt (fn () => "Considering " ^ string_of_int (length facts) ^
   3.529 -                             " facts");
   3.530 -    (if thres1 < 0.0 then
   3.531 -       facts
   3.532 -     else if thres0 > 1.0 orelse thres0 > thres1 then
   3.533 -       []
   3.534 -     else
   3.535 -       relevance_filter ctxt thres0 decay max_facts is_built_in_const fudge
   3.536 -           facts hyp_ts
   3.537 -           (concl_t |> theory_constify fudge (Context.theory_name thy)))
   3.538 -  end
   3.539 -
   3.540 -end;
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Fri Jul 20 22:19:45 2012 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,691 +0,0 @@
     4.4 -(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML
     4.5 -    Author:     Jasmin Blanchette, TU Muenchen
     4.6 -
     4.7 -Sledgehammer's machine-learning-based relevance filter (MaSh).
     4.8 -*)
     4.9 -
    4.10 -signature SLEDGEHAMMER_FILTER_MASH =
    4.11 -sig
    4.12 -  type status = ATP_Problem_Generate.status
    4.13 -  type stature = ATP_Problem_Generate.stature
    4.14 -  type fact = Sledgehammer_Fact.fact
    4.15 -  type fact_override = Sledgehammer_Fact.fact_override
    4.16 -  type params = Sledgehammer_Provers.params
    4.17 -  type relevance_fudge = Sledgehammer_Provers.relevance_fudge
    4.18 -  type prover_result = Sledgehammer_Provers.prover_result
    4.19 -
    4.20 -  val trace : bool Config.T
    4.21 -  val MaShN : string
    4.22 -  val mepoN : string
    4.23 -  val mashN : string
    4.24 -  val meshN : string
    4.25 -  val fact_filters : string list
    4.26 -  val escape_meta : string -> string
    4.27 -  val escape_metas : string list -> string
    4.28 -  val unescape_meta : string -> string
    4.29 -  val unescape_metas : string -> string list
    4.30 -  val extract_query : string -> string * string list
    4.31 -  val nickname_of : thm -> string
    4.32 -  val suggested_facts : string list -> ('a * thm) list -> ('a * thm) list
    4.33 -  val mesh_facts :
    4.34 -    int -> (('a * thm) list * ('a * thm) list) list -> ('a * thm) list
    4.35 -  val is_likely_tautology_or_too_meta : thm -> bool
    4.36 -  val theory_ord : theory * theory -> order
    4.37 -  val thm_ord : thm * thm -> order
    4.38 -  val features_of :
    4.39 -    Proof.context -> string -> theory -> status -> term list -> string list
    4.40 -  val isabelle_dependencies_of : unit Symtab.table -> thm -> string list
    4.41 -  val goal_of_thm : theory -> thm -> thm
    4.42 -  val run_prover_for_mash :
    4.43 -    Proof.context -> params -> string -> fact list -> thm -> prover_result
    4.44 -  val mash_CLEAR : Proof.context -> unit
    4.45 -  val mash_INIT :
    4.46 -    Proof.context -> bool
    4.47 -    -> (string * string list * string list * string list) list -> unit
    4.48 -  val mash_ADD :
    4.49 -    Proof.context -> bool
    4.50 -    -> (string * string list * string list * string list) list -> unit
    4.51 -  val mash_QUERY :
    4.52 -    Proof.context -> bool -> int -> string list * string list -> string list
    4.53 -  val mash_unlearn : Proof.context -> unit
    4.54 -  val mash_could_suggest_facts : unit -> bool
    4.55 -  val mash_can_suggest_facts : Proof.context -> bool
    4.56 -  val mash_suggest_facts :
    4.57 -    Proof.context -> params -> string -> int -> term list -> term
    4.58 -    -> ('a * thm) list -> ('a * thm) list * ('a * thm) list
    4.59 -  val mash_learn_thy :
    4.60 -    Proof.context -> params -> theory -> Time.time -> fact list -> string
    4.61 -  val mash_learn_proof :
    4.62 -    Proof.context -> params -> term -> ('a * thm) list -> thm list -> unit
    4.63 -  val relevant_facts :
    4.64 -    Proof.context -> params -> string -> int -> fact_override -> term list
    4.65 -    -> term -> fact list -> fact list
    4.66 -  val kill_learners : unit -> unit
    4.67 -  val running_learners : unit -> unit
    4.68 -end;
    4.69 -
    4.70 -structure Sledgehammer_Filter_MaSh : SLEDGEHAMMER_FILTER_MASH =
    4.71 -struct
    4.72 -
    4.73 -open ATP_Util
    4.74 -open ATP_Problem_Generate
    4.75 -open Sledgehammer_Util
    4.76 -open Sledgehammer_Fact
    4.77 -open Sledgehammer_Filter_Iter
    4.78 -open Sledgehammer_Provers
    4.79 -open Sledgehammer_Minimize
    4.80 -
    4.81 -val trace =
    4.82 -  Attrib.setup_config_bool @{binding sledgehammer_filter_mash_trace} (K false)
    4.83 -fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
    4.84 -
    4.85 -val MaShN = "MaSh"
    4.86 -
    4.87 -val mepoN = "mepo"
    4.88 -val mashN = "mash"
    4.89 -val meshN = "mesh"
    4.90 -
    4.91 -val fact_filters = [meshN, mepoN, mashN]
    4.92 -
    4.93 -fun mash_home () = getenv "MASH_HOME"
    4.94 -fun mash_state_dir () =
    4.95 -  getenv "ISABELLE_HOME_USER" ^ "/mash"
    4.96 -  |> tap (Isabelle_System.mkdir o Path.explode)
    4.97 -fun mash_state_path () = mash_state_dir () ^ "/state" |> Path.explode
    4.98 -
    4.99 -
   4.100 -(*** Isabelle helpers ***)
   4.101 -
   4.102 -fun meta_char c =
   4.103 -  if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse
   4.104 -     c = #")" orelse c = #"," then
   4.105 -    String.str c
   4.106 -  else
   4.107 -    (* fixed width, in case more digits follow *)
   4.108 -    "\\" ^ stringN_of_int 3 (Char.ord c)
   4.109 -
   4.110 -fun unmeta_chars accum [] = String.implode (rev accum)
   4.111 -  | unmeta_chars accum (#"\\" :: d1 :: d2 :: d3 :: cs) =
   4.112 -    (case Int.fromString (String.implode [d1, d2, d3]) of
   4.113 -       SOME n => unmeta_chars (Char.chr n :: accum) cs
   4.114 -     | NONE => "" (* error *))
   4.115 -  | unmeta_chars _ (#"\\" :: _) = "" (* error *)
   4.116 -  | unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs
   4.117 -
   4.118 -val escape_meta = String.translate meta_char
   4.119 -val escape_metas = map escape_meta #> space_implode " "
   4.120 -val unescape_meta = String.explode #> unmeta_chars []
   4.121 -val unescape_metas =
   4.122 -  space_explode " " #> filter_out (curry (op =) "") #> map unescape_meta
   4.123 -
   4.124 -fun extract_query line =
   4.125 -  case space_explode ":" line of
   4.126 -    [goal_name, suggs] => (unescape_meta goal_name, unescape_metas suggs)
   4.127 -  | _ => ("", [])
   4.128 -
   4.129 -fun parent_of_local_thm th =
   4.130 -  let
   4.131 -    val thy = th |> Thm.theory_of_thm
   4.132 -    val facts = thy |> Global_Theory.facts_of
   4.133 -    val space = facts |> Facts.space_of
   4.134 -    fun id_of s = #id (Name_Space.the_entry space s)
   4.135 -    fun max_id (s', _) (s, id) =
   4.136 -      let val id' = id_of s' in if id > id' then (s, id) else (s', id') end
   4.137 -  in ("", ~1) |> Facts.fold_static max_id facts |> fst end
   4.138 -
   4.139 -val local_prefix = "local" ^ Long_Name.separator
   4.140 -
   4.141 -fun nickname_of th =
   4.142 -  let val hint = Thm.get_name_hint th in
   4.143 -    (* FIXME: There must be a better way to detect local facts. *)
   4.144 -    case try (unprefix local_prefix) hint of
   4.145 -      SOME suff =>
   4.146 -      parent_of_local_thm th ^ Long_Name.separator ^ Long_Name.separator ^ suff
   4.147 -    | NONE => hint
   4.148 -  end
   4.149 -
   4.150 -fun suggested_facts suggs facts =
   4.151 -  let
   4.152 -    fun add_fact (fact as (_, th)) = Symtab.default (nickname_of th, fact)
   4.153 -    val tab = Symtab.empty |> fold add_fact facts
   4.154 -  in map_filter (Symtab.lookup tab) suggs end
   4.155 -
   4.156 -(* Ad hoc score function roughly based on Blanchette's Ringberg 2011 data. *)
   4.157 -fun score x = Math.pow (1.5, 15.5 - 0.05 * Real.fromInt x) + 15.0
   4.158 -
   4.159 -fun sum_sq_avg [] = 0
   4.160 -  | sum_sq_avg xs =
   4.161 -    Real.ceil (100000.0 * fold (curry (op +) o score) xs 0.0) div length xs
   4.162 -
   4.163 -fun mesh_facts max_facts [(selected, unknown)] =
   4.164 -    take max_facts selected @ take (max_facts - length selected) unknown
   4.165 -  | mesh_facts max_facts mess =
   4.166 -    let
   4.167 -      val mess = mess |> map (apfst (`length))
   4.168 -      val fact_eq = Thm.eq_thm o pairself snd
   4.169 -      fun score_in fact ((sel_len, sels), unks) =
   4.170 -        case find_index (curry fact_eq fact) sels of
   4.171 -          ~1 => (case find_index (curry fact_eq fact) unks of
   4.172 -                   ~1 => SOME sel_len
   4.173 -                 | _ => NONE)
   4.174 -        | j => SOME j
   4.175 -      fun score_of fact = mess |> map_filter (score_in fact) |> sum_sq_avg
   4.176 -      val facts = fold (union fact_eq o take max_facts o snd o fst) mess []
   4.177 -    in
   4.178 -      facts |> map (`score_of) |> sort (int_ord o swap o pairself fst)
   4.179 -            |> map snd |> take max_facts
   4.180 -    end
   4.181 -
   4.182 -val thy_feature_prefix = "y_"
   4.183 -
   4.184 -val thy_feature_name_of = prefix thy_feature_prefix
   4.185 -val const_name_of = prefix const_prefix
   4.186 -val type_name_of = prefix type_const_prefix
   4.187 -val class_name_of = prefix class_prefix
   4.188 -
   4.189 -fun is_likely_tautology_or_too_meta th =
   4.190 -  let
   4.191 -    val is_boring_const = member (op =) atp_widely_irrelevant_consts
   4.192 -    fun is_boring_bool t =
   4.193 -      not (exists_Const (not o is_boring_const o fst) t) orelse
   4.194 -      exists_type (exists_subtype (curry (op =) @{typ prop})) t
   4.195 -    fun is_boring_prop (@{const Trueprop} $ t) = is_boring_bool t
   4.196 -      | is_boring_prop (@{const "==>"} $ t $ u) =
   4.197 -        is_boring_prop t andalso is_boring_prop u
   4.198 -      | is_boring_prop (Const (@{const_name all}, _) $ (Abs (_, _, t)) $ u) =
   4.199 -        is_boring_prop t andalso is_boring_prop u
   4.200 -      | is_boring_prop (Const (@{const_name "=="}, _) $ t $ u) =
   4.201 -        is_boring_bool t andalso is_boring_bool u
   4.202 -      | is_boring_prop _ = true
   4.203 -  in
   4.204 -    is_boring_prop (prop_of th) andalso not (Thm.eq_thm_prop (@{thm ext}, th))
   4.205 -  end
   4.206 -
   4.207 -fun theory_ord p =
   4.208 -  if Theory.eq_thy p then
   4.209 -    EQUAL
   4.210 -  else if Theory.subthy p then
   4.211 -    LESS
   4.212 -  else if Theory.subthy (swap p) then
   4.213 -    GREATER
   4.214 -  else case int_ord (pairself (length o Theory.ancestors_of) p) of
   4.215 -    EQUAL => string_ord (pairself Context.theory_name p)
   4.216 -  | order => order
   4.217 -
   4.218 -val thm_ord = theory_ord o pairself theory_of_thm
   4.219 -
   4.220 -val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
   4.221 -
   4.222 -fun interesting_terms_types_and_classes ctxt prover term_max_depth
   4.223 -                                        type_max_depth ts =
   4.224 -  let
   4.225 -    fun is_bad_const (x as (s, _)) args =
   4.226 -      member (op =) atp_logical_consts s orelse
   4.227 -      fst (is_built_in_const_for_prover ctxt prover x args)
   4.228 -    fun add_classes @{sort type} = I
   4.229 -      | add_classes S = union (op =) (map class_name_of S)
   4.230 -    fun do_add_type (Type (s, Ts)) =
   4.231 -        (not (member (op =) bad_types s) ? insert (op =) (type_name_of s))
   4.232 -        #> fold do_add_type Ts
   4.233 -      | do_add_type (TFree (_, S)) = add_classes S
   4.234 -      | do_add_type (TVar (_, S)) = add_classes S
   4.235 -    fun add_type T = type_max_depth >= 0 ? do_add_type T
   4.236 -    fun mk_app s args =
   4.237 -      if member (op <>) args "" then s ^ "(" ^ space_implode "," args ^ ")"
   4.238 -      else s
   4.239 -    fun patternify ~1 _ = ""
   4.240 -      | patternify depth t =
   4.241 -        case strip_comb t of
   4.242 -          (Const (s, _), args) =>
   4.243 -          mk_app (const_name_of s) (map (patternify (depth - 1)) args)
   4.244 -        | _ => ""
   4.245 -    fun add_term_patterns ~1 _ = I
   4.246 -      | add_term_patterns depth t =
   4.247 -        insert (op =) (patternify depth t)
   4.248 -        #> add_term_patterns (depth - 1) t
   4.249 -    val add_term = add_term_patterns term_max_depth
   4.250 -    fun add_patterns t =
   4.251 -      let val (head, args) = strip_comb t in
   4.252 -        (case head of
   4.253 -           Const (x as (_, T)) =>
   4.254 -           not (is_bad_const x args) ? (add_term t #> add_type T)
   4.255 -         | Free (_, T) => add_type T
   4.256 -         | Var (_, T) => add_type T
   4.257 -         | Abs (_, T, body) => add_type T #> add_patterns body
   4.258 -         | _ => I)
   4.259 -        #> fold add_patterns args
   4.260 -      end
   4.261 -  in [] |> fold add_patterns ts end
   4.262 -
   4.263 -fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1})
   4.264 -
   4.265 -val term_max_depth = 1
   4.266 -val type_max_depth = 1
   4.267 -
   4.268 -(* TODO: Generate type classes for types? *)
   4.269 -fun features_of ctxt prover thy status ts =
   4.270 -  thy_feature_name_of (Context.theory_name thy) ::
   4.271 -  interesting_terms_types_and_classes ctxt prover term_max_depth type_max_depth
   4.272 -                                      ts
   4.273 -  |> forall is_lambda_free ts ? cons "no_lams"
   4.274 -  |> forall (not o exists_Const is_exists) ts ? cons "no_skos"
   4.275 -  |> (case status of
   4.276 -        General => I
   4.277 -      | Induction => cons "induction"
   4.278 -      | Intro => cons "intro"
   4.279 -      | Inductive => cons "inductive"
   4.280 -      | Elim => cons "elim"
   4.281 -      | Simp => cons "simp"
   4.282 -      | Def => cons "def")
   4.283 -
   4.284 -fun isabelle_dependencies_of all_facts = thms_in_proof (SOME all_facts)
   4.285 -
   4.286 -val freezeT = Type.legacy_freeze_type
   4.287 -
   4.288 -fun freeze (t $ u) = freeze t $ freeze u
   4.289 -  | freeze (Abs (s, T, t)) = Abs (s, freezeT T, freeze t)
   4.290 -  | freeze (Var ((s, _), T)) = Free (s, freezeT T)
   4.291 -  | freeze (Const (s, T)) = Const (s, freezeT T)
   4.292 -  | freeze (Free (s, T)) = Free (s, freezeT T)
   4.293 -  | freeze t = t
   4.294 -
   4.295 -fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init
   4.296 -
   4.297 -fun run_prover_for_mash ctxt params prover facts goal =
   4.298 -  let
   4.299 -    val problem =
   4.300 -      {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,
   4.301 -       facts = facts |> map (apfst (apfst (fn name => name ())))
   4.302 -                     |> map Untranslated_Fact}
   4.303 -    val prover = get_minimizing_prover ctxt Normal (K ()) prover
   4.304 -  in prover params (K (K (K ""))) problem end
   4.305 -
   4.306 -
   4.307 -(*** Low-level communication with MaSh ***)
   4.308 -
   4.309 -fun write_file (xs, f) file =
   4.310 -  let val path = Path.explode file in
   4.311 -    File.write path "";
   4.312 -    xs |> chunk_list 500
   4.313 -       |> List.app (File.append path o space_implode "" o map f)
   4.314 -  end
   4.315 -
   4.316 -fun mash_info overlord =
   4.317 -  if overlord then (getenv "ISABELLE_HOME_USER", "")
   4.318 -  else (getenv "ISABELLE_TMP", serial_string ())
   4.319 -
   4.320 -fun run_mash ctxt overlord (temp_dir, serial) core =
   4.321 -  let
   4.322 -    val log_file = temp_dir ^ "/mash_log" ^ serial
   4.323 -    val err_file = temp_dir ^ "/mash_err" ^ serial
   4.324 -    val command =
   4.325 -      mash_home () ^ "/mash.py --quiet --outputDir " ^ mash_state_dir () ^
   4.326 -      " --log " ^ log_file ^ " " ^ core ^ " 2>&1 > " ^ err_file
   4.327 -  in
   4.328 -    trace_msg ctxt (fn () => "Running " ^ command);
   4.329 -    write_file ([], K "") log_file;
   4.330 -    write_file ([], K "") err_file;
   4.331 -    Isabelle_System.bash command;
   4.332 -    if overlord then ()
   4.333 -    else (map (File.rm o Path.explode) [log_file, err_file]; ());
   4.334 -    trace_msg ctxt (K "Done")
   4.335 -  end
   4.336 -
   4.337 -(* TODO: Eliminate code once "mash.py" handles sequences of ADD commands as fast
   4.338 -   as a single INIT. *)
   4.339 -fun run_mash_init ctxt overlord write_access write_feats write_deps =
   4.340 -  let
   4.341 -    val info as (temp_dir, serial) = mash_info overlord
   4.342 -    val in_dir = temp_dir ^ "/mash_init" ^ serial
   4.343 -    val in_dir_path = in_dir |> Path.explode |> tap Isabelle_System.mkdir
   4.344 -  in
   4.345 -    write_file write_access (in_dir ^ "/mash_accessibility");
   4.346 -    write_file write_feats (in_dir ^ "/mash_features");
   4.347 -    write_file write_deps (in_dir ^ "/mash_dependencies");
   4.348 -    run_mash ctxt overlord info ("--init --inputDir " ^ in_dir);
   4.349 -    (* FIXME: temporary hack *)
   4.350 -    if overlord then ()
   4.351 -    else (Isabelle_System.bash ("rm -r -f " ^ File.shell_path in_dir_path); ())
   4.352 -  end
   4.353 -
   4.354 -fun run_mash_commands ctxt overlord save max_suggs write_cmds read_suggs =
   4.355 -  let
   4.356 -    val info as (temp_dir, serial) = mash_info overlord
   4.357 -    val sugg_file = temp_dir ^ "/mash_suggs" ^ serial
   4.358 -    val cmd_file = temp_dir ^ "/mash_commands" ^ serial
   4.359 -  in
   4.360 -    write_file ([], K "") sugg_file;
   4.361 -    write_file write_cmds cmd_file;
   4.362 -    run_mash ctxt overlord info
   4.363 -             ("--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^
   4.364 -              " --numberOfPredictions " ^ string_of_int max_suggs ^
   4.365 -              (if save then " --saveModel" else ""));
   4.366 -    read_suggs (fn () => File.read_lines (Path.explode sugg_file))
   4.367 -    |> tap (fn _ =>
   4.368 -               if overlord then ()
   4.369 -               else (map (File.rm o Path.explode) [sugg_file, cmd_file]; ()))
   4.370 -  end
   4.371 -
   4.372 -fun str_of_update (name, parents, feats, deps) =
   4.373 -  "! " ^ escape_meta name ^ ": " ^ escape_metas parents ^ "; " ^
   4.374 -  escape_metas feats ^ "; " ^ escape_metas deps ^ "\n"
   4.375 -
   4.376 -fun str_of_query (parents, feats) =
   4.377 -  "? " ^ escape_metas parents ^ "; " ^ escape_metas feats
   4.378 -
   4.379 -fun init_str_of_update get (upd as (name, _, _, _)) =
   4.380 -  escape_meta name ^ ": " ^ escape_metas (get upd) ^ "\n"
   4.381 -
   4.382 -fun mash_CLEAR ctxt =
   4.383 -  let val path = mash_state_dir () |> Path.explode in
   4.384 -    trace_msg ctxt (K "MaSh CLEAR");
   4.385 -    File.fold_dir (fn file => fn () =>
   4.386 -                      File.rm (Path.append path (Path.basic file)))
   4.387 -                  path ()
   4.388 -  end
   4.389 -
   4.390 -fun mash_INIT ctxt _ [] = mash_CLEAR ctxt
   4.391 -  | mash_INIT ctxt overlord upds =
   4.392 -    (trace_msg ctxt (fn () => "MaSh INIT " ^
   4.393 -         elide_string 1000 (space_implode " " (map #1 upds)));
   4.394 -     run_mash_init ctxt overlord (upds, init_str_of_update #2)
   4.395 -                   (upds, init_str_of_update #3) (upds, init_str_of_update #4))
   4.396 -
   4.397 -fun mash_ADD _ _ [] = ()
   4.398 -  | mash_ADD ctxt overlord upds =
   4.399 -    (trace_msg ctxt (fn () => "MaSh ADD " ^
   4.400 -         elide_string 1000 (space_implode " " (map #1 upds)));
   4.401 -     run_mash_commands ctxt overlord true 0 (upds, str_of_update) (K ()))
   4.402 -
   4.403 -fun mash_QUERY ctxt overlord max_suggs (query as (_, feats)) =
   4.404 -  (trace_msg ctxt (fn () => "MaSh QUERY " ^ space_implode " " feats);
   4.405 -   run_mash_commands ctxt overlord false max_suggs
   4.406 -       ([query], str_of_query)
   4.407 -       (fn suggs => snd (extract_query (List.last (suggs ()))))
   4.408 -   handle List.Empty => [])
   4.409 -
   4.410 -
   4.411 -(*** High-level communication with MaSh ***)
   4.412 -
   4.413 -fun try_graph ctxt when def f =
   4.414 -  f ()
   4.415 -  handle Graph.CYCLES (cycle :: _) =>
   4.416 -         (trace_msg ctxt (fn () =>
   4.417 -              "Cycle involving " ^ commas cycle ^ " when " ^ when); def)
   4.418 -       | Graph.UNDEF name =>
   4.419 -         (trace_msg ctxt (fn () =>
   4.420 -              "Unknown fact " ^ quote name ^ " when " ^ when); def)
   4.421 -
   4.422 -type mash_state =
   4.423 -  {thys : bool Symtab.table,
   4.424 -   fact_graph : unit Graph.T}
   4.425 -
   4.426 -val empty_state = {thys = Symtab.empty, fact_graph = Graph.empty}
   4.427 -
   4.428 -local
   4.429 -
   4.430 -fun mash_load _ (state as (true, _)) = state
   4.431 -  | mash_load ctxt _ =
   4.432 -    let val path = mash_state_path () in
   4.433 -      (true,
   4.434 -       case try File.read_lines path of
   4.435 -         SOME (comp_thys :: incomp_thys :: fact_lines) =>
   4.436 -         let
   4.437 -           fun add_thy comp thy = Symtab.update (thy, comp)
   4.438 -           fun add_edge_to name parent =
   4.439 -             Graph.default_node (parent, ())
   4.440 -             #> Graph.add_edge (parent, name)
   4.441 -           fun add_fact_line line =
   4.442 -             case extract_query line of
   4.443 -               ("", _) => I (* shouldn't happen *)
   4.444 -             | (name, parents) =>
   4.445 -               Graph.default_node (name, ())
   4.446 -               #> fold (add_edge_to name) parents
   4.447 -           val thys =
   4.448 -             Symtab.empty |> fold (add_thy true) (unescape_metas comp_thys)
   4.449 -                          |> fold (add_thy false) (unescape_metas incomp_thys)
   4.450 -           val fact_graph =
   4.451 -             try_graph ctxt "loading state" Graph.empty (fn () =>
   4.452 -                 Graph.empty |> fold add_fact_line fact_lines)
   4.453 -         in {thys = thys, fact_graph = fact_graph} end
   4.454 -       | _ => empty_state)
   4.455 -    end
   4.456 -
   4.457 -fun mash_save ({thys, fact_graph, ...} : mash_state) =
   4.458 -  let
   4.459 -    val path = mash_state_path ()
   4.460 -    val thys = Symtab.dest thys
   4.461 -    val line_for_thys = escape_metas o AList.find (op =) thys
   4.462 -    fun fact_line_for name parents =
   4.463 -      escape_meta name ^ ": " ^ escape_metas parents
   4.464 -    val append_fact = File.append path o suffix "\n" oo fact_line_for
   4.465 -  in
   4.466 -    File.write path (line_for_thys true ^ "\n" ^ line_for_thys false ^ "\n");
   4.467 -    Graph.fold (fn (name, ((), (parents, _))) => fn () =>
   4.468 -                   append_fact name (Graph.Keys.dest parents))
   4.469 -        fact_graph ()
   4.470 -  end
   4.471 -
   4.472 -val global_state =
   4.473 -  Synchronized.var "Sledgehammer_Filter_MaSh.global_state" (false, empty_state)
   4.474 -
   4.475 -in
   4.476 -
   4.477 -fun mash_map ctxt f =
   4.478 -  Synchronized.change global_state (mash_load ctxt ##> (f #> tap mash_save))
   4.479 -
   4.480 -fun mash_get ctxt =
   4.481 -  Synchronized.change_result global_state (mash_load ctxt #> `snd)
   4.482 -
   4.483 -fun mash_unlearn ctxt =
   4.484 -  Synchronized.change global_state (fn _ =>
   4.485 -      (mash_CLEAR ctxt; File.write (mash_state_path ()) "";
   4.486 -       (true, empty_state)))
   4.487 -
   4.488 -end
   4.489 -
   4.490 -fun mash_could_suggest_facts () = mash_home () <> ""
   4.491 -fun mash_can_suggest_facts ctxt =
   4.492 -  not (Graph.is_empty (#fact_graph (mash_get ctxt)))
   4.493 -
   4.494 -fun parents_wrt_facts facts fact_graph =
   4.495 -  let
   4.496 -    val facts = [] |> fold (cons o nickname_of o snd) facts
   4.497 -    val tab = Symtab.empty |> fold (fn name => Symtab.update (name, ())) facts
   4.498 -    fun insert_not_seen seen name =
   4.499 -      not (member (op =) seen name) ? insert (op =) name
   4.500 -    fun parents_of _ parents [] = parents
   4.501 -      | parents_of seen parents (name :: names) =
   4.502 -        if Symtab.defined tab name then
   4.503 -          parents_of (name :: seen) (name :: parents) names
   4.504 -        else
   4.505 -          parents_of (name :: seen) parents
   4.506 -                     (Graph.Keys.fold (insert_not_seen seen)
   4.507 -                                      (Graph.imm_preds fact_graph name) names)
   4.508 -  in parents_of [] [] (Graph.maximals fact_graph) end
   4.509 -
   4.510 -(* Generate more suggestions than requested, because some might be thrown out
   4.511 -   later for various reasons and "meshing" gives better results with some
   4.512 -   slack. *)
   4.513 -fun max_suggs_of max_facts = max_facts + Int.min (200, max_facts)
   4.514 -
   4.515 -fun is_fact_in_graph fact_graph (_, th) =
   4.516 -  can (Graph.get_node fact_graph) (nickname_of th)
   4.517 -
   4.518 -fun mash_suggest_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
   4.519 -                       concl_t facts =
   4.520 -  let
   4.521 -    val thy = Proof_Context.theory_of ctxt
   4.522 -    val fact_graph = #fact_graph (mash_get ctxt)
   4.523 -    val parents = parents_wrt_facts facts fact_graph
   4.524 -    val feats = features_of ctxt prover thy General (concl_t :: hyp_ts)
   4.525 -    val suggs =
   4.526 -      if Graph.is_empty fact_graph then []
   4.527 -      else mash_QUERY ctxt overlord (max_suggs_of max_facts) (parents, feats)
   4.528 -    val selected = facts |> suggested_facts suggs
   4.529 -    val unknown = facts |> filter_out (is_fact_in_graph fact_graph)
   4.530 -  in (selected, unknown) end
   4.531 -
   4.532 -fun add_thys_for thy =
   4.533 -  let fun add comp thy = Symtab.update (Context.theory_name thy, comp) in
   4.534 -    add false thy #> fold (add true) (Theory.ancestors_of thy)
   4.535 -  end
   4.536 -
   4.537 -fun update_fact_graph ctxt (name, parents, feats, deps) (upds, graph) =
   4.538 -  let
   4.539 -    fun maybe_add_from from (accum as (parents, graph)) =
   4.540 -      try_graph ctxt "updating graph" accum (fn () =>
   4.541 -          (from :: parents, Graph.add_edge_acyclic (from, name) graph))
   4.542 -    val graph = graph |> Graph.default_node (name, ())
   4.543 -    val (parents, graph) = ([], graph) |> fold maybe_add_from parents
   4.544 -    val (deps, graph) = ([], graph) |> fold maybe_add_from deps
   4.545 -  in ((name, parents, feats, deps) :: upds, graph) end
   4.546 -
   4.547 -val pass1_learn_timeout_factor = 0.5
   4.548 -
   4.549 -(* Too many dependencies is a sign that a decision procedure is at work. There
   4.550 -   isn't much too learn from such proofs. *)
   4.551 -val max_dependencies = 10
   4.552 -
   4.553 -(* The timeout is understood in a very slack fashion. *)
   4.554 -fun mash_learn_thy ctxt ({provers, verbose, overlord, ...} : params) thy timeout
   4.555 -                   facts =
   4.556 -  let
   4.557 -    val timer = Timer.startRealTimer ()
   4.558 -    val prover = hd provers
   4.559 -    fun timed_out frac =
   4.560 -      Time.> (Timer.checkRealTimer timer, time_mult frac timeout)
   4.561 -    val {fact_graph, ...} = mash_get ctxt
   4.562 -    val new_facts =
   4.563 -      facts |> filter_out (is_fact_in_graph fact_graph)
   4.564 -            |> sort (thm_ord o pairself snd)
   4.565 -  in
   4.566 -    if null new_facts then
   4.567 -      ""
   4.568 -    else
   4.569 -      let
   4.570 -        val ths = facts |> map snd
   4.571 -        val all_names =
   4.572 -          ths |> filter_out is_likely_tautology_or_too_meta
   4.573 -              |> map (rpair () o nickname_of)
   4.574 -              |> Symtab.make
   4.575 -        fun trim_deps deps = if length deps > max_dependencies then [] else deps
   4.576 -        fun do_fact _ (accum as (_, true)) = accum
   4.577 -          | do_fact ((_, (_, status)), th) ((parents, upds), false) =
   4.578 -            let
   4.579 -              val name = nickname_of th
   4.580 -              val feats =
   4.581 -                features_of ctxt prover (theory_of_thm th) status [prop_of th]
   4.582 -              val deps = isabelle_dependencies_of all_names th |> trim_deps
   4.583 -              val upd = (name, parents, feats, deps)
   4.584 -            in (([name], upd :: upds), timed_out pass1_learn_timeout_factor) end
   4.585 -        val parents = parents_wrt_facts facts fact_graph
   4.586 -        val ((_, upds), _) =
   4.587 -          ((parents, []), false) |> fold do_fact new_facts |>> apsnd rev
   4.588 -        val n = length upds
   4.589 -        fun trans {thys, fact_graph} =
   4.590 -          let
   4.591 -            val mash_INIT_or_ADD =
   4.592 -              if Graph.is_empty fact_graph then mash_INIT else mash_ADD
   4.593 -            val (upds, fact_graph) =
   4.594 -              ([], fact_graph) |> fold (update_fact_graph ctxt) upds
   4.595 -          in
   4.596 -            (mash_INIT_or_ADD ctxt overlord (rev upds);
   4.597 -             {thys = thys |> add_thys_for thy,
   4.598 -              fact_graph = fact_graph})
   4.599 -          end
   4.600 -      in
   4.601 -        mash_map ctxt trans;
   4.602 -        if verbose then
   4.603 -          "Processed " ^ string_of_int n ^ " proof" ^ plural_s n ^
   4.604 -          (if verbose then
   4.605 -             " in " ^ string_from_time (Timer.checkRealTimer timer)
   4.606 -           else
   4.607 -             "") ^ "."
   4.608 -        else
   4.609 -          ""
   4.610 -      end
   4.611 -  end
   4.612 -
   4.613 -fun mash_learn_proof ctxt ({provers, overlord, ...} : params) t facts used_ths =
   4.614 -  let
   4.615 -    val thy = Proof_Context.theory_of ctxt
   4.616 -    val prover = hd provers
   4.617 -    val name = ATP_Util.timestamp () ^ " " ^ serial_string () (* fresh enough *)
   4.618 -    val feats = features_of ctxt prover thy General [t]
   4.619 -    val deps = used_ths |> map nickname_of
   4.620 -  in
   4.621 -    mash_map ctxt (fn {thys, fact_graph} =>
   4.622 -        let
   4.623 -          val parents = parents_wrt_facts facts fact_graph
   4.624 -          val upds = [(name, parents, feats, deps)]
   4.625 -          val (upds, fact_graph) =
   4.626 -            ([], fact_graph) |> fold (update_fact_graph ctxt) upds
   4.627 -        in
   4.628 -          mash_ADD ctxt overlord upds;
   4.629 -          {thys = thys, fact_graph = fact_graph}
   4.630 -        end)
   4.631 -  end
   4.632 -
   4.633 -(* The threshold should be large enough so that MaSh doesn't kick in for Auto
   4.634 -   Sledgehammer and Try. *)
   4.635 -val min_secs_for_learning = 15
   4.636 -val learn_timeout_factor = 2.0
   4.637 -
   4.638 -fun relevant_facts ctxt (params as {learn, fact_filter, timeout, ...}) prover
   4.639 -        max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts =
   4.640 -  if not (subset (op =) (the_list fact_filter, fact_filters)) then
   4.641 -    error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".")
   4.642 -  else if only then
   4.643 -    facts
   4.644 -  else if max_facts <= 0 orelse null facts then
   4.645 -    []
   4.646 -  else
   4.647 -    let
   4.648 -      val thy = Proof_Context.theory_of ctxt
   4.649 -      fun maybe_learn () =
   4.650 -        if not learn orelse Async_Manager.has_running_threads MaShN then
   4.651 -          ()
   4.652 -        else if Time.toSeconds timeout >= min_secs_for_learning then
   4.653 -          let
   4.654 -            val soft_timeout = time_mult learn_timeout_factor timeout
   4.655 -            val hard_timeout = time_mult 4.0 soft_timeout
   4.656 -            val birth_time = Time.now ()
   4.657 -            val death_time = Time.+ (birth_time, hard_timeout)
   4.658 -            val desc = ("machine learner for Sledgehammer", "")
   4.659 -          in
   4.660 -            Async_Manager.launch MaShN birth_time death_time desc
   4.661 -                (fn () =>
   4.662 -                    (true, mash_learn_thy ctxt params thy soft_timeout facts))
   4.663 -          end
   4.664 -        else
   4.665 -          ()
   4.666 -      val fact_filter =
   4.667 -        case fact_filter of
   4.668 -          SOME ff => (() |> ff <> mepoN ? maybe_learn; ff)
   4.669 -        | NONE =>
   4.670 -          if mash_can_suggest_facts ctxt then (maybe_learn (); meshN)
   4.671 -          else if mash_could_suggest_facts () then (maybe_learn (); mepoN)
   4.672 -          else mepoN
   4.673 -      val add_ths = Attrib.eval_thms ctxt add
   4.674 -      fun prepend_facts ths accepts =
   4.675 -        ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @
   4.676 -         (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)))
   4.677 -        |> take max_facts
   4.678 -      fun iter () =
   4.679 -        iterative_relevant_facts ctxt params prover max_facts NONE hyp_ts
   4.680 -                                 concl_t facts
   4.681 -      fun mash () =
   4.682 -        mash_suggest_facts ctxt params prover max_facts hyp_ts concl_t facts
   4.683 -      val mess =
   4.684 -        [] |> (if fact_filter <> mashN then cons (iter (), []) else I)
   4.685 -           |> (if fact_filter <> mepoN then cons (mash ()) else I)
   4.686 -    in
   4.687 -      mesh_facts max_facts mess
   4.688 -      |> not (null add_ths) ? prepend_facts add_ths
   4.689 -    end
   4.690 -
   4.691 -fun kill_learners () = Async_Manager.kill_threads MaShN "learner"
   4.692 -fun running_learners () = Async_Manager.running_threads MaShN "learner"
   4.693 -
   4.694 -end;
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:45 2012 +0200
     5.3 @@ -0,0 +1,691 @@
     5.4 +(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_mash.ML
     5.5 +    Author:     Jasmin Blanchette, TU Muenchen
     5.6 +
     5.7 +Sledgehammer's machine-learning-based relevance filter (MaSh).
     5.8 +*)
     5.9 +
    5.10 +signature SLEDGEHAMMER_FILTER_MASH =
    5.11 +sig
    5.12 +  type status = ATP_Problem_Generate.status
    5.13 +  type stature = ATP_Problem_Generate.stature
    5.14 +  type fact = Sledgehammer_Fact.fact
    5.15 +  type fact_override = Sledgehammer_Fact.fact_override
    5.16 +  type params = Sledgehammer_Provers.params
    5.17 +  type relevance_fudge = Sledgehammer_Provers.relevance_fudge
    5.18 +  type prover_result = Sledgehammer_Provers.prover_result
    5.19 +
    5.20 +  val trace : bool Config.T
    5.21 +  val MaShN : string
    5.22 +  val mepoN : string
    5.23 +  val mashN : string
    5.24 +  val meshN : string
    5.25 +  val fact_filters : string list
    5.26 +  val escape_meta : string -> string
    5.27 +  val escape_metas : string list -> string
    5.28 +  val unescape_meta : string -> string
    5.29 +  val unescape_metas : string -> string list
    5.30 +  val extract_query : string -> string * string list
    5.31 +  val nickname_of : thm -> string
    5.32 +  val suggested_facts : string list -> ('a * thm) list -> ('a * thm) list
    5.33 +  val mesh_facts :
    5.34 +    int -> (('a * thm) list * ('a * thm) list) list -> ('a * thm) list
    5.35 +  val is_likely_tautology_or_too_meta : thm -> bool
    5.36 +  val theory_ord : theory * theory -> order
    5.37 +  val thm_ord : thm * thm -> order
    5.38 +  val features_of :
    5.39 +    Proof.context -> string -> theory -> status -> term list -> string list
    5.40 +  val isabelle_dependencies_of : unit Symtab.table -> thm -> string list
    5.41 +  val goal_of_thm : theory -> thm -> thm
    5.42 +  val run_prover_for_mash :
    5.43 +    Proof.context -> params -> string -> fact list -> thm -> prover_result
    5.44 +  val mash_CLEAR : Proof.context -> unit
    5.45 +  val mash_INIT :
    5.46 +    Proof.context -> bool
    5.47 +    -> (string * string list * string list * string list) list -> unit
    5.48 +  val mash_ADD :
    5.49 +    Proof.context -> bool
    5.50 +    -> (string * string list * string list * string list) list -> unit
    5.51 +  val mash_QUERY :
    5.52 +    Proof.context -> bool -> int -> string list * string list -> string list
    5.53 +  val mash_unlearn : Proof.context -> unit
    5.54 +  val mash_could_suggest_facts : unit -> bool
    5.55 +  val mash_can_suggest_facts : Proof.context -> bool
    5.56 +  val mash_suggest_facts :
    5.57 +    Proof.context -> params -> string -> int -> term list -> term
    5.58 +    -> ('a * thm) list -> ('a * thm) list * ('a * thm) list
    5.59 +  val mash_learn_thy :
    5.60 +    Proof.context -> params -> theory -> Time.time -> fact list -> string
    5.61 +  val mash_learn_proof :
    5.62 +    Proof.context -> params -> term -> ('a * thm) list -> thm list -> unit
    5.63 +  val relevant_facts :
    5.64 +    Proof.context -> params -> string -> int -> fact_override -> term list
    5.65 +    -> term -> fact list -> fact list
    5.66 +  val kill_learners : unit -> unit
    5.67 +  val running_learners : unit -> unit
    5.68 +end;
    5.69 +
    5.70 +structure Sledgehammer_Filter_MaSh : SLEDGEHAMMER_FILTER_MASH =
    5.71 +struct
    5.72 +
    5.73 +open ATP_Util
    5.74 +open ATP_Problem_Generate
    5.75 +open Sledgehammer_Util
    5.76 +open Sledgehammer_Fact
    5.77 +open Sledgehammer_Filter_Iter
    5.78 +open Sledgehammer_Provers
    5.79 +open Sledgehammer_Minimize
    5.80 +
    5.81 +val trace =
    5.82 +  Attrib.setup_config_bool @{binding sledgehammer_mash_trace} (K false)
    5.83 +fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
    5.84 +
    5.85 +val MaShN = "MaSh"
    5.86 +
    5.87 +val mepoN = "mepo"
    5.88 +val mashN = "mash"
    5.89 +val meshN = "mesh"
    5.90 +
    5.91 +val fact_filters = [meshN, mepoN, mashN]
    5.92 +
    5.93 +fun mash_home () = getenv "MASH_HOME"
    5.94 +fun mash_state_dir () =
    5.95 +  getenv "ISABELLE_HOME_USER" ^ "/mash"
    5.96 +  |> tap (Isabelle_System.mkdir o Path.explode)
    5.97 +fun mash_state_path () = mash_state_dir () ^ "/state" |> Path.explode
    5.98 +
    5.99 +
   5.100 +(*** Isabelle helpers ***)
   5.101 +
   5.102 +fun meta_char c =
   5.103 +  if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse
   5.104 +     c = #")" orelse c = #"," then
   5.105 +    String.str c
   5.106 +  else
   5.107 +    (* fixed width, in case more digits follow *)
   5.108 +    "\\" ^ stringN_of_int 3 (Char.ord c)
   5.109 +
   5.110 +fun unmeta_chars accum [] = String.implode (rev accum)
   5.111 +  | unmeta_chars accum (#"\\" :: d1 :: d2 :: d3 :: cs) =
   5.112 +    (case Int.fromString (String.implode [d1, d2, d3]) of
   5.113 +       SOME n => unmeta_chars (Char.chr n :: accum) cs
   5.114 +     | NONE => "" (* error *))
   5.115 +  | unmeta_chars _ (#"\\" :: _) = "" (* error *)
   5.116 +  | unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs
   5.117 +
   5.118 +val escape_meta = String.translate meta_char
   5.119 +val escape_metas = map escape_meta #> space_implode " "
   5.120 +val unescape_meta = String.explode #> unmeta_chars []
   5.121 +val unescape_metas =
   5.122 +  space_explode " " #> filter_out (curry (op =) "") #> map unescape_meta
   5.123 +
   5.124 +fun extract_query line =
   5.125 +  case space_explode ":" line of
   5.126 +    [goal_name, suggs] => (unescape_meta goal_name, unescape_metas suggs)
   5.127 +  | _ => ("", [])
   5.128 +
   5.129 +fun parent_of_local_thm th =
   5.130 +  let
   5.131 +    val thy = th |> Thm.theory_of_thm
   5.132 +    val facts = thy |> Global_Theory.facts_of
   5.133 +    val space = facts |> Facts.space_of
   5.134 +    fun id_of s = #id (Name_Space.the_entry space s)
   5.135 +    fun max_id (s', _) (s, id) =
   5.136 +      let val id' = id_of s' in if id > id' then (s, id) else (s', id') end
   5.137 +  in ("", ~1) |> Facts.fold_static max_id facts |> fst end
   5.138 +
   5.139 +val local_prefix = "local" ^ Long_Name.separator
   5.140 +
   5.141 +fun nickname_of th =
   5.142 +  let val hint = Thm.get_name_hint th in
   5.143 +    (* FIXME: There must be a better way to detect local facts. *)
   5.144 +    case try (unprefix local_prefix) hint of
   5.145 +      SOME suff =>
   5.146 +      parent_of_local_thm th ^ Long_Name.separator ^ Long_Name.separator ^ suff
   5.147 +    | NONE => hint
   5.148 +  end
   5.149 +
   5.150 +fun suggested_facts suggs facts =
   5.151 +  let
   5.152 +    fun add_fact (fact as (_, th)) = Symtab.default (nickname_of th, fact)
   5.153 +    val tab = Symtab.empty |> fold add_fact facts
   5.154 +  in map_filter (Symtab.lookup tab) suggs end
   5.155 +
   5.156 +(* Ad hoc score function roughly based on Blanchette's Ringberg 2011 data. *)
   5.157 +fun score x = Math.pow (1.5, 15.5 - 0.05 * Real.fromInt x) + 15.0
   5.158 +
   5.159 +fun sum_sq_avg [] = 0
   5.160 +  | sum_sq_avg xs =
   5.161 +    Real.ceil (100000.0 * fold (curry (op +) o score) xs 0.0) div length xs
   5.162 +
   5.163 +fun mesh_facts max_facts [(selected, unknown)] =
   5.164 +    take max_facts selected @ take (max_facts - length selected) unknown
   5.165 +  | mesh_facts max_facts mess =
   5.166 +    let
   5.167 +      val mess = mess |> map (apfst (`length))
   5.168 +      val fact_eq = Thm.eq_thm o pairself snd
   5.169 +      fun score_in fact ((sel_len, sels), unks) =
   5.170 +        case find_index (curry fact_eq fact) sels of
   5.171 +          ~1 => (case find_index (curry fact_eq fact) unks of
   5.172 +                   ~1 => SOME sel_len
   5.173 +                 | _ => NONE)
   5.174 +        | j => SOME j
   5.175 +      fun score_of fact = mess |> map_filter (score_in fact) |> sum_sq_avg
   5.176 +      val facts = fold (union fact_eq o take max_facts o snd o fst) mess []
   5.177 +    in
   5.178 +      facts |> map (`score_of) |> sort (int_ord o swap o pairself fst)
   5.179 +            |> map snd |> take max_facts
   5.180 +    end
   5.181 +
   5.182 +val thy_feature_prefix = "y_"
   5.183 +
   5.184 +val thy_feature_name_of = prefix thy_feature_prefix
   5.185 +val const_name_of = prefix const_prefix
   5.186 +val type_name_of = prefix type_const_prefix
   5.187 +val class_name_of = prefix class_prefix
   5.188 +
   5.189 +fun is_likely_tautology_or_too_meta th =
   5.190 +  let
   5.191 +    val is_boring_const = member (op =) atp_widely_irrelevant_consts
   5.192 +    fun is_boring_bool t =
   5.193 +      not (exists_Const (not o is_boring_const o fst) t) orelse
   5.194 +      exists_type (exists_subtype (curry (op =) @{typ prop})) t
   5.195 +    fun is_boring_prop (@{const Trueprop} $ t) = is_boring_bool t
   5.196 +      | is_boring_prop (@{const "==>"} $ t $ u) =
   5.197 +        is_boring_prop t andalso is_boring_prop u
   5.198 +      | is_boring_prop (Const (@{const_name all}, _) $ (Abs (_, _, t)) $ u) =
   5.199 +        is_boring_prop t andalso is_boring_prop u
   5.200 +      | is_boring_prop (Const (@{const_name "=="}, _) $ t $ u) =
   5.201 +        is_boring_bool t andalso is_boring_bool u
   5.202 +      | is_boring_prop _ = true
   5.203 +  in
   5.204 +    is_boring_prop (prop_of th) andalso not (Thm.eq_thm_prop (@{thm ext}, th))
   5.205 +  end
   5.206 +
   5.207 +fun theory_ord p =
   5.208 +  if Theory.eq_thy p then
   5.209 +    EQUAL
   5.210 +  else if Theory.subthy p then
   5.211 +    LESS
   5.212 +  else if Theory.subthy (swap p) then
   5.213 +    GREATER
   5.214 +  else case int_ord (pairself (length o Theory.ancestors_of) p) of
   5.215 +    EQUAL => string_ord (pairself Context.theory_name p)
   5.216 +  | order => order
   5.217 +
   5.218 +val thm_ord = theory_ord o pairself theory_of_thm
   5.219 +
   5.220 +val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
   5.221 +
   5.222 +fun interesting_terms_types_and_classes ctxt prover term_max_depth
   5.223 +                                        type_max_depth ts =
   5.224 +  let
   5.225 +    fun is_bad_const (x as (s, _)) args =
   5.226 +      member (op =) atp_logical_consts s orelse
   5.227 +      fst (is_built_in_const_for_prover ctxt prover x args)
   5.228 +    fun add_classes @{sort type} = I
   5.229 +      | add_classes S = union (op =) (map class_name_of S)
   5.230 +    fun do_add_type (Type (s, Ts)) =
   5.231 +        (not (member (op =) bad_types s) ? insert (op =) (type_name_of s))
   5.232 +        #> fold do_add_type Ts
   5.233 +      | do_add_type (TFree (_, S)) = add_classes S
   5.234 +      | do_add_type (TVar (_, S)) = add_classes S
   5.235 +    fun add_type T = type_max_depth >= 0 ? do_add_type T
   5.236 +    fun mk_app s args =
   5.237 +      if member (op <>) args "" then s ^ "(" ^ space_implode "," args ^ ")"
   5.238 +      else s
   5.239 +    fun patternify ~1 _ = ""
   5.240 +      | patternify depth t =
   5.241 +        case strip_comb t of
   5.242 +          (Const (s, _), args) =>
   5.243 +          mk_app (const_name_of s) (map (patternify (depth - 1)) args)
   5.244 +        | _ => ""
   5.245 +    fun add_term_patterns ~1 _ = I
   5.246 +      | add_term_patterns depth t =
   5.247 +        insert (op =) (patternify depth t)
   5.248 +        #> add_term_patterns (depth - 1) t
   5.249 +    val add_term = add_term_patterns term_max_depth
   5.250 +    fun add_patterns t =
   5.251 +      let val (head, args) = strip_comb t in
   5.252 +        (case head of
   5.253 +           Const (x as (_, T)) =>
   5.254 +           not (is_bad_const x args) ? (add_term t #> add_type T)
   5.255 +         | Free (_, T) => add_type T
   5.256 +         | Var (_, T) => add_type T
   5.257 +         | Abs (_, T, body) => add_type T #> add_patterns body
   5.258 +         | _ => I)
   5.259 +        #> fold add_patterns args
   5.260 +      end
   5.261 +  in [] |> fold add_patterns ts end
   5.262 +
   5.263 +fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1})
   5.264 +
   5.265 +val term_max_depth = 1
   5.266 +val type_max_depth = 1
   5.267 +
   5.268 +(* TODO: Generate type classes for types? *)
   5.269 +fun features_of ctxt prover thy status ts =
   5.270 +  thy_feature_name_of (Context.theory_name thy) ::
   5.271 +  interesting_terms_types_and_classes ctxt prover term_max_depth type_max_depth
   5.272 +                                      ts
   5.273 +  |> forall is_lambda_free ts ? cons "no_lams"
   5.274 +  |> forall (not o exists_Const is_exists) ts ? cons "no_skos"
   5.275 +  |> (case status of
   5.276 +        General => I
   5.277 +      | Induction => cons "induction"
   5.278 +      | Intro => cons "intro"
   5.279 +      | Inductive => cons "inductive"
   5.280 +      | Elim => cons "elim"
   5.281 +      | Simp => cons "simp"
   5.282 +      | Def => cons "def")
   5.283 +
   5.284 +fun isabelle_dependencies_of all_facts = thms_in_proof (SOME all_facts)
   5.285 +
   5.286 +val freezeT = Type.legacy_freeze_type
   5.287 +
   5.288 +fun freeze (t $ u) = freeze t $ freeze u
   5.289 +  | freeze (Abs (s, T, t)) = Abs (s, freezeT T, freeze t)
   5.290 +  | freeze (Var ((s, _), T)) = Free (s, freezeT T)
   5.291 +  | freeze (Const (s, T)) = Const (s, freezeT T)
   5.292 +  | freeze (Free (s, T)) = Free (s, freezeT T)
   5.293 +  | freeze t = t
   5.294 +
   5.295 +fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init
   5.296 +
   5.297 +fun run_prover_for_mash ctxt params prover facts goal =
   5.298 +  let
   5.299 +    val problem =
   5.300 +      {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,
   5.301 +       facts = facts |> map (apfst (apfst (fn name => name ())))
   5.302 +                     |> map Untranslated_Fact}
   5.303 +    val prover = get_minimizing_prover ctxt Normal (K ()) prover
   5.304 +  in prover params (K (K (K ""))) problem end
   5.305 +
   5.306 +
   5.307 +(*** Low-level communication with MaSh ***)
   5.308 +
   5.309 +fun write_file (xs, f) file =
   5.310 +  let val path = Path.explode file in
   5.311 +    File.write path "";
   5.312 +    xs |> chunk_list 500
   5.313 +       |> List.app (File.append path o space_implode "" o map f)
   5.314 +  end
   5.315 +
   5.316 +fun mash_info overlord =
   5.317 +  if overlord then (getenv "ISABELLE_HOME_USER", "")
   5.318 +  else (getenv "ISABELLE_TMP", serial_string ())
   5.319 +
   5.320 +fun run_mash ctxt overlord (temp_dir, serial) core =
   5.321 +  let
   5.322 +    val log_file = temp_dir ^ "/mash_log" ^ serial
   5.323 +    val err_file = temp_dir ^ "/mash_err" ^ serial
   5.324 +    val command =
   5.325 +      mash_home () ^ "/mash.py --quiet --outputDir " ^ mash_state_dir () ^
   5.326 +      " --log " ^ log_file ^ " " ^ core ^ " 2>&1 > " ^ err_file
   5.327 +  in
   5.328 +    trace_msg ctxt (fn () => "Running " ^ command);
   5.329 +    write_file ([], K "") log_file;
   5.330 +    write_file ([], K "") err_file;
   5.331 +    Isabelle_System.bash command;
   5.332 +    if overlord then ()
   5.333 +    else (map (File.rm o Path.explode) [log_file, err_file]; ());
   5.334 +    trace_msg ctxt (K "Done")
   5.335 +  end
   5.336 +
   5.337 +(* TODO: Eliminate code once "mash.py" handles sequences of ADD commands as fast
   5.338 +   as a single INIT. *)
   5.339 +fun run_mash_init ctxt overlord write_access write_feats write_deps =
   5.340 +  let
   5.341 +    val info as (temp_dir, serial) = mash_info overlord
   5.342 +    val in_dir = temp_dir ^ "/mash_init" ^ serial
   5.343 +    val in_dir_path = in_dir |> Path.explode |> tap Isabelle_System.mkdir
   5.344 +  in
   5.345 +    write_file write_access (in_dir ^ "/mash_accessibility");
   5.346 +    write_file write_feats (in_dir ^ "/mash_features");
   5.347 +    write_file write_deps (in_dir ^ "/mash_dependencies");
   5.348 +    run_mash ctxt overlord info ("--init --inputDir " ^ in_dir);
   5.349 +    (* FIXME: temporary hack *)
   5.350 +    if overlord then ()
   5.351 +    else (Isabelle_System.bash ("rm -r -f " ^ File.shell_path in_dir_path); ())
   5.352 +  end
   5.353 +
   5.354 +fun run_mash_commands ctxt overlord save max_suggs write_cmds read_suggs =
   5.355 +  let
   5.356 +    val info as (temp_dir, serial) = mash_info overlord
   5.357 +    val sugg_file = temp_dir ^ "/mash_suggs" ^ serial
   5.358 +    val cmd_file = temp_dir ^ "/mash_commands" ^ serial
   5.359 +  in
   5.360 +    write_file ([], K "") sugg_file;
   5.361 +    write_file write_cmds cmd_file;
   5.362 +    run_mash ctxt overlord info
   5.363 +             ("--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^
   5.364 +              " --numberOfPredictions " ^ string_of_int max_suggs ^
   5.365 +              (if save then " --saveModel" else ""));
   5.366 +    read_suggs (fn () => File.read_lines (Path.explode sugg_file))
   5.367 +    |> tap (fn _ =>
   5.368 +               if overlord then ()
   5.369 +               else (map (File.rm o Path.explode) [sugg_file, cmd_file]; ()))
   5.370 +  end
   5.371 +
   5.372 +fun str_of_update (name, parents, feats, deps) =
   5.373 +  "! " ^ escape_meta name ^ ": " ^ escape_metas parents ^ "; " ^
   5.374 +  escape_metas feats ^ "; " ^ escape_metas deps ^ "\n"
   5.375 +
   5.376 +fun str_of_query (parents, feats) =
   5.377 +  "? " ^ escape_metas parents ^ "; " ^ escape_metas feats
   5.378 +
   5.379 +fun init_str_of_update get (upd as (name, _, _, _)) =
   5.380 +  escape_meta name ^ ": " ^ escape_metas (get upd) ^ "\n"
   5.381 +
   5.382 +fun mash_CLEAR ctxt =
   5.383 +  let val path = mash_state_dir () |> Path.explode in
   5.384 +    trace_msg ctxt (K "MaSh CLEAR");
   5.385 +    File.fold_dir (fn file => fn () =>
   5.386 +                      File.rm (Path.append path (Path.basic file)))
   5.387 +                  path ()
   5.388 +  end
   5.389 +
   5.390 +fun mash_INIT ctxt _ [] = mash_CLEAR ctxt
   5.391 +  | mash_INIT ctxt overlord upds =
   5.392 +    (trace_msg ctxt (fn () => "MaSh INIT " ^
   5.393 +         elide_string 1000 (space_implode " " (map #1 upds)));
   5.394 +     run_mash_init ctxt overlord (upds, init_str_of_update #2)
   5.395 +                   (upds, init_str_of_update #3) (upds, init_str_of_update #4))
   5.396 +
   5.397 +fun mash_ADD _ _ [] = ()
   5.398 +  | mash_ADD ctxt overlord upds =
   5.399 +    (trace_msg ctxt (fn () => "MaSh ADD " ^
   5.400 +         elide_string 1000 (space_implode " " (map #1 upds)));
   5.401 +     run_mash_commands ctxt overlord true 0 (upds, str_of_update) (K ()))
   5.402 +
   5.403 +fun mash_QUERY ctxt overlord max_suggs (query as (_, feats)) =
   5.404 +  (trace_msg ctxt (fn () => "MaSh QUERY " ^ space_implode " " feats);
   5.405 +   run_mash_commands ctxt overlord false max_suggs
   5.406 +       ([query], str_of_query)
   5.407 +       (fn suggs => snd (extract_query (List.last (suggs ()))))
   5.408 +   handle List.Empty => [])
   5.409 +
   5.410 +
   5.411 +(*** High-level communication with MaSh ***)
   5.412 +
   5.413 +fun try_graph ctxt when def f =
   5.414 +  f ()
   5.415 +  handle Graph.CYCLES (cycle :: _) =>
   5.416 +         (trace_msg ctxt (fn () =>
   5.417 +              "Cycle involving " ^ commas cycle ^ " when " ^ when); def)
   5.418 +       | Graph.UNDEF name =>
   5.419 +         (trace_msg ctxt (fn () =>
   5.420 +              "Unknown fact " ^ quote name ^ " when " ^ when); def)
   5.421 +
   5.422 +type mash_state =
   5.423 +  {thys : bool Symtab.table,
   5.424 +   fact_graph : unit Graph.T}
   5.425 +
   5.426 +val empty_state = {thys = Symtab.empty, fact_graph = Graph.empty}
   5.427 +
   5.428 +local
   5.429 +
   5.430 +fun mash_load _ (state as (true, _)) = state
   5.431 +  | mash_load ctxt _ =
   5.432 +    let val path = mash_state_path () in
   5.433 +      (true,
   5.434 +       case try File.read_lines path of
   5.435 +         SOME (comp_thys :: incomp_thys :: fact_lines) =>
   5.436 +         let
   5.437 +           fun add_thy comp thy = Symtab.update (thy, comp)
   5.438 +           fun add_edge_to name parent =
   5.439 +             Graph.default_node (parent, ())
   5.440 +             #> Graph.add_edge (parent, name)
   5.441 +           fun add_fact_line line =
   5.442 +             case extract_query line of
   5.443 +               ("", _) => I (* shouldn't happen *)
   5.444 +             | (name, parents) =>
   5.445 +               Graph.default_node (name, ())
   5.446 +               #> fold (add_edge_to name) parents
   5.447 +           val thys =
   5.448 +             Symtab.empty |> fold (add_thy true) (unescape_metas comp_thys)
   5.449 +                          |> fold (add_thy false) (unescape_metas incomp_thys)
   5.450 +           val fact_graph =
   5.451 +             try_graph ctxt "loading state" Graph.empty (fn () =>
   5.452 +                 Graph.empty |> fold add_fact_line fact_lines)
   5.453 +         in {thys = thys, fact_graph = fact_graph} end
   5.454 +       | _ => empty_state)
   5.455 +    end
   5.456 +
   5.457 +fun mash_save ({thys, fact_graph, ...} : mash_state) =
   5.458 +  let
   5.459 +    val path = mash_state_path ()
   5.460 +    val thys = Symtab.dest thys
   5.461 +    val line_for_thys = escape_metas o AList.find (op =) thys
   5.462 +    fun fact_line_for name parents =
   5.463 +      escape_meta name ^ ": " ^ escape_metas parents
   5.464 +    val append_fact = File.append path o suffix "\n" oo fact_line_for
   5.465 +  in
   5.466 +    File.write path (line_for_thys true ^ "\n" ^ line_for_thys false ^ "\n");
   5.467 +    Graph.fold (fn (name, ((), (parents, _))) => fn () =>
   5.468 +                   append_fact name (Graph.Keys.dest parents))
   5.469 +        fact_graph ()
   5.470 +  end
   5.471 +
   5.472 +val global_state =
   5.473 +  Synchronized.var "Sledgehammer_Filter_MaSh.global_state" (false, empty_state)
   5.474 +
   5.475 +in
   5.476 +
   5.477 +fun mash_map ctxt f =
   5.478 +  Synchronized.change global_state (mash_load ctxt ##> (f #> tap mash_save))
   5.479 +
   5.480 +fun mash_get ctxt =
   5.481 +  Synchronized.change_result global_state (mash_load ctxt #> `snd)
   5.482 +
   5.483 +fun mash_unlearn ctxt =
   5.484 +  Synchronized.change global_state (fn _ =>
   5.485 +      (mash_CLEAR ctxt; File.write (mash_state_path ()) "";
   5.486 +       (true, empty_state)))
   5.487 +
   5.488 +end
   5.489 +
   5.490 +fun mash_could_suggest_facts () = mash_home () <> ""
   5.491 +fun mash_can_suggest_facts ctxt =
   5.492 +  not (Graph.is_empty (#fact_graph (mash_get ctxt)))
   5.493 +
   5.494 +fun parents_wrt_facts facts fact_graph =
   5.495 +  let
   5.496 +    val facts = [] |> fold (cons o nickname_of o snd) facts
   5.497 +    val tab = Symtab.empty |> fold (fn name => Symtab.update (name, ())) facts
   5.498 +    fun insert_not_seen seen name =
   5.499 +      not (member (op =) seen name) ? insert (op =) name
   5.500 +    fun parents_of _ parents [] = parents
   5.501 +      | parents_of seen parents (name :: names) =
   5.502 +        if Symtab.defined tab name then
   5.503 +          parents_of (name :: seen) (name :: parents) names
   5.504 +        else
   5.505 +          parents_of (name :: seen) parents
   5.506 +                     (Graph.Keys.fold (insert_not_seen seen)
   5.507 +                                      (Graph.imm_preds fact_graph name) names)
   5.508 +  in parents_of [] [] (Graph.maximals fact_graph) end
   5.509 +
   5.510 +(* Generate more suggestions than requested, because some might be thrown out
   5.511 +   later for various reasons and "meshing" gives better results with some
   5.512 +   slack. *)
   5.513 +fun max_suggs_of max_facts = max_facts + Int.min (200, max_facts)
   5.514 +
   5.515 +fun is_fact_in_graph fact_graph (_, th) =
   5.516 +  can (Graph.get_node fact_graph) (nickname_of th)
   5.517 +
   5.518 +fun mash_suggest_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
   5.519 +                       concl_t facts =
   5.520 +  let
   5.521 +    val thy = Proof_Context.theory_of ctxt
   5.522 +    val fact_graph = #fact_graph (mash_get ctxt)
   5.523 +    val parents = parents_wrt_facts facts fact_graph
   5.524 +    val feats = features_of ctxt prover thy General (concl_t :: hyp_ts)
   5.525 +    val suggs =
   5.526 +      if Graph.is_empty fact_graph then []
   5.527 +      else mash_QUERY ctxt overlord (max_suggs_of max_facts) (parents, feats)
   5.528 +    val selected = facts |> suggested_facts suggs
   5.529 +    val unknown = facts |> filter_out (is_fact_in_graph fact_graph)
   5.530 +  in (selected, unknown) end
   5.531 +
   5.532 +fun add_thys_for thy =
   5.533 +  let fun add comp thy = Symtab.update (Context.theory_name thy, comp) in
   5.534 +    add false thy #> fold (add true) (Theory.ancestors_of thy)
   5.535 +  end
   5.536 +
   5.537 +fun update_fact_graph ctxt (name, parents, feats, deps) (upds, graph) =
   5.538 +  let
   5.539 +    fun maybe_add_from from (accum as (parents, graph)) =
   5.540 +      try_graph ctxt "updating graph" accum (fn () =>
   5.541 +          (from :: parents, Graph.add_edge_acyclic (from, name) graph))
   5.542 +    val graph = graph |> Graph.default_node (name, ())
   5.543 +    val (parents, graph) = ([], graph) |> fold maybe_add_from parents
   5.544 +    val (deps, graph) = ([], graph) |> fold maybe_add_from deps
   5.545 +  in ((name, parents, feats, deps) :: upds, graph) end
   5.546 +
   5.547 +val pass1_learn_timeout_factor = 0.5
   5.548 +
   5.549 +(* Too many dependencies is a sign that a decision procedure is at work. There
   5.550 +   isn't much too learn from such proofs. *)
   5.551 +val max_dependencies = 10
   5.552 +
   5.553 +(* The timeout is understood in a very slack fashion. *)
   5.554 +fun mash_learn_thy ctxt ({provers, verbose, overlord, ...} : params) thy timeout
   5.555 +                   facts =
   5.556 +  let
   5.557 +    val timer = Timer.startRealTimer ()
   5.558 +    val prover = hd provers
   5.559 +    fun timed_out frac =
   5.560 +      Time.> (Timer.checkRealTimer timer, time_mult frac timeout)
   5.561 +    val {fact_graph, ...} = mash_get ctxt
   5.562 +    val new_facts =
   5.563 +      facts |> filter_out (is_fact_in_graph fact_graph)
   5.564 +            |> sort (thm_ord o pairself snd)
   5.565 +  in
   5.566 +    if null new_facts then
   5.567 +      ""
   5.568 +    else
   5.569 +      let
   5.570 +        val ths = facts |> map snd
   5.571 +        val all_names =
   5.572 +          ths |> filter_out is_likely_tautology_or_too_meta
   5.573 +              |> map (rpair () o nickname_of)
   5.574 +              |> Symtab.make
   5.575 +        fun trim_deps deps = if length deps > max_dependencies then [] else deps
   5.576 +        fun do_fact _ (accum as (_, true)) = accum
   5.577 +          | do_fact ((_, (_, status)), th) ((parents, upds), false) =
   5.578 +            let
   5.579 +              val name = nickname_of th
   5.580 +              val feats =
   5.581 +                features_of ctxt prover (theory_of_thm th) status [prop_of th]
   5.582 +              val deps = isabelle_dependencies_of all_names th |> trim_deps
   5.583 +              val upd = (name, parents, feats, deps)
   5.584 +            in (([name], upd :: upds), timed_out pass1_learn_timeout_factor) end
   5.585 +        val parents = parents_wrt_facts facts fact_graph
   5.586 +        val ((_, upds), _) =
   5.587 +          ((parents, []), false) |> fold do_fact new_facts |>> apsnd rev
   5.588 +        val n = length upds
   5.589 +        fun trans {thys, fact_graph} =
   5.590 +          let
   5.591 +            val mash_INIT_or_ADD =
   5.592 +              if Graph.is_empty fact_graph then mash_INIT else mash_ADD
   5.593 +            val (upds, fact_graph) =
   5.594 +              ([], fact_graph) |> fold (update_fact_graph ctxt) upds
   5.595 +          in
   5.596 +            (mash_INIT_or_ADD ctxt overlord (rev upds);
   5.597 +             {thys = thys |> add_thys_for thy,
   5.598 +              fact_graph = fact_graph})
   5.599 +          end
   5.600 +      in
   5.601 +        mash_map ctxt trans;
   5.602 +        if verbose then
   5.603 +          "Processed " ^ string_of_int n ^ " proof" ^ plural_s n ^
   5.604 +          (if verbose then
   5.605 +             " in " ^ string_from_time (Timer.checkRealTimer timer)
   5.606 +           else
   5.607 +             "") ^ "."
   5.608 +        else
   5.609 +          ""
   5.610 +      end
   5.611 +  end
   5.612 +
   5.613 +fun mash_learn_proof ctxt ({provers, overlord, ...} : params) t facts used_ths =
   5.614 +  let
   5.615 +    val thy = Proof_Context.theory_of ctxt
   5.616 +    val prover = hd provers
   5.617 +    val name = ATP_Util.timestamp () ^ " " ^ serial_string () (* fresh enough *)
   5.618 +    val feats = features_of ctxt prover thy General [t]
   5.619 +    val deps = used_ths |> map nickname_of
   5.620 +  in
   5.621 +    mash_map ctxt (fn {thys, fact_graph} =>
   5.622 +        let
   5.623 +          val parents = parents_wrt_facts facts fact_graph
   5.624 +          val upds = [(name, parents, feats, deps)]
   5.625 +          val (upds, fact_graph) =
   5.626 +            ([], fact_graph) |> fold (update_fact_graph ctxt) upds
   5.627 +        in
   5.628 +          mash_ADD ctxt overlord upds;
   5.629 +          {thys = thys, fact_graph = fact_graph}
   5.630 +        end)
   5.631 +  end
   5.632 +
   5.633 +(* The threshold should be large enough so that MaSh doesn't kick in for Auto
   5.634 +   Sledgehammer and Try. *)
   5.635 +val min_secs_for_learning = 15
   5.636 +val learn_timeout_factor = 2.0
   5.637 +
   5.638 +fun relevant_facts ctxt (params as {learn, fact_filter, timeout, ...}) prover
   5.639 +        max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts =
   5.640 +  if not (subset (op =) (the_list fact_filter, fact_filters)) then
   5.641 +    error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".")
   5.642 +  else if only then
   5.643 +    facts
   5.644 +  else if max_facts <= 0 orelse null facts then
   5.645 +    []
   5.646 +  else
   5.647 +    let
   5.648 +      val thy = Proof_Context.theory_of ctxt
   5.649 +      fun maybe_learn () =
   5.650 +        if not learn orelse Async_Manager.has_running_threads MaShN then
   5.651 +          ()
   5.652 +        else if Time.toSeconds timeout >= min_secs_for_learning then
   5.653 +          let
   5.654 +            val soft_timeout = time_mult learn_timeout_factor timeout
   5.655 +            val hard_timeout = time_mult 4.0 soft_timeout
   5.656 +            val birth_time = Time.now ()
   5.657 +            val death_time = Time.+ (birth_time, hard_timeout)
   5.658 +            val desc = ("machine learner for Sledgehammer", "")
   5.659 +          in
   5.660 +            Async_Manager.launch MaShN birth_time death_time desc
   5.661 +                (fn () =>
   5.662 +                    (true, mash_learn_thy ctxt params thy soft_timeout facts))
   5.663 +          end
   5.664 +        else
   5.665 +          ()
   5.666 +      val fact_filter =
   5.667 +        case fact_filter of
   5.668 +          SOME ff => (() |> ff <> mepoN ? maybe_learn; ff)
   5.669 +        | NONE =>
   5.670 +          if mash_can_suggest_facts ctxt then (maybe_learn (); meshN)
   5.671 +          else if mash_could_suggest_facts () then (maybe_learn (); mepoN)
   5.672 +          else mepoN
   5.673 +      val add_ths = Attrib.eval_thms ctxt add
   5.674 +      fun prepend_facts ths accepts =
   5.675 +        ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @
   5.676 +         (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)))
   5.677 +        |> take max_facts
   5.678 +      fun iter () =
   5.679 +        iterative_relevant_facts ctxt params prover max_facts NONE hyp_ts
   5.680 +                                 concl_t facts
   5.681 +      fun mash () =
   5.682 +        mash_suggest_facts ctxt params prover max_facts hyp_ts concl_t facts
   5.683 +      val mess =
   5.684 +        [] |> (if fact_filter <> mashN then cons (iter (), []) else I)
   5.685 +           |> (if fact_filter <> mepoN then cons (mash ()) else I)
   5.686 +    in
   5.687 +      mesh_facts max_facts mess
   5.688 +      |> not (null add_ths) ? prepend_facts add_ths
   5.689 +    end
   5.690 +
   5.691 +fun kill_learners () = Async_Manager.kill_threads MaShN "learner"
   5.692 +fun running_learners () = Async_Manager.running_threads MaShN "learner"
   5.693 +
   5.694 +end;
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Fri Jul 20 22:19:45 2012 +0200
     6.3 @@ -0,0 +1,537 @@
     6.4 +(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
     6.5 +    Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     6.6 +    Author:     Jasmin Blanchette, TU Muenchen
     6.7 +
     6.8 +Sledgehammer's iterative relevance filter (MePo = Meng-Paulson).
     6.9 +*)
    6.10 +
    6.11 +signature SLEDGEHAMMER_FILTER_ITER =
    6.12 +sig
    6.13 +  type stature = ATP_Problem_Generate.stature
    6.14 +  type fact = Sledgehammer_Fact.fact
    6.15 +  type params = Sledgehammer_Provers.params
    6.16 +  type relevance_fudge = Sledgehammer_Provers.relevance_fudge
    6.17 +
    6.18 +  val trace : bool Config.T
    6.19 +  val pseudo_abs_name : string
    6.20 +  val pseudo_skolem_prefix : string
    6.21 +  val const_names_in_fact :
    6.22 +    theory -> (string * typ -> term list -> bool * term list) -> term
    6.23 +    -> string list
    6.24 +  val iterative_relevant_facts :
    6.25 +    Proof.context -> params -> string -> int -> relevance_fudge option
    6.26 +    -> term list -> term -> fact list -> fact list
    6.27 +end;
    6.28 +
    6.29 +structure Sledgehammer_Filter_Iter : SLEDGEHAMMER_FILTER_ITER =
    6.30 +struct
    6.31 +
    6.32 +open ATP_Problem_Generate
    6.33 +open Sledgehammer_Fact
    6.34 +open Sledgehammer_Provers
    6.35 +
    6.36 +val trace =
    6.37 +  Attrib.setup_config_bool @{binding sledgehammer_filter_iter_trace} (K false)
    6.38 +fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
    6.39 +
    6.40 +val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
    6.41 +val pseudo_abs_name = sledgehammer_prefix ^ "abs"
    6.42 +val pseudo_skolem_prefix = sledgehammer_prefix ^ "sko"
    6.43 +val theory_const_suffix = Long_Name.separator ^ " 1"
    6.44 +
    6.45 +fun order_of_type (Type (@{type_name fun}, [T1, T2])) =
    6.46 +    Int.max (order_of_type T1 + 1, order_of_type T2)
    6.47 +  | order_of_type (Type (_, Ts)) = fold (Integer.max o order_of_type) Ts 0
    6.48 +  | order_of_type _ = 0
    6.49 +
    6.50 +(* An abstraction of Isabelle types and first-order terms *)
    6.51 +datatype pattern = PVar | PApp of string * pattern list
    6.52 +datatype ptype = PType of int * pattern list
    6.53 +
    6.54 +fun string_for_pattern PVar = "_"
    6.55 +  | string_for_pattern (PApp (s, ps)) =
    6.56 +    if null ps then s else s ^ string_for_patterns ps
    6.57 +and string_for_patterns ps = "(" ^ commas (map string_for_pattern ps) ^ ")"
    6.58 +fun string_for_ptype (PType (_, ps)) = string_for_patterns ps
    6.59 +
    6.60 +(*Is the second type an instance of the first one?*)
    6.61 +fun match_pattern (PVar, _) = true
    6.62 +  | match_pattern (PApp _, PVar) = false
    6.63 +  | match_pattern (PApp (s, ps), PApp (t, qs)) =
    6.64 +    s = t andalso match_patterns (ps, qs)
    6.65 +and match_patterns (_, []) = true
    6.66 +  | match_patterns ([], _) = false
    6.67 +  | match_patterns (p :: ps, q :: qs) =
    6.68 +    match_pattern (p, q) andalso match_patterns (ps, qs)
    6.69 +fun match_ptype (PType (_, ps), PType (_, qs)) = match_patterns (ps, qs)
    6.70 +
    6.71 +(* Is there a unifiable constant? *)
    6.72 +fun pconst_mem f consts (s, ps) =
    6.73 +  exists (curry (match_ptype o f) ps)
    6.74 +         (map snd (filter (curry (op =) s o fst) consts))
    6.75 +fun pconst_hyper_mem f const_tab (s, ps) =
    6.76 +  exists (curry (match_ptype o f) ps) (these (Symtab.lookup const_tab s))
    6.77 +
    6.78 +fun pattern_for_type (Type (s, Ts)) = PApp (s, map pattern_for_type Ts)
    6.79 +  | pattern_for_type (TFree (s, _)) = PApp (s, [])
    6.80 +  | pattern_for_type (TVar _) = PVar
    6.81 +
    6.82 +(* Pairs a constant with the list of its type instantiations. *)
    6.83 +fun ptype thy const x =
    6.84 +  (if const then map pattern_for_type (these (try (Sign.const_typargs thy) x))
    6.85 +   else [])
    6.86 +fun rich_ptype thy const (s, T) =
    6.87 +  PType (order_of_type T, ptype thy const (s, T))
    6.88 +fun rich_pconst thy const (s, T) = (s, rich_ptype thy const (s, T))
    6.89 +
    6.90 +fun string_for_hyper_pconst (s, ps) =
    6.91 +  s ^ "{" ^ commas (map string_for_ptype ps) ^ "}"
    6.92 +
    6.93 +(* Add a pconstant to the table, but a [] entry means a standard
    6.94 +   connective, which we ignore.*)
    6.95 +fun add_pconst_to_table also_skolem (s, p) =
    6.96 +  if (not also_skolem andalso String.isPrefix pseudo_skolem_prefix s) then I
    6.97 +  else Symtab.map_default (s, [p]) (insert (op =) p)
    6.98 +
    6.99 +(* Set constants tend to pull in too many irrelevant facts. We limit the damage
   6.100 +   by treating them more or less as if they were built-in but add their
   6.101 +   axiomatization at the end. *)
   6.102 +val set_consts = [@{const_name Collect}, @{const_name Set.member}]
   6.103 +val set_thms = @{thms Collect_mem_eq mem_Collect_eq Collect_cong}
   6.104 +
   6.105 +fun add_pconsts_in_term thy is_built_in_const also_skolems pos =
   6.106 +  let
   6.107 +    val flip = Option.map not
   6.108 +    (* We include free variables, as well as constants, to handle locales. For
   6.109 +       each quantifiers that must necessarily be skolemized by the automatic
   6.110 +       prover, we introduce a fresh constant to simulate the effect of
   6.111 +       Skolemization. *)
   6.112 +    fun do_const const ext_arg (x as (s, _)) ts =
   6.113 +      let val (built_in, ts) = is_built_in_const x ts in
   6.114 +        if member (op =) set_consts s then
   6.115 +          fold (do_term ext_arg) ts
   6.116 +        else
   6.117 +          (not built_in
   6.118 +           ? add_pconst_to_table also_skolems (rich_pconst thy const x))
   6.119 +          #> fold (do_term false) ts
   6.120 +      end
   6.121 +    and do_term ext_arg t =
   6.122 +      case strip_comb t of
   6.123 +        (Const x, ts) => do_const true ext_arg x ts
   6.124 +      | (Free x, ts) => do_const false ext_arg x ts
   6.125 +      | (Abs (_, T, t'), ts) =>
   6.126 +        ((null ts andalso not ext_arg)
   6.127 +         (* Since lambdas on the right-hand side of equalities are usually
   6.128 +            extensionalized later by "abs_extensionalize_term", we don't
   6.129 +            penalize them here. *)
   6.130 +         ? add_pconst_to_table true (pseudo_abs_name,
   6.131 +                                     PType (order_of_type T + 1, [])))
   6.132 +        #> fold (do_term false) (t' :: ts)
   6.133 +      | (_, ts) => fold (do_term false) ts
   6.134 +    fun do_quantifier will_surely_be_skolemized abs_T body_t =
   6.135 +      do_formula pos body_t
   6.136 +      #> (if also_skolems andalso will_surely_be_skolemized then
   6.137 +            add_pconst_to_table true (pseudo_skolem_prefix ^ serial_string (),
   6.138 +                                      PType (order_of_type abs_T, []))
   6.139 +          else
   6.140 +            I)
   6.141 +    and do_term_or_formula ext_arg T =
   6.142 +      if T = HOLogic.boolT then do_formula NONE else do_term ext_arg
   6.143 +    and do_formula pos t =
   6.144 +      case t of
   6.145 +        Const (@{const_name all}, _) $ Abs (_, T, t') =>
   6.146 +        do_quantifier (pos = SOME false) T t'
   6.147 +      | @{const "==>"} $ t1 $ t2 =>
   6.148 +        do_formula (flip pos) t1 #> do_formula pos t2
   6.149 +      | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
   6.150 +        do_term_or_formula false T t1 #> do_term_or_formula true T t2
   6.151 +      | @{const Trueprop} $ t1 => do_formula pos t1
   6.152 +      | @{const False} => I
   6.153 +      | @{const True} => I
   6.154 +      | @{const Not} $ t1 => do_formula (flip pos) t1
   6.155 +      | Const (@{const_name All}, _) $ Abs (_, T, t') =>
   6.156 +        do_quantifier (pos = SOME false) T t'
   6.157 +      | Const (@{const_name Ex}, _) $ Abs (_, T, t') =>
   6.158 +        do_quantifier (pos = SOME true) T t'
   6.159 +      | @{const HOL.conj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
   6.160 +      | @{const HOL.disj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
   6.161 +      | @{const HOL.implies} $ t1 $ t2 =>
   6.162 +        do_formula (flip pos) t1 #> do_formula pos t2
   6.163 +      | Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2 =>
   6.164 +        do_term_or_formula false T t1 #> do_term_or_formula true T t2
   6.165 +      | Const (@{const_name If}, Type (_, [_, Type (_, [T, _])]))
   6.166 +        $ t1 $ t2 $ t3 =>
   6.167 +        do_formula NONE t1 #> fold (do_term_or_formula false T) [t2, t3]
   6.168 +      | Const (@{const_name Ex1}, _) $ Abs (_, T, t') =>
   6.169 +        do_quantifier (is_some pos) T t'
   6.170 +      | Const (@{const_name Ball}, _) $ t1 $ Abs (_, T, t') =>
   6.171 +        do_quantifier (pos = SOME false) T
   6.172 +                      (HOLogic.mk_imp (incr_boundvars 1 t1 $ Bound 0, t'))
   6.173 +      | Const (@{const_name Bex}, _) $ t1 $ Abs (_, T, t') =>
   6.174 +        do_quantifier (pos = SOME true) T
   6.175 +                      (HOLogic.mk_conj (incr_boundvars 1 t1 $ Bound 0, t'))
   6.176 +      | (t0 as Const (_, @{typ bool})) $ t1 =>
   6.177 +        do_term false t0 #> do_formula pos t1  (* theory constant *)
   6.178 +      | _ => do_term false t
   6.179 +  in do_formula pos end
   6.180 +
   6.181 +fun pconsts_in_fact thy is_built_in_const t =
   6.182 +  Symtab.fold (fn (s, pss) => fold (cons o pair s) pss)
   6.183 +              (Symtab.empty |> add_pconsts_in_term thy is_built_in_const true
   6.184 +                                                   (SOME true) t) []
   6.185 +
   6.186 +val const_names_in_fact = map fst ooo pconsts_in_fact
   6.187 +
   6.188 +(* Inserts a dummy "constant" referring to the theory name, so that relevance
   6.189 +   takes the given theory into account. *)
   6.190 +fun theory_constify ({theory_const_rel_weight, theory_const_irrel_weight, ...}
   6.191 +                     : relevance_fudge) thy_name t =
   6.192 +  if exists (curry (op <) 0.0) [theory_const_rel_weight,
   6.193 +                                theory_const_irrel_weight] then
   6.194 +    Const (thy_name ^ theory_const_suffix, @{typ bool}) $ t
   6.195 +  else
   6.196 +    t
   6.197 +
   6.198 +fun theory_const_prop_of fudge th =
   6.199 +  theory_constify fudge (Context.theory_name (theory_of_thm th)) (prop_of th)
   6.200 +
   6.201 +fun pair_consts_fact thy is_built_in_const fudge fact =
   6.202 +  case fact |> snd |> theory_const_prop_of fudge
   6.203 +            |> pconsts_in_fact thy is_built_in_const of
   6.204 +    [] => NONE
   6.205 +  | consts => SOME ((fact, consts), NONE)
   6.206 +
   6.207 +(* A two-dimensional symbol table counts frequencies of constants. It's keyed
   6.208 +   first by constant name and second by its list of type instantiations. For the
   6.209 +   latter, we need a linear ordering on "pattern list". *)
   6.210 +
   6.211 +fun pattern_ord p =
   6.212 +  case p of
   6.213 +    (PVar, PVar) => EQUAL
   6.214 +  | (PVar, PApp _) => LESS
   6.215 +  | (PApp _, PVar) => GREATER
   6.216 +  | (PApp q1, PApp q2) =>
   6.217 +    prod_ord fast_string_ord (dict_ord pattern_ord) (q1, q2)
   6.218 +fun ptype_ord (PType p, PType q) =
   6.219 +  prod_ord (dict_ord pattern_ord) int_ord (swap p, swap q)
   6.220 +
   6.221 +structure PType_Tab = Table(type key = ptype val ord = ptype_ord)
   6.222 +
   6.223 +fun count_fact_consts thy fudge =
   6.224 +  let
   6.225 +    fun do_const const (s, T) ts =
   6.226 +      (* Two-dimensional table update. Constant maps to types maps to count. *)
   6.227 +      PType_Tab.map_default (rich_ptype thy const (s, T), 0) (Integer.add 1)
   6.228 +      |> Symtab.map_default (s, PType_Tab.empty)
   6.229 +      #> fold do_term ts
   6.230 +    and do_term t =
   6.231 +      case strip_comb t of
   6.232 +        (Const x, ts) => do_const true x ts
   6.233 +      | (Free x, ts) => do_const false x ts
   6.234 +      | (Abs (_, _, t'), ts) => fold do_term (t' :: ts)
   6.235 +      | (_, ts) => fold do_term ts
   6.236 +  in do_term o theory_const_prop_of fudge o snd end
   6.237 +
   6.238 +fun pow_int _ 0 = 1.0
   6.239 +  | pow_int x 1 = x
   6.240 +  | pow_int x n = if n > 0 then x * pow_int x (n - 1) else pow_int x (n + 1) / x
   6.241 +
   6.242 +(*The frequency of a constant is the sum of those of all instances of its type.*)
   6.243 +fun pconst_freq match const_tab (c, ps) =
   6.244 +  PType_Tab.fold (fn (qs, m) => match (ps, qs) ? Integer.add m)
   6.245 +                 (the (Symtab.lookup const_tab c)) 0
   6.246 +
   6.247 +
   6.248 +(* A surprising number of theorems contain only a few significant constants.
   6.249 +   These include all induction rules, and other general theorems. *)
   6.250 +
   6.251 +(* "log" seems best in practice. A constant function of one ignores the constant
   6.252 +   frequencies. Rare constants give more points if they are relevant than less
   6.253 +   rare ones. *)
   6.254 +fun rel_weight_for _ freq = 1.0 + 2.0 / Math.ln (Real.fromInt freq + 1.0)
   6.255 +
   6.256 +(* Irrelevant constants are treated differently. We associate lower penalties to
   6.257 +   very rare constants and very common ones -- the former because they can't
   6.258 +   lead to the inclusion of too many new facts, and the latter because they are
   6.259 +   so common as to be of little interest. *)
   6.260 +fun irrel_weight_for ({worse_irrel_freq, higher_order_irrel_weight, ...}
   6.261 +                      : relevance_fudge) order freq =
   6.262 +  let val (k, x) = worse_irrel_freq |> `Real.ceil in
   6.263 +    (if freq < k then Math.ln (Real.fromInt (freq + 1)) / Math.ln x
   6.264 +     else rel_weight_for order freq / rel_weight_for order k)
   6.265 +    * pow_int higher_order_irrel_weight (order - 1)
   6.266 +  end
   6.267 +
   6.268 +fun multiplier_for_const_name local_const_multiplier s =
   6.269 +  if String.isSubstring "." s then 1.0 else local_const_multiplier
   6.270 +
   6.271 +(* Computes a constant's weight, as determined by its frequency. *)
   6.272 +fun generic_pconst_weight local_const_multiplier abs_weight skolem_weight
   6.273 +                          theory_const_weight chained_const_weight weight_for f
   6.274 +                          const_tab chained_const_tab (c as (s, PType (m, _))) =
   6.275 +  if s = pseudo_abs_name then
   6.276 +    abs_weight
   6.277 +  else if String.isPrefix pseudo_skolem_prefix s then
   6.278 +    skolem_weight
   6.279 +  else if String.isSuffix theory_const_suffix s then
   6.280 +    theory_const_weight
   6.281 +  else
   6.282 +    multiplier_for_const_name local_const_multiplier s
   6.283 +    * weight_for m (pconst_freq (match_ptype o f) const_tab c)
   6.284 +    |> (if chained_const_weight < 1.0 andalso
   6.285 +           pconst_hyper_mem I chained_const_tab c then
   6.286 +          curry (op *) chained_const_weight
   6.287 +        else
   6.288 +          I)
   6.289 +
   6.290 +fun rel_pconst_weight ({local_const_multiplier, abs_rel_weight,
   6.291 +                        theory_const_rel_weight, ...} : relevance_fudge)
   6.292 +                      const_tab =
   6.293 +  generic_pconst_weight local_const_multiplier abs_rel_weight 0.0
   6.294 +                        theory_const_rel_weight 0.0 rel_weight_for I const_tab
   6.295 +                        Symtab.empty
   6.296 +
   6.297 +fun irrel_pconst_weight (fudge as {local_const_multiplier, abs_irrel_weight,
   6.298 +                                   skolem_irrel_weight,
   6.299 +                                   theory_const_irrel_weight,
   6.300 +                                   chained_const_irrel_weight, ...})
   6.301 +                        const_tab chained_const_tab =
   6.302 +  generic_pconst_weight local_const_multiplier abs_irrel_weight
   6.303 +                        skolem_irrel_weight theory_const_irrel_weight
   6.304 +                        chained_const_irrel_weight (irrel_weight_for fudge) swap
   6.305 +                        const_tab chained_const_tab
   6.306 +
   6.307 +fun stature_bonus ({intro_bonus, ...} : relevance_fudge) (_, Intro) =
   6.308 +    intro_bonus
   6.309 +  | stature_bonus {elim_bonus, ...} (_, Elim) = elim_bonus
   6.310 +  | stature_bonus {simp_bonus, ...} (_, Simp) = simp_bonus
   6.311 +  | stature_bonus {local_bonus, ...} (Local, _) = local_bonus
   6.312 +  | stature_bonus {assum_bonus, ...} (Assum, _) = assum_bonus
   6.313 +  | stature_bonus {chained_bonus, ...} (Chained, _) = chained_bonus
   6.314 +  | stature_bonus _ _ = 0.0
   6.315 +
   6.316 +fun is_odd_const_name s =
   6.317 +  s = pseudo_abs_name orelse String.isPrefix pseudo_skolem_prefix s orelse
   6.318 +  String.isSuffix theory_const_suffix s
   6.319 +
   6.320 +fun fact_weight fudge stature const_tab relevant_consts chained_consts
   6.321 +                fact_consts =
   6.322 +  case fact_consts |> List.partition (pconst_hyper_mem I relevant_consts)
   6.323 +                   ||> filter_out (pconst_hyper_mem swap relevant_consts) of
   6.324 +    ([], _) => 0.0
   6.325 +  | (rel, irrel) =>
   6.326 +    if forall (forall (is_odd_const_name o fst)) [rel, irrel] then
   6.327 +      0.0
   6.328 +    else
   6.329 +      let
   6.330 +        val irrel = irrel |> filter_out (pconst_mem swap rel)
   6.331 +        val rel_weight =
   6.332 +          0.0 |> fold (curry (op +) o rel_pconst_weight fudge const_tab) rel
   6.333 +        val irrel_weight =
   6.334 +          ~ (stature_bonus fudge stature)
   6.335 +          |> fold (curry (op +)
   6.336 +                   o irrel_pconst_weight fudge const_tab chained_consts) irrel
   6.337 +        val res = rel_weight / (rel_weight + irrel_weight)
   6.338 +      in if Real.isFinite res then res else 0.0 end
   6.339 +
   6.340 +fun take_most_relevant ctxt max_facts remaining_max
   6.341 +        ({max_imperfect, max_imperfect_exp, ...} : relevance_fudge)
   6.342 +        (candidates : ((fact * (string * ptype) list) * real) list) =
   6.343 +  let
   6.344 +    val max_imperfect =
   6.345 +      Real.ceil (Math.pow (max_imperfect,
   6.346 +                    Math.pow (Real.fromInt remaining_max
   6.347 +                              / Real.fromInt max_facts, max_imperfect_exp)))
   6.348 +    val (perfect, imperfect) =
   6.349 +      candidates |> sort (Real.compare o swap o pairself snd)
   6.350 +                 |> take_prefix (fn (_, w) => w > 0.99999)
   6.351 +    val ((accepts, more_rejects), rejects) =
   6.352 +      chop max_imperfect imperfect |>> append perfect |>> chop remaining_max
   6.353 +  in
   6.354 +    trace_msg ctxt (fn () =>
   6.355 +        "Actually passed (" ^ string_of_int (length accepts) ^ " of " ^
   6.356 +        string_of_int (length candidates) ^ "): " ^
   6.357 +        (accepts |> map (fn ((((name, _), _), _), weight) =>
   6.358 +                            name () ^ " [" ^ Real.toString weight ^ "]")
   6.359 +                 |> commas));
   6.360 +    (accepts, more_rejects @ rejects)
   6.361 +  end
   6.362 +
   6.363 +fun if_empty_replace_with_scope thy is_built_in_const facts sc tab =
   6.364 +  if Symtab.is_empty tab then
   6.365 +    Symtab.empty
   6.366 +    |> fold (add_pconsts_in_term thy is_built_in_const false (SOME false))
   6.367 +            (map_filter (fn ((_, (sc', _)), th) =>
   6.368 +                            if sc' = sc then SOME (prop_of th) else NONE) facts)
   6.369 +  else
   6.370 +    tab
   6.371 +
   6.372 +fun consider_arities is_built_in_const th =
   6.373 +  let
   6.374 +    fun aux _ _ NONE = NONE
   6.375 +      | aux t args (SOME tab) =
   6.376 +        case t of
   6.377 +          t1 $ t2 => SOME tab |> aux t1 (t2 :: args) |> aux t2 []
   6.378 +        | Const (x as (s, _)) =>
   6.379 +          (if is_built_in_const x args |> fst then
   6.380 +             SOME tab
   6.381 +           else case Symtab.lookup tab s of
   6.382 +             NONE => SOME (Symtab.update (s, length args) tab)
   6.383 +           | SOME n => if n = length args then SOME tab else NONE)
   6.384 +        | _ => SOME tab
   6.385 +  in aux (prop_of th) [] end
   6.386 +
   6.387 +(* FIXME: This is currently only useful for polymorphic type encodings. *)
   6.388 +fun could_benefit_from_ext is_built_in_const facts =
   6.389 +  fold (consider_arities is_built_in_const o snd) facts (SOME Symtab.empty)
   6.390 +  |> is_none
   6.391 +
   6.392 +(* High enough so that it isn't wrongly considered as very relevant (e.g., for E
   6.393 +   weights), but low enough so that it is unlikely to be truncated away if few
   6.394 +   facts are included. *)
   6.395 +val special_fact_index = 75
   6.396 +
   6.397 +fun relevance_filter ctxt thres0 decay max_facts is_built_in_const
   6.398 +        (fudge as {threshold_divisor, ridiculous_threshold, ...}) facts hyp_ts
   6.399 +        concl_t =
   6.400 +  let
   6.401 +    val thy = Proof_Context.theory_of ctxt
   6.402 +    val const_tab = fold (count_fact_consts thy fudge) facts Symtab.empty
   6.403 +    val add_pconsts = add_pconsts_in_term thy is_built_in_const false o SOME
   6.404 +    val chained_ts =
   6.405 +      facts |> map_filter (fn ((_, (Chained, _)), th) => SOME (prop_of th)
   6.406 +                            | _ => NONE)
   6.407 +    val chained_const_tab = Symtab.empty |> fold (add_pconsts true) chained_ts
   6.408 +    val goal_const_tab =
   6.409 +      Symtab.empty |> fold (add_pconsts true) hyp_ts
   6.410 +                   |> add_pconsts false concl_t
   6.411 +      |> (fn tab => if Symtab.is_empty tab then chained_const_tab else tab)
   6.412 +      |> fold (if_empty_replace_with_scope thy is_built_in_const facts)
   6.413 +              [Chained, Assum, Local]
   6.414 +    fun iter j remaining_max thres rel_const_tab hopeless hopeful =
   6.415 +      let
   6.416 +        fun relevant [] _ [] =
   6.417 +            (* Nothing has been added this iteration. *)
   6.418 +            if j = 0 andalso thres >= ridiculous_threshold then
   6.419 +              (* First iteration? Try again. *)
   6.420 +              iter 0 max_facts (thres / threshold_divisor) rel_const_tab
   6.421 +                   hopeless hopeful
   6.422 +            else
   6.423 +              []
   6.424 +          | relevant candidates rejects [] =
   6.425 +            let
   6.426 +              val (accepts, more_rejects) =
   6.427 +                take_most_relevant ctxt max_facts remaining_max fudge candidates
   6.428 +              val rel_const_tab' =
   6.429 +                rel_const_tab
   6.430 +                |> fold (add_pconst_to_table false) (maps (snd o fst) accepts)
   6.431 +              fun is_dirty (c, _) =
   6.432 +                Symtab.lookup rel_const_tab' c <> Symtab.lookup rel_const_tab c
   6.433 +              val (hopeful_rejects, hopeless_rejects) =
   6.434 +                 (rejects @ hopeless, ([], []))
   6.435 +                 |-> fold (fn (ax as (_, consts), old_weight) =>
   6.436 +                              if exists is_dirty consts then
   6.437 +                                apfst (cons (ax, NONE))
   6.438 +                              else
   6.439 +                                apsnd (cons (ax, old_weight)))
   6.440 +                 |>> append (more_rejects
   6.441 +                             |> map (fn (ax as (_, consts), old_weight) =>
   6.442 +                                        (ax, if exists is_dirty consts then NONE
   6.443 +                                             else SOME old_weight)))
   6.444 +              val thres =
   6.445 +                1.0 - (1.0 - thres)
   6.446 +                      * Math.pow (decay, Real.fromInt (length accepts))
   6.447 +              val remaining_max = remaining_max - length accepts
   6.448 +            in
   6.449 +              trace_msg ctxt (fn () => "New or updated constants: " ^
   6.450 +                  commas (rel_const_tab' |> Symtab.dest
   6.451 +                          |> subtract (op =) (rel_const_tab |> Symtab.dest)
   6.452 +                          |> map string_for_hyper_pconst));
   6.453 +              map (fst o fst) accepts @
   6.454 +              (if remaining_max = 0 then
   6.455 +                 []
   6.456 +               else
   6.457 +                 iter (j + 1) remaining_max thres rel_const_tab'
   6.458 +                      hopeless_rejects hopeful_rejects)
   6.459 +            end
   6.460 +          | relevant candidates rejects
   6.461 +                     (((ax as (((_, stature), _), fact_consts)), cached_weight)
   6.462 +                      :: hopeful) =
   6.463 +            let
   6.464 +              val weight =
   6.465 +                case cached_weight of
   6.466 +                  SOME w => w
   6.467 +                | NONE => fact_weight fudge stature const_tab rel_const_tab
   6.468 +                                      chained_const_tab fact_consts
   6.469 +            in
   6.470 +              if weight >= thres then
   6.471 +                relevant ((ax, weight) :: candidates) rejects hopeful
   6.472 +              else
   6.473 +                relevant candidates ((ax, weight) :: rejects) hopeful
   6.474 +            end
   6.475 +        in
   6.476 +          trace_msg ctxt (fn () =>
   6.477 +              "ITERATION " ^ string_of_int j ^ ": current threshold: " ^
   6.478 +              Real.toString thres ^ ", constants: " ^
   6.479 +              commas (rel_const_tab |> Symtab.dest
   6.480 +                      |> filter (curry (op <>) [] o snd)
   6.481 +                      |> map string_for_hyper_pconst));
   6.482 +          relevant [] [] hopeful
   6.483 +        end
   6.484 +    fun uses_const s t =
   6.485 +      fold_aterms (curry (fn (Const (s', _), false) => s' = s | (_, b) => b)) t
   6.486 +                  false
   6.487 +    fun uses_const_anywhere accepts s =
   6.488 +      exists (uses_const s o prop_of o snd) accepts orelse
   6.489 +      exists (uses_const s) (concl_t :: hyp_ts)
   6.490 +    fun add_set_const_thms accepts =
   6.491 +      exists (uses_const_anywhere accepts) set_consts ? append set_thms
   6.492 +    fun insert_into_facts accepts [] = accepts
   6.493 +      | insert_into_facts accepts ths =
   6.494 +        let
   6.495 +          val add = facts |> filter (member Thm.eq_thm_prop ths o snd)
   6.496 +          val (bef, after) =
   6.497 +            accepts |> filter_out (member Thm.eq_thm_prop ths o snd)
   6.498 +                    |> take (max_facts - length add)
   6.499 +                    |> chop special_fact_index
   6.500 +        in bef @ add @ after end
   6.501 +    fun insert_special_facts accepts =
   6.502 +       (* FIXME: get rid of "ext" here once it is treated as a helper *)
   6.503 +       [] |> could_benefit_from_ext is_built_in_const accepts ? cons @{thm ext}
   6.504 +          |> add_set_const_thms accepts
   6.505 +          |> insert_into_facts accepts
   6.506 +  in
   6.507 +    facts |> map_filter (pair_consts_fact thy is_built_in_const fudge)
   6.508 +          |> iter 0 max_facts thres0 goal_const_tab []
   6.509 +          |> insert_special_facts
   6.510 +          |> tap (fn accepts => trace_msg ctxt (fn () =>
   6.511 +                      "Total relevant: " ^ string_of_int (length accepts)))
   6.512 +  end
   6.513 +
   6.514 +fun iterative_relevant_facts ctxt
   6.515 +        ({fact_thresholds = (thres0, thres1), ...} : params) prover
   6.516 +        max_facts fudge hyp_ts concl_t facts =
   6.517 +  let
   6.518 +    val thy = Proof_Context.theory_of ctxt
   6.519 +    val is_built_in_const =
   6.520 +      Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover
   6.521 +    val fudge =
   6.522 +      case fudge of
   6.523 +        SOME fudge => fudge
   6.524 +      | NONE => Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover
   6.525 +    val decay = Math.pow ((1.0 - thres1) / (1.0 - thres0),
   6.526 +                          1.0 / Real.fromInt (max_facts + 1))
   6.527 +  in
   6.528 +    trace_msg ctxt (fn () => "Considering " ^ string_of_int (length facts) ^
   6.529 +                             " facts");
   6.530 +    (if thres1 < 0.0 then
   6.531 +       facts
   6.532 +     else if thres0 > 1.0 orelse thres0 > thres1 then
   6.533 +       []
   6.534 +     else
   6.535 +       relevance_filter ctxt thres0 decay max_facts is_built_in_const fudge
   6.536 +           facts hyp_ts
   6.537 +           (concl_t |> theory_constify fudge (Context.theory_name thy)))
   6.538 +  end
   6.539 +
   6.540 +end;