author  blanchet 
Tue, 21 Dec 2010 06:53:20 +0100  
changeset 41338  ffd730fcf0ac 
parent 41337  263fe1670067 
child 41357  ae76960d86a2 
permissions  rwrr 
32564  1 
(* Title: HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML 
2 
Author: Jasmin Blanchette and Sascha Boehme and Tobias Nipkow, TU Munich 

32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset

3 
*) 
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset

4 

594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset

5 
structure Mirabelle_Sledgehammer : MIRABELLE_ACTION = 
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset

6 
struct 
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset

7 

32521  8 
val proverK = "prover" 
32541  9 
val prover_timeoutK = "prover_timeout" 
32521  10 
val keepK = "keep" 
11 
val full_typesK = "full_types" 

41155
85da8cbb4966
added support for "type_sys" option to Mirabelle
blanchet
parents:
41154
diff
changeset

12 
val type_sysK = "type_sys" 
32525  13 
val minimizeK = "minimize" 
14 
val minimize_timeoutK = "minimize_timeout" 

34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

15 
val metis_ftK = "metis_ft" 
32521  16 

17 
fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: " 

32525  18 
fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): " 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

19 
fun reconstructor_tag reconstructor id = 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

20 
"#" ^ string_of_int id ^ " " ^ (!reconstructor) ^ " (sledgehammer): " 
32521  21 

32525  22 
val separator = "" 
23 

32521  24 

32549  25 
datatype sh_data = ShData of { 
26 
calls: int, 

27 
success: int, 

39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

28 
nontriv_calls: int, 
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

29 
nontriv_success: int, 
32585  30 
lemmas: int, 
32818  31 
max_lems: int, 
32549  32 
time_isa: int, 
40062  33 
time_prover: int, 
34 
time_prover_fail: int} 

32549  35 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

36 
datatype re_data = ReData of { 
32549  37 
calls: int, 
38 
success: int, 

39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

39 
nontriv_calls: int, 
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

40 
nontriv_success: int, 
32676  41 
proofs: int, 
32549  42 
time: int, 
32550  43 
timeout: int, 
32990  44 
lemmas: int * int * int, 
39341
d2b981a0429a
indicate triviality in the list of proved things
blanchet
parents:
39340
diff
changeset

45 
posns: (Position.T * bool) list 
32550  46 
} 
32549  47 

32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

48 
datatype min_data = MinData of { 
32609  49 
succs: int, 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35830
diff
changeset

50 
ab_ratios: int 
32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

51 
} 
32521  52 

32818  53 
fun make_sh_data 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

54 
(calls,success,nontriv_calls,nontriv_success,lemmas,max_lems,time_isa, 
40062  55 
time_prover,time_prover_fail) = 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

56 
ShData{calls=calls, success=success, nontriv_calls=nontriv_calls, 
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

57 
nontriv_success=nontriv_success, lemmas=lemmas, max_lems=max_lems, 
40062  58 
time_isa=time_isa, time_prover=time_prover, 
59 
time_prover_fail=time_prover_fail} 

32521  60 

35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35830
diff
changeset

61 
fun make_min_data (succs, ab_ratios) = 
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35830
diff
changeset

62 
MinData{succs=succs, ab_ratios=ab_ratios} 
32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

63 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

64 
fun make_re_data (calls,success,nontriv_calls,nontriv_success,proofs,time, 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

65 
timeout,lemmas,posns) = 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

66 
ReData{calls=calls, success=success, nontriv_calls=nontriv_calls, 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

67 
nontriv_success=nontriv_success, proofs=proofs, time=time, 
32990  68 
timeout=timeout, lemmas=lemmas, posns=posns} 
32549  69 

39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

70 
val empty_sh_data = make_sh_data (0, 0, 0, 0, 0, 0, 0, 0, 0) 
35871
c93bda4fdf15
remove the iteration counter from Sledgehammer's minimizer
blanchet
parents:
35867
diff
changeset

71 
val empty_min_data = make_min_data (0, 0) 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

72 
val empty_re_data = make_re_data (0, 0, 0, 0, 0, 0, 0, (0,0,0), []) 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

73 

39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

74 
fun tuple_of_sh_data (ShData {calls, success, nontriv_calls, nontriv_success, 
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

75 
lemmas, max_lems, time_isa, 
40062  76 
time_prover, time_prover_fail}) = (calls, success, nontriv_calls, 
77 
nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail) 

34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

78 

35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35830
diff
changeset

79 
fun tuple_of_min_data (MinData {succs, ab_ratios}) = (succs, ab_ratios) 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

80 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

