equal
deleted
inserted
replaced
37 Proof.context -> bool -> bool -> unit Symtab.table -> thm list -> thm list |
37 Proof.context -> bool -> bool -> unit Symtab.table -> thm list -> thm list |
38 -> status Termtab.table -> raw_fact list |
38 -> status Termtab.table -> raw_fact list |
39 val nearly_all_facts : |
39 val nearly_all_facts : |
40 Proof.context -> bool -> fact_override -> unit Symtab.table |
40 Proof.context -> bool -> fact_override -> unit Symtab.table |
41 -> status Termtab.table -> thm list -> term list -> term -> raw_fact list |
41 -> status Termtab.table -> thm list -> term list -> term -> raw_fact list |
42 val drop_duplicate_facts: theory -> raw_fact list -> raw_fact list |
42 val drop_duplicate_facts : raw_fact list -> raw_fact list |
43 end; |
43 end; |
44 |
44 |
45 structure Sledgehammer_Fact : SLEDGEHAMMER_FACT = |
45 structure Sledgehammer_Fact : SLEDGEHAMMER_FACT = |
46 struct |
46 struct |
47 |
47 |
58 del : (Facts.ref * Attrib.src list) list, |
58 del : (Facts.ref * Attrib.src list) list, |
59 only : bool} |
59 only : bool} |
60 |
60 |
61 (* gracefully handle huge background theories *) |
61 (* gracefully handle huge background theories *) |
62 val max_facts_for_duplicates = 50000 |
62 val max_facts_for_duplicates = 50000 |
63 val max_facts_for_duplicate_matching = 25000 |
|
64 val max_facts_for_complex_check = 25000 |
63 val max_facts_for_complex_check = 25000 |
65 val max_simps_for_clasimpset = 10000 |
64 val max_simps_for_clasimpset = 10000 |
66 |
65 |
67 (* experimental feature *) |
66 (* experimental feature *) |
68 val instantiate_inducts = |
67 val instantiate_inducts = |
550 facts |
549 facts |
551 end) |
550 end) |
552 |> maybe_instantiate_inducts ctxt hyp_ts concl_t |
551 |> maybe_instantiate_inducts ctxt hyp_ts concl_t |
553 end |
552 end |
554 |
553 |
555 fun drop_duplicate_facts thy facts = |
554 fun drop_duplicate_facts facts = |
556 let val num_facts = length facts in |
555 let val num_facts = length facts in |
557 facts |> num_facts <= max_facts_for_duplicates |
556 facts |> num_facts <= max_facts_for_duplicates ? fact_distinct (op aconv) |
558 ? fact_distinct (if num_facts > max_facts_for_duplicate_matching then op aconv |
|
559 else Pattern.matches thy o swap) |
|
560 end |
557 end |
561 |
558 |
562 end; |
559 end; |