author  blanchet 
Mon, 15 Sep 2014 10:49:07 +0200  
changeset 58335  a5a3b576fcfb 
parent 56467  8d7d6f17c6a7 
child 58842  22b87ab47d3b 
permissions  rwrr 
43018  1 
(* Title: Tools/try.ML 
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset

2 
Author: Jasmin Blanchette, TU Muenchen 
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset

3 

43018  4 
Manager for tools that should be tried on conjectures. 
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset

5 
*) 
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset

6 

43018  7 
signature TRY = 
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset

8 
sig 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

9 
type tool = 
52639  10 
string * (int * string * (bool > Proof.state > bool * (string * Proof.state))) 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

11 

abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

12 
val tryN : string 
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset

13 

43028
1c451bbb3ad7
repaired theory merging and defined/used helpers
blanchet
parents:
43024
diff
changeset

14 
val serial_commas : string > string list > string list 
1c451bbb3ad7
repaired theory merging and defined/used helpers
blanchet
parents:
43024
diff
changeset

15 
val subgoal_count : Proof.state > int 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

16 
val get_tools : theory > tool list 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

17 
val try_tools : Proof.state > (string * string) option 
52641
c56b6fa636e8
hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
wenzelm
parents:
52639
diff
changeset

18 
val tool_setup : tool > unit 
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset

19 
end; 
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset

20 

43018  21 
structure Try : TRY = 
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset

22 
struct 
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset

23 

43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

24 
type tool = 
52639  25 
string * (int * string * (bool > Proof.state > bool * (string * Proof.state))) 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

26 

abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

27 
val tryN = "try" 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

28 

abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

29 

33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset

30 
(* preferences *) 
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset

31 

ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset

32 
val _ = 
52639  33 
ProofGeneral.preference_option ProofGeneral.category_tracing 
52645  34 
(SOME "4.0") 
56467  35 
@{system_option auto_time_limit} 
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
52006
diff
changeset

36 
"autotrytimelimit" 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
52006
diff
changeset

37 
"Time limit for automatically tried tools (in seconds)" 
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset

38 

ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset

39 

43028
1c451bbb3ad7
repaired theory merging and defined/used helpers
blanchet
parents:
43024
diff
changeset

40 
(* helpers *) 
1c451bbb3ad7
repaired theory merging and defined/used helpers
blanchet
parents:
43024
diff
changeset

41 

1c451bbb3ad7
repaired theory merging and defined/used helpers
blanchet
parents:
43024
diff
changeset

42 
fun serial_commas _ [] = ["??"] 
1c451bbb3ad7
repaired theory merging and defined/used helpers
blanchet
parents:
43024
diff
changeset

43 
 serial_commas _ [s] = [s] 
1c451bbb3ad7
repaired theory merging and defined/used helpers
blanchet
parents:
43024
diff
changeset

44 
 serial_commas conj [s1, s2] = [s1, conj, s2] 
1c451bbb3ad7
repaired theory merging and defined/used helpers
blanchet
parents:
43024
diff
changeset

45 
 serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3] 
1c451bbb3ad7
repaired theory merging and defined/used helpers
blanchet
parents:
43024
diff
changeset

46 
 serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss 
1c451bbb3ad7
repaired theory merging and defined/used helpers
blanchet
parents:
43024
diff
changeset

47 

1c451bbb3ad7
repaired theory merging and defined/used helpers
blanchet
parents:
43024
diff
changeset

48 
val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal 
1c451bbb3ad7
repaired theory merging and defined/used helpers
blanchet
parents:
43024
diff
changeset

49 

1c451bbb3ad7
repaired theory merging and defined/used helpers
blanchet
parents:
43024
diff
changeset

50 

33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset

51 
(* configuration *) 
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset

52 

43061  53 
fun tool_ord ((name1, (weight1, _, _)), (name2, (weight2, _, _))) = 
54 
prod_ord int_ord string_ord ((weight1, name1), (weight2, name2)) 