81 
fun tuple_of_re_data (ReData {calls, success, nontriv_calls, nontriv_success, 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

82 
proofs, time, timeout, lemmas, posns}) = (calls, success, nontriv_calls, 
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

83 
nontriv_success, proofs, time, timeout, lemmas, posns) 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

84 

08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

85 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

86 
datatype reconstructor_mode = 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

87 
Unminimized  Minimized  UnminimizedFT  MinimizedFT 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

88 

08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

89 
datatype data = Data of { 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

90 
sh: sh_data, 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

91 
min: min_data, 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

92 
re_u: re_data, (* reconstructor with unminimized set of lemmas *) 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

93 
re_m: re_data, (* reconstructor with minimized set of lemmas *) 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

94 
re_uft: re_data, (* reconstructor with unminimized set of lemmas and fullytyped *) 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

95 
re_mft: re_data, (* reconstructor with minimized set of lemmas and fullytyped *) 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

96 
mini: bool (* with minimization *) 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

97 
} 
32521  98 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

99 
fun make_data (sh, min, re_u, re_m, re_uft, re_mft, mini) = 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

100 
Data {sh=sh, min=min, re_u=re_u, re_m=re_m, re_uft=re_uft, re_mft=re_mft, 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

101 
mini=mini} 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

102 

08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

103 
val empty_data = make_data (empty_sh_data, empty_min_data, 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

104 
empty_re_data, empty_re_data, empty_re_data, empty_re_data, false) 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

105 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

106 
fun map_sh_data f (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) = 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

107 
let val sh' = make_sh_data (f (tuple_of_sh_data sh)) 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

108 
in make_data (sh', min, re_u, re_m, re_uft, re_mft, mini) end 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

109 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

110 
fun map_min_data f (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) = 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

111 
let val min' = make_min_data (f (tuple_of_min_data min)) 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

112 
in make_data (sh, min', re_u, re_m, re_uft, re_mft, mini) end 
32521  113 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

114 
fun map_re_data f m (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) = 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

115 
let 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

116 
fun map_me g Unminimized (u, m, uft, mft) = (g u, m, uft, mft) 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

117 
 map_me g Minimized (u, m, uft, mft) = (u, g m, uft, mft) 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

118 
 map_me g UnminimizedFT (u, m, uft, mft) = (u, m, g uft, mft) 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

119 
 map_me g MinimizedFT (u, m, uft, mft) = (u, m, uft, g mft) 
32521  120 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

121 
val f' = make_re_data o f o tuple_of_re_data 
32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

122 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

123 
val (re_u', re_m', re_uft', re_mft') = 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

124 
map_me f' m (re_u, re_m, re_uft, re_mft) 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

125 
in make_data (sh, min, re_u', re_m', re_uft', re_mft', mini) end 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

126 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

127 
fun set_mini mini (Data {sh, min, re_u, re_m, re_uft, re_mft, ...}) = 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

128 
make_data (sh, min, re_u, re_m, re_uft, re_mft, mini) 
32990  129 

130 
fun inc_max (n:int) (s,sos,m) = (s+n, sos + n*n, Int.max(m,n)); 

32521  131 

32818  132 
val inc_sh_calls = map_sh_data 
40062  133 
(fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) 
134 
=> (calls + 1, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail)) 

32549  135 

32818  136 
val inc_sh_success = map_sh_data 
40062  137 
(fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) 
138 
=> (calls, success + 1, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)) 

39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

139 

ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

140 
val inc_sh_nontriv_calls = map_sh_data 
40062  141 
(fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) 
142 
=> (calls, success, nontriv_calls + 1, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail)) 

39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

143 

ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

144 
val inc_sh_nontriv_success = map_sh_data 
40062  145 
(fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) 
146 
=> (calls, success, nontriv_calls, nontriv_success + 1, lemmas,max_lems, time_isa, time_prover, time_prover_fail)) 

32585  147 

32818  148 
fun inc_sh_lemmas n = map_sh_data 
40062  149 
(fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) 
150 
=> (calls,success,nontriv_calls, nontriv_success, lemmas+n,max_lems,time_isa,time_prover,time_prover_fail)) 

32521  151 

32818  152 
fun inc_sh_max_lems n = map_sh_data 
40062  153 
(fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) 
154 
=> (calls,success,nontriv_calls, nontriv_success, lemmas,Int.max(max_lems,n),time_isa,time_prover,time_prover_fail)) 

32549  155 

32818  156 
fun inc_sh_time_isa t = map_sh_data 
40062  157 
(fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) 
158 
=> (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa + t,time_prover,time_prover_fail)) 

32818  159 

40062  160 
fun inc_sh_time_prover t = map_sh_data 
161 
(fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) 

