author  blanchet 
Wed, 18 Jul 2012 08:44:04 +0200  
changeset 48314  ee33ba3c0e05 
parent 48313  0faafdffa662 
child 48315  82d6e46c673f 
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 
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

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

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

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

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

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

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

48311  26 
val extract_query : string > string * string list 
48312  27 
val suggested_facts : string list > fact list > fact list 
48313
0faafdffa662
mesh facts by taking into consideration whether a fact is known to MeSh
blanchet
parents:
48312
diff
changeset

28 
val mesh_facts : int > (fact list * int option) list > fact list 
48299  29 
val all_non_tautological_facts_of : 
30 
theory > status Termtab.table > fact list 

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

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

32 
val thm_ord : thm * thm > order 
48312  33 
val thy_facts_from_thms : fact list > string list Symtab.table 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

34 
val has_thy : theory > thm > bool 
48303
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

35 
val parent_facts : theory > string list Symtab.table > string list 
48302  36 
val features_of : theory > status > term list > string list 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

37 
val isabelle_dependencies_of : string list > thm > string list 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

38 
val goal_of_thm : theory > thm > thm 
48296
e7f01b7e244e
gracefully handle the case of empty theories when going up the accessibility chain
blanchet
parents:
48293
diff
changeset

39 
val run_prover : Proof.context > params > fact list > thm > prover_result 
48304  40 
val thy_name_of_fact : string > string 
48308  41 
val mash_RESET : Proof.context > unit 
42 
val mash_ADD : 

43 
Proof.context > (string * string list * string list * string list) list 

44 
> unit 

45 
val mash_DEL : Proof.context > string list > string list > unit 

48311  46 
val mash_QUERY : Proof.context > string list * string list > string list 
48308  47 
val mash_reset : Proof.context > unit 
48 
val mash_can_suggest_facts : Proof.context > bool 

48298  49 
val mash_suggest_facts : 
48311  50 
Proof.context > params > string > term list > term > fact list 
51 
> fact list 

48308  52 
val mash_can_learn_thy : Proof.context > theory > bool 
53 
val mash_learn_thy : Proof.context > theory > real > unit 

48309  54 
val mash_learn_proof : Proof.context > theory > term > thm list > unit 
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset

55 
val relevant_facts : 
48292  56 
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

57 
> term > fact list > fact list 
48248  58 
end; 
59 

60 
structure Sledgehammer_Filter_MaSh : SLEDGEHAMMER_FILTER_MASH = 

61 
struct 

48249  62 

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

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

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

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

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

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

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

69 

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

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

73 

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

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

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

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

77 

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

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

79 

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

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

81 
fun mash_state_dir () = 
48309  82 
getenv "ISABELLE_HOME_USER" ^ "/mash" 
83 
> tap (fn dir => Isabelle_System.mkdir (Path.explode dir)) 

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

84 
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

85 

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

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

87 

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

89 
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

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

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

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

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

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

95 

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

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

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

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

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

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

103 

104 
val escape_meta = String.translate meta_char 

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

105 
val escape_metas = map escape_meta #> space_implode " " 
48308  106 
val unescape_meta = unmeta_chars [] o String.explode 
107 
val unescape_metas = map unescape_meta o space_explode " " 

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

108 

48311  109 
val explode_suggs = 
110 
space_explode " " #> filter_out (curry (op =) "") #> map unescape_meta 

111 
fun extract_query line = 

112 
case space_explode ":" line of 

113 
[goal_name, suggs] => (unescape_meta goal_name, explode_suggs suggs) 

48312  114 
 _ => ("", []) 
48311  115 

116 
fun find_suggested facts sugg = 

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

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

119 

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

120 
fun sum_avg n xs = 
0faafdffa662
mesh facts by taking into consideration whether a fact is known to MeSh
blanchet
parents:
48312
diff
changeset

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

122 

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

123 
fun mesh_facts max_facts [(facts, _)] = facts > take max_facts 
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

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

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

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