43028
1c451bbb3ad7
repaired theory merging and defined/used helpers
blanchet
parents:
43024
diff
changeset

55 

33600  56 
structure Data = Theory_Data 
57 
( 

43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

58 
type T = tool list 
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset

59 
val empty = [] 
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset

60 
val extend = I 
43028
1c451bbb3ad7
repaired theory merging and defined/used helpers
blanchet
parents:
43024
diff
changeset

61 
fun merge data : T = Ord_List.merge tool_ord data 
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset

62 
) 
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset

63 

43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

64 
val get_tools = Data.get 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

65 

43028
1c451bbb3ad7
repaired theory merging and defined/used helpers
blanchet
parents:
43024
diff
changeset

66 
val register_tool = Data.map o Ord_List.insert tool_ord 
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset

67 

52641
c56b6fa636e8
hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
wenzelm
parents:
52639
diff
changeset

68 

43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

69 
(* try command *) 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

70 

abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

71 
fun try_tools state = 
43028
1c451bbb3ad7
repaired theory merging and defined/used helpers
blanchet
parents:
43024
diff
changeset

72 
if subgoal_count state = 0 then 
1c451bbb3ad7
repaired theory merging and defined/used helpers
blanchet
parents:
43024
diff
changeset

73 
(Output.urgent_message "No subgoal!"; NONE) 
1c451bbb3ad7
repaired theory merging and defined/used helpers
blanchet
parents:
43024
diff
changeset

74 
else 
1c451bbb3ad7
repaired theory merging and defined/used helpers
blanchet
parents:
43024
diff
changeset

75 
get_tools (Proof.theory_of state) 
1c451bbb3ad7
repaired theory merging and defined/used helpers
blanchet
parents:
43024
diff
changeset

76 
> tap (fn tools => 
1c451bbb3ad7
repaired theory merging and defined/used helpers
blanchet
parents:
43024
diff
changeset

77 
"Trying " ^ space_implode " " 
1c451bbb3ad7
repaired theory merging and defined/used helpers
blanchet
parents:
43024
diff
changeset

78 
(serial_commas "and" (map (quote o fst) tools)) ^ "..." 
1c451bbb3ad7
repaired theory merging and defined/used helpers
blanchet
parents:
43024
diff
changeset

79 
> Output.urgent_message) 
1c451bbb3ad7
repaired theory merging and defined/used helpers
blanchet
parents:
43024
diff
changeset

80 
> Par_List.get_some 
1c451bbb3ad7
repaired theory merging and defined/used helpers
blanchet
parents:
43024
diff
changeset

81 
(fn (name, (_, _, tool)) => 
1c451bbb3ad7
repaired theory merging and defined/used helpers
blanchet
parents:
43024
diff
changeset

82 
case try (tool false) state of 
1c451bbb3ad7
repaired theory merging and defined/used helpers
blanchet
parents:
43024
diff
changeset

83 
SOME (true, (outcome_code, _)) => SOME (name, outcome_code) 
1c451bbb3ad7
repaired theory merging and defined/used helpers
blanchet
parents:
43024
diff
changeset

84 
 _ => NONE) 
1c451bbb3ad7
repaired theory merging and defined/used helpers
blanchet
parents:
43024
diff
changeset

85 
> tap (fn NONE => Output.urgent_message "Tried in vain."  _ => ()) 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

86 

abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

87 
val _ = 
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
43061
diff
changeset

88 
Outer_Syntax.improper_command @{command_spec "try"} 
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
43061
diff
changeset

89 
"try a combination of automatic proving and disproving tools" 
51557
4e4b56b7a3a5
more robust access Toplevel.proof_of  prefer warning via Toplevel.unknown_proof over hard crash (notably for skipped proofs);
wenzelm
parents:
46961
diff
changeset

90 
(Scan.succeed (Toplevel.unknown_proof o Toplevel.keep (ignore o try_tools o Toplevel.proof_of))) 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

91 

33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset

92 

52641
c56b6fa636e8
hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
wenzelm
parents:
52639
diff
changeset