162 
=> (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover + t,time_prover_fail)) 

32521  163 

40062  164 
fun inc_sh_time_prover_fail t = map_sh_data 
165 
(fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) 

166 
=> (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail + t)) 

32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

167 

32818  168 
val inc_min_succs = map_min_data 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35830
diff
changeset

169 
(fn (succs,ab_ratios) => (succs+1, ab_ratios)) 
32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

170 

32818  171 
fun inc_min_ab_ratios r = map_min_data 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35830
diff
changeset

172 
(fn (succs, ab_ratios) => (succs, ab_ratios+r)) 
32549  173 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

174 
val inc_reconstructor_calls = map_re_data 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

175 
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) 
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

176 
=> (calls + 1, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns)) 
32533  177 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

178 
val inc_reconstructor_success = map_re_data 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

179 
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) 
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

180 
=> (calls, success + 1, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns)) 
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

181 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

182 
val inc_reconstructor_nontriv_calls = map_re_data 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

183 
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) 
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

184 
=> (calls, success, nontriv_calls + 1, nontriv_success, proofs, time, timeout, lemmas,posns)) 
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

185 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

186 
val inc_reconstructor_nontriv_success = map_re_data 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

187 
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) 
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

188 
=> (calls, success, nontriv_calls, nontriv_success + 1, proofs, time, timeout, lemmas,posns)) 
32676  189 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

190 
val inc_reconstructor_proofs = map_re_data 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

191 
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) 
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

192 
=> (calls, success, nontriv_calls, nontriv_success, proofs + 1, time, timeout, lemmas,posns)) 
32551
421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset

193 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

194 
fun inc_reconstructor_time m t = map_re_data 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

195 
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) 
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

196 
=> (calls, success, nontriv_calls, nontriv_success, proofs, time + t, timeout, lemmas,posns)) m 
32536  197 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

198 
val inc_reconstructor_timeout = map_re_data 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

199 
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) 
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

200 
=> (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout + 1, lemmas,posns)) 
32549  201 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

202 
fun inc_reconstructor_lemmas m n = map_re_data 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

203 
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) 
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

204 
=> (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, inc_max n lemmas, posns)) m 
32551
421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset

205 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

206 
fun inc_reconstructor_posns m pos = map_re_data 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

207 
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) 
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

208 
=> (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, pos::posns)) m 
32521  209 

210 
local 

211 

212 
val str = string_of_int 

213 
val str3 = Real.fmt (StringCvt.FIX (SOME 3)) 

214 
fun percentage a b = string_of_int (a * 100 div b) 

215 
fun time t = Real.fromInt t / 1000.0 

216 
fun avg_time t n = 

217 
if n > 0 then (Real.fromInt t / 1000.0) / Real.fromInt n else 0.0 

218 

34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

219 
fun log_sh_data log 
40062  220 
(calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail) = 
32818  221 
(log ("Total number of sledgehammer calls: " ^ str calls); 
222 
log ("Number of successful sledgehammer calls: " ^ str success); 

223 
log ("Number of sledgehammer lemmas: " ^ str lemmas); 

224 
log ("Max number of sledgehammer lemmas: " ^ str max_lems); 

225 
log ("Success rate: " ^ percentage success calls ^ "%"); 

39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

226 
log ("Total number of nontrivial sledgehammer calls: " ^ str nontriv_calls); 
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

227 
log ("Number of successful nontrivial sledgehammer calls: " ^ str nontriv_success); 
32818  228 
log ("Total time for sledgehammer calls (Isabelle): " ^ str3 (time time_isa)); 
40062  229 
log ("Total time for successful sledgehammer calls (ATP): " ^ str3 (time time_prover)); 
230 
log ("Total time for failed sledgehammer calls (ATP): " ^ str3 (time time_prover_fail)); 

32536  231 
log ("Average time for sledgehammer calls (Isabelle): " ^ 
32818  232 
str3 (avg_time time_isa calls)); 
32533  233 
log ("Average time for successful sledgehammer calls (ATP): " ^ 
40062  234 
str3 (avg_time time_prover success)); 
32536  235 
log ("Average time for failed sledgehammer calls (ATP): " ^ 
40062  236 
str3 (avg_time time_prover_fail (calls  success))) 
32533  237 
) 
32521  238 

32551
421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset

239 

39341
d2b981a0429a
indicate triviality in the list of proved things
blanchet
parents:
39340
diff
changeset

240 
fun str_of_pos (pos, triv) = 
32551
421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset

241 
let val str0 = string_of_int o the_default 0 
39341
d2b981a0429a
indicate triviality in the list of proved things
blanchet
parents:
39340
diff
changeset

