author  blanchet 
Fri, 20 Jul 2012 22:19:46 +0200  
changeset 48392  ca998fa08cd9 
parent 48390  4147f2bc4442 
child 48394  82fc8c956cdc 
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 

48311  31 
val extract_query : string > string * string list 
48378  32 
val nickname_of : thm > string 
48321  33 
val suggested_facts : string list > ('a * thm) list > ('a * thm) list 
34 
val mesh_facts : 

35 
int > (('a * thm) list * ('a * thm) list) list > ('a * thm) list 

48324  36 
val is_likely_tautology_or_too_meta : thm > bool 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

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

39 
val goal_of_thm : theory > thm > thm 
48321  40 
val run_prover_for_mash : 
48318  41 
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

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

43 
Proof.context > string > theory > stature > term list > string list 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

44 
val isar_dependencies_of : unit Symtab.table > thm > string list 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

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

46 
Proof.context > params > string > bool > fact list > unit Symtab.table 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

47 
> thm > string list 
48332
271a4a6af734
optimize parent computation in MaSh + remove temporary files
blanchet
parents:
48330
diff
changeset

48 
val mash_CLEAR : Proof.context > unit 
48308  49 
val mash_ADD : 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

50 
Proof.context > bool 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

51 
> (string * string list * string list * string list) list > unit 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

52 
val mash_QUERY : 
48318  53 
Proof.context > bool > int > string list * string list > string list 
48332
271a4a6af734
optimize parent computation in MaSh + remove temporary files
blanchet
parents:
48330
diff
changeset

54 
val mash_unlearn : Proof.context > unit 
48318  55 
val mash_could_suggest_facts : unit > bool 
48321  56 
val mash_can_suggest_facts : Proof.context > bool 
48298  57 
val mash_suggest_facts : 
48321  58 
Proof.context > params > string > int > term list > term 
59 
> ('a * thm) list > ('a * thm) list * ('a * thm) list 

48383  60 
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

61 
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

62 
> unit 
48390
4147f2bc4442
add versioning to MaSh state + cleanup dead code
blanchet
parents:
48389
diff
changeset

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

64 
Proof.context > params > string > bool > bool > Time.time > fact list 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

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

66 
val mash_learn : Proof.context > params > bool > unit 
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset

67 
val relevant_facts : 
48292  68 
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

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

70 
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

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

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

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

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

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

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

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

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

84 

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

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

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

90 

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

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

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

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

94 

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

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

96 

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

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

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

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

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

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

102 

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

103 
fun mash_home () = getenv "MASH_HOME" 
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

104 
fun mash_state_dir () = 
48309  105 
getenv "ISABELLE_HOME_USER" ^ "/mash" 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

106 
> tap (Isabelle_System.mkdir o Path.explode) 
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

107 
fun mash_state_path () = mash_state_dir () ^ "/state" > Path.explode 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

108 

48330  109 

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

110 
(*** Isabelle helpers ***) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

111 

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

113 
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

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

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

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

117 
(* fixed width, in case more digits follow *) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

119 

48308  120 
fun unmeta_chars accum [] = String.implode (rev accum) 
121 
 unmeta_chars accum (#"\\" :: d1 :: d2 :: d3 :: cs) = 

122 
(case Int.fromString (String.implode [d1, d2, d3]) of 

123 
SOME n => unmeta_chars (Char.chr n :: accum) cs 

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

125 
 unmeta_chars _ (#"\\" :: _) = "" (* error *) 

126 
 unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs 

127 

128 
val escape_meta = String.translate meta_char 

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

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

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

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

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

133 

48311  134 
fun extract_query line = 
135 
case space_explode ":" line of 

48315
82d6e46c673f
fixed order of accessibles + other tweaks to MaSh
blanchet
parents:
48314
diff
changeset

136 
[goal_name, suggs] => (unescape_meta goal_name, unescape_metas suggs) 
48312  137 
 _ => ("", []) 
48311  138 

48378  139 
fun parent_of_local_thm th = 
140 
let 

141 
val thy = th > Thm.theory_of_thm 

142 
val facts = thy > Global_Theory.facts_of 

143 
val space = facts > Facts.space_of 

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

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

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

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

148 

149 
val local_prefix = "local" ^ Long_Name.separator 

150 

151 
fun nickname_of th = 

152 
let val hint = Thm.get_name_hint th in 

153 
(* FIXME: There must be a better way to detect local facts. *) 

154 
case try (unprefix local_prefix) hint of 

155 
SOME suff => 

156 
parent_of_local_thm th ^ Long_Name.separator ^ Long_Name.separator ^ suff 

157 
 NONE => hint 

158 
end 

159 

48330  160 
fun suggested_facts suggs facts = 
161 
let 

48378  162 
fun add_fact (fact as (_, th)) = Symtab.default (nickname_of th, fact) 
48330  163 
val tab = Symtab.empty > fold add_fact facts 
164 
in map_filter (Symtab.lookup tab) suggs end 

48311  165 

48329
5781c4620245
use better score function, based on previous evaluation (cf. Deduct 2011 slides)
blanchet
parents:
48328
diff
changeset

166 
(* Ad hoc score function roughly based on Blanchette's Ringberg 2011 data. *) 
5781c4620245
use better score function, based on previous evaluation (cf. Deduct 2011 slides)
blanchet
parents:
48328
diff
changeset

167 
fun score x = Math.pow (1.5, 15.5  0.05 * Real.fromInt x) + 15.0 
48328
ca0b7d19dd62
attempt at meshing according to more meaningful factors
blanchet
parents:
48327
diff
changeset

168 

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

169 
fun sum_sq_avg [] = 0 
48329
5781c4620245
use better score function, based on previous evaluation (cf. Deduct 2011 slides)
blanchet
parents:
48328
diff
changeset

170 
 sum_sq_avg xs = 
5781c4620245
use better score function, based on previous evaluation (cf. Deduct 2011 slides)
blanchet
parents:
48328
diff
changeset

171 
Real.ceil (100000.0 * fold (curry (op +) o score) xs 0.0) div length xs 
48313
0faafdffa662
mesh facts by taking into consideration whether a fact is known to MeSh
blanchet
parents:
48312
diff
changeset

172 

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

173 
fun mesh_facts max_facts [(selected, unknown)] = 
891a24a48155
improved meshing of MaSh and MengPaulson if some MaSh suggestions are cutoff (the common case)
blanchet
parents:
48319
diff
changeset

174 
take max_facts selected @ take (max_facts  length selected) unknown 
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

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

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

177 
val mess = mess > map (apfst (`length)) 
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

178 
val fact_eq = Thm.eq_thm o pairself snd 
48320
891a24a48155
improved meshing of MaSh and MengPaulson if some MaSh suggestions are cutoff (the common case)
blanchet
parents:
48319
diff
changeset

179 
fun score_in fact ((sel_len, sels), unks) = 
891a24a48155
improved meshing of MaSh and MengPaulson if some MaSh suggestions are cutoff (the common case)
blanchet
parents:
48319
diff
changeset

180 
case find_index (curry fact_eq fact) sels of 
891a24a48155
improved meshing of MaSh and MengPaulson if some MaSh suggestions are cutoff (the common case)
blanchet
parents:
48319
diff
changeset

181 
~1 => (case find_index (curry fact_eq fact) unks of 
48329
5781c4620245
use better score function, based on previous evaluation (cf. Deduct 2011 slides)
blanchet
parents:
48328
diff
changeset

182 
~1 => SOME sel_len 
48320
891a24a48155
improved meshing of MaSh and MengPaulson if some MaSh suggestions are cutoff (the common case)
blanchet
parents:
48319
diff
changeset

183 
 _ => NONE) 
48329
5781c4620245
use better score function, based on previous evaluation (cf. Deduct 2011 slides)
blanchet
parents:
48328
diff
changeset

184 
 j => SOME j 
48328
ca0b7d19dd62
attempt at meshing according to more meaningful factors
blanchet
parents:
48327
diff
changeset

185 
fun score_of fact = mess > map_filter (score_in fact) > sum_sq_avg 
48320
891a24a48155
improved meshing of MaSh and MengPaulson if some MaSh suggestions are cutoff (the common case)
blanchet
parents:
48319
diff
changeset

186 
val facts = fold (union fact_eq 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

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

188 
facts > map (`score_of) > sort (int_ord o swap o pairself fst) 
ca0b7d19dd62
attempt at meshing according to more meaningful factors
blanchet
parents:
48327
diff
changeset

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

190 
end 
48312  191 

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

192 
val thy_feature_prefix = "y_" 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

193 

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

194 
val thy_feature_name_of = prefix thy_feature_prefix 
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

195 
val const_name_of = prefix const_prefix 
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

196 
val type_name_of = prefix type_const_prefix 
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

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

198 

48324  199 
fun is_likely_tautology_or_too_meta th = 
200 
let 

201 
val is_boring_const = member (op =) atp_widely_irrelevant_consts 

202 
fun is_boring_bool t = 

203 
not (exists_Const (not o is_boring_const o fst) t) orelse 

204 
exists_type (exists_subtype (curry (op =) @{typ prop})) t 

205 
fun is_boring_prop (@{const Trueprop} $ t) = is_boring_bool t 

206 
 is_boring_prop (@{const "==>"} $ t $ u) = 

207 
is_boring_prop t andalso is_boring_prop u 

208 
 is_boring_prop (Const (@{const_name all}, _) $ (Abs (_, _, t)) $ u) = 

209 
is_boring_prop t andalso is_boring_prop u 

210 
 is_boring_prop (Const (@{const_name "=="}, _) $ t $ u) = 

211 
is_boring_bool t andalso is_boring_bool u 

212 
 is_boring_prop _ = true 

213 
in 

214 
is_boring_prop (prop_of th) andalso not (Thm.eq_thm_prop (@{thm ext}, th)) 

215 
end 

216 

217 
fun theory_ord p = 

218 
if Theory.eq_thy p then 

219 
EQUAL 

220 
else if Theory.subthy p then 

221 
LESS 

222 
else if Theory.subthy (swap p) then 

223 
GREATER 

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

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

226 
 order => order 

227 

228 
val thm_ord = theory_ord o pairself theory_of_thm 

229 

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

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

231 

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

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

233 
 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

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

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

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

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

238 

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

239 
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

240 

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

241 
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

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

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

244 
{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

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

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

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

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

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

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

251 

48326  252 
val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}] 
253 

48318  254 
fun interesting_terms_types_and_classes ctxt prover term_max_depth 
255 
type_max_depth ts = 

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

256 
let 
48318  257 
fun is_bad_const (x as (s, _)) args = 
258 
member (op =) atp_logical_consts s orelse 

259 
fst (is_built_in_const_for_prover ctxt prover x args) 

48304  260 
fun add_classes @{sort type} = I 
261 
 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

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

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

264 
#> fold do_add_type Ts 
48304  265 
 do_add_type (TFree (_, S)) = add_classes S 
266 
 do_add_type (TVar (_, S)) = add_classes S 

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

267 
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

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

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

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

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

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

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

274 
(Const (s, _), args) => 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

275 
mk_app (const_name_of s) (map (patternify (depth  1)) args) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

276 
 _ => "" 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

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

279 
insert (op =) (patternify depth t) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

280 
#> add_term_patterns (depth  1) t 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

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

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

284 
(case head of 
48318  285 
Const (x as (_, T)) => 
286 
not (is_bad_const x args) ? (add_term t #> add_type T) 

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

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

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

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

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

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

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

294 

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

295 
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

296 

48297  297 
val term_max_depth = 1 
298 
val type_max_depth = 1 

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

299 

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

300 
(* TODO: Generate type classes for types? *) 
48385  301 
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

302 
thy_feature_name_of (Context.theory_name thy) :: 
48318  303 
interesting_terms_types_and_classes ctxt prover term_max_depth type_max_depth 
304 
ts 

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

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

306 
> forall (not o exists_Const is_exists) ts ? cons "no_skos" 
48385  307 
> scope <> Global ? cons "local" 
48302  308 
> (case status of 
309 
General => I 

310 
 Induction => cons "induction" 

311 
 Intro => cons "intro" 

312 
 Inductive => cons "inductive" 

313 
 Elim => cons "elim" 

314 
 Simp => cons "simp" 

315 
 Def => cons "def") 

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

316 

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

317 
fun isar_dependencies_of all_facts = thms_in_proof (SOME all_facts) 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

318 

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

319 
val atp_dep_default_max_fact = 50 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

320 

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

321 
fun atp_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover auto 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

322 
facts all_names th = 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

323 
case isar_dependencies_of all_names th of 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

324 
[] => [] 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

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

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

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

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

329 
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

330 
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

331 
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

332 
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

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

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

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

336 
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

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

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

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

340 
facts > iterative_relevant_facts ctxt params prover 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

341 
(max_facts > the_default atp_dep_default_max_fact) NONE 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

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

343 
> fold (add_isar_dep facts) isar_deps 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

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

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

346 
if verbose andalso not auto then 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

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

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

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

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

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

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

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

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

355 
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

356 
{outcome = NONE, used_facts, ...} => 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

357 
(if verbose andalso not auto then 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

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

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

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

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

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

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

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

365 
used_facts > map fst) 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

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

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

368 

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

369 

48302  370 
(*** Lowlevel communication with MaSh ***) 
371 

48323  372 
fun write_file (xs, f) file = 
48318  373 
let val path = Path.explode file in 
48323  374 
File.write path ""; 
375 
xs > chunk_list 500 

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

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

378 

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

379 
fun mash_info overlord = 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

380 
if overlord then (getenv "ISABELLE_HOME_USER", "") 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

381 
else (getenv "ISABELLE_TMP", serial_string ()) 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

382 

48382
641af72b0059
added possibility of running external MaSh commands asynchronously
blanchet
parents:
48381
diff
changeset

383 
fun and_rm_files overlord flags files = 
641af72b0059
added possibility of running external MaSh commands asynchronously
blanchet
parents:
48381
diff
changeset

384 
if overlord then 
641af72b0059
added possibility of running external MaSh commands asynchronously
blanchet
parents:
48381
diff
changeset

385 
"" 
641af72b0059
added possibility of running external MaSh commands asynchronously
blanchet
parents:
48381
diff
changeset

386 
else 
641af72b0059
added possibility of running external MaSh commands asynchronously
blanchet
parents:
48381
diff
changeset

387 
" && rm f" ^ flags ^ "  " ^ 
641af72b0059
added possibility of running external MaSh commands asynchronously
blanchet
parents:
48381
diff
changeset

388 
space_implode " " (map File.shell_quote files) 
641af72b0059
added possibility of running external MaSh commands asynchronously
blanchet
parents:
48381
diff
changeset

389 

641af72b0059
added possibility of running external MaSh commands asynchronously
blanchet
parents:
48381
diff
changeset

390 
fun run_mash ctxt overlord (temp_dir, serial) async core = 
48311  391 
let 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

392 
val log_file = temp_dir ^ "/mash_log" ^ serial 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

393 
val err_file = temp_dir ^ "/mash_err" ^ serial 
48311  394 
val command = 
48382
641af72b0059
added possibility of running external MaSh commands asynchronously
blanchet
parents:
48381
diff
changeset

395 
"(" ^ mash_home () ^ "/mash quiet outputDir " ^ mash_state_dir () ^ 
641af72b0059
added possibility of running external MaSh commands asynchronously
blanchet
parents:
48381
diff
changeset

396 
" log " ^ log_file ^ " " ^ core ^ ") 2>&1 > " ^ err_file ^ 
641af72b0059
added possibility of running external MaSh commands asynchronously
blanchet
parents:
48381
diff
changeset

397 
and_rm_files overlord "" [log_file, err_file] ^ 
641af72b0059
added possibility of running external MaSh commands asynchronously
blanchet
parents:
48381
diff
changeset

398 
(if async then " &" else "") 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

399 
in 
48382
641af72b0059
added possibility of running external MaSh commands asynchronously
blanchet
parents:
48381
diff
changeset

400 
trace_msg ctxt (fn () => 
641af72b0059
added possibility of running external MaSh commands asynchronously
blanchet
parents:
48381
diff
changeset

401 
(if async then "Launching " else "Running ") ^ command); 
48323  402 
write_file ([], K "") log_file; 
403 
write_file ([], K "") err_file; 

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

404 
Isabelle_System.bash command; 
48382
641af72b0059
added possibility of running external MaSh commands asynchronously
blanchet
parents:
48381
diff
changeset

405 
if not async then trace_msg ctxt (K "Done") else () 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

407 

48383  408 
fun run_mash_commands ctxt overlord save max_suggs write_cmds read_suggs = 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

410 
val info as (temp_dir, serial) = mash_info overlord 
48318  411 
val sugg_file = temp_dir ^ "/mash_suggs" ^ serial 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

412 
val cmd_file = temp_dir ^ "/mash_commands" ^ serial 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

413 
in 
48323  414 
write_file ([], K "") sugg_file; 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

415 
write_file write_cmds cmd_file; 
48383  416 
run_mash ctxt overlord info false 
48318  417 
("inputFile " ^ cmd_file ^ " predictions " ^ sugg_file ^ 
418 
" numberOfPredictions " ^ string_of_int max_suggs ^ 

48382
641af72b0059
added possibility of running external MaSh commands asynchronously
blanchet
parents:
48381
diff
changeset

419 
(if save then " saveModel" else "") ^ 
641af72b0059
added possibility of running external MaSh commands asynchronously
blanchet
parents:
48381
diff
changeset

420 
(and_rm_files overlord "" [sugg_file, cmd_file])); 
48318  421 
read_suggs (fn () => File.read_lines (Path.explode sugg_file)) 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

423 

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

424 
fun str_of_update (name, parents, feats, deps) = 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

425 
"! " ^ escape_meta name ^ ": " ^ escape_metas parents ^ "; " ^ 
48311  426 
escape_metas feats ^ "; " ^ escape_metas deps ^ "\n" 
427 

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

428 
fun str_of_query (parents, feats) = 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

429 
"? " ^ escape_metas parents ^ "; " ^ escape_metas feats 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

430 

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

431 
fun mash_CLEAR ctxt = 
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

432 
let val path = mash_state_dir () > Path.explode in 
48332
271a4a6af734
optimize parent computation in MaSh + remove temporary files
blanchet
parents:
48330
diff
changeset

433 
trace_msg ctxt (K "MaSh CLEAR"); 
48309  434 
File.fold_dir (fn file => fn () => 
435 
File.rm (Path.append path (Path.basic file))) 

436 
path () 

437 
end 

48302  438 

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

439 
fun mash_ADD _ _ [] = () 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

440 
 mash_ADD ctxt overlord upds = 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

441 
(trace_msg ctxt (fn () => "MaSh ADD " ^ 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

442 
elide_string 1000 (space_implode " " (map #1 upds))); 
48383  443 
run_mash_commands ctxt overlord true 0 (upds, str_of_update) (K ())) 
48302  444 

48318  445 
fun mash_QUERY ctxt overlord max_suggs (query as (_, feats)) = 
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

446 
(trace_msg ctxt (fn () => "MaSh QUERY " ^ space_implode " " feats); 
48383  447 
run_mash_commands ctxt overlord false max_suggs 
48323  448 
([query], str_of_query) 
48318  449 
(fn suggs => snd (extract_query (List.last (suggs ())))) 
48311  450 
handle List.Empty => []) 
48302  451 

452 

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

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

454 

48321  455 
fun try_graph ctxt when def f = 
456 
f () 

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

458 
(trace_msg ctxt (fn () => 

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

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

460 
 Graph.DUP name => 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

461 
(trace_msg ctxt (fn () => 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

462 
"Duplicate fact " ^ quote name ^ " when " ^ when); def) 
48321  463 
 Graph.UNDEF name => 
464 
(trace_msg ctxt (fn () => 

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

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

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

467 
if Exn.is_interrupt exn then 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

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

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

470 
(trace_msg ctxt (fn () => 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

471 
"Internal error when " ^ when ^ ":\n" ^ 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

472 
ML_Compiler.exn_message exn); def) 
48321  473 

48390
4147f2bc4442
add versioning to MaSh state + cleanup dead code
blanchet
parents:
48389
diff
changeset

474 
type mash_state = {fact_graph : unit Graph.T} 
48301  475 

48390
4147f2bc4442
add versioning to MaSh state + cleanup dead code
blanchet
parents:
48389
diff
changeset

476 
val empty_state = {fact_graph = Graph.empty} 
48301  477 

478 
local 

479 

48390
4147f2bc4442
add versioning to MaSh state + cleanup dead code
blanchet
parents:
48389
diff
changeset

480 
val version = "*** MaSh 0.0 ***" 
4147f2bc4442
add versioning to MaSh state + cleanup dead code
blanchet
parents:
48389
diff
changeset

481 

4147f2bc4442
add versioning to MaSh state + cleanup dead code
blanchet
parents:
48389
diff
changeset

482 
fun load _ (state as (true, _)) = state 
4147f2bc4442
add versioning to MaSh state + cleanup dead code
blanchet
parents:
48389
diff
changeset

483 
 load ctxt _ = 
48309  484 
let val path = mash_state_path () in 
48302  485 
(true, 
486 
case try File.read_lines path of 

48390
4147f2bc4442
add versioning to MaSh state + cleanup dead code
blanchet
parents:
48389
diff
changeset

487 
SOME (version' :: fact_lines) => 
48302  488 
let 
48322
8a8d71e34297
fixed MaSh state load code so it works even if the facts are read in disorder
blanchet
parents:
48321
diff
changeset

489 
fun add_edge_to name parent = 
8a8d71e34297
fixed MaSh state load code so it works even if the facts are read in disorder
blanchet
parents:
48321
diff
changeset

490 
Graph.default_node (parent, ()) 
8a8d71e34297
fixed MaSh state load code so it works even if the facts are read in disorder
blanchet
parents:
48321
diff
changeset

491 
#> Graph.add_edge (parent, name) 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

492 
fun add_fact_line line = 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

494 
("", _) => I (* shouldn't happen *) 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

495 
 (name, parents) => 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

496 
Graph.default_node (name, ()) 
48322
8a8d71e34297
fixed MaSh state load code so it works even if the facts are read in disorder
blanchet
parents:
48321
diff
changeset

497 
#> fold (add_edge_to name) parents 
48321  498 
val fact_graph = 
48322
8a8d71e34297
fixed MaSh state load code so it works even if the facts are read in disorder
blanchet
parents:
48321
diff
changeset

499 
try_graph ctxt "loading state" Graph.empty (fn () => 
48390
4147f2bc4442
add versioning to MaSh state + cleanup dead code
blanchet
parents:
48389
diff
changeset

500 
Graph.empty > version' = version 
4147f2bc4442
add versioning to MaSh state + cleanup dead code
blanchet
parents:
48389
diff
changeset

501 
? fold add_fact_line fact_lines) 
4147f2bc4442
add versioning to MaSh state + cleanup dead code
blanchet
parents:
48389
diff
changeset

502 
in {fact_graph = fact_graph} end 
48304  503 
 _ => empty_state) 
48302  504 
end 
48249  505 

48390
4147f2bc4442
add versioning to MaSh state + cleanup dead code
blanchet
parents:
48389
diff
changeset

506 
fun save {fact_graph} = 
48301  507 
let 
48309  508 
val path = mash_state_path () 
48318  509 
fun fact_line_for name parents = 
510 
escape_meta name ^ ": " ^ escape_metas parents 

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

511 
val append_fact = File.append path o suffix "\n" oo fact_line_for 
48301  512 
in 
48390
4147f2bc4442
add versioning to MaSh state + cleanup dead code
blanchet
parents:
48389
diff
changeset

513 
File.write path (version ^ "\n"); 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

514 
Graph.fold (fn (name, ((), (parents, _))) => fn () => 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

515 
append_fact name (Graph.Keys.dest parents)) 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

516 
fact_graph () 
48301  517 
end 
518 

48302  519 
val global_state = 
48381  520 
Synchronized.var "Sledgehammer_MaSh.global_state" (false, empty_state) 
48301  521 

522 
in 

523 

48321  524 
fun mash_map ctxt f = 
48390
4147f2bc4442
add versioning to MaSh state + cleanup dead code
blanchet
parents:
48389
diff
changeset

525 
Synchronized.change global_state (load ctxt ##> (f #> tap save)) 
48302  526 

48321  527 
fun mash_get ctxt = 
48390
4147f2bc4442
add versioning to MaSh state + cleanup dead code
blanchet
parents:
48389
diff
changeset

528 
Synchronized.change_result global_state (load ctxt #> `snd) 
48302  529 

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

530 
fun mash_unlearn ctxt = 
48302  531 
Synchronized.change global_state (fn _ => 
48332
271a4a6af734
optimize parent computation in MaSh + remove temporary files
blanchet
parents:
48330
diff
changeset

532 
(mash_CLEAR ctxt; File.write (mash_state_path ()) ""; 
48308  533 
(true, empty_state))) 
48301  534 

535 
end 

536 

48318  537 
fun mash_could_suggest_facts () = mash_home () <> "" 
48321  538 
fun mash_can_suggest_facts ctxt = 
539 
not (Graph.is_empty (#fact_graph (mash_get ctxt))) 

48249  540 

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

541 
fun parents_wrt_facts facts fact_graph = 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

542 
let 
48378  543 
val facts = [] > fold (cons o nickname_of o snd) facts 
48330  544 
val tab = Symtab.empty > fold (fn name => Symtab.update (name, ())) facts 
48377  545 
fun insert_not_seen seen name = 
546 
not (member (op =) seen name) ? insert (op =) name 

48378  547 
fun parents_of _ parents [] = parents 
48377  548 
 parents_of seen parents (name :: names) = 
48332
271a4a6af734
optimize parent computation in MaSh + remove temporary files
blanchet
parents:
48330
diff
changeset

549 
if Symtab.defined tab name then 
48377  550 
parents_of (name :: seen) (name :: parents) names 
48332
271a4a6af734
optimize parent computation in MaSh + remove temporary files
blanchet
parents:
48330
diff
changeset

551 
else 
48377  552 
parents_of (name :: seen) parents 
553 
(Graph.Keys.fold (insert_not_seen seen) 

554 
(Graph.imm_preds fact_graph name) names) 

555 
in parents_of [] [] (Graph.maximals fact_graph) end 

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

556 

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

559 
slack. *) 

560 
fun max_suggs_of max_facts = max_facts + Int.min (200, max_facts) 

561 

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

562 
fun is_fact_in_graph fact_graph (_, th) = 
48378  563 
can (Graph.get_node fact_graph) (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

564 

48318  565 
fun mash_suggest_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts 
566 
concl_t facts = 

48301  567 
let 
48302  568 
val thy = Proof_Context.theory_of ctxt 
48321  569 
val fact_graph = #fact_graph (mash_get ctxt) 
48332
271a4a6af734
optimize parent computation in MaSh + remove temporary files
blanchet
parents:
48330
diff
changeset

570 
val parents = parents_wrt_facts facts fact_graph 
48385  571 
val feats = features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts) 
48318  572 
val suggs = 
48320
891a24a48155
improved meshing of MaSh and MengPaulson if some MaSh suggestions are cutoff (the common case)
blanchet
parents:
48319
diff
changeset

573 
if Graph.is_empty fact_graph then [] 
891a24a48155
improved meshing of MaSh and MengPaulson if some MaSh suggestions are cutoff (the common case)
blanchet
parents:
48319
diff
changeset

574 
else mash_QUERY ctxt overlord (max_suggs_of max_facts) (parents, feats) 
891a24a48155
improved meshing of MaSh and MengPaulson if some MaSh suggestions are cutoff (the common case)
blanchet
parents:
48319
diff
changeset

575 
val selected = facts > suggested_facts suggs 
891a24a48155
improved meshing of MaSh and MengPaulson if some MaSh suggestions are cutoff (the common case)
blanchet
parents:
48319
diff
changeset

576 
val unknown = facts > filter_out (is_fact_in_graph fact_graph) 
891a24a48155
improved meshing of MaSh and MengPaulson if some MaSh suggestions are cutoff (the common case)
blanchet
parents:
48319
diff
changeset

577 
in (selected, unknown) end 
48249  578 

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

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

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

581 
fun maybe_add_from from (accum as (parents, graph)) = 
48321  582 
try_graph ctxt "updating graph" accum (fn () => 
583 
(from :: parents, Graph.add_edge_acyclic (from, name) graph)) 

584 
val graph = graph > Graph.default_node (name, ()) 

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

585 
val (parents, graph) = ([], graph) > fold maybe_add_from parents 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

586 
val (deps, graph) = ([], graph) > fold maybe_add_from deps 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

587 
in ((name, parents, feats, deps) :: upds, graph) end 
48306  588 

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

589 
val learn_timeout_slack = 2.0 
48318  590 

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

591 
fun launch_thread timeout task = 
48383  592 
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

593 
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

594 
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

595 
val death_time = Time.+ (birth_time, hard_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

596 
val desc = ("machine learner for Sledgehammer", "") 
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

597 
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

598 

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

599 
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

600 
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

601 
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

602 
() 
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

603 
else 
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

604 
launch_thread 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

605 
(fn () => 
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

606 
let 
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

607 
val thy = Proof_Context.theory_of ctxt 
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

608 
val name = timestamp () ^ " " ^ serial_string () (* freshish *) 
48385  609 
val feats = features_of ctxt prover thy (Local, General) [t] 
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

610 
val deps = used_ths > map nickname_of 
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

611 
in 
48390
4147f2bc4442
add versioning to MaSh state + cleanup dead code
blanchet
parents:
48389
diff
changeset

612 
mash_map ctxt (fn {fact_graph} => 
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

613 
let 
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

614 
val parents = parents_wrt_facts facts fact_graph 
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

615 
val upds = [(name, parents, feats, deps)] 
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

616 
val (upds, fact_graph) = 
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

617 
([], fact_graph) > fold (update_fact_graph ctxt) upds 
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

618 
in 
48390
4147f2bc4442
add versioning to MaSh state + cleanup dead code
blanchet
parents:
48389
diff
changeset

619 
mash_ADD ctxt overlord upds; {fact_graph = fact_graph} 
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

620 
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

621 
(true, "") 
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

622 
end) 
48383  623 

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

624 
fun sendback sub = 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

625 
Markup.markup Isabelle_Markup.sendback (sledgehammerN ^ " " ^ sub) 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

626 

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

627 
(* Too many dependencies is a sign that a decision procedure is at work. There 
271a4a6af734
optimize parent computation in MaSh + remove temporary files
blanchet
parents:
48330
diff
changeset

628 
isn't much too learn from such proofs. *) 
271a4a6af734
optimize parent computation in MaSh + remove temporary files
blanchet
parents:
48330
diff
changeset

629 
val max_dependencies = 10 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

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

631 

48318  632 
(* The timeout is understood in a very slack fashion. *) 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

633 
fun mash_learn_facts ctxt (params as {debug, verbose, overlord, timeout, ...}) 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

634 
prover auto atp learn_timeout facts = 
48304  635 
let 
48318  636 
val timer = Timer.startRealTimer () 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

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

638 
Time.+ (Timer.checkRealTimer timer, commit_timeout) 
48390
4147f2bc4442
add versioning to MaSh state + cleanup dead code
blanchet
parents:
48389
diff
changeset

639 
val {fact_graph} = mash_get ctxt 
48320
891a24a48155
improved meshing of MaSh and MengPaulson if some MaSh suggestions are cutoff (the common case)
blanchet
parents:
48319
diff
changeset

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

641 
facts > filter_out (is_fact_in_graph fact_graph) 
891a24a48155
improved meshing of MaSh and MengPaulson if some MaSh suggestions are cutoff (the common case)
blanchet
parents:
48319
diff
changeset

642 
> sort (thm_ord o pairself snd) 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

643 
val num_new_facts = length new_facts 
48308  644 
in 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

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

646 
(if not auto then 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

647 
" " ^ string_of_int num_new_facts ^ " fact" ^ 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

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

649 
(if atp then " (ATP timeout: " ^ string_from_time timeout ^ ")" else "") 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

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

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

652 
> Output.urgent_message; 
48308  653 
if null new_facts then 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

654 
if verbose orelse not auto then 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

655 
"Nothing to learn.\n\nHint: Try " ^ sendback relearn_isarN ^ " or " ^ 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

656 
sendback relearn_atpN ^ " to learn from scratch." 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

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

658 
"" 
48308  659 
else 
48304  660 
let 
48308  661 
val ths = facts > map snd 
48315
82d6e46c673f
fixed order of accessibles + other tweaks to MaSh
blanchet
parents:
48314
diff
changeset

662 
val all_names = 
48324  663 
ths > filter_out is_likely_tautology_or_too_meta 
48378  664 
> map (rpair () o nickname_of) 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

665 
> Symtab.make 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

666 
fun do_commit [] state = state 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

667 
 do_commit upds {fact_graph} = 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

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

669 
val (upds, fact_graph) = 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

670 
([], fact_graph) > fold (update_fact_graph ctxt) upds 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

671 
in mash_ADD ctxt overlord (rev upds); {fact_graph = fact_graph} end 
48332
271a4a6af734
optimize parent computation in MaSh + remove temporary files
blanchet
parents:
48330
diff
changeset

672 
fun trim_deps deps = if length deps > max_dependencies then [] else deps 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

673 
fun commit last upds = 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

674 
(if debug andalso not auto then Output.urgent_message "Committing..." 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

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

676 
mash_map ctxt (do_commit (rev upds)); 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

677 
if not last andalso not auto then 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

678 
let val num_upds = length upds in 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

679 
"Processed " ^ string_of_int num_upds ^ " fact" ^ 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

680 
plural_s num_upds ^ " in the last " ^ 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

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

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

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

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

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

686 
fun do_fact _ (accum as (_, (_, _, _, true))) = accum 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

687 
 do_fact ((_, stature), th) 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

688 
(upds, (parents, n, next_commit, false)) = 
48318  689 
let 
48378  690 
val name = nickname_of th 
48332
271a4a6af734
optimize parent computation in MaSh + remove temporary files
blanchet
parents:
48330
diff
changeset

691 
val feats = 
48385  692 
features_of ctxt prover (theory_of_thm th) stature [prop_of th] 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

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

694 
(if atp then atp_dependencies_of ctxt params prover auto facts 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

695 
else isar_dependencies_of) all_names th 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

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

697 
val upds = (name, parents, feats, deps) :: upds 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

698 
val (upds, next_commit) = 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

699 
if Time.> (Timer.checkRealTimer timer, next_commit) then 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

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

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

702 
(upds, next_commit) 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

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

704 
Time.> (Timer.checkRealTimer timer, learn_timeout) 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

705 
in (upds, ([name], n + 1, next_commit, timed_out)) end 
48332
271a4a6af734
optimize parent computation in MaSh + remove temporary files
blanchet
parents:
48330
diff
changeset

706 
val parents = parents_wrt_facts facts fact_graph 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

707 
val (upds, (_, n, _, _)) = 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

708 
([], (parents, 0, next_commit_time (), false)) 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

709 
> fold do_fact new_facts 
48318  710 
in 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

711 
commit true upds; 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

712 
if verbose orelse not auto then 
48383  713 
"Learned " ^ string_of_int n ^ " 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

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

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

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

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

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

719 
"" 
48318  720 
end 
48308  721 
end 
48304  722 

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

723 
fun mash_learn ctxt (params as {provers, ...}) atp = 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

725 
val thy = Proof_Context.theory_of ctxt 
48383  726 
val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt 
727 
val facts = all_facts_of thy css_table 

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

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

729 
mash_learn_facts ctxt params (hd provers) false atp infinite_timeout facts 
48383  730 
> Output.urgent_message 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

731 
end 
48249  732 

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

735 
val min_secs_for_learning = 15 

736 

48321  737 
fun relevant_facts ctxt (params as {learn, fact_filter, timeout, ...}) prover 
738 
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

739 
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

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

741 
else if only then 
48289  742 
facts 
48321  743 
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

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

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

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

747 
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

748 
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

749 
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

750 
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

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

752 
(fn () => (true, mash_learn_facts ctxt params prover true false 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

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

754 
end 
48318  755 
else 
756 
() 

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

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

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

759 
SOME ff => (() > ff <> mepoN ? maybe_learn; ff) 
48318  760 
 NONE => 
48386
b903ea11b3bc
use good old MePo filter for SMT solvers by default, since arithmetic is builtin for them
blanchet
parents:
48385
diff
changeset

761 
if is_smt_prover ctxt prover then mepoN 
b903ea11b3bc
use good old MePo filter for SMT solvers by default, since arithmetic is builtin for them
blanchet
parents:
48385
diff
changeset

762 
else if mash_can_suggest_facts ctxt then (maybe_learn (); meshN) 
48379
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (MengPaulson)
blanchet
parents:
48378
diff
changeset

763 
else if mash_could_suggest_facts () then (maybe_learn (); mepoN) 
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (MengPaulson)
blanchet
parents:
48378
diff
changeset

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

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

767 
((facts > filter (member Thm.eq_thm_prop ths o snd)) @ 
48292  768 
(accepts > filter_out (member Thm.eq_thm_prop ths o snd))) 
48293  769 
> take max_facts 
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

770 
fun iter () = 
48298  771 
iterative_relevant_facts ctxt params prover max_facts NONE hyp_ts 
772 
concl_t facts 

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

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

774 
mash_suggest_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

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

776 
[] > (if fact_filter <> mashN then cons (iter (), []) else I) 
48379
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (MengPaulson)
blanchet
parents:
48378
diff
changeset

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

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

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

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

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

782 

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

783 
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

784 
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

785 

48248  786 
end; 