author  blanchet 
Sat, 01 Dec 2012 23:55:39 +0100  
changeset 50311  c9d7ccd090e1 
parent 50310  b00eeb8e352e 
child 50319  dddcaeb92e11 
permissions  rwrr 
48380  1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer_mash.ML 
48248  2 
Author: Jasmin Blanchette, TU Muenchen 
3 

4 
Sledgehammer's machinelearningbased relevance filter (MaSh). 

5 
*) 

6 

48381  7 
signature SLEDGEHAMMER_MASH = 
48248  8 
sig 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

9 
type stature = ATP_Problem_Generate.stature 
48296
e7f01b7e244e
gracefully handle the case of empty theories when going up the accessibility chain
blanchet
parents:
48293
diff
changeset

10 
type fact = Sledgehammer_Fact.fact 
e7f01b7e244e
gracefully handle the case of empty theories when going up the accessibility chain
blanchet
parents:
48293
diff
changeset

11 
type fact_override = Sledgehammer_Fact.fact_override 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

12 
type params = Sledgehammer_Provers.params 
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset

13 
type relevance_fudge = Sledgehammer_Provers.relevance_fudge 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

14 
type prover_result = Sledgehammer_Provers.prover_result 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

15 

48308  16 
val trace : bool Config.T 
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

17 
val MaShN : string 
48379
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (MengPaulson)
blanchet
parents:
48378
diff
changeset

18 
val mepoN : string 
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (MengPaulson)
blanchet
parents:
48378
diff
changeset

19 
val mashN : string 
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

20 
val meshN : string 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

21 
val unlearnN : string 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

22 
val learn_isarN : string 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

23 
val learn_atpN : string 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

24 
val relearn_isarN : string 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

25 
val relearn_atpN : string 
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

26 
val fact_filters : string list 
48303
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

27 
val escape_meta : string > string 
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

28 
val escape_metas : string list > string 
48308  29 
val unescape_meta : string > string 
30 
val unescape_metas : string > string list 

48406  31 
val extract_query : string > string * (string * real) list 
50311  32 
val mash_CLEAR : Proof.context > unit 
33 
val mash_ADD : 

34 
Proof.context > bool 

35 
> (string * string list * string list * string list) list > unit 

36 
val mash_REPROVE : 

37 
Proof.context > bool > (string * string list) list > unit 

38 
val mash_QUERY : 

39 
Proof.context > bool > int > string list * string list 

40 
> (string * real) list 

41 
val mash_unlearn : Proof.context > unit 