242 
in 
d2b981a0429a
indicate triviality in the list of proved things
blanchet
parents:
39340
diff
changeset

243 
str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos) ^ 
d2b981a0429a
indicate triviality in the list of proved things
blanchet
parents:
39340
diff
changeset

244 
(if triv then "[T]" else "") 
d2b981a0429a
indicate triviality in the list of proved things
blanchet
parents:
39340
diff
changeset

245 
end 
32551
421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset

246 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

247 
fun log_re_data log tag sh_calls (re_calls, re_success, re_nontriv_calls, 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

248 
re_nontriv_success, re_proofs, re_time, re_timeout, 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

249 
(lemmas, lems_sos, lems_max), re_posns) = 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

250 
(log ("Total number of " ^ tag ^ "reconstructor calls: " ^ str re_calls); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

251 
log ("Number of successful " ^ tag ^ "reconstructor calls: " ^ str re_success ^ 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

252 
" (proof: " ^ str re_proofs ^ ")"); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

253 
log ("Number of " ^ tag ^ "reconstructor timeouts: " ^ str re_timeout); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

254 
log ("Success rate: " ^ percentage re_success sh_calls ^ "%"); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

255 
log ("Total number of nontrivial " ^ tag ^ "reconstructor calls: " ^ str re_nontriv_calls); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

256 
log ("Number of successful nontrivial " ^ tag ^ "reconstructor calls: " ^ str re_nontriv_success ^ 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

257 
" (proof: " ^ str re_proofs ^ ")"); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

258 
log ("Number of successful " ^ tag ^ "reconstructor lemmas: " ^ str lemmas); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

259 
log ("SOS of successful " ^ tag ^ "reconstructor lemmas: " ^ str lems_sos); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

260 
log ("Max number of successful " ^ tag ^ "reconstructor lemmas: " ^ str lems_max); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

261 
log ("Total time for successful " ^ tag ^ "reconstructor calls: " ^ str3 (time re_time)); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

262 
log ("Average time for successful " ^ tag ^ "reconstructor calls: " ^ 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

263 
str3 (avg_time re_time re_success)); 
32551
421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset

264 
if tag="" 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

265 
then log ("Proved: " ^ space_implode " " (map str_of_pos re_posns)) 
32551
421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset

266 
else () 
421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset

267 
) 
32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

268 

35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35830
diff
changeset

269 
fun log_min_data log (succs, ab_ratios) = 
32609  270 
(log ("Number of successful minimizations: " ^ string_of_int succs); 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35830
diff
changeset

271 
log ("After/before ratios: " ^ string_of_int ab_ratios) 
32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

272 
) 
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

273 

32521  274 
in 
275 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

276 
fun log_data id log (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) = 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

277 
let 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

278 
val ShData {calls=sh_calls, ...} = sh 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

279 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

280 
fun app_if (ReData {calls, ...}) f = if calls > 0 then f () else () 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

281 
fun log_re tag m = 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

282 
log_re_data log tag sh_calls (tuple_of_re_data m) 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

283 
fun log_reconstructor (tag1, m1) (tag2, m2) = app_if m1 (fn () => 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

284 
(log_re tag1 m1; log ""; app_if m2 (fn () => log_re tag2 m2))) 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

285 
in 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

286 
if sh_calls > 0 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

287 
then 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

288 
(log ("\n\n\nReport #" ^ string_of_int id ^ ":\n"); 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

289 
log_sh_data log (tuple_of_sh_data sh); 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

290 
log ""; 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

291 
if not mini 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

292 
then log_reconstructor ("", re_u) ("fullytyped ", re_uft) 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

293 
else 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

294 
app_if re_u (fn () => 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

295 
(log_reconstructor ("unminimized ", re_u) ("unminimized fullytyped ", re_uft); 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

296 
log ""; 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

297 
app_if re_m (fn () => 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

298 
(log_min_data log (tuple_of_min_data min); log ""; 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

299 
log_reconstructor ("", re_m) ("fullytyped ", re_mft)))))) 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

300 
else () 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

301 
end 
32521  302 

303 
end 

304 

305 

306 
(* Warning: we implicitly assume singlethreaded execution here! *) 

32740  307 
val data = Unsynchronized.ref ([] : (int * data) list) 
32521  308 

32740  309 
fun init id thy = (Unsynchronized.change data (cons (id, empty_data)); thy) 
32567
de411627a985
explicitly export type abbreviations (as usual in SML97);
wenzelm
parents:
32564
diff
changeset

310 
fun done id ({log, ...}: Mirabelle.done_args) = 
32521  311 
AList.lookup (op =) (!data) id 
312 
> Option.map (log_data id log) 

