1327 [] => accepts |
1327 [] => accepts |
1328 | _ => (facts |> filter in_add |> map fact_of_raw_fact) @ |
1328 | _ => (facts |> filter in_add |> map fact_of_raw_fact) @ |
1329 (accepts |> filter_out in_add)) |
1329 (accepts |> filter_out in_add)) |
1330 |> take max_facts |
1330 |> take max_facts |
1331 fun mepo () = |
1331 fun mepo () = |
1332 mepo_suggested_facts ctxt params prover max_facts NONE hyp_ts concl_t |
1332 (mepo_suggested_facts ctxt params prover max_facts NONE hyp_ts concl_t facts |
1333 facts |
1333 |> weight_facts_steeply, []) |
1334 |> weight_facts_steeply |
|
1335 fun mash () = |
1334 fun mash () = |
1336 mash_suggested_facts ctxt params prover (generous_max_facts max_facts) |
1335 mash_suggested_facts ctxt params prover (generous_max_facts max_facts) hyp_ts concl_t facts |
1337 hyp_ts concl_t facts |
|
1338 |>> weight_facts_steeply |
1336 |>> weight_facts_steeply |
1339 val mess = |
1337 val mess = |
1340 (* the order is important for the "case" expression below *) |
1338 (* the order is important for the "case" expression below *) |
1341 [] |> (if effective_fact_filter <> mepoN then |
1339 [] |> effective_fact_filter <> mepoN ? cons (mash_weight, mash) |
1342 cons (mash_weight, (mash ())) |
1340 |> effective_fact_filter <> mashN ? cons (mepo_weight, mepo) |
1343 else |
1341 |> Par_List.map (apsnd (fn f => f ())) |
1344 I) |
1342 val mesh = mesh_facts (eq_snd Thm.eq_thm_prop) max_facts mess |> add_and_take |
1345 |> (if effective_fact_filter <> mashN then |
|
1346 cons (mepo_weight, (mepo (), [])) |
|
1347 else |
|
1348 I) |
|
1349 val mesh = |
|
1350 mesh_facts (eq_snd Thm.eq_thm_prop) max_facts mess |
|
1351 |> add_and_take |
|
1352 in |
1343 in |
1353 if save then MaSh.save ctxt overlord else (); |
1344 if save then MaSh.save ctxt overlord else (); |
1354 case (fact_filter, mess) of |
1345 case (fact_filter, mess) of |
1355 (NONE, [(_, (mepo, _)), (_, (mash, _))]) => |
1346 (NONE, [(_, (mepo, _)), (_, (mash, _))]) => |
1356 [(meshN, mesh), (mepoN, mepo |> map fst |> add_and_take), |
1347 [(meshN, mesh), (mepoN, mepo |> map fst |> add_and_take), |