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 auto_minimize_threshold : int Unsynchronized.ref |
17 val get_minimizing_prover : Proof.context -> bool -> string -> prover |
17 val get_minimizing_prover : Proof.context -> bool -> string -> prover |
18 val run_sledgehammer : |
18 val run_sledgehammer : |
19 params -> bool -> int -> relevance_override -> (string -> minimize_command) |
19 params -> bool -> int -> relevance_override -> (string -> minimize_command) |
20 -> Proof.state -> bool * Proof.state |
20 -> Proof.state -> bool * Proof.state |
21 end; |
21 end; |
40 (if blocking then |
40 (if blocking then |
41 "" |
41 "" |
42 else |
42 else |
43 "\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))) |
44 |
44 |
45 val auto_minimization_threshold = Unsynchronized.ref (!binary_threshold) |
45 val auto_minimize_threshold = Unsynchronized.ref (!binary_threshold) |
46 |
46 |
47 fun get_minimizing_prover ctxt auto name (params as {debug, verbose, ...}) |
47 fun get_minimizing_prover ctxt auto name (params as {debug, verbose, ...}) |
48 minimize_command |
48 minimize_command |
49 (problem as {state, subgoal, subgoal_count, facts, ...}) = |
49 (problem as {state, subgoal, subgoal_count, facts, ...}) = |
50 get_prover ctxt auto name params minimize_command problem |
50 get_prover ctxt auto name params minimize_command problem |
52 if is_some outcome then |
52 if is_some outcome then |
53 result |
53 result |
54 else |
54 else |
55 let |
55 let |
56 val (used_facts, message) = |
56 val (used_facts, message) = |
57 if length used_facts >= !auto_minimization_threshold then |
57 if length used_facts >= !auto_minimize_threshold then |
58 minimize_facts name params (not verbose) subgoal subgoal_count |
58 minimize_facts name params (not verbose) subgoal subgoal_count |
59 state |
59 state |
60 (filter_used_facts used_facts |
60 (filter_used_facts used_facts |
61 (map (apsnd single o untranslated_fact) facts)) |
61 (map (apsnd single o untranslated_fact) facts)) |
62 |>> Option.map (map fst) |
62 |>> Option.map (map fst) |