313 
> K () 

314 

32740  315 
fun change_data id f = (Unsynchronized.change data (AList.map_entry (op =) id f); ()) 
32521  316 

317 

40069  318 
fun get_prover ctxt args = 
33016
b73b74fe23c3
proper exceptions instead of unhandled partiality
boehmes
parents:
32991
diff
changeset

319 
let 
40062  320 
fun default_prover_name () = 
40069  321 
hd (#provers (Sledgehammer_Isar.default_params ctxt [])) 
33016
b73b74fe23c3
proper exceptions instead of unhandled partiality
boehmes
parents:
32991
diff
changeset

322 
handle Empty => error "No ATP available." 
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
40983
diff
changeset

323 
fun get_prover name = 
41264  324 
(name, Sledgehammer_Run.get_minimizing_prover ctxt false name) 
33016
b73b74fe23c3
proper exceptions instead of unhandled partiality
boehmes
parents:
32991
diff
changeset

325 
in 
b73b74fe23c3
proper exceptions instead of unhandled partiality
boehmes
parents:
32991
diff
changeset

326 
(case AList.lookup (op =) args proverK of 
40062  327 
SOME name => get_prover name 
328 
 NONE => get_prover (default_prover_name ())) 

33016
b73b74fe23c3
proper exceptions instead of unhandled partiality
boehmes
parents:
32991
diff
changeset

329 
end 
32525  330 

38988  331 
type locality = Sledgehammer_Filter.locality 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38700
diff
changeset

332 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

333 
(* hack *) 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

334 
fun reconstructor_from_msg msg = 
41154  335 
if String.isSubstring "metisFT" msg then "metisFT" 
336 
else if String.isSubstring "metis" msg then "metis" 

337 
else "smt" 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

338 

32521  339 
local 
340 

32536  341 
datatype sh_result = 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38700
diff
changeset

342 
SH_OK of int * int * (string * locality) list  
32536  343 
SH_FAIL of int * int  
344 
SH_ERROR 

345 

41155
85da8cbb4966
added support for "type_sys" option to Mirabelle
blanchet
parents:
41154
diff
changeset

346 
fun run_sh prover_name prover type_sys hard_timeout timeout dir st = 
32521  347 
let 
38998  348 
val {context = ctxt, facts = chained_ths, goal} = Proof.goal st 
349 
val i = 1 

41337
263fe1670067
mechanism to keep SMT input and output files around in Mirabelle
blanchet
parents:
41276
diff
changeset

350 
fun change_dir (SOME dir) = 
263fe1670067
mechanism to keep SMT input and output files around in Mirabelle
blanchet
parents:
41276
diff
changeset

351 
Config.put Sledgehammer_Provers.dest_dir dir 
263fe1670067
mechanism to keep SMT input and output files around in Mirabelle
blanchet
parents:
41276
diff
changeset

352 
#> Config.put SMT_Config.debug_files 
41338  353 
(dir ^ "/" ^ Name.desymbolize false (ATP_Problem.timestamp ()) ^ "_" 
354 
^ serial_string ()) 

39321  355 
 change_dir NONE = I 
356 
val st' = 

357 
st > Proof.map_context 

358 
(change_dir dir 

41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
40983
diff
changeset

359 
#> Config.put Sledgehammer_Provers.measure_run_time true) 
41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41091
diff
changeset

360 
val params as {type_sys, relevance_thresholds, max_relevant, ...} = 
40069  361 
Sledgehammer_Isar.default_params ctxt 
40554
ff446d5e9a62
turn on Sledgehammer verbosity so we can track down crashes
blanchet
parents:
40526
diff
changeset

362 
[("verbose", "true"), 
41155
85da8cbb4966
added support for "type_sys" option to Mirabelle
blanchet
parents:
41154
diff
changeset

363 
("type_sys", type_sys), 
40554
ff446d5e9a62
turn on Sledgehammer verbosity so we can track down crashes
blanchet
parents:
40526
diff
changeset

364 
("timeout", Int.toString timeout)] 
40062  365 
val default_max_relevant = 
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
40983
diff
changeset

366 
Sledgehammer_Provers.default_max_relevant_for_prover ctxt prover_name 
40369
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40301
diff
changeset

367 
val is_built_in_const = 
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
40983
diff
changeset

368 
Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover_name 
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40694
diff
changeset

369 
val relevance_fudge = 
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
40983
diff
changeset

370 
Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

371 
val relevance_override = {add = [], del = [], only = false} 
38998  372 
val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i 
41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41091
diff
changeset

373 
val no_dangerous_types = 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41091
diff
changeset

374 
Sledgehammer_ATP_Translate.types_dangerous_types type_sys 
32574
719426c9e1eb
added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents:
32571
diff
changeset

375 
val time_limit = 
719426c9e1eb
added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents:
32571
diff
changeset

376 
(case hard_timeout of 
719426c9e1eb
added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents:
32571
diff
changeset

377 
NONE => I 
719426c9e1eb
added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents:
32571
diff
changeset

378 
 SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs)) 
41274  379 
val ({outcome, message, used_facts, run_time_in_msecs} 
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
40983
diff
changeset

380 
: Sledgehammer_Provers.prover_result, 
41275  381 
time_isa) = time_limit (Mirabelle.cpu_time (fn () => 
382 
let 

383 
val facts = 

384 
Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types 

385 
relevance_thresholds 

386 
(the_default default_max_relevant max_relevant) is_built_in_const 

387 
relevance_fudge relevance_override chained_ths hyp_ts concl_t 

388 
val problem = 

389 
{state = st', goal = goal, subgoal = i, 

390 
subgoal_count = Sledgehammer_Util.subgoal_count st, 

391 
facts = facts > map Sledgehammer_Provers.Untranslated_Fact, 

392 
smt_head = NONE} 

393 
in prover params (K "") problem end)) () 

41274  394 
handle TimeLimit.TimeOut => 
395 
({outcome = SOME ATP_Proof.TimedOut, message = "", used_facts = [], 

396 
run_time_in_msecs = NONE}, ~1) 

40374
443b426e05ea
make Mirabelle work correctly if the prover (e.g. the SMT solver) returns no timing information
blanchet
parents:
40372
diff
changeset

397 
val time_prover = run_time_in_msecs > the_default ~1 
32521  398 
in 
36405  399 
case outcome of 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40200
diff
changeset

400 
NONE => (message, SH_OK (time_isa, time_prover, used_facts)) 
40062  401 
 SOME _ => (message, SH_FAIL (time_isa, time_prover)) 
32521  402 
end 
37994
b04307085a09
make TPTP generator accept full firstorder formulas
blanchet
parents:
37631
diff
changeset

403 
handle ERROR msg => ("error: " ^ msg, SH_ERROR) 
32521  404 

32454
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset

405 
fun thms_of_name ctxt name = 
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset

406 
let 
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset

407 
val lex = Keyword.get_lexicons 
32454
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset

408 
val get = maps (ProofContext.get_fact ctxt o fst) 
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset

409 
in 
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset

410 
Source.of_string name 
40526  411 
> Symbol.source 
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36954
diff
changeset

412 
> Token.source {do_recover=SOME false} lex Position.start 
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36954
diff
changeset

413 
> Token.source_proper 
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36954
diff
changeset

414 
> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE 
32454
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset

415 
> Source.exhaust 
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset

416 
end 
32452
d84edd022efe
apply metis with found theorems in case sledgehammer was successful
boehmes
parents:
32434
diff
changeset

417 

32498
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset

418 
in 
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset

419 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

420 
fun run_sledgehammer trivial args reconstructor named_thms id ({pre=st, log, ...}: Mirabelle.run_args) = 
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset

421 
let 
39340  422 
val triv_str = if trivial then "[T] " else "" 
32536  423 
val _ = change_data id inc_sh_calls 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

424 
val _ = if trivial then () else change_data id inc_sh_nontriv_calls 
40069  425 
val (prover_name, prover) = get_prover (Proof.context_of st) args 
41155
85da8cbb4966
added support for "type_sys" option to Mirabelle
blanchet
parents:
41154
diff
changeset

426 
val type_sys = AList.lookup (op =) args type_sysK > the_default "smart" 
32525  427 
val dir = AList.lookup (op =) args keepK 
32541  428 
val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30) 
41268  429 
(* always use a hard timeout, but give some slack so that the automatic 
430 
minimizer has a chance to do its magic *) 

