6 *) |
6 *) |
7 |
7 |
8 signature SLEDGEHAMMER_MASH = |
8 signature SLEDGEHAMMER_MASH = |
9 sig |
9 sig |
10 type stature = ATP_Problem_Generate.stature |
10 type stature = ATP_Problem_Generate.stature |
11 type raw_fact = Sledgehammer_Fact.raw_fact |
11 type lazy_fact = Sledgehammer_Fact.lazy_fact |
12 type fact = Sledgehammer_Fact.fact |
12 type fact = Sledgehammer_Fact.fact |
13 type fact_override = Sledgehammer_Fact.fact_override |
13 type fact_override = Sledgehammer_Fact.fact_override |
14 type params = Sledgehammer_Prover.params |
14 type params = Sledgehammer_Prover.params |
15 type prover_result = Sledgehammer_Prover.prover_result |
15 type prover_result = Sledgehammer_Prover.prover_result |
16 |
16 |
54 val run_prover_for_mash : Proof.context -> params -> string -> string -> fact list -> thm -> |
54 val run_prover_for_mash : Proof.context -> params -> string -> string -> fact list -> thm -> |
55 prover_result |
55 prover_result |
56 val features_of : Proof.context -> string -> stature -> term list -> string list |
56 val features_of : Proof.context -> string -> stature -> term list -> string list |
57 val trim_dependencies : string list -> string list option |
57 val trim_dependencies : string list -> string list option |
58 val isar_dependencies_of : string Symtab.table * string Symtab.table -> thm -> string list option |
58 val isar_dependencies_of : string Symtab.table * string Symtab.table -> thm -> string list option |
59 val prover_dependencies_of : Proof.context -> params -> string -> int -> raw_fact list -> |
59 val prover_dependencies_of : Proof.context -> params -> string -> int -> lazy_fact list -> |
60 string Symtab.table * string Symtab.table -> thm -> bool * string list |
60 string Symtab.table * string Symtab.table -> thm -> bool * string list |
61 val attach_parents_to_facts : ('a * thm) list -> ('a * thm) list -> |
61 val attach_parents_to_facts : ('a * thm) list -> ('a * thm) list -> |
62 (string list * ('a * thm)) list |
62 (string list * ('a * thm)) list |
63 val num_extra_feature_facts : int |
63 val num_extra_feature_facts : int |
64 val extra_feature_factor : real |
64 val extra_feature_factor : real |
65 val weight_facts_smoothly : 'a list -> ('a * real) list |
65 val weight_facts_smoothly : 'a list -> ('a * real) list |
66 val weight_facts_steeply : 'a list -> ('a * real) list |
66 val weight_facts_steeply : 'a list -> ('a * real) list |
67 val find_mash_suggestions : Proof.context -> int -> string list -> ('a * thm) list -> |
67 val find_mash_suggestions : Proof.context -> int -> string list -> ('a * thm) list -> |
68 ('a * thm) list -> ('a * thm) list -> ('a * thm) list * ('a * thm) list |
68 ('a * thm) list -> ('a * thm) list -> ('a * thm) list * ('a * thm) list |
69 val mash_suggested_facts : Proof.context -> string -> params -> int -> term list -> term -> |
69 val mash_suggested_facts : Proof.context -> string -> params -> int -> term list -> term -> |
70 raw_fact list -> fact list * fact list |
70 lazy_fact list -> fact list * fact list |
71 |
71 |
72 val mash_unlearn : Proof.context -> unit |
72 val mash_unlearn : Proof.context -> unit |
73 val mash_learn_proof : Proof.context -> params -> term -> thm list -> unit |
73 val mash_learn_proof : Proof.context -> params -> term -> thm list -> unit |
74 val mash_learn_facts : Proof.context -> params -> string -> int -> bool -> Time.time -> |
74 val mash_learn_facts : Proof.context -> params -> string -> int -> bool -> Time.time -> |
75 raw_fact list -> string |
75 lazy_fact list -> string |
76 val mash_learn : Proof.context -> params -> fact_override -> thm list -> bool -> unit |
76 val mash_learn : Proof.context -> params -> fact_override -> thm list -> bool -> unit |
77 val mash_can_suggest_facts : Proof.context -> bool |
77 val mash_can_suggest_facts : Proof.context -> bool |
78 val mash_can_suggest_facts_fast : Proof.context -> bool |
78 val mash_can_suggest_facts_fast : Proof.context -> bool |
79 |
79 |
80 val generous_max_suggestions : int -> int |
80 val generous_max_suggestions : int -> int |
81 val mepo_weight : real |
81 val mepo_weight : real |
82 val mash_weight : real |
82 val mash_weight : real |
83 val relevant_facts : Proof.context -> params -> string -> int -> fact_override -> term list -> |
83 val relevant_facts : Proof.context -> params -> string -> int -> fact_override -> term list -> |
84 term -> raw_fact list -> (string * fact list) list |
84 term -> lazy_fact list -> (string * fact list) list |
85 end; |
85 end; |
86 |
86 |
87 structure Sledgehammer_MaSh : SLEDGEHAMMER_MASH = |
87 structure Sledgehammer_MaSh : SLEDGEHAMMER_MASH = |
88 struct |
88 struct |
89 |
89 |
1535 fun relevant_facts ctxt (params as {verbose, learn, fact_filter, timeout, ...}) prover |
1535 fun relevant_facts ctxt (params as {verbose, learn, fact_filter, timeout, ...}) prover |
1536 max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts = |
1536 max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts = |
1537 if not (subset (op =) (the_list fact_filter, fact_filters)) then |
1537 if not (subset (op =) (the_list fact_filter, fact_filters)) then |
1538 error ("Unknown fact filter: " ^ quote (the fact_filter)) |
1538 error ("Unknown fact filter: " ^ quote (the fact_filter)) |
1539 else if only then |
1539 else if only then |
1540 [("", map fact_of_raw_fact facts)] |
1540 [("", map fact_of_lazy_fact facts)] |
1541 else if max_facts <= 0 orelse null facts then |
1541 else if max_facts <= 0 orelse null facts then |
1542 [("", [])] |
1542 [("", [])] |
1543 else |
1543 else |
1544 let |
1544 let |
1545 val thy_name = Context.theory_name (Proof_Context.theory_of ctxt) |
1545 val thy_name = Context.theory_name (Proof_Context.theory_of ctxt) |