equal
deleted
inserted
replaced
11 type relevance_override = Sledgehammer_Filter.relevance_override |
11 type relevance_override = Sledgehammer_Filter.relevance_override |
12 type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command |
12 type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command |
13 type params = Sledgehammer_Provers.params |
13 type params = Sledgehammer_Provers.params |
14 type prover = Sledgehammer_Provers.prover |
14 type prover = Sledgehammer_Provers.prover |
15 |
15 |
|
16 val auto_minimization_threshold : int Unsynchronized.ref |
16 val get_minimizing_prover : Proof.context -> bool -> string -> prover |
17 val get_minimizing_prover : Proof.context -> bool -> string -> prover |
17 val run_sledgehammer : |
18 val run_sledgehammer : |
18 params -> bool -> int -> relevance_override -> (string -> minimize_command) |
19 params -> bool -> int -> relevance_override -> (string -> minimize_command) |
19 -> Proof.state -> bool * Proof.state |
20 -> Proof.state -> bool * Proof.state |
20 end; |
21 end; |
39 (if blocking then |
40 (if blocking then |
40 "" |
41 "" |
41 else |
42 else |
42 "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))) |
43 "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))) |
43 |
44 |
44 val implicit_minimization_threshold = 50 |
45 val auto_minimization_threshold = Unsynchronized.ref 50 |
45 |
46 |
46 fun get_minimizing_prover ctxt auto name (params as {debug, verbose, ...}) |
47 fun get_minimizing_prover ctxt auto name (params as {debug, verbose, ...}) |
47 minimize_command |
48 minimize_command |
48 (problem as {state, subgoal, subgoal_count, facts, ...}) = |
49 (problem as {state, subgoal, subgoal_count, facts, ...}) = |
49 get_prover ctxt auto name params minimize_command problem |
50 get_prover ctxt auto name params minimize_command problem |
51 if is_some outcome then |
52 if is_some outcome then |
52 result |
53 result |
53 else |
54 else |
54 let |
55 let |
55 val (used_facts, message) = |
56 val (used_facts, message) = |
56 if length used_facts >= implicit_minimization_threshold then |
57 if length used_facts >= !auto_minimization_threshold then |
57 minimize_facts params (not verbose) subgoal subgoal_count |
58 minimize_facts name params (not verbose) subgoal subgoal_count |
58 state |
59 state |
59 (filter_used_facts used_facts |
60 (filter_used_facts used_facts |
60 (map (apsnd single o untranslated_fact) facts)) |
61 (map (apsnd single o untranslated_fact) facts)) |
61 |>> Option.map (map fst) |
62 |>> Option.map (map fst) |
62 else |
63 else |