431 
val hard_timeout = SOME (2 * timeout) 

41155
85da8cbb4966
added support for "type_sys" option to Mirabelle
blanchet
parents:
41154
diff
changeset

432 
val (msg, result) = 
85da8cbb4966
added support for "type_sys" option to Mirabelle
blanchet
parents:
41154
diff
changeset

433 
run_sh prover_name prover type_sys hard_timeout timeout dir st 
32525  434 
in 
32536  435 
case result of 
40062  436 
SH_OK (time_isa, time_prover, names) => 
38700  437 
let 
39377  438 
fun get_thms (_, Sledgehammer_Filter.Chained) = NONE 
38826  439 
 get_thms (name, loc) = 
440 
SOME ((name, loc), thms_of_name (Proof.context_of st) name) 

32525  441 
in 
32818  442 
change_data id inc_sh_success; 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

443 
if trivial then () else change_data id inc_sh_nontriv_success; 
32818  444 
change_data id (inc_sh_lemmas (length names)); 
445 
change_data id (inc_sh_max_lems (length names)); 

446 
change_data id (inc_sh_time_isa time_isa); 

40062  447 
change_data id (inc_sh_time_prover time_prover); 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

448 
reconstructor := reconstructor_from_msg msg; 
38826  449 
named_thms := SOME (map_filter get_thms names); 
39340  450 
log (sh_tag id ^ triv_str ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^ 
40062  451 
string_of_int time_prover ^ ") [" ^ prover_name ^ "]:\n" ^ msg) 
32525  452 
end 
40062  453 
 SH_FAIL (time_isa, time_prover) => 