48378  42 
val nickname_of : thm > string 
48406  43 
val suggested_facts : 
44 
(string * 'a) list > ('b * thm) list > (('b * thm) * 'a) list 

48321  45 
val mesh_facts : 
48406  46 
int > ((('a * thm) * real) list * ('a * thm) list) list > ('a * thm) list 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

47 
val theory_ord : theory * theory > order 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

48 
val thm_ord : thm * thm > order 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

49 
val goal_of_thm : theory > thm > thm 
48321  50 
val run_prover_for_mash : 
48318  51 
Proof.context > params > string > fact list > thm > prover_result 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

52 
val features_of : 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

53 
Proof.context > string > theory > stature > term list > string list 
48404  54 
val isar_dependencies_of : unit Symtab.table > thm > string list option 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

55 
val atp_dependencies_of : 
48404  56 
Proof.context > params > string > int > fact list > unit Symtab.table 
48665  57 
> thm > bool * string list option 
48406  58 
val mash_suggested_facts : 
48321  59 
Proof.context > params > string > int > term list > term 
48435  60 
> fact list > (fact * real) list * fact list 
48383  61 
val mash_learn_proof : 
48384
83dc102041e6
learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents:
48383
diff
changeset

62 
Proof.context > params > string > term > ('a * thm) list > thm list 
83dc102041e6
learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents:
48383
diff
changeset

63 
> unit 
48395
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset

64 
val mash_learn : 
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset

65 
Proof.context > params > fact_override > thm list > bool > unit 
50311  66 
val is_mash_enabled : unit > bool 
67 
val mash_can_suggest_facts : Proof.context > bool 

48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset

68 
val relevant_facts : 
48292  69 
Proof.context > params > string > int > fact_override > term list 
48296
e7f01b7e244e
gracefully handle the case of empty theories when going up the accessibility chain
blanchet
parents:
48293
diff
changeset

70 
> term > fact list > fact list 
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

71 
val kill_learners : unit > unit 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

72 
val running_learners : unit > unit 
48248  73 
end; 
74 

48381  75 
structure Sledgehammer_MaSh : SLEDGEHAMMER_MASH = 
48248  76 
struct 
48249  77 

48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

78 
open ATP_Util 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

79 
open ATP_Problem_Generate 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

80 
open Sledgehammer_Util 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

81 
open Sledgehammer_Fact 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

82 
open Sledgehammer_Provers 
48318  83 
open Sledgehammer_Minimize 
48381  84 
open Sledgehammer_MePo 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

85 

48308  86 
val trace = 
48380  87 
Attrib.setup_config_bool @{binding sledgehammer_mash_trace} (K false) 
48308  88 
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else () 
89 

48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

90 
val MaShN = "MaSh" 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

91 

48379
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (MengPaulson)
blanchet
parents:
48378
diff
changeset

92 
val mepoN = "mepo" 
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

93 
val mashN = "mash" 
48379
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (MengPaulson)
blanchet
parents:
48378
diff
changeset

94 
val meshN = "mesh" 
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

95 

48379
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (MengPaulson)
blanchet
parents:
48378
diff
changeset

96 
val fact_filters = [meshN, mepoN, mashN] 
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

97 

48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

98 
val unlearnN = "unlearn" 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

99 
val learn_isarN = "learn_isar" 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

100 
val learn_atpN = "learn_atp" 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

101 
val relearn_isarN = "relearn_isar" 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

102 
val relearn_atpN = "relearn_atp" 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

103 

50310  104 
fun mash_script () = Path.explode "$ISABELLE_SLEDGEHAMMER_MASH/src/mash.py" 
48394
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset

105 
fun mash_model_dir () = 
50310  106 
Path.explode "$ISABELLE_HOME_USER/mash" 
107 
> tap Isabelle_System.mkdir 

48394
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset

108 
val mash_state_dir = mash_model_dir 
50310  109 
fun mash_state_file () = Path.append (mash_state_dir ()) (Path.explode "state") 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

110 

48330  111 

50311  112 
(*** Lowlevel communication with MaSh ***) 
113 

114 
fun wipe_out_file file = (try (File.rm o Path.explode) file; ()) 

115 

116 
fun write_file banner (xs, f) file = 

117 
let val path = Path.explode file in 

118 
case banner of SOME s => File.write path s  NONE => (); 

119 
xs > chunk_list 500 

120 
> List.app (File.append path o space_implode "" o map f) 

121 
end 

122 

123 
fun run_mash_tool ctxt overlord save max_suggs write_cmds read_suggs = 

124 
let 

125 
val (temp_dir, serial) = 

126 
if overlord then (getenv "ISABELLE_HOME_USER", "") 

127 
else (getenv "ISABELLE_TMP", serial_string ()) 

128 
val log_file = if overlord then temp_dir ^ "/mash_log" else "/dev/null" 

129 
val err_file = temp_dir ^ "/mash_err" ^ serial 

130 
val sugg_file = temp_dir ^ "/mash_suggs" ^ serial 

131 
val cmd_file = temp_dir ^ "/mash_commands" ^ serial 

132 
val core = 

133 
"inputFile " ^ cmd_file ^ " predictions " ^ sugg_file ^ 

134 
" numberOfPredictions " ^ string_of_int max_suggs ^ 

135 
(if save then " saveModel" else "") 

136 
val command = 

137 
Path.implode (mash_script ()) ^ " quiet outputDir " ^ 

138 
Path.implode (mash_model_dir ()) ^ " log " ^ log_file ^ " " ^ core ^ 

139 
" >& " ^ err_file 

140 
> tap (fn _ => trace_msg ctxt (fn () => 

141 
case try File.read (Path.explode err_file) of 

142 
NONE => "Done" 

143 
 SOME "" => "Done" 

144 
 SOME s => "Error: " ^ elide_string 1000 s)) 

145 
fun run_on () = 

146 
(Isabelle_System.bash command; 

147 
read_suggs (fn () => 

148 
try File.read_lines (Path.explode sugg_file) > these)) 

149 
fun clean_up () = 

150 
if overlord then () 

151 
else List.app wipe_out_file [err_file, sugg_file, cmd_file] 

152 
in 

153 
write_file (SOME "") ([], K "") sugg_file; 

154 
write_file (SOME "") write_cmds cmd_file; 

155 
trace_msg ctxt (fn () => "Running " ^ command); 

156 
with_cleanup clean_up run_on () 

157 
end 

48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

158 

48308  159 
fun meta_char c = 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

160 
if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

161 
c = #")" orelse c = #"," then 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

162 
String.str c 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

163 
else 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

164 
(* fixed width, in case more digits follow *) 
48395
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset

165 
"%" ^ stringN_of_int 3 (Char.ord c) 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

166 

48308  167 
fun unmeta_chars accum [] = String.implode (rev accum) 
48395
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset

168 
 unmeta_chars accum (#"%" :: d1 :: d2 :: d3 :: cs) = 
48308  169 
(case Int.fromString (String.implode [d1, d2, d3]) of 
170 
SOME n => unmeta_chars (Char.chr n :: accum) cs 

171 
 NONE => "" (* error *)) 

48395
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset

172 
 unmeta_chars _ (#"%" :: _) = "" (* error *) 
48308  173 
 unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs 
174 

175 
val escape_meta = String.translate meta_char 

48303
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

176 
val escape_metas = map escape_meta #> space_implode " " 
48315
82d6e46c673f
fixed order of accessibles + other tweaks to MaSh
blanchet
parents:
48314
diff
changeset

177 
val unescape_meta = String.explode #> unmeta_chars [] 
82d6e46c673f
fixed order of accessibles + other tweaks to MaSh
blanchet
parents:
48314
diff
changeset

178 
val unescape_metas = 
82d6e46c673f
fixed order of accessibles + other tweaks to MaSh
blanchet
parents:
48314
diff
changeset

179 
space_explode " " #> filter_out (curry (op =) "") #> map unescape_meta 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

180 

50311  181 
fun str_of_add (name, parents, feats, deps) = 
182 
"! " ^ escape_meta name ^ ": " ^ escape_metas parents ^ "; " ^ 

183 
escape_metas feats ^ "; " ^ escape_metas deps ^ "\n" 

48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

184 

50311  185 
fun str_of_reprove (name, deps) = 
186 
"p " ^ escape_meta name ^ ": " ^ escape_metas deps ^ "\n" 

187 

188 
fun str_of_query (parents, feats) = 

189 
"? " ^ escape_metas parents ^ "; " ^ escape_metas feats ^ "\n" 

48406  190 

191 
fun extract_suggestion sugg = 

192 
case space_explode "=" sugg of 

193 
[name, weight] => 

194 
SOME (unescape_meta name, Real.fromString weight > the_default 0.0) 

195 
 _ => NONE 

196 

48311  197 
fun extract_query line = 
198 
case space_explode ":" line of 

48406  199 
[goal, suggs] => 
200 
(unescape_meta goal, 

201 
map_filter extract_suggestion (space_explode " " suggs)) 

48312  202 
 _ => ("", []) 
48311  203 

50311  204 
fun mash_CLEAR ctxt = 
205 
let val path = mash_model_dir () in 

206 
trace_msg ctxt (K "MaSh CLEAR"); 

207 
File.fold_dir (fn file => fn _ => 

208 
try File.rm (Path.append path (Path.basic file))) 

209 
path NONE; 

210 
() 

211 
end 

212 

213 
fun mash_ADD _ _ [] = () 

214 
 mash_ADD ctxt overlord adds = 

215 
(trace_msg ctxt (fn () => "MaSh ADD " ^ 

216 
elide_string 1000 (space_implode " " (map #1 adds))); 

217 
run_mash_tool ctxt overlord true 0 (adds, str_of_add) (K ())) 

218 

219 
fun mash_REPROVE _ _ [] = () 

220 
 mash_REPROVE ctxt overlord reps = 

221 
(trace_msg ctxt (fn () => "MaSh REPROVE " ^ 

222 
elide_string 1000 (space_implode " " (map #1 reps))); 

223 
run_mash_tool ctxt overlord true 0 (reps, str_of_reprove) (K ())) 

224 

225 
fun mash_QUERY ctxt overlord max_suggs (query as (_, feats)) = 

226 
(trace_msg ctxt (fn () => "MaSh QUERY " ^ space_implode " " feats); 

227 
run_mash_tool ctxt overlord false max_suggs 

228 
([query], str_of_query) 

229 
(fn suggs => 

230 
case suggs () of 

231 
[] => [] 

232 
 suggs => snd (extract_query (List.last suggs))) 

233 
handle List.Empty => []) 

234 

235 

236 
(*** Middlelevel communication with MaSh ***) 

237 

238 
datatype proof_kind = Isar_Proof  ATP_Proof  Isar_Proof_wegen_ATP_Flop 

239 

240 
fun str_of_proof_kind Isar_Proof = "i" 

241 
 str_of_proof_kind ATP_Proof = "a" 

242 
 str_of_proof_kind Isar_Proof_wegen_ATP_Flop = "x" 

243 

244 
fun proof_kind_of_str "i" = Isar_Proof 

245 
 proof_kind_of_str "a" = ATP_Proof 

246 
 proof_kind_of_str "x" = Isar_Proof_wegen_ATP_Flop 

247 

248 
(* FIXME: Here a "Graph.update_node" function would be useful *) 

249 
fun update_fact_graph_node (name, kind) = 

250 
Graph.default_node (name, Isar_Proof) 

251 
#> kind <> Isar_Proof ? Graph.map_node name (K kind) 

252 

253 
fun try_graph ctxt when def f = 

254 
f () 

255 
handle Graph.CYCLES (cycle :: _) => 

256 
(trace_msg ctxt (fn () => 

257 
"Cycle involving " ^ commas cycle ^ " when " ^ when); def) 

258 
 Graph.DUP name => 

259 
(trace_msg ctxt (fn () => 

260 
"Duplicate fact " ^ quote name ^ " when " ^ when); def) 

261 
 Graph.UNDEF name => 

262 
(trace_msg ctxt (fn () => 

263 
"Unknown fact " ^ quote name ^ " when " ^ when); def) 

264 
 exn => 

265 
if Exn.is_interrupt exn then 

266 
reraise exn 

267 
else 

268 
(trace_msg ctxt (fn () => 

269 
"Internal error when " ^ when ^ ":\n" ^ 

270 
ML_Compiler.exn_message exn); def) 

271 

272 
fun graph_info G = 

273 
string_of_int (length (Graph.keys G)) ^ " node(s), " ^ 

274 
string_of_int (fold (Integer.add o length o snd) (Graph.dest G) 0) ^ 

275 
" edge(s), " ^ 

276 
string_of_int (length (Graph.minimals G)) ^ " minimal, " ^ 

277 
string_of_int (length (Graph.maximals G)) ^ " maximal" 

278 

279 
type mash_state = {fact_G : unit Graph.T, dirty : string list option} 

280 

281 
val empty_state = {fact_G = Graph.empty, dirty = SOME []} 

282 

283 
local 

284 

285 
val version = "*** MaSh 0.0 ***" 

286 

287 
fun extract_node line = 

288 
case space_explode ":" line of 

289 
[head, parents] => 

290 
(case space_explode " " head of 

291 
[kind, name] => 

292 
SOME (unescape_meta name, unescape_metas parents, 

293 
try proof_kind_of_str kind > the_default Isar_Proof) 

294 
 _ => NONE) 

295 
 _ => NONE 

296 

297 
fun load _ (state as (true, _)) = state 

298 
 load ctxt _ = 

299 
let val path = mash_state_file () in 

300 
(true, 

301 
case try File.read_lines path of 

302 
SOME (version' :: node_lines) => 

303 
let 

304 
fun add_edge_to name parent = 

305 
Graph.default_node (parent, Isar_Proof) 

306 
#> Graph.add_edge (parent, name) 

307 
fun add_node line = 

308 
case extract_node line of 

309 
NONE => I (* shouldn't happen *) 

310 
 SOME (name, parents, kind) => 

311 
update_fact_graph_node (name, kind) 

312 
#> fold (add_edge_to name) parents 

313 
val fact_G = 

314 
try_graph ctxt "loading state" Graph.empty (fn () => 

315 
Graph.empty > version' = version ? fold add_node node_lines) 

316 
in 

317 
trace_msg ctxt (fn () => 

318 
"Loaded fact graph (" ^ graph_info fact_G ^ ")"); 

319 
{fact_G = fact_G, dirty = SOME []} 

320 
end 

321 
 _ => empty_state) 

322 
end 

323 

324 
fun save _ (state as {dirty = SOME [], ...}) = state 

325 
 save ctxt {fact_G, dirty} = 

326 
let 

327 
fun str_of_entry (name, parents, kind) = 

328 
str_of_proof_kind kind ^ " " ^ escape_meta name ^ ": " ^ 

329 
escape_metas parents ^ "\n" 

330 
fun append_entry (name, (kind, (parents, _))) = 

331 
cons (name, Graph.Keys.dest parents, kind) 

332 
val (banner, entries) = 

333 
case dirty of 

334 
SOME names => 

335 
(NONE, fold (append_entry o Graph.get_entry fact_G) names []) 

336 
 NONE => (SOME (version ^ "\n"), Graph.fold append_entry fact_G []) 

337 
in 

338 
write_file banner (entries, str_of_entry) 

339 
(Path.implode (mash_state_file ())); 

340 
trace_msg ctxt (fn () => 

341 
"Saved fact graph (" ^ graph_info fact_G ^ 

342 
(case dirty of 

343 
SOME dirty => 

344 
"; " ^ string_of_int (length dirty) ^ " dirty fact(s)" 

345 
 _ => "") ^ ")"); 

346 
{fact_G = fact_G, dirty = SOME []} 

347 
end 

348 

349 
val global_state = 

350 
Synchronized.var "Sledgehammer_MaSh.global_state" (false, empty_state) 

351 

352 
in 

353 

354 
fun mash_map ctxt f = 

355 
Synchronized.change global_state (load ctxt ##> (f #> save ctxt)) 

356 

357 
fun mash_peek ctxt f = 

358 
Synchronized.change_result global_state (load ctxt #> `snd #>> f) 

359 

360 
fun mash_get ctxt = 

361 
Synchronized.change_result global_state (load ctxt #> `snd) 

362 

363 
fun mash_unlearn ctxt = 

364 
Synchronized.change global_state (fn _ => 

365 
(mash_CLEAR ctxt; (* also removes the state file *) 

366 
(true, empty_state))) 

367 

368 
end 

369 

370 

371 
(*** Isabelle helpers ***) 

372 

48378  373 
fun parent_of_local_thm th = 
374 
let 

375 
val thy = th > Thm.theory_of_thm 

376 
val facts = thy > Global_Theory.facts_of 

377 
val space = facts > Facts.space_of 

378 
fun id_of s = #id (Name_Space.the_entry space s) 

379 
fun max_id (s', _) (s, id) = 

380 
let val id' = id_of s' in if id > id' then (s, id) else (s', id') end 

381 
in ("", ~1) > Facts.fold_static max_id facts > fst end 

382 

383 
val local_prefix = "local" ^ Long_Name.separator 

384 

385 
fun nickname_of th = 

48394
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset

386 
if Thm.has_name_hint th then 
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset

387 
let val hint = Thm.get_name_hint th in 
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset

388 
(* FIXME: There must be a better way to detect local facts. *) 
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset

389 
case try (unprefix local_prefix) hint of 
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset

390 
SOME suf => 
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset

391 
parent_of_local_thm th ^ Long_Name.separator ^ Long_Name.separator ^ suf 
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset

392 
 NONE => hint 
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset

393 
end 
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset

394 
else 
50047
45684acf0b94
thread context correctly when printing backquoted facts
blanchet
parents:
49997
diff
changeset

395 
backquote_thm (Proof_Context.init_global (Thm.theory_of_thm th)) th 
48378  396 

48330  397 
fun suggested_facts suggs facts = 
398 
let 

48378  399 
fun add_fact (fact as (_, th)) = Symtab.default (nickname_of th, fact) 
48330  400 
val tab = Symtab.empty > fold add_fact facts 
48406  401 
fun find_sugg (name, weight) = 
402 
Symtab.lookup tab name > Option.map (rpair weight) 

403 
in map_filter find_sugg suggs end 

48311  404 

48406  405 
fun sum_avg [] = 0 
48407  406 
 sum_avg xs = 
407 
Real.ceil (100000000.0 * fold (curry (op +)) xs 0.0) div length xs 

48328
ca0b7d19dd62
attempt at meshing according to more meaningful factors
blanchet
parents:
48327
diff
changeset

408 

48406  409 
fun normalize_scores [] = [] 
410 
 normalize_scores ((fact, score) :: tail) = 

411 
(fact, 1.0) :: map (apsnd (curry Real.* (1.0 / score))) tail 

48313
0faafdffa662
mesh facts by taking into consideration whether a fact is known to MeSh
blanchet
parents:
48312
diff
changeset

412 

48406  413 
fun mesh_facts max_facts [(sels, unks)] = 
414 
map fst (take max_facts sels) @ take (max_facts  length sels) unks 

48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

415 
 mesh_facts max_facts mess = 
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

416 
let 
48406  417 
val mess = mess > map (apfst (normalize_scores #> `length)) 
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

418 
val fact_eq = Thm.eq_thm o pairself snd 
48406  419 
fun score_at sels = try (nth sels) #> Option.map snd 
48320
891a24a48155
improved meshing of MaSh and MengPaulson if some MaSh suggestions are cutoff (the common case)
blanchet
parents:
48319
diff
changeset

420 
fun score_in fact ((sel_len, sels), unks) = 
48406  421 
case find_index (curry fact_eq fact o fst) sels of 
48320
891a24a48155
improved meshing of MaSh and MengPaulson if some MaSh suggestions are cutoff (the common case)
blanchet
parents:
48319
diff
changeset

422 
~1 => (case find_index (curry fact_eq fact) unks of 
48406  423 
~1 => score_at sels sel_len 
48320
891a24a48155
improved meshing of MaSh and MengPaulson if some MaSh suggestions are cutoff (the common case)
blanchet
parents:
48319
diff
changeset

424 
 _ => NONE) 
48406  425 
 rank => score_at sels rank 
426 
fun weight_of fact = mess > map_filter (score_in fact) > sum_avg 

427 
val facts = 

428 
fold (union fact_eq o map fst o take max_facts o snd o fst) mess [] 

48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

429 
in 
48406  430 
facts > map (`weight_of) > sort (int_ord o swap o pairself fst) 
48328
ca0b7d19dd62
attempt at meshing according to more meaningful factors
blanchet
parents:
48327
diff
changeset

431 
> map snd > take max_facts 
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

432 
end 
48312  433 

48395
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset

434 
val thy_feature_name_of = prefix "y" 
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset

435 
val const_name_of = prefix "c" 
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset

436 
val type_name_of = prefix "t" 
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset

437 
val class_name_of = prefix "s" 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

438 

48324  439 
fun theory_ord p = 
440 
if Theory.eq_thy p then 

441 
EQUAL 

442 
else if Theory.subthy p then 

443 
LESS 

444 
else if Theory.subthy (swap p) then 

445 
GREATER 

446 
else case int_ord (pairself (length o Theory.ancestors_of) p) of 

447 
EQUAL => string_ord (pairself Context.theory_name p) 

448 
 order => order 

449 

450 
val thm_ord = theory_ord o pairself theory_of_thm 

451 

48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

452 
val freezeT = Type.legacy_freeze_type 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

453 

ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

454 
fun freeze (t $ u) = freeze t $ freeze u 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

455 
 freeze (Abs (s, T, t)) = Abs (s, freezeT T, freeze t) 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

456 
 freeze (Var ((s, _), T)) = Free (s, freezeT T) 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

457 
 freeze (Const (s, T)) = Const (s, freezeT T) 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

458 
 freeze (Free (s, T)) = Free (s, freezeT T) 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

459 
 freeze t = t 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

460 

ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

461 
fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

462 

ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

463 
fun run_prover_for_mash ctxt params prover facts goal = 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

464 
let 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

465 
val problem = 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

466 
{state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1, 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

467 
facts = facts > map (apfst (apfst (fn name => name ()))) 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

468 
> map Untranslated_Fact} 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

469 
in 
48399
4bacc8983b3d
learn from SMT proofs when they can be minimized by Metis
blanchet
parents:
48398
diff
changeset

470 
get_minimizing_prover ctxt MaSh (K (K ())) prover params (K (K (K ""))) 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

471 
problem 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

472 
end 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

473 

48326  474 
val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}] 
475 

48398  476 
val logical_consts = 
477 
[@{const_name prop}, @{const_name Pure.conjunction}] @ atp_logical_consts 

478 

48318  479 
fun interesting_terms_types_and_classes ctxt prover term_max_depth 
480 
type_max_depth ts = 

48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

481 
let 
48318  482 
fun is_bad_const (x as (s, _)) args = 
48398  483 
member (op =) logical_consts s orelse 
48318  484 
fst (is_built_in_const_for_prover ctxt prover x args) 
48304  485 
fun add_classes @{sort type} = I 
486 
 add_classes S = union (op =) (map class_name_of S) 

48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

487 
fun do_add_type (Type (s, Ts)) = 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

488 
(not (member (op =) bad_types s) ? insert (op =) (type_name_of s)) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

489 
#> fold do_add_type Ts 
48304  490 
 do_add_type (TFree (_, S)) = add_classes S 
491 
 do_add_type (TVar (_, S)) = add_classes S 

48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

492 
fun add_type T = type_max_depth >= 0 ? do_add_type T 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

493 
fun mk_app s args = 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

494 
if member (op <>) args "" then s ^ "(" ^ space_implode "," args ^ ")" 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

495 
else s 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

496 
fun patternify ~1 _ = "" 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

497 
 patternify depth t = 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

498 
case strip_comb t of 
48398  499 
(Const (x as (s, _)), args) => 
500 
if is_bad_const x args then "" 

501 
else mk_app (const_name_of s) (map (patternify (depth  1)) args) 

48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

502 
 _ => "" 
48406  503 
fun add_pattern depth t = 
504 
case patternify depth t of "" => I  s => insert (op =) s 

48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

505 
fun add_term_patterns ~1 _ = I 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

506 
 add_term_patterns depth t = 
48406  507 
add_pattern depth t #> add_term_patterns (depth  1) t 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

508 
val add_term = add_term_patterns term_max_depth 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

509 
fun add_patterns t = 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

510 
let val (head, args) = strip_comb t in 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

511 
(case head of 
48398  512 
Const (_, T) => add_term t #> add_type T 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

513 
 Free (_, T) => add_type T 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

514 
 Var (_, T) => add_type T 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

515 
 Abs (_, T, body) => add_type T #> add_patterns body 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

516 
 _ => I) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

517 
#> fold add_patterns args 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

518 
end 
48326  519 
in [] > fold add_patterns ts end 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

520 

6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

521 
fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1}) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

522 

48297  523 
val term_max_depth = 1 
524 
val type_max_depth = 1 

48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

525 

6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

526 
(* TODO: Generate type classes for types? *) 
48385  527 
fun features_of ctxt prover thy (scope, status) ts = 
48303
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

528 
thy_feature_name_of (Context.theory_name thy) :: 
48318  529 
interesting_terms_types_and_classes ctxt prover term_max_depth type_max_depth 
530 
ts 

48332
271a4a6af734
optimize parent computation in MaSh + remove temporary files
blanchet
parents:
48330
diff
changeset

531 
> forall is_lambda_free ts ? cons "no_lams" 
271a4a6af734
optimize parent computation in MaSh + remove temporary files
blanchet
parents:
48330
diff
changeset

532 
> forall (not o exists_Const is_exists) ts ? cons "no_skos" 
48385  533 
> scope <> Global ? cons "local" 
48438
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset

534 
> (case string_of_status status of "" => I  s => cons s) 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

535 

48665  536 
(* Too many dependencies is a sign that a crazy decision procedure is at work. 
537 
There isn't much to learn from such proofs. *) 

538 
val max_dependencies = 100 

539 
val atp_dependency_default_max_facts = 50 

48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

540 

48438
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset

541 
(* "type_definition_xxx" facts are characterized by their use of "CollectI". *) 
48441  542 
val typedef_deps = [@{thm CollectI} > nickname_of] 
48438
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset

543 

3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset

544 
(* "Rep_xxx_inject", "Abs_xxx_inverse", etc., are derived using these facts. *) 
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset

545 
val typedef_ths = 
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset

546 
@{thms type_definition.Abs_inverse type_definition.Rep_inverse 
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset

547 
type_definition.Rep type_definition.Rep_inject 
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset

548 
type_definition.Abs_inject type_definition.Rep_cases 
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset

549 
type_definition.Abs_cases type_definition.Rep_induct 
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset

550 
type_definition.Abs_induct type_definition.Rep_range 
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset

551 
type_definition.Abs_image} 
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset

552 
> map nickname_of 
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset

553 

48441  554 
fun is_size_def [dep] th = 
555 
(case first_field ".recs" dep of 

556 
SOME (pref, _) => 

557 
(case first_field ".size" (nickname_of th) of 

558 
SOME (pref', _) => pref = pref' 

559 
 NONE => false) 

560 
 NONE => false) 

561 
 is_size_def _ _ = false 

562 

563 
fun trim_dependencies th deps = 

48668
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset

564 
if length deps > max_dependencies then 
48438
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset

565 
NONE 
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset

566 
else 
48668
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset

567 
SOME (if deps = typedef_deps orelse 
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset

568 
exists (member (op =) typedef_ths) deps orelse 
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset

569 
is_size_def deps th then 
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset

570 
[] 
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset

571 
else 
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset

572 
deps) 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

573 

48441  574 
fun isar_dependencies_of all_names th = 
575 
th > thms_in_proof (SOME all_names) > trim_dependencies th 

48404  576 

577 
fun atp_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover 

578 
auto_level facts all_names th = 

48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

579 
case isar_dependencies_of all_names th of 
48665  580 
SOME [] => (false, SOME []) 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

581 
 isar_deps => 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

582 
let 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

583 
val thy = Proof_Context.theory_of ctxt 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

584 
val goal = goal_of_thm thy th 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

585 
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

586 
val facts = facts > filter (fn (_, th') => thm_ord (th', th) = LESS) 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

587 
fun fix_name ((_, stature), th) = ((fn () => nickname_of th, stature), th) 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

588 
fun is_dep dep (_, th) = nickname_of th = dep 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

589 
fun add_isar_dep facts dep accum = 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

590 
if exists (is_dep dep) accum then 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

591 
accum 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

592 
else case find_first (is_dep dep) facts of 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

593 
SOME ((name, status), th) => accum @ [((name, status), th)] 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

594 
 NONE => accum (* shouldn't happen *) 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

595 
val facts = 
48406  596 
facts > mepo_suggested_facts ctxt params prover 
48665  597 
(max_facts > the_default atp_dependency_default_max_facts) 
48404  598 
NONE hyp_ts concl_t 
599 
> fold (add_isar_dep facts) (these isar_deps) 

48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

600 
> map fix_name 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

601 
in 
48404  602 
if verbose andalso auto_level = 0 then 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

603 
let val num_facts = length facts in 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

604 
"MaSh: " ^ quote prover ^ " on " ^ quote (nickname_of th) ^ 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

605 
" with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

606 
"." 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

607 
> Output.urgent_message 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

608 
end 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

609 
else 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

610 
(); 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

611 
case run_prover_for_mash ctxt params prover facts goal of 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

612 
{outcome = NONE, used_facts, ...} => 
48404  613 
(if verbose andalso auto_level = 0 then 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

614 
let val num_facts = length used_facts in 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

615 
"Found proof with " ^ string_of_int num_facts ^ " fact" ^ 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

616 
plural_s num_facts ^ "." 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

617 
> Output.urgent_message 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

618 
end 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

619 
else 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

620 
(); 
48665  621 
case used_facts > map fst > trim_dependencies th of 
622 
NONE => (false, isar_deps) 

623 
 atp_deps => (true, atp_deps)) 

624 
 _ => (false, isar_deps) 

48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

625 
end 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

626 

6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

627 

6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

628 
(*** Highlevel communication with MaSh ***) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

629 

48407  630 
fun num_keys keys = Graph.Keys.fold (K (Integer.add 1)) keys 0 
48400  631 

48407  632 
fun maximal_in_graph fact_G facts = 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

633 
let 
48378  634 
val facts = [] > fold (cons o nickname_of o snd) facts 
48407  635 
val tab = Symtab.empty > fold (fn name => Symtab.default (name, ())) facts 
636 
fun insert_new seen name = 

637 
not (Symtab.defined seen name) ? insert (op =) name 

638 
fun find_maxes _ (maxs, []) = map snd maxs 

639 
 find_maxes seen (maxs, new :: news) = 

640 
find_maxes 

641 
(seen > num_keys (Graph.imm_succs fact_G new) > 1 

642 
? Symtab.default (new, ())) 

643 
(if Symtab.defined tab new then 

644 
let 

645 
val newp = Graph.all_preds fact_G [new] 

646 
fun is_ancestor x yp = member (op =) yp x 

647 
val maxs = 

648 
maxs > filter (fn (_, max) => not (is_ancestor max newp)) 

649 
in 

650 
if exists (is_ancestor new o fst) maxs then 

651 
(maxs, news) 

652 
else 

653 
((newp, new) 

654 
:: filter_out (fn (_, max) => is_ancestor max newp) maxs, 

655 
news) 

656 
end 

657 
else 

658 
(maxs, Graph.Keys.fold (insert_new seen) 

659 
(Graph.imm_preds fact_G new) news)) 

660 
in find_maxes Symtab.empty ([], Graph.maximals fact_G) end 

48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

661 

48318  662 
(* Generate more suggestions than requested, because some might be thrown out 
663 
later for various reasons and "meshing" gives better results with some 

664 
slack. *) 

48434
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset

665 
fun max_suggs_of max_facts = max_facts + Int.min (50, max_facts) 
48318  666 

48400  667 
fun is_fact_in_graph fact_G (_, th) = 
668 
can (Graph.get_node fact_G) (nickname_of th) 

48320
891a24a48155
improved meshing of MaSh and MengPaulson if some MaSh suggestions are cutoff (the common case)
blanchet
parents:
48319
diff
changeset

669 

48442  670 
fun interleave 0 _ _ = [] 
671 
 interleave n [] ys = take n ys 

672 
 interleave n xs [] = take n xs 

673 
 interleave 1 (x :: _) _ = [x] 

674 
 interleave n (x :: xs) (y :: ys) = x :: y :: interleave (n  2) xs ys 

48435  675 

48406  676 
fun mash_suggested_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts 
677 
concl_t facts = 

48301  678 
let 
48302  679 
val thy = Proof_Context.theory_of ctxt 
48434
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset

680 
val (fact_G, suggs) = 
48699  681 
mash_peek ctxt (fn {fact_G, ...} => 
48434
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset

682 
if Graph.is_empty fact_G then 
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset

683 
(fact_G, []) 
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset

684 
else 
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset

685 
let 
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset

686 
val parents = maximal_in_graph fact_G facts 
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset

687 
val feats = 
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset

688 
features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts) 
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset

689 
in 
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset

690 
(fact_G, mash_QUERY ctxt overlord (max_suggs_of max_facts) 
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset

691 
(parents, feats)) 
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset

692 
end) 
48435  693 
val sels = 
48408  694 
facts > suggested_facts suggs 
695 
(* The weights currently returned by "mash.py" are too extreme to 

696 
make any sense. *) 

48435  697 
> map fst 
698 
val (unk_global, unk_local) = 

699 
facts > filter_out (is_fact_in_graph fact_G) 

48442  700 
> List.partition (fn ((_, (scope, _)), _) => scope = Global) 
701 
in (interleave max_facts unk_local sels > weight_mepo_facts, unk_global) end 

48249  702 

48668
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset

703 
fun add_wrt_fact_graph ctxt (name, parents, feats, deps) (adds, graph) = 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

704 
let 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

705 
fun maybe_add_from from (accum as (parents, graph)) = 
48321  706 
try_graph ctxt "updating graph" accum (fn () => 
707 
(from :: parents, Graph.add_edge_acyclic (from, name) graph)) 

48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

708 
val graph = graph > Graph.default_node (name, Isar_Proof) 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

709 
val (parents, graph) = ([], graph) > fold maybe_add_from parents 
48407  710 
val (deps, _) = ([], graph) > fold maybe_add_from deps 
48404  711 
in ((name, parents, feats, deps) :: adds, graph) end 
48306  712 

48668
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset

713 
fun reprove_wrt_fact_graph ctxt (name, deps) (reps, graph) = 
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset

714 
let 
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset

715 
fun maybe_rep_from from (accum as (parents, graph)) = 
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset

716 
try_graph ctxt "updating graph" accum (fn () => 
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset

717 
(from :: parents, Graph.add_edge_acyclic (from, name) graph)) 
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

718 
val graph = graph > update_fact_graph_node (name, ATP_Proof) 
48668
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset

719 
val (deps, _) = ([], graph) > fold maybe_rep_from deps 
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset

720 
in ((name, deps) :: reps, graph) end 
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset

721 

48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

722 
fun flop_wrt_fact_graph name = 
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

723 
update_fact_graph_node (name, Isar_Proof_wegen_ATP_Flop) 
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

724 

48384
83dc102041e6
learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents:
48383
diff
changeset

725 
val learn_timeout_slack = 2.0 
48318  726 

48384
83dc102041e6
learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents:
48383
diff
changeset

727 
fun launch_thread timeout task = 
48383  728 
let 
48384
83dc102041e6
learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents:
48383
diff
changeset

729 
val hard_timeout = time_mult learn_timeout_slack timeout 
83dc102041e6
learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents:
48383
diff
changeset

730 
val birth_time = Time.now () 
83dc102041e6
learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents:
48383
diff
changeset

731 
val death_time = Time.+ (birth_time, hard_timeout) 
48442  732 
val desc = ("Machine learner for Sledgehammer", "") 
48384
83dc102041e6
learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents:
48383
diff
changeset

733 
in Async_Manager.launch MaShN birth_time death_time desc task end 
83dc102041e6
learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents:
48383
diff
changeset

734 

48400  735 
fun freshish_name () = 
736 
Date.fmt ".%Y_%m_%d_%H_%M_%S__" (Date.fromTimeLocal (Time.now ())) ^ 

737 
serial_string () 

738 

48384
83dc102041e6
learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents:
48383
diff
changeset

739 
fun mash_learn_proof ctxt ({overlord, timeout, ...} : params) prover t facts 
83dc102041e6
learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents:
48383
diff
changeset

740 
used_ths = 
83dc102041e6
learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents:
48383
diff
changeset

741 
if is_smt_prover ctxt prover then 
83dc102041e6
learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents:
48383
diff
changeset

742 
() 
83dc102041e6
learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents:
48383
diff
changeset

743 
else 
48403
1f214c653c80
don't store fresh names in fact graph, since these cannot be the parents of any other facts
blanchet
parents:
48401
diff
changeset

744 
launch_thread timeout (fn () => 
1f214c653c80
don't store fresh names in fact graph, since these cannot be the parents of any other facts
blanchet
parents:
48401
diff
changeset

745 
let 
1f214c653c80
don't store fresh names in fact graph, since these cannot be the parents of any other facts
blanchet
parents:
48401
diff
changeset

746 
val thy = Proof_Context.theory_of ctxt 
1f214c653c80
don't store fresh names in fact graph, since these cannot be the parents of any other facts
blanchet
parents:
48401
diff
changeset

747 
val name = freshish_name () 
1f214c653c80
don't store fresh names in fact graph, since these cannot be the parents of any other facts
blanchet
parents:
48401
diff
changeset

748 
val feats = features_of ctxt prover thy (Local, General) [t] 
1f214c653c80
don't store fresh names in fact graph, since these cannot be the parents of any other facts
blanchet
parents:
48401
diff
changeset

749 
val deps = used_ths > map nickname_of 
1f214c653c80
don't store fresh names in fact graph, since these cannot be the parents of any other facts
blanchet
parents:
48401
diff
changeset

750 
in 
48699  751 
mash_peek ctxt (fn {fact_G, ...} => 
48434
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset

752 
let val parents = maximal_in_graph fact_G facts in 
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset

753 
mash_ADD ctxt overlord [(name, parents, feats, deps)] 
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset

754 
end); 
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset

755 
(true, "") 
48403
1f214c653c80
don't store fresh names in fact graph, since these cannot be the parents of any other facts
blanchet
parents:
48401
diff
changeset

756 
end) 
48383  757 

50163
c62ce309dc26
more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
50047
diff
changeset

758 
fun sendback sub = Sendback.markup (sledgehammerN ^ " " ^ sub) 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

759 

ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

760 
val commit_timeout = seconds 30.0 
48332
271a4a6af734
optimize parent computation in MaSh + remove temporary files
blanchet
parents:
48330
diff
changeset

761 

48318  762 
(* The timeout is understood in a very slack fashion. *) 
48404  763 
fun mash_learn_facts ctxt (params as {debug, verbose, overlord, ...}) prover 
764 
auto_level atp learn_timeout facts = 

48304  765 
let 
48318  766 
val timer = Timer.startRealTimer () 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

767 
fun next_commit_time () = 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

768 
Time.+ (Timer.checkRealTimer timer, commit_timeout) 
48699  769 
val {fact_G, ...} = mash_get ctxt 
48400  770 
val (old_facts, new_facts) = 
48667
ac58317ef11f
rule out same "technical" theories for MePo as for MaSh
blanchet
parents:
48665
diff
changeset

771 
facts > List.partition (is_fact_in_graph fact_G) 
48400  772 
> sort (thm_ord o pairself snd) 
48308  773 
in 
48404  774 
if null new_facts andalso (not atp orelse null old_facts) then 
775 
if auto_level < 2 then 

776 
"No new " ^ (if atp then "ATP" else "Isar") ^ " proofs to learn." ^ 

777 
(if auto_level = 0 andalso not atp then 

778 
"\n\nHint: Try " ^ sendback learn_atpN ^ " to learn from ATP proofs." 

779 
else 

780 
"") 

48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

781 
else 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

782 
"" 
48308  783 
else 
48304  784 
let 
48315
82d6e46c673f
fixed order of accessibles + other tweaks to MaSh
blanchet
parents:
48314
diff
changeset

785 
val all_names = 
49997
dbbf9578e712
made MaSh more robust in the face of duplicate "nicknames" (which can happen e.g. if you have a lemma called foo(1) and another called foo_1 in the same theory)
blanchet
parents:
48699
diff
changeset

786 
Symtab.empty 
dbbf9578e712
made MaSh more robust in the face of duplicate "nicknames" (which can happen e.g. if you have a lemma called foo(1) and another called foo_1 in the same theory)
blanchet
parents:
48699
diff
changeset

787 
> fold Symtab.update (facts > map (rpair () o nickname_of o snd)) 
48439
67a6bcbd3587
removed MaSh junk arising from primrec definitions
blanchet
parents:
48438
diff
changeset

788 
fun deps_of status th = 
67a6bcbd3587
removed MaSh junk arising from primrec definitions
blanchet
parents:
48438
diff
changeset

789 
if status = Non_Rec_Def orelse status = Rec_Def then 
67a6bcbd3587
removed MaSh junk arising from primrec definitions
blanchet
parents:
48438
diff
changeset

790 
SOME [] 
67a6bcbd3587
removed MaSh junk arising from primrec definitions
blanchet
parents:
48438
diff
changeset

791 
else if atp then 
67a6bcbd3587
removed MaSh junk arising from primrec definitions
blanchet
parents:
48438
diff
changeset

792 
atp_dependencies_of ctxt params prover auto_level facts all_names th 
48665  793 
> (fn (false, _) => NONE  (true, deps) => deps) 
48404  794 
else 
48439
67a6bcbd3587
removed MaSh junk arising from primrec definitions
blanchet
parents:
48438
diff
changeset

795 
isar_dependencies_of all_names th 
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

796 
fun do_commit [] [] [] state = state 
48699  797 
 do_commit adds reps flops {fact_G, dirty} = 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

798 
let 
48699  799 
val was_empty = Graph.is_empty fact_G 
48404  800 
val (adds, fact_G) = 
48668
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset

801 
([], fact_G) > fold (add_wrt_fact_graph ctxt) adds 
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset

802 
val (reps, fact_G) = 
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset

803 
([], fact_G) > fold (reprove_wrt_fact_graph ctxt) reps 
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

804 
val fact_G = fact_G > fold flop_wrt_fact_graph flops 
48699  805 
val dirty = 
806 
case (was_empty, dirty, reps) of 

807 
(false, SOME names, []) => SOME (map #1 adds @ names) 

808 
 _ => NONE 

48404  809 
in 
810 
mash_ADD ctxt overlord (rev adds); 

811 
mash_REPROVE ctxt overlord reps; 

48699  812 
{fact_G = fact_G, dirty = dirty} 
48404  813 
end 
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

814 
fun commit last adds reps flops = 
48404  815 
(if debug andalso auto_level = 0 then 
816 
Output.urgent_message "Committing..." 

817 
else 

818 
(); 

48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

819 
mash_map ctxt (do_commit (rev adds) reps flops); 
48404  820 
if not last andalso auto_level = 0 then 
821 
let val num_proofs = length adds + length reps in 

822 
"Learned " ^ string_of_int num_proofs ^ " " ^ 

823 
(if atp then "ATP" else "Isar") ^ " proof" ^ 

824 
plural_s num_proofs ^ " in the last " ^ 

48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

825 
string_from_time commit_timeout ^ "." 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

826 
> Output.urgent_message 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

827 
end 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

828 
else 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

829 
()) 
48404  830 
fun learn_new_fact _ (accum as (_, (_, _, _, true))) = accum 
48439
67a6bcbd3587
removed MaSh junk arising from primrec definitions
blanchet
parents:
48438
diff
changeset

831 
 learn_new_fact ((_, stature as (_, status)), th) 
48404  832 
(adds, (parents, n, next_commit, _)) = 
48318  833 
let 
48378  834 
val name = nickname_of th 
48332
271a4a6af734
optimize parent computation in MaSh + remove temporary files
blanchet
parents:
48330
diff
changeset

835 
val feats = 
48385  836 
features_of ctxt prover (theory_of_thm th) stature [prop_of th] 
48439
67a6bcbd3587
removed MaSh junk arising from primrec definitions
blanchet
parents:
48438
diff
changeset

837 
val deps = deps_of status th > these 
48394
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset

838 
val n = n > not (null deps) ? Integer.add 1 
48404  839 
val adds = (name, parents, feats, deps) :: adds 
840 
val (adds, next_commit) = 

48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

841 
if Time.> (Timer.checkRealTimer timer, next_commit) then 
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

842 
(commit false adds [] []; ([], next_commit_time ())) 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

843 
else 
48404  844 
(adds, next_commit) 
845 
val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout) 

846 
in (adds, ([name], n, next_commit, timed_out)) end 

847 
val n = 

848 
if null new_facts then 

849 
0 

850 
else 

851 
let 

852 
val last_th = new_facts > List.last > snd 

853 
(* crude approximation *) 

854 
val ancestors = 

855 
old_facts 

856 
> filter (fn (_, th) => thm_ord (th, last_th) <> GREATER) 

48407  857 
val parents = maximal_in_graph fact_G ancestors 
48404  858 
val (adds, (_, n, _, _)) = 
859 
([], (parents, 0, next_commit_time (), false)) 

860 
> fold learn_new_fact new_facts 

48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

861 
in commit true adds [] []; n end 
48404  862 
fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum 
48439
67a6bcbd3587
removed MaSh junk arising from primrec definitions
blanchet
parents:
48438
diff
changeset

863 
 relearn_old_fact ((_, (_, status)), th) 
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

864 
((reps, flops), (n, next_commit, _)) = 
48404  865 
let 
866 
val name = nickname_of th 

48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

867 
val (n, reps, flops) = 
48439
67a6bcbd3587
removed MaSh junk arising from primrec definitions
blanchet
parents:
48438
diff
changeset

868 
case deps_of status th of 
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

869 
SOME deps => (n + 1, (name, deps) :: reps, flops) 
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

870 
 NONE => (n, reps, name :: flops) 
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

871 
val (reps, flops, next_commit) = 
48404  872 
if Time.> (Timer.checkRealTimer timer, next_commit) then 
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

873 
(commit false [] reps flops; ([], [], next_commit_time ())) 
48404  874 
else 
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

875 
(reps, flops, next_commit) 
48404  876 
val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout) 
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

877 
in ((reps, flops), (n, next_commit, timed_out)) end 
48404  878 
val n = 
48433  879 
if not atp orelse null old_facts then 
48404  880 
n 
881 
else 

882 
let 

48668
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset

883 
val max_isar = 1000 * max_dependencies 
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

884 
fun kind_of_proof th = 
48668
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset

885 
try (Graph.get_node fact_G) (nickname_of th) 
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

886 
> the_default Isar_Proof 
48406  887 
fun priority_of (_, th) = 
48668
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset

888 
random_range 0 max_isar 
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

889 
+ (case kind_of_proof th of 
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

890 
Isar_Proof => 0 
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

891 
 ATP_Proof => 2 * max_isar 
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

892 
 Isar_Proof_wegen_ATP_Flop => max_isar) 
48404  893 
 500 * (th > isar_dependencies_of all_names 
894 
> Option.map length 

895 
> the_default max_dependencies) 

896 
val old_facts = 

48406  897 
old_facts > map (`priority_of) 
48404  898 
> sort (int_ord o pairself fst) 
899 
> map snd 

48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

900 
val ((reps, flops), (n, _, _)) = 
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

901 
(([], []), (n, next_commit_time (), false)) 
48404  902 
> fold relearn_old_fact old_facts 
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

903 
in commit true [] reps flops; n end 
48318  904 
in 
48404  905 
if verbose orelse auto_level < 2 then 
906 
"Learned " ^ string_of_int n ^ " nontrivial " ^ 

907 
(if atp then "ATP" else "Isar") ^ " proof" ^ plural_s n ^ 

48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

908 
(if verbose then 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

909 
" in " ^ string_from_time (Timer.checkRealTimer timer) 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

910 
else 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

911 
"") ^ "." 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

912 
else 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

913 
"" 
48318  914 
end 
48308  915 
end 
48304  916 

48404  917 
fun mash_learn ctxt (params as {provers, timeout, ...}) fact_override chained 
918 
atp = 

48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

919 
let 
48396  920 
val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt 
48395
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset

921 
val ctxt = ctxt > Config.put instantiate_inducts false 
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset

922 
val facts = 
48396  923 
nearly_all_facts ctxt false fact_override Symtab.empty css chained [] 
924 
@{prop True} 

48404  925 
val num_facts = length facts 
926 
val prover = hd provers 

927 
fun learn auto_level atp = 

928 
mash_learn_facts ctxt params prover auto_level atp infinite_timeout facts 

929 
> Output.urgent_message 

48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

930 
in 
48404  931 
(if atp then 
932 
("MaShing through " ^ string_of_int num_facts ^ " fact" ^ 

933 
plural_s num_facts ^ " for ATP proofs (" ^ quote prover ^ " timeout: " ^ 

934 
string_from_time timeout ^ ").\n\nCollecting Isar proofs first..." 

935 
> Output.urgent_message; 

936 
learn 1 false; 

937 
"Now collecting ATP proofs. This may take several hours. You can \ 

938 
\safely stop the learning process at any point." 

939 
> Output.urgent_message; 

940 
learn 0 true) 

941 
else 

942 
("MaShing through " ^ string_of_int num_facts ^ " fact" ^ 

943 
plural_s num_facts ^ " for Isar proofs..." 

944 
> Output.urgent_message; 

945 
learn 0 false)) 

48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

946 
end 
48249  947 

50311  948 
fun is_mash_enabled () = (getenv "MASH" = "yes") 
949 
fun mash_can_suggest_facts ctxt = not (Graph.is_empty (#fact_G (mash_get ctxt))) 

950 

48318  951 
(* The threshold should be large enough so that MaSh doesn't kick in for Auto 
952 
Sledgehammer and Try. *) 

953 
val min_secs_for_learning = 15 

954 

48321  955 
fun relevant_facts ctxt (params as {learn, fact_filter, timeout, ...}) prover 
956 
max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts = 

48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

957 
if not (subset (op =) (the_list fact_filter, fact_filters)) then 
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

958 
error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".") 
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

959 
else if only then 
48289  960 
facts 
48321  961 
else if max_facts <= 0 orelse null facts then 
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset

962 
[] 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset

963 
else 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset

964 
let 
48327
568b3193e53e
don't include hidden facts in relevance filter + tweak MaSh learning
blanchet
parents:
48326
diff
changeset

965 
fun maybe_learn () = 
48384
83dc102041e6
learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents:
48383
diff
changeset

966 
if learn andalso not (Async_Manager.has_running_threads MaShN) andalso 
83dc102041e6
learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents:
48383
diff
changeset

967 
Time.toSeconds timeout >= min_secs_for_learning then 
83dc102041e6
learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents:
48383
diff
changeset

968 
let val timeout = time_mult learn_timeout_slack timeout in 
83dc102041e6
learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents:
48383
diff
changeset

969 
launch_thread timeout 
48404  970 
(fn () => (true, mash_learn_facts ctxt params prover 2 false 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

971 
timeout facts)) 
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

972 
end 
48318  973 
else 
974 
() 

48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

975 
val fact_filter = 
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

976 
case fact_filter of 
48379
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (MengPaulson)
blanchet
parents:
48378
diff
changeset

977 
SOME ff => (() > ff <> mepoN ? maybe_learn; ff) 
48318  978 
 NONE => 
48407  979 
if is_smt_prover ctxt prover then 
980 
mepoN 

50229  981 
else if is_mash_enabled () then 
48407  982 
(maybe_learn (); 
983 
if mash_can_suggest_facts ctxt then meshN else mepoN) 

984 
else 

985 
mepoN 

48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset

986 
val add_ths = Attrib.eval_thms ctxt add 
48292  987 
fun prepend_facts ths accepts = 
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset

988 
((facts > filter (member Thm.eq_thm_prop ths o snd)) @ 
48292  989 
(accepts > filter_out (member Thm.eq_thm_prop ths o snd))) 
48293  990 
> take max_facts 
48406  991 
fun mepo () = 
992 
facts > mepo_suggested_facts ctxt params prover max_facts NONE hyp_ts 

993 
concl_t 

994 
> weight_mepo_facts 

48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

995 
fun mash () = 
48406  996 
mash_suggested_facts ctxt params prover max_facts hyp_ts concl_t facts 
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

997 
val mess = 
48406  998 
[] > (if fact_filter <> mashN then cons (mepo (), []) else I) 
48379
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (MengPaulson)
blanchet
parents:
48378
diff
changeset

999 
> (if fact_filter <> mepoN then cons (mash ()) else I) 
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset

1000 
in 
48313
0faafdffa662
mesh facts by taking into consideration whether a fact is known to MeSh
blanchet
parents:
48312
diff
changeset

1001 
mesh_facts max_facts mess 
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset

1002 
> not (null add_ths) ? prepend_facts add_ths 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset

1003 
end 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset

1004 

48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

1005 
fun kill_learners () = Async_Manager.kill_threads MaShN "learner" 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

1006 
fun running_learners () = Async_Manager.running_threads MaShN "learner" 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

1007 

48248  1008 
end; 