author  blanchet 
Wed, 18 Jul 2012 08:44:04 +0200  
changeset 48324  3ee5b5589402 
parent 48323  7b5f7ca25d17 
child 48325  2ec05ef3e593 
permissions  rwrr 
48248  1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML 
2 
Author: Jasmin Blanchette, TU Muenchen 

3 

4 
Sledgehammer's machinelearningbased relevance filter (MaSh). 

5 
*) 

6 

7 
signature SLEDGEHAMMER_FILTER_MASH = 

8 
sig 

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

9 
type status = ATP_Problem_Generate.status 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

10 
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

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

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

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

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

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

16 

48308  17 
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

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

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

20 
val iterN : string 
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

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

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

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

24 
val escape_metas : string list > string 
48308  25 
val unescape_meta : string > string 
26 
val unescape_metas : string > string list 

48311  27 
val extract_query : string > string * string list 
48321  28 
val suggested_facts : string list > ('a * thm) list > ('a * thm) list 
29 
val mesh_facts : 

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

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

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

33 
val thm_ord : thm * thm > order 
48318  34 
val features_of : 
35 
Proof.context > string > theory > status > term list > string list 

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

36 
val isabelle_dependencies_of : unit Symtab.table > thm > string list 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

37 
val goal_of_thm : theory > thm > thm 
48321  38 
val run_prover_for_mash : 
48318  39 
Proof.context > params > string > fact list > thm > prover_result 
48308  40 
val mash_RESET : Proof.context > unit 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

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

43 
> (string * string list * string list * string list) list > unit 
48308  44 
val mash_ADD : 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

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

