author  wenzelm 
Thu, 07 Apr 2016 20:51:52 +0200  
changeset 62908  d7009a515733 
parent 62519  a564458f94db 
child 63690  48a2c88091d7 
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 = 
58892
20aa19ecf2cc
eliminated obsolete Proof.goal_message  print outcome more directly;
wenzelm
parents:
58848
diff
changeset

10 
string * (int * string * (bool > Proof.state > bool * (string * string list))) 
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 = 
58892
20aa19ecf2cc
eliminated obsolete Proof.goal_message  print outcome more directly;
wenzelm
parents:
58848
diff
changeset

25 
string * (int * string * (bool > Proof.state > bool * (string * string list))) 
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 

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

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

31 

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

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

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

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

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

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

37 

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

39 

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

40 

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

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

42 

43061  43 
fun tool_ord ((name1, (weight1, _, _)), (name2, (weight2, _, _))) = 
44 
prod_ord int_ord string_ord ((weight1, name1), (weight2, name2)) 

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

45 

33600  46 
structure Data = Theory_Data 
47 
( 

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

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

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

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

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

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

53 

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

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

55 

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

56 
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

57 

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

58 

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

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

60 

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

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

62 
if subgoal_count state = 0 then 
58843  63 
(writeln "No subgoal!"; NONE) 
43028
1c451bbb3ad7
repaired theory merging and defined/used helpers
blanchet
parents:
43024
diff
changeset

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

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

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

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

68 
(serial_commas "and" (map (quote o fst) tools)) ^ "..." 
58843  69 
> writeln) 
43028
1c451bbb3ad7
repaired theory merging and defined/used helpers
blanchet
parents:
43024
diff
changeset

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

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

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

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

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

76 

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

77 
val _ = 
59936
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59582
diff
changeset

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

79 
"try a combination of automatic proving and disproving tools" 
60190
906de96ba68a
allow diagnostic proof commands with skip_proofs;
wenzelm
parents:
60094
diff
changeset

80 
(Scan.succeed (Toplevel.keep_proof (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

81 

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

82 

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

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

84 

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

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

86 
get_tools (Proof.theory_of state) 
52639  87 
> 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

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

89 
case try (tool true) state of 
58892
20aa19ecf2cc
eliminated obsolete Proof.goal_message  print outcome more directly;
wenzelm
parents:
58848
diff
changeset

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

91 
 _ => NONE) 
58892
20aa19ecf2cc
eliminated obsolete Proof.goal_message  print outcome more directly;
wenzelm
parents:
58848
diff
changeset

92 
> the_default [] 
40931  93 

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

94 

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

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

96 

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

97 
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

98 
Command.print_function ("auto_" ^ name) 
58923  99 
(fn {keywords, command_name, ...} => 
100 
if Keyword.is_theory_goal keywords command_name andalso Options.default_bool auto then 

52651  101 
SOME 
56467  102 
{delay = SOME (seconds (Options.default_real @{system_option auto_time_start})), 
52651  103 
pri = ~ weight, 
104 
persistent = true, 

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

105 
strict = true, 
52651  106 
print_fn = fn _ => fn st => 
107 
let 

108 
val state = Toplevel.proof_of st 

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

109 
> Proof.map_context (Context_Position.set_visible false) 
56467  110 
val auto_time_limit = Options.default_real @{system_option auto_time_limit} 
52651  111 
in 
112 
if auto_time_limit > 0.0 then 

62519  113 
(case Timeout.apply (seconds auto_time_limit) (fn () => tool true state) () of 
59184
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
58923
diff
changeset

114 
(true, (_, outcome)) => List.app Output.information outcome 
52651  115 
 _ => ()) 
116 
else () 

62505  117 
end handle exn => if Exn.is_interrupt exn then Exn.reraise exn else ()} 
52648  118 
else NONE) 
52641
c56b6fa636e8
hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
wenzelm
parents:
52639
diff
changeset

119 

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

120 

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

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

122 

53171  123 
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

124 

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

125 
end; 