32536  454 
let 
455 
val _ = change_data id (inc_sh_time_isa time_isa) 

40062  456 
val _ = change_data id (inc_sh_time_prover_fail time_prover) 
39340  457 
in log (sh_tag id ^ triv_str ^ "failed: " ^ msg) end 
32536  458 
 SH_ERROR => log (sh_tag id ^ "failed: " ^ msg) 
32525  459 
end 
460 

461 
end 

462 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

463 
fun run_minimize args reconstructor named_thms id 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

464 
({pre=st, log, ...}: Mirabelle.run_args) = 
32525  465 
let 
40069  466 
val ctxt = Proof.context_of st 
32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

467 
val n0 = length (these (!named_thms)) 
40069  468 
val (prover_name, _) = get_prover ctxt args 
41155
85da8cbb4966
added support for "type_sys" option to Mirabelle
blanchet
parents:
41154
diff
changeset

469 
val type_sys = AList.lookup (op =) args type_sysK > the_default "smart" 
32525  470 
val timeout = 
471 
AList.lookup (op =) args minimize_timeoutK 

40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
40554
diff
changeset

472 
> Option.map (fst o read_int o raw_explode) (* FIXME Symbol.explode (?) *) 
32525  473 
> the_default 5 
40069  474 
val params = Sledgehammer_Isar.default_params ctxt 
41155
85da8cbb4966
added support for "type_sys" option to Mirabelle
blanchet
parents:
41154
diff
changeset

475 
[("provers", prover_name), 
85da8cbb4966
added support for "type_sys" option to Mirabelle
blanchet
parents:
41154
diff
changeset

476 
("verbose", "true"), 
85da8cbb4966
added support for "type_sys" option to Mirabelle
blanchet
parents:
41154
diff
changeset

477 
("type_sys", type_sys), 
40554
ff446d5e9a62
turn on Sledgehammer verbosity so we can track down crashes
blanchet
parents:
40526
diff
changeset

478 
("timeout", Int.toString timeout)] 
37587  479 
val minimize = 
41266  480 
Sledgehammer_Minimize.minimize_facts prover_name params true 1 
40065  481 
(Sledgehammer_Util.subgoal_count st) 
32525  482 
val _ = log separator 
483 
in 

35971  484 
case minimize st (these (!named_thms)) of 
35871
c93bda4fdf15
remove the iteration counter from Sledgehammer's minimizer
blanchet
parents:
35867
diff
changeset

485 
(SOME named_thms', msg) => 
32609  486 
(change_data id inc_min_succs; 
487 
change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0)); 

32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

488 
if length named_thms' = n0 
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

489 
then log (minimize_tag id ^ "already minimal") 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

490 
else (reconstructor := reconstructor_from_msg msg; 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

491 
named_thms := SOME named_thms'; 
32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

492 
log (minimize_tag id ^ "succeeded:\n" ^ msg)) 
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

493 
) 
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

494 
 (NONE, msg) => log (minimize_tag id ^ "failed: " ^ msg) 
32525  495 
end 
496 

497 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

498 
fun run_reconstructor trivial full m name reconstructor named_thms id 
32567
de411627a985
explicitly export type abbreviations (as usual in SML97);
wenzelm
parents:
32564
diff
changeset

