equal
deleted
inserted
replaced
9 type stature = ATP_Problem_Generate.stature |
9 type stature = ATP_Problem_Generate.stature |
10 type raw_fact = Sledgehammer_Fact.raw_fact |
10 type raw_fact = Sledgehammer_Fact.raw_fact |
11 type fact = Sledgehammer_Fact.fact |
11 type fact = Sledgehammer_Fact.fact |
12 type fact_override = Sledgehammer_Fact.fact_override |
12 type fact_override = Sledgehammer_Fact.fact_override |
13 type params = Sledgehammer_Provers.params |
13 type params = Sledgehammer_Provers.params |
14 type relevance_fudge = Sledgehammer_Provers.relevance_fudge |
|
15 type prover_result = Sledgehammer_Provers.prover_result |
14 type prover_result = Sledgehammer_Provers.prover_result |
16 |
15 |
17 val trace : bool Config.T |
16 val trace : bool Config.T |
18 val MePoN : string |
17 val MePoN : string |
19 val MaShN : string |
18 val MaShN : string |
774 else case find_first (is_dep dep) facts of |
773 else case find_first (is_dep dep) facts of |
775 SOME ((_, status), th) => accum @ [(("", status), th)] |
774 SOME ((_, status), th) => accum @ [(("", status), th)] |
776 | NONE => accum (* shouldn't happen *) |
775 | NONE => accum (* shouldn't happen *) |
777 val facts = |
776 val facts = |
778 facts |
777 facts |
779 |> mepo_suggested_facts ctxt params prover |
778 |> mepo_suggested_facts ctxt params (max_facts |> the_default prover_default_max_facts) NONE |
780 (max_facts |> the_default prover_default_max_facts) NONE hyp_ts |
779 hyp_ts concl_t |
781 concl_t |
|
782 |> fold (add_isar_dep facts) isar_deps |
780 |> fold (add_isar_dep facts) isar_deps |
783 |> map nickify |
781 |> map nickify |
784 in |
782 in |
785 if verbose andalso auto_level = 0 then |
783 if verbose andalso auto_level = 0 then |
786 let val num_facts = length facts in |
784 let val num_facts = length facts in |
1327 [] => accepts |
1325 [] => accepts |
1328 | _ => (facts |> filter in_add |> map fact_of_raw_fact) @ |
1326 | _ => (facts |> filter in_add |> map fact_of_raw_fact) @ |
1329 (accepts |> filter_out in_add)) |
1327 (accepts |> filter_out in_add)) |
1330 |> take max_facts |
1328 |> take max_facts |
1331 fun mepo () = |
1329 fun mepo () = |
1332 (mepo_suggested_facts ctxt params prover max_facts NONE hyp_ts concl_t facts |
1330 (mepo_suggested_facts ctxt params max_facts NONE hyp_ts concl_t facts |
1333 |> weight_facts_steeply, []) |
1331 |> weight_facts_steeply, []) |
1334 fun mash () = |
1332 fun mash () = |
1335 mash_suggested_facts ctxt params prover (generous_max_facts max_facts) hyp_ts concl_t facts |
1333 mash_suggested_facts ctxt params prover (generous_max_facts max_facts) hyp_ts concl_t facts |
1336 |>> weight_facts_steeply |
1334 |>> weight_facts_steeply |
1337 val mess = |
1335 val mess = |