author  wenzelm 
Sat, 25 May 2013 17:40:44 +0200  
changeset 52147  9943f8067f11 
parent 52017  bc0238c1f73a 
child 52639  df830310e550 
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 

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

37 
val _ = 
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
52006
diff
changeset

38 
ProofGeneral.preference_real ProofGeneral.category_tracing 
52017
bc0238c1f73a
clarified preferences: "override" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck in PG 4.x;
wenzelm
parents:
52007
diff
changeset

39 
NONE 
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
52006
diff
changeset

40 
auto_time_limit 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
52006
diff
changeset

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

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

43 

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

44 

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

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

46 

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

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

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

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

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

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

52 

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

53 
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

54 

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

55 

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

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

57 

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

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

60 

33600  61 
structure Data = Theory_Data 
62 
( 

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

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

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

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

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

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

68 

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

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

70 

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

71 
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

72 

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

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

74 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

90 

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

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

92 
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

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

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

95 

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

96 

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

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

98 

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

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

100 
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

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

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

103 
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

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

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

106 
> the_default state 
40931  107 

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

108 
val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state => 
43018  109 
if interact andalso not (!Toplevel.quiet) andalso !auto_time_limit > 0.0 then 
51594  110 
TimeLimit.timeLimit (seconds (!auto_time_limit)) auto_try state 
40931  111 
handle TimeLimit.TimeOut => state 
112 
else 

113 
state)) 

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

114 

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

115 
end; 