127 
val fact_eq = Thm.eq_thm o pairself snd 
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

128 
fun score_in fact (facts, def) = 
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

129 
case find_index (curry fact_eq fact) facts of 
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

130 
~1 => def 
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

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

132 
fun score_of fact = mess > map_filter (score_in fact) > sum_avg n 
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

133 
val facts = fold (union fact_eq o take max_facts o fst) mess [] 
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

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

135 
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

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

137 
end 
48312  138 

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

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

140 

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

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

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

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

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

145 

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

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

147 

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

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

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

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

151 

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

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

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

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

155 

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

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

157 
[@{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

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

159 
@{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

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

161 

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

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

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

164 
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

165 

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

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

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

168 
[] => false 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

169 
 Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

170 

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

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

172 

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

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

174 

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

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

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

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

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

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

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

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

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

183 
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

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

185 
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

186 
end 
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 
end 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

189 

48302  190 
fun interesting_terms_types_and_classes term_max_depth type_max_depth ts = 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

192 
val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}] 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

193 
val bad_consts = atp_widely_irrelevant_consts 
48304  194 
fun add_classes @{sort type} = I 
195 
 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

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

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

198 
#> fold do_add_type Ts 
48304  199 
 do_add_type (TFree (_, S)) = add_classes S 
200 
 do_add_type (TVar (_, S)) = add_classes S 

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

201 
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

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

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

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

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

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

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

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

209 
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

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

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

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

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

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

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

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

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

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

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

220 
not (member (op =) bad_consts s) ? (add_term t #> add_type T) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

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

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

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

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

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

228 

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

229 
fun is_likely_tautology th = 
48302  230 
null (interesting_terms_types_and_classes 0 ~1 [prop_of th]) andalso 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

231 
not (Thm.eq_thm_prop (@{thm ext}, th)) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

232 

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

233 
fun is_too_meta thy th = 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

234 
fastype_of (Object_Logic.atomize_term thy (prop_of th)) <> @{typ bool} 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

235 

48299  236 
fun all_non_tautological_facts_of thy css_table = 
237 
all_facts_of thy css_table 

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

238 
> filter_out ((is_likely_tautology orf is_too_meta thy) o snd) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

239 

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

240 
fun theory_ord p = 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

241 
if Theory.eq_thy p then EQUAL 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

242 
else if Theory.subthy p then LESS 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

243 
else if Theory.subthy (swap p) then GREATER 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

245 

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

246 
val thm_ord = theory_ord o pairself theory_of_thm 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

247 

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

248 
(* ### FIXME: optimize *) 
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

249 
fun thy_facts_from_thms ths = 
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

250 
ths > map (snd #> `(theory_of_thm #> Context.theory_name)) 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

251 
> AList.group (op =) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

252 
> sort (int_ord o pairself (length o Theory.ancestors_of o theory_of_thm 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

253 
o hd o snd)) 
48303
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

254 
> map (apsnd (sort (rev_order o thm_ord) #> map Thm.get_name_hint)) 
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

255 
> Symtab.make 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

256 

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

257 
fun has_thy thy th = 
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

258 
Context.theory_name thy = Context.theory_name (theory_of_thm th) 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

259 

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

260 
fun parent_facts thy thy_facts = 
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

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

262 
fun add_last thy = 
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

263 
case Symtab.lookup thy_facts (Context.theory_name thy) of 
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

264 
SOME (last_fact :: _) => insert (op =) last_fact 
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

265 
 _ => add_parent thy 
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

266 
and add_parent thy = fold add_last (Theory.parents_of thy) 
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

267 
in add_parent thy [] end 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

268 

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

269 
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

270 

48297  271 
val term_max_depth = 1 
272 
val type_max_depth = 1 

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

273 

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

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

276 
thy_feature_name_of (Context.theory_name thy) :: 
48302  277 
interesting_terms_types_and_classes term_max_depth type_max_depth ts 
278 
> exists (not o is_lambda_free) ts ? cons "lambdas" 

279 
> exists (exists_Const is_exists) ts ? cons "skolems" 

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

281 
> (case status of 

282 
General => I 

283 
 Induction => cons "induction" 

284 
 Intro => cons "intro" 

285 
 Inductive => cons "inductive" 

286 
 Elim => cons "elim" 

287 
 Simp => cons "simp" 

288 
 Def => cons "def") 

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

289 

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

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

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

292 

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

293 
val freezeT = Type.legacy_freeze_type 
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 freeze (t $ u) = freeze t $ freeze u 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

296 
 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

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

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

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

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

301 

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

302 
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

303 

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

304 
fun run_prover ctxt (params as {provers, ...}) facts goal = 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

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

307 
{state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1, 
48289  308 
facts = facts > map (apfst (apfst (fn name => name ()))) 
309 
> map Sledgehammer_Provers.Untranslated_Fact} 

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

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

311 
Sledgehammer_Minimize.get_minimizing_prover ctxt 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

312 
Sledgehammer_Provers.Normal (hd provers) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

314 

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

315 
fun accessibility_of thy thy_facts = 
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

316 
case Symtab.lookup thy_facts (Context.theory_name thy) of 
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

317 
SOME (fact :: _) => [fact] 
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

318 
 _ => parent_facts thy thy_facts 
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

319 

48304  320 
val thy_name_of_fact = hd o Long_Name.explode 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

321 

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

322 

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

48311  325 
fun run_mash ctxt save write_cmds read_preds = 
326 
let 

327 
val temp_dir = getenv "ISABELLE_TMP" 

328 
val serial = serial_string () 

329 
val cmd_file = temp_dir ^ "/mash_commands." ^ serial 

330 
val cmd_path = Path.explode cmd_file 

331 
val pred_file = temp_dir ^ "/mash_preds." ^ serial 

332 
val log_file = temp_dir ^ "/mash_log." ^ serial 

333 
val command = 

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

334 
mash_home () ^ "/mash.py quiet inputFile " ^ cmd_file ^ 
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

335 
" outputDir " ^ mash_state_dir () ^ " predictions " ^ pred_file ^ 
48313
0faafdffa662
mesh facts by taking into consideration whether a fact is known to MeSh
blanchet
parents:
48312
diff
changeset

336 
" log " ^ log_file ^ " numberOfPredictions 1000" ^ 
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

337 
(if save then " saveModel" else "") 
48311  338 
val _ = File.write cmd_path "" 
339 
val _ = write_cmds (File.append cmd_path) 

340 
val _ = trace_msg ctxt (fn () => " running " ^ command) 

341 
val _ = Isabelle_System.bash command 

342 
in read_preds (fn () => File.read_lines (Path.explode pred_file)) end 

343 

344 
fun str_of_update (fact, access, feats, deps) = 

345 
"! " ^ escape_meta fact ^ ": " ^ escape_metas access ^ "; " ^ 

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

347 

348 
fun str_of_query (access, feats) = 

349 
"? " ^ escape_metas access ^ "; " ^ escape_metas feats 

350 

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

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

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

356 
path () 

357 
end 

48302  358 

48309  359 
fun mash_ADD _ [] = () 
48311  360 
 mash_ADD ctxt upds = 
361 
(trace_msg ctxt (fn () => "MaSh ADD " ^ space_implode " " (map #1 upds)); 

362 
run_mash ctxt true (fn append => List.app (append o str_of_update) upds) 

363 
(K ())) 

48302  364 

48308  365 
fun mash_DEL ctxt facts feats = 
366 
trace_msg ctxt (fn () => 

367 
"MaSh DEL " ^ escape_metas facts ^ "; " ^ escape_metas feats) 

48302  368 

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

370 
(trace_msg ctxt (fn () => "MaSh QUERY " ^ space_implode " " feats); 
48311  371 
run_mash ctxt false (fn append => append (str_of_query query)) 
372 
(fn preds => snd (extract_query (List.last (preds ())))) 

373 
handle List.Empty => []) 

48302  374 

375 

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

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

377 

48301  378 
type mash_state = 
48308  379 
{dirty_thys : unit Symtab.table, 
48301  380 
thy_facts : string list Symtab.table} 
381 

48304  382 
val empty_state = 
48308  383 
{dirty_thys = Symtab.empty, 
48301  384 
thy_facts = Symtab.empty} 
385 

386 
local 

387 

388 
fun mash_load (state as (true, _)) = state 

389 
 mash_load _ = 

48309  390 
let val path = mash_state_path () in 
48302  391 
(true, 
392 
case try File.read_lines path of 

48308  393 
SOME (dirty_line :: facts_lines) => 
48302  394 
let 
48306  395 
fun dirty_thys_of_line line = 
48308  396 
Symtab.make (line > unescape_metas > map (rpair ())) 
48302  397 
fun add_facts_line line = 
48308  398 
case unescape_metas line of 
48302  399 
thy :: facts => Symtab.update_new (thy, facts) 
400 
 _ => I (* shouldn't happen *) 

401 
in 

48308  402 
{dirty_thys = dirty_thys_of_line dirty_line, 
48302  403 
thy_facts = fold add_facts_line facts_lines Symtab.empty} 
404 
end 

48304  405 
 _ => empty_state) 
48302  406 
end 
48249  407 

48308  408 
fun mash_save ({dirty_thys, thy_facts} : mash_state) = 
48301  409 
let 
48309  410 
val path = mash_state_path () 
48308  411 
val dirty_line = (escape_metas (Symtab.keys dirty_thys)) ^ "\n" 
48303
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

412 
fun fact_line_for (thy, facts) = escape_metas (thy :: facts) ^ "\n" 
48301  413 
in 
48308  414 
File.write path dirty_line; 
48301  415 
Symtab.fold (fn thy_fact => fn () => 
48308  416 
File.append path (fact_line_for thy_fact)) thy_facts () 
48301  417 
end 
418 

48302  419 
val global_state = 
48304  420 
Synchronized.var "Sledgehammer_Filter_MaSh.global_state" (false, empty_state) 
48301  421 

422 
in 

423 

48306  424 
fun mash_map f = 
48302  425 
Synchronized.change global_state (mash_load ##> (f #> tap mash_save)) 
426 

48304  427 
fun mash_get () = Synchronized.change_result global_state (mash_load #> `snd) 
48302  428 

48308  429 
fun mash_reset ctxt = 
48302  430 
Synchronized.change global_state (fn _ => 
48309  431 
(mash_RESET ctxt; File.write (mash_state_path ()) ""; 
48308  432 
(true, empty_state))) 
48301  433 

434 
end 

435 

48308  436 
fun mash_can_suggest_facts (_ : Proof.context) = 
437 
not (Symtab.is_empty (#thy_facts (mash_get ()))) 

48249  438 

48311  439 
fun mash_suggest_facts ctxt params prover hyp_ts concl_t facts = 
48301  440 
let 
48302  441 
val thy = Proof_Context.theory_of ctxt 
48311  442 
val thy_facts = #thy_facts (mash_get ()) 
443 
val access = accessibility_of thy thy_facts 

48302  444 
val feats = features_of thy General (concl_t :: hyp_ts) 
48311  445 
val suggs = mash_QUERY ctxt (access, feats) 
446 
in suggested_facts suggs facts end 

48249  447 

48308  448 
fun mash_can_learn_thy (_ : Proof.context) thy = 
48306  449 
not (Symtab.defined (#dirty_thys (mash_get ())) (Context.theory_name thy)) 
48304  450 

451 
fun is_fact_in_thy_facts thy_facts fact = 

452 
case Symtab.lookup thy_facts (thy_name_of_fact fact) of 

453 
SOME facts => member (op =) facts fact 

454 
 NONE => false 

48249  455 

48306  456 
fun zip_facts news [] = news 
457 
 zip_facts [] olds = olds 

458 
 zip_facts (new :: news) (old :: olds) = 

459 
if new = old then 

460 
new :: zip_facts news olds 

461 
else if member (op =) news old then 

462 
old :: zip_facts (filter_out (curry (op =) old) news) olds 

463 
else if member (op =) olds new then 

464 
new :: zip_facts news (filter_out (curry (op =) new) olds) 

465 
else 

466 
new :: old :: zip_facts news olds 

467 

468 
fun add_thy_facts_from_thys new old = 

469 
let 

470 
fun add_thy (thy, new_facts) = 

471 
case Symtab.lookup old thy of 

472 
SOME old_facts => Symtab.update (thy, zip_facts old_facts new_facts) 

473 
 NONE => Symtab.update_new (thy, new_facts) 

474 
in old > Symtab.fold add_thy new end 

475 

48308  476 
fun mash_learn_thy ctxt thy timeout = 
48304  477 
let 
478 
val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt 

479 
val facts = all_non_tautological_facts_of thy css_table 

48306  480 
val {thy_facts, ...} = mash_get () 
48304  481 
fun is_old (_, th) = is_fact_in_thy_facts thy_facts (Thm.get_name_hint th) 
482 
val (old_facts, new_facts) = 

483 
facts > List.partition is_old > sort (thm_ord o pairself snd) 

48308  484 
in 
485 
if null new_facts then 

486 
() 

487 
else 

48304  488 
let 
48308  489 
val ths = facts > map snd 
490 
val all_names = ths > map Thm.get_name_hint 

48311  491 
fun do_fact ((_, (_, status)), th) (prevs, upds) = 
48308  492 
let 
493 
val name = Thm.get_name_hint th 

494 
val feats = features_of thy status [prop_of th] 

495 
val deps = isabelle_dependencies_of all_names th 

48311  496 
val upd = (name, prevs, feats, deps) 
497 
in ([name], upd :: upds) end 

48308  498 
val parents = parent_facts thy thy_facts 
48311  499 
val (_, upds) = (parents, []) > fold do_fact new_facts 
48308  500 
val new_thy_facts = new_facts > thy_facts_from_thms 
501 
fun trans {dirty_thys, thy_facts} = 

48311  502 
(mash_ADD ctxt (rev upds); 
48308  503 
{dirty_thys = dirty_thys, 
504 
thy_facts = thy_facts > add_thy_facts_from_thys new_thy_facts}) 

505 
in mash_map trans end 

506 
end 

48304  507 

48309  508 
fun mash_learn_proof ctxt thy t ths = 
509 
mash_map (fn state as {dirty_thys, thy_facts} => 

510 
let val deps = ths > map Thm.get_name_hint in 

511 
if forall (is_fact_in_thy_facts thy_facts) deps then 

512 
let 

513 
val fact = ATP_Util.timestamp () (* should be fairly fresh *) 

514 
val access = accessibility_of thy thy_facts 

515 
val feats = features_of thy General [t] 

516 
in 

517 
mash_ADD ctxt [(fact, access, feats, deps)]; 

518 
{dirty_thys = dirty_thys, thy_facts = thy_facts} 

519 
end 

520 
else 

521 
state 

522 
end) 

48249  523 

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

524 
fun relevant_facts ctxt (params as {fact_filter, ...}) prover max_facts 
48298  525 
({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

526 
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

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

528 
else if only then 
48289  529 
facts 
48293  530 
else if max_facts <= 0 then 
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset

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

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

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

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

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

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

537 
 NONE => if mash_home () = "" then iterN else meshN 
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset

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

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

543 
fun iter () = 
48298  544 
iterative_relevant_facts ctxt params prover max_facts NONE hyp_ts 
545 
concl_t facts 

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

546 
> (fn facts => (facts, SOME (length facts))) 
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

547 
fun mash () = 
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

548 
(facts > mash_suggest_facts ctxt params prover hyp_ts concl_t, NONE) 
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

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

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

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

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

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

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

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

556 

48248  557 
end; 