47 
val mash_QUERY : 
48318  48 
Proof.context > bool > int > string list * string list > string list 
48308  49 
val mash_reset : Proof.context > unit 
48318  50 
val mash_could_suggest_facts : unit > bool 
48321  51 
val mash_can_suggest_facts : Proof.context > bool 
48298  52 
val mash_suggest_facts : 
48321  53 
Proof.context > params > string > int > term list > term 
54 
> ('a * thm) list > ('a * thm) list * ('a * thm) list 

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

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

56 
Proof.context > params > theory > Time.time > fact list > string 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

57 
val mash_learn_proof : 
48321  58 
Proof.context > params > term > ('a * thm) list > thm list > unit 
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset

59 
val relevant_facts : 
48292  60 
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

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

62 
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

63 
val running_learners : unit > unit 
48248  64 
end; 
65 

66 
structure Sledgehammer_Filter_MaSh : SLEDGEHAMMER_FILTER_MASH = 

67 
struct 

48249  68 

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

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

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

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

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

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

74 
open Sledgehammer_Provers 
48318  75 
open Sledgehammer_Minimize 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

76 

48308  77 
val trace = 
78 
Attrib.setup_config_bool @{binding sledgehammer_filter_mash_trace} (K false) 

79 
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else () 

80 

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

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

82 

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

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

84 
val iterN = "iter" 
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

85 
val mashN = "mash" 
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

86 

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

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

88 

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

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

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

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

93 
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

94 

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

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

96 

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

98 
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

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

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

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

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

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

104 

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

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

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

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

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

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

112 

113 
val escape_meta = String.translate meta_char 

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

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

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

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

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

118 

48311  119 
fun extract_query line = 
120 
case space_explode ":" line of 

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

121 
[goal_name, suggs] => (unescape_meta goal_name, unescape_metas suggs) 
48312  122 
 _ => ("", []) 
48311  123 

124 
fun find_suggested facts sugg = 

125 
find_first (fn (_, th) => Thm.get_name_hint th = sugg) facts 

126 
fun suggested_facts suggs facts = map_filter (find_suggested facts) suggs 

127 

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

128 
fun sum_avg _ [] = 1000000000 (* big number *) 
891a24a48155
improved meshing of MaSh and MengPaulson if some MaSh suggestions are cutoff (the common case)
blanchet
parents:
48319
diff
changeset

129 
 sum_avg n xs = fold (Integer.add o Integer.mult n) xs 0 div (length xs) 
48313
0faafdffa662
mesh facts by taking into consideration whether a fact is known to MeSh
blanchet
parents:
48312
diff
changeset

130 

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

131 
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

132 
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

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

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

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

136 
val n = length mess 
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

137 
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

138 
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

139 
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

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

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

142 
 _ => NONE) 
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

143 
 j => SOME j 
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

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

145 
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

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

147 
facts > map (`score_of) > sort (int_ord o pairself fst) > map snd 
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

148 
> take max_facts 
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

149 
end 
48312  150 

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

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

152 

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

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

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

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

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

157 

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

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

159 

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

160 
fun has_bool @{typ bool} = true 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

161 
 has_bool (Type (_, Ts)) = exists has_bool Ts 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

162 
 has_bool _ = false 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

163 

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

164 
fun has_fun (Type (@{type_name fun}, _)) = true 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

165 
 has_fun (Type (_, Ts)) = exists has_fun Ts 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

166 
 has_fun _ = false 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

167 

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

168 
val is_conn = member (op =) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

169 
[@{const_name Trueprop}, @{const_name HOL.conj}, @{const_name HOL.disj}, 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

170 
@{const_name HOL.implies}, @{const_name Not}, 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

171 
@{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex}, 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

172 
@{const_name HOL.eq}] 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

173 

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

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

175 
exists_Const (fn (c, T) => 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

176 
not (is_conn c) andalso exists has_bool (binder_types T)) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

177 

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

178 
fun higher_inst_const thy (s, T) = 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

180 
[] => false 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

181 
 Ts => length (binder_types (Sign.the_const_type thy s)) <> length Ts 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

182 
handle TYPE _ => false 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

183 

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

184 
val binders = [@{const_name All}, @{const_name Ex}] 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

185 

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

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

187 

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

188 
fun is_fo_term thy t = 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

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

191 
t > Envir.beta_eta_contract 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

193 
> Object_Logic.atomize_term thy 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

195 
Term.is_first_order binders t andalso 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

196 
not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

197 
 _ => false) t orelse 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

198 
has_bool_arg_const t orelse exists_Const (higher_inst_const thy) t) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

200 

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

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

202 

48324  203 
fun is_likely_tautology_or_too_meta th = 
204 
let 

205 
val is_boring_const = member (op =) atp_widely_irrelevant_consts 

206 
fun is_boring_bool t = 

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

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

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

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

211 
is_boring_prop t andalso is_boring_prop u 

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

213 
is_boring_prop t andalso is_boring_prop u 

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

215 
is_boring_bool t andalso is_boring_bool u 

216 
 is_boring_prop _ = true 

217 
in 

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

219 
end 

220 

221 
fun theory_ord p = 

222 
if Theory.eq_thy p then 

223 
EQUAL 

224 
else if Theory.subthy p then 

225 
LESS 

226 
else if Theory.subthy (swap p) then 

227 
GREATER 

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

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

230 
 order => order 

231 

232 
val thm_ord = theory_ord o pairself theory_of_thm 

233 

48318  234 
fun interesting_terms_types_and_classes ctxt prover term_max_depth 
235 
type_max_depth ts = 

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

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

237 
val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}] 
48318  238 
fun is_bad_const (x as (s, _)) args = 
239 
member (op =) atp_logical_consts s orelse 

240 
fst (is_built_in_const_for_prover ctxt prover x args) 

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

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

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

245 
#> fold do_add_type Ts 
48304  246 
 do_add_type (TFree (_, S)) = add_classes S 
247 
 do_add_type (TVar (_, S)) = add_classes S 

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

248 
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

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

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

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

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

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

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

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

256 
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

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

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

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

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

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

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

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

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

265 
(case head of 
48318  266 
Const (x as (_, T)) => 
267 
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

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

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

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

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

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

273 
end 
48302  274 
in [] > fold add_patterns ts > sort string_ord end 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

275 

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

276 
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

277 

48297  278 
val term_max_depth = 1 
279 
val type_max_depth = 1 

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

280 

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

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

283 
thy_feature_name_of (Context.theory_name thy) :: 
48318  284 
interesting_terms_types_and_classes ctxt prover term_max_depth type_max_depth 
285 
ts 

48302  286 
> exists (not o is_lambda_free) ts ? cons "lambdas" 
287 
> exists (exists_Const is_exists) ts ? cons "skolems" 

288 
> exists (not o is_fo_term thy) ts ? cons "ho" 

289 
> (case status of 

290 
General => I 

291 
 Induction => cons "induction" 

292 
 Intro => cons "intro" 

293 
 Inductive => cons "inductive" 

294 
 Elim => cons "elim" 

295 
 Simp => cons "simp" 

296 
 Def => cons "def") 

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

297 

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

298 
fun isabelle_dependencies_of all_facts = 
48303
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

299 
thms_in_proof (SOME all_facts) #> sort string_ord 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

300 

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

301 
val freezeT = Type.legacy_freeze_type 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

302 

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

303 
fun freeze (t $ u) = freeze t $ freeze u 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

304 
 freeze (Abs (s, T, t)) = Abs (s, freezeT T, freeze t) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

305 
 freeze (Var ((s, _), T)) = Free (s, freezeT T) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

306 
 freeze (Const (s, T)) = Const (s, freezeT T) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

307 
 freeze (Free (s, T)) = Free (s, freezeT T) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

309 

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

310 
fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

311 

48321  312 
fun run_prover_for_mash ctxt params prover facts goal = 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

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

315 
{state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1, 
48289  316 
facts = facts > map (apfst (apfst (fn name => name ()))) 
48318  317 
> map Untranslated_Fact} 
48321  318 
val prover = get_minimizing_prover ctxt Normal (K ()) prover 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

319 
in prover params (K (K (K ""))) problem end 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

320 

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

321 

48302  322 
(*** Lowlevel communication with MaSh ***) 
323 

48323  324 
fun write_file (xs, f) file = 
48318  325 
let val path = Path.explode file in 
48323  326 
File.write path ""; 
327 
xs > chunk_list 500 

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

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

330 

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

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

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

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

334 

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

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

337 
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

338 
val err_file = temp_dir ^ "/mash_err" ^ serial 
48311  339 
val command = 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

340 
mash_home () ^ "/mash.py quiet outputDir " ^ mash_state_dir () ^ 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

341 
" log " ^ log_file ^ " " ^ core ^ " 2>&1 > " ^ err_file 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

343 
trace_msg ctxt (fn () => "Running " ^ command); 
48323  344 
write_file ([], K "") log_file; 
345 
write_file ([], K "") err_file; 

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

346 
Isabelle_System.bash command; () 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

348 

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

349 
fun run_mash_init ctxt overlord write_access write_feats write_deps = 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

351 
val info as (temp_dir, serial) = mash_info overlord 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

353 
> tap (Isabelle_System.mkdir o Path.explode) 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

355 
write_file write_access (in_dir ^ "/mash_accessibility"); 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

356 
write_file write_feats (in_dir ^ "/mash_features"); 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

357 
write_file write_deps (in_dir ^ "/mash_dependencies"); 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

358 
run_mash ctxt info ("init inputDir " ^ in_dir) 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

360 

48318  361 
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

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

363 
val info as (temp_dir, serial) = mash_info overlord 
48318  364 
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

365 
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

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

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

369 
run_mash ctxt info 
48318  370 
("inputFile " ^ cmd_file ^ " predictions " ^ sugg_file ^ 
371 
" numberOfPredictions " ^ string_of_int max_suggs ^ 

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

372 
(if save then " saveModel" else "")); 
48318  373 
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

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

375 

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

376 
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

377 
"! " ^ escape_meta name ^ ": " ^ escape_metas parents ^ "; " ^ 
48311  378 
escape_metas feats ^ "; " ^ escape_metas deps ^ "\n" 
379 

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

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

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

382 

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

383 
fun init_str_of_update get (upd as (name, _, _, _)) = 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

384 
escape_meta name ^ ": " ^ escape_metas (get upd) ^ "\n" 
48311  385 

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

387 
let val path = mash_state_dir () > Path.explode in 
48309  388 
trace_msg ctxt (K "MaSh RESET"); 
389 
File.fold_dir (fn file => fn () => 

390 
File.rm (Path.append path (Path.basic file))) 

391 
path () 

392 
end 

48302  393 

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

394 
fun mash_INIT ctxt _ [] = mash_RESET ctxt 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

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

397 
elide_string 1000 (space_implode " " (map #1 upds))); 
48323  398 
run_mash_init ctxt overlord (upds, init_str_of_update #2) 
399 
(upds, init_str_of_update #3) (upds, init_str_of_update #4)) 

48302  400 

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

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

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

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

404 
elide_string 1000 (space_implode " " (map #1 upds))); 
48323  405 
run_mash_commands ctxt overlord true 0 (upds, str_of_update) (K ())) 
48302  406 

48318  407 
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

408 
(trace_msg ctxt (fn () => "MaSh QUERY " ^ space_implode " " feats); 
48318  409 
run_mash_commands ctxt overlord false max_suggs 
48323  410 
([query], str_of_query) 
48318  411 
(fn suggs => snd (extract_query (List.last (suggs ())))) 
48311  412 
handle List.Empty => []) 
48302  413 

414 

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

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

416 

48321  417 
fun try_graph ctxt when def f = 
418 
f () 

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

420 
(trace_msg ctxt (fn () => 

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

422 
 Graph.UNDEF name => 

423 
(trace_msg ctxt (fn () => 

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

425 

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

427 
{thys : bool Symtab.table, 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

428 
fact_graph : unit Graph.T} 
48301  429 

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

430 
val empty_state = {thys = Symtab.empty, fact_graph = Graph.empty} 
48301  431 

432 
local 

433 

48321  434 
fun mash_load _ (state as (true, _)) = state 
435 
 mash_load ctxt _ = 

48309  436 
let val path = mash_state_path () in 
48302  437 
(true, 
438 
case try File.read_lines path of 

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

439 
SOME (comp_thys :: incomp_thys :: fact_lines) => 
48302  440 
let 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

441 
fun add_thy comp thy = Symtab.update (thy, comp) 
48322
8a8d71e34297
fixed MaSh state load code so it works even if the facts are read in disorder
blanchet
parents:
48321
diff
changeset

442 
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

443 
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

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

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

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

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

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

449 
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

450 
#> fold (add_edge_to name) parents 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

452 
Symtab.empty > fold (add_thy true) (unescape_metas comp_thys) 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

453 
> fold (add_thy false) (unescape_metas incomp_thys) 
48321  454 
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

455 
try_graph ctxt "loading state" Graph.empty (fn () => 
48321  456 
Graph.empty > fold add_fact_line fact_lines) 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

457 
in {thys = thys, fact_graph = fact_graph} end 
48304  458 
 _ => empty_state) 
48302  459 
end 
48249  460 

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

461 
fun mash_save ({thys, fact_graph, ...} : mash_state) = 
48301  462 
let 
48309  463 
val path = mash_state_path () 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

464 
val thys = Symtab.dest thys 
48318  465 
val line_for_thys = escape_metas o AList.find (op =) thys 
466 
fun fact_line_for name parents = 

467 
escape_meta name ^ ": " ^ escape_metas parents 

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

468 
val append_fact = File.append path o suffix "\n" oo fact_line_for 
48301  469 
in 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

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

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

473 
fact_graph () 
48301  474 
end 
475 

48302  476 
val global_state = 
48304  477 
Synchronized.var "Sledgehammer_Filter_MaSh.global_state" (false, empty_state) 
48301  478 

479 
in 

480 

48321  481 
fun mash_map ctxt f = 
482 
Synchronized.change global_state (mash_load ctxt ##> (f #> tap mash_save)) 

48302  483 

48321  484 
fun mash_get ctxt = 
485 
Synchronized.change_result global_state (mash_load ctxt #> `snd) 

48302  486 

48308  487 
fun mash_reset ctxt = 
48302  488 
Synchronized.change global_state (fn _ => 
48309  489 
(mash_RESET ctxt; File.write (mash_state_path ()) ""; 
48308  490 
(true, empty_state))) 
48301  491 

492 
end 

493 

48318  494 
fun mash_could_suggest_facts () = mash_home () <> "" 
48321  495 
fun mash_can_suggest_facts ctxt = 
496 
not (Graph.is_empty (#fact_graph (mash_get ctxt))) 

48249  497 

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

499 
let 
48318  500 
val graph_facts = Symtab.make (map (rpair ()) (Graph.keys fact_graph)) 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

501 
val facts = 
48321  502 
try_graph ctxt "when computing ancestor facts" [] (fn () => 
503 
[] > fold (cons o Thm.get_name_hint o snd) facts 

504 
> filter (Symtab.defined graph_facts) 

505 
> Graph.all_preds fact_graph) 

48318  506 
val facts = Symtab.empty > fold (fn name => Symtab.update (name, ())) facts 
48321  507 
in 
508 
try_graph ctxt "when computing parent facts" [] (fn () => 

509 
fact_graph > Graph.restrict (Symtab.defined facts) > Graph.maximals) 

510 
end 

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

511 

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

514 
slack. *) 

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

516 

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

517 
fun is_fact_in_graph fact_graph (_, th) = 
891a24a48155
improved meshing of MaSh and MengPaulson if some MaSh suggestions are cutoff (the common case)
blanchet
parents:
48319
diff
changeset

518 
can (Graph.get_node fact_graph) (Thm.get_name_hint th) 
891a24a48155
improved meshing of MaSh and MengPaulson if some MaSh suggestions are cutoff (the common case)
blanchet
parents:
48319
diff
changeset

519 

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

48301  522 
let 
48302  523 
val thy = Proof_Context.theory_of ctxt 
48321  524 
val fact_graph = #fact_graph (mash_get ctxt) 
525 
val parents = parents_wrt_facts ctxt facts fact_graph 

48318  526 
val feats = features_of ctxt prover thy General (concl_t :: hyp_ts) 
527 
val suggs = 

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

528 
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

529 
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

530 
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

531 
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

532 
in (selected, unknown) end 
48249  533 

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

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

535 
let fun add comp thy = Symtab.update (Context.theory_name thy, comp) in 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

536 
add false thy #> fold (add true) (Theory.ancestors_of thy) 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

537 
end 
48249  538 

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

539 
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

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

541 
fun maybe_add_from from (accum as (parents, graph)) = 
48321  542 
try_graph ctxt "updating graph" accum (fn () => 
543 
(from :: parents, Graph.add_edge_acyclic (from, name) graph)) 

544 
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

545 
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

546 
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

547 
in ((name, parents, feats, deps) :: upds, graph) end 
48306  548 

48318  549 
val pass1_learn_timeout_factor = 0.5 
550 

551 
(* The timeout is understood in a very slack fashion. *) 

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

552 
fun mash_learn_thy ctxt ({provers, verbose, overlord, ...} : params) thy timeout 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

553 
facts = 
48304  554 
let 
48318  555 
val timer = Timer.startRealTimer () 
48324  556 
fun check_timer s = 
557 
tracing ("*** " ^ s ^ " " ^ PolyML.makestring (Timer.checkRealTimer timer)) 

48318  558 
val prover = hd provers 
559 
fun timed_out frac = 

560 
Time.> (Timer.checkRealTimer timer, time_mult frac timeout) 

48324  561 
val _ = check_timer "begin" (*###*) 
48321  562 
val {fact_graph, ...} = mash_get ctxt 
48324  563 
val _ = check_timer " got" (*###*) 
48320
891a24a48155
improved meshing of MaSh and MengPaulson if some MaSh suggestions are cutoff (the common case)
blanchet
parents:
48319
diff
changeset

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

565 
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

566 
> sort (thm_ord o pairself snd) 
48324  567 
val _ = check_timer " new facts" (*###*) 
48308  568 
in 
569 
if null new_facts then 

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

570 
"" 
48308  571 
else 
48304  572 
let 
48308  573 
val ths = facts > map snd 
48315
82d6e46c673f
fixed order of accessibles + other tweaks to MaSh
blanchet
parents:
48314
diff
changeset

574 
val all_names = 
48324  575 
ths > filter_out is_likely_tautology_or_too_meta 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

576 
> map (rpair () o Thm.get_name_hint) 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

577 
> Symtab.make 
48324  578 
val _ = check_timer " all names" (*###*) 
48318  579 
fun do_fact _ (accum as (_, true)) = accum 
580 
 do_fact ((_, (_, status)), th) ((parents, upds), false) = 

581 
let 

582 
val name = Thm.get_name_hint th 

583 
val feats = features_of ctxt prover thy status [prop_of th] 

584 
val deps = isabelle_dependencies_of all_names th 

585 
val upd = (name, parents, feats, deps) 

586 
in (([name], upd :: upds), timed_out pass1_learn_timeout_factor) end 

48321  587 
val parents = parents_wrt_facts ctxt facts fact_graph 
48324  588 
val _ = check_timer " parents" (*###*) 
48318  589 
val ((_, upds), _) = 
590 
((parents, []), false) > fold do_fact new_facts >> apsnd rev 

48324  591 
val _ = check_timer " did facts" (*###*) 
48318  592 
val n = length upds 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

593 
fun trans {thys, fact_graph} = 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

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

596 
if Graph.is_empty fact_graph then mash_INIT else mash_ADD 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

597 
val (upds, fact_graph) = 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

598 
([], fact_graph) > fold (update_fact_graph ctxt) upds 
48324  599 
val _ = check_timer " updated" (*###*) 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

601 
(mash_INIT_or_ADD ctxt overlord (rev upds); 
48324  602 
check_timer " inited/added" (*###*); 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

603 
{thys = thys > add_thys_for thy, 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

605 
end 
48318  606 
in 
48321  607 
mash_map ctxt trans; 
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

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

609 
"Processed " ^ string_of_int n ^ " proof" ^ plural_s n ^ 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

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

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

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

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

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

615 
"" 
48318  616 
end 
48308  617 
end 
48304  618 

48321  619 
fun mash_learn_proof ctxt ({provers, overlord, ...} : params) t facts used_ths = 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

621 
val thy = Proof_Context.theory_of ctxt 
48318  622 
val prover = hd provers 
623 
val name = ATP_Util.timestamp () ^ serial_string () (* fresh enough *) 

624 
val feats = features_of ctxt prover thy General [t] 

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

625 
val deps = used_ths > map Thm.get_name_hint 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

626 
in 
48321  627 
mash_map ctxt (fn {thys, fact_graph} => 
48309  628 
let 
48321  629 
val parents = parents_wrt_facts ctxt facts fact_graph 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

630 
val upds = [(name, parents, feats, deps)] 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

631 
val (upds, fact_graph) = 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

632 
([], fact_graph) > fold (update_fact_graph ctxt) upds 
48309  633 
in 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

635 
{thys = thys, fact_graph = fact_graph} 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

637 
end 
48249  638 

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

641 
val min_secs_for_learning = 15 

642 
val short_learn_timeout_factor = 0.2 

643 
val long_learn_timeout_factor = 4.0 

644 

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

647 
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

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

649 
else if only then 
48289  650 
facts 
48321  651 
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

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

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

654 
let 
48318  655 
val thy = Proof_Context.theory_of ctxt 
656 
fun maybe_learn can_suggest = 

48321  657 
if not learn orelse Async_Manager.has_running_threads MaShN then 
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

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

659 
else if Time.toSeconds timeout >= min_secs_for_learning then 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

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

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

662 
if can_suggest then short_learn_timeout_factor 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

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

664 
val soft_timeout = time_mult factor timeout 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

665 
val hard_timeout = time_mult 2.0 soft_timeout 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

666 
val birth_time = Time.now () 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

667 
val death_time = Time.+ (birth_time, hard_timeout) 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

668 
val desc = ("machine learner for Sledgehammer", "") 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

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

670 
Async_Manager.launch MaShN birth_time death_time desc 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

671 
(fn () => 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

672 
(true, mash_learn_thy ctxt params thy soft_timeout facts)) 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

673 
end 
48318  674 
else 
675 
() 

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

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

677 
case fact_filter of 
48318  678 
SOME ff => 
48321  679 
(if ff <> iterN then maybe_learn (mash_can_suggest_facts ctxt) 
680 
else (); ff) 

48318  681 
 NONE => 
48321  682 
if mash_can_suggest_facts ctxt then (maybe_learn true; meshN) 
48318  683 
else if mash_could_suggest_facts () then (maybe_learn false; iterN) 
684 
else iterN 

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

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

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

690 
fun iter () = 
48298  691 
iterative_relevant_facts ctxt params prover max_facts NONE hyp_ts 
692 
concl_t facts 

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

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

694 
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

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

696 
[] > (if fact_filter <> mashN then cons (iter (), []) else I) 
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

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

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

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

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

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

702 

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

703 
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

704 
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

705 

48248  706 
end; 