author  wenzelm 
Wed, 27 Mar 2013 17:58:07 +0100  
changeset 51557  4e4b56b7a3a5 
parent 46961  5c6955f487e5 
child 51594  89bfe7a33615 
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 = 
43024
58150aa44941
prioritize try and auto try's tools, with fast ones first, with a slight preference for provers vs. counterexample generators
blanchet
parents:
43021
diff
changeset

10 
string * (int * bool Unsynchronized.ref 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

11 
* (bool > Proof.state > bool * (string * Proof.state))) 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

12 

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

13 
val tryN : string 
43018  14 
val auto_time_limit: real Unsynchronized.ref 
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset

15 

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

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

17 
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

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

19 
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

20 
val try_tools : Proof.state > (string * string) option 
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset

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

22 

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

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

25 

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

26 
type tool = 
43024
58150aa44941
prioritize try and auto try's tools, with fast ones first, with a slight preference for provers vs. counterexample generators
blanchet
parents:
43021
diff
changeset

27 
string * (int * bool Unsynchronized.ref 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

28 
* (bool > Proof.state > bool * (string * Proof.state))) 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

29 

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

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

31 

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

32 

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

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

34 

43018  35 
val auto_time_limit = Unsynchronized.ref 4.0 
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset

36 

43018  37 
val auto_try_time_limitN = "autotrytimelimit" 
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset

38 
val _ = 
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset

39 
ProofGeneralPgip.add_preference Preferences.category_tracing 
43018  40 
(Preferences.real_pref auto_time_limit 
41 
auto_try_time_limitN "Time limit for automatically tried tools (in seconds).") 

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

42 

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

43 

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

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

45 

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

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

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

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

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

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

51 

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

52 
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

53 

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

54 

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

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

56 

43061  57 
fun tool_ord ((name1, (weight1, _, _)), (name2, (weight2, _, _))) = 
58 
prod_ord int_ord string_ord ((weight1, name1), (weight2, name2)) 

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

59 

33600  60 
structure Data = Theory_Data 
61 
( 

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

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

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

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

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

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

67 

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

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

69 

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

70 
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

71 

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

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

73 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

88 
> 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

89 

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

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

91 
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

92 
"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

93 
(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

94 

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

95 

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

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

97 

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

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

99 
get_tools (Proof.theory_of state) 
43024
58150aa44941
prioritize try and auto try's tools, with fast ones first, with a slight preference for provers vs. counterexample generators
blanchet
parents:
43021
diff
changeset

100 
> map_filter (fn (_, (_, auto, tool)) => if !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

101 
> 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

102 
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

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

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

105 
> the_default state 
40931  106 

107 
(* Too large values are understood as milliseconds, ensuring compatibility with 

108 
old setting files. No users can possibly in their right mind want the user 

109 
interface to block for more than 100 seconds. *) 

110 
fun smart_seconds r = 

111 
seconds (if r >= 100.0 then 

43018  112 
(legacy_feature (quote auto_try_time_limitN ^ 
40931  113 
" expressed in milliseconds  use seconds instead"); 0.001 * r) 
114 
else 

115 
r) 

116 

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

117 
val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state => 
43018  118 
if interact andalso not (!Toplevel.quiet) andalso !auto_time_limit > 0.0 then 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

119 
TimeLimit.timeLimit (smart_seconds (!auto_time_limit)) auto_try state 
40931  120 
handle TimeLimit.TimeOut => state 
121 
else 

122 
state)) 

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

123 

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

124 
end; 