499 
({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) = 
32525  500 
let 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

501 
fun do_reconstructor thms ctxt = 
41154  502 
(if !reconstructor = "smt" then 
503 
SMT_Solver.smt_tac 

504 
else if full orelse !reconstructor = "metisFT" then 

505 
Metis_Tactics.metisFT_tac 

506 
else 

507 
Metis_Tactics.metis_tac) ctxt thms 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

508 
fun apply_reconstructor thms = 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

509 
Mirabelle.can_apply timeout (do_reconstructor thms) st 
32521  510 

511 
fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")" 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

512 
 with_time (true, t) = (change_data id (inc_reconstructor_success m); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

513 
if trivial then () 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

514 
else change_data id (inc_reconstructor_nontriv_success m); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

515 
change_data id (inc_reconstructor_lemmas m (length named_thms)); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

516 
change_data id (inc_reconstructor_time m t); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

517 
change_data id (inc_reconstructor_posns m (pos, trivial)); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

518 
if name = "proof" then change_data id (inc_reconstructor_proofs m) 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

519 
else (); 
32521  520 
"succeeded (" ^ string_of_int t ^ ")") 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

521 
fun timed_reconstructor thms = 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

522 
(with_time (Mirabelle.cpu_time apply_reconstructor thms), true) 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

523 
handle TimeLimit.TimeOut => (change_data id (inc_reconstructor_timeout m); 
34052  524 
("timeout", false)) 
525 
 ERROR msg => ("error: " ^ msg, false) 

32521  526 

32525  527 
val _ = log separator 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

528 
val _ = change_data id (inc_reconstructor_calls m) 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

529 
val _ = if trivial then () 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

530 
else change_data id (inc_reconstructor_nontriv_calls m) 
32521  531 
in 
32525  532 
maps snd named_thms 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

533 
> timed_reconstructor 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

534 
>> log o prefix (reconstructor_tag reconstructor id) 
34052  535 
> snd 
32521  536 
end 
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset

537 

41276
285aea0c153c
two layers of timeouts seem to be less reliable than a single layer
blanchet
parents:
41275
diff
changeset

538 
val try_timeout = seconds 5.0 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

539 

34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

540 
fun sledgehammer_action args id (st as {pre, name, ...}: Mirabelle.run_args) = 
35592
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

541 
let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in 
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

542 
if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal 
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

543 
then () else 
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

544 
let 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

545 
val reconstructor = Unsynchronized.ref "" 
38700  546 
val named_thms = 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38700
diff
changeset

547 
Unsynchronized.ref (NONE : ((string * locality) * thm list) list option) 
35592
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

548 
val minimize = AList.defined (op =) args minimizeK 
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

549 
val metis_ft = AList.defined (op =) args metis_ftK 
41276
285aea0c153c
two layers of timeouts seem to be less reliable than a single layer
blanchet
parents:
41275
diff
changeset

550 
val trivial = Try.invoke_try (SOME try_timeout) pre 
285aea0c153c
two layers of timeouts seem to be less reliable than a single layer
blanchet
parents:
41275
diff
changeset

551 
handle TimeLimit.TimeOut => false 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

552 
fun apply_reconstructor m1 m2 = 
35592
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

553 
if metis_ft 
34052  554 
then 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

555 
if not (Mirabelle.catch_result (reconstructor_tag reconstructor) false 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

556 
(run_reconstructor trivial false m1 name reconstructor 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

557 
(these (!named_thms))) id st) 
35592
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

558 
then 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

559 
(Mirabelle.catch_result (reconstructor_tag reconstructor) false 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

560 
(run_reconstructor trivial true m2 name reconstructor 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

561 
(these (!named_thms))) id st; ()) 
35592
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

562 
else () 
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

563 
else 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

564 
(Mirabelle.catch_result (reconstructor_tag reconstructor) false 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

565 
(run_reconstructor trivial false m1 name reconstructor 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

566 
(these (!named_thms))) id st; ()) 
35592
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

567 
in 
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

568 
change_data id (set_mini minimize); 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

569 
Mirabelle.catch sh_tag (run_sledgehammer trivial args reconstructor 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

570 
named_thms) id st; 
35592
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

571 
if is_some (!named_thms) 
32612  572 
then 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

573 
(apply_reconstructor Unminimized UnminimizedFT; 
35592
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

574 
if minimize andalso not (null (these (!named_thms))) 
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

575 
then 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

576 
(Mirabelle.catch minimize_tag 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

577 
(run_minimize args reconstructor named_thms) id st; 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

578 
apply_reconstructor Minimized MinimizedFT) 
35592
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

579 
else ()) 
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

580 
else () 
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

581 
end 
32818  582 
end 
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset

583 

32511  584 
fun invoke args = 
32515
e7c0d3c0494a
Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform),
boehmes
parents:
32511
diff
changeset

585 
let 
36373
66af0a49de39
move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents:
36294
diff
changeset

586 
val _ = Sledgehammer_Isar.full_types := AList.defined (op =) args full_typesK 
32521  587 
in Mirabelle.register (init, sledgehammer_action args, done) end 
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset

588 

594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset

589 
end 