93 
(* automatic try (TTY) *) 
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset

94 

43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

95 
fun auto_try state = 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

96 
get_tools (Proof.theory_of state) 
52639  97 
> map_filter (fn (_, (_, auto, tool)) => if Options.default_bool auto then SOME tool else NONE) 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

98 
> Par_List.get_some (fn tool => 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

99 
case try (tool true) state of 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

100 
SOME (true, (_, state)) => SOME state 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

101 
 _ => NONE) 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

102 
> the_default state 
40931  103 

33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset

104 
val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state => 
52639  105 
let 
56467  106 
val auto_time_limit = Options.default_real @{system_option auto_time_limit} 
52639  107 
in 
108 
if interact andalso not (!Toplevel.quiet) andalso auto_time_limit > 0.0 then 

109 
TimeLimit.timeLimit (seconds auto_time_limit) auto_try state 

110 
handle TimeLimit.TimeOut => state 

111 
else 

112 
state 

113 
end)) 

33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset

114 

52641
c56b6fa636e8
hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
wenzelm
parents:
52639
diff
changeset

115 

c56b6fa636e8
hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
wenzelm
parents:
52639
diff
changeset

116 
(* asynchronous print function (PIDE) *) 
c56b6fa636e8
hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
wenzelm
parents:
52639
diff
changeset

117 

c56b6fa636e8
hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
wenzelm
parents:
52639
diff
changeset

118 
fun print_function ((name, (weight, auto, tool)): tool) = 
53839
274a892b1230
avoid clash of auto print functions with query operations, notably sledgehammer (cf. 3461985dcbc3);
wenzelm
parents:
53171
diff
changeset

119 
Command.print_function ("auto_" ^ name) 
52850
9fff9f78240a
support print functions with explicit arguments, as provided by overlays;
wenzelm
parents:
52762
diff
changeset

120 
(fn {command_name, ...} => 
52641
c56b6fa636e8
hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
wenzelm
parents:
52639
diff
changeset

121 
if Keyword.is_theory_goal command_name andalso Options.default_bool auto then 
52651  122 
SOME 
56467  123 
{delay = SOME (seconds (Options.default_real @{system_option auto_time_start})), 
52651  124 
pri = ~ weight, 
125 
persistent = true, 

52953
2c927b7501c5
explicit "strict" flag for print functions (flipped internal meaning);
wenzelm
parents:
52850
diff
changeset

126 
strict = true, 
52651  127 
print_fn = fn _ => fn st => 
128 
let 

129 
val state = Toplevel.proof_of st 

52652
ebdbd5c79a13
avoid spurious warnings, notably of 'try0' about already declared simps etc.;
wenzelm
parents:
52651
diff
changeset

130 
> Proof.map_context (Context_Position.set_visible false) 
56467  131 
val auto_time_limit = Options.default_real @{system_option auto_time_limit} 
52651  132 
in 
133 
if auto_time_limit > 0.0 then 

134 
(case TimeLimit.timeLimit (seconds auto_time_limit) (fn () => tool true state) () of 

135 
(true, (_, state')) => 

136 
List.app Pretty.writeln (Proof.pretty_goal_messages state') 

137 
 _ => ()) 

138 
else () 

139 
end handle exn => if Exn.is_interrupt exn then reraise exn else ()} 

52648  140 
else NONE) 
52641
c56b6fa636e8
hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
wenzelm
parents:
52639
diff
changeset

141 

c56b6fa636e8
hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
wenzelm
parents:
52639
diff
changeset

142 

c56b6fa636e8
hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
wenzelm
parents:
52639
diff
changeset

143 
(* hybrid tool setup *) 
c56b6fa636e8
hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
wenzelm
parents:
52639
diff
changeset

144 

53171  145 
fun tool_setup tool = (Theory.setup (register_tool tool); print_function tool) 
52641
c56b6fa636e8
hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
wenzelm
parents:
52639
diff
changeset

146 

33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset

147 
end; 