author  blanchet 
Wed, 18 Jul 2012 08:44:04 +0200  
changeset 48316  252f45c04042 
parent 48315  82d6e46c673f 
child 48318  325c8fd0d762 
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 
48315
82d6e46c673f
fixed order of accessibles + other tweaks to MaSh
blanchet
parents:
48314
diff
changeset

29 
val is_likely_tautology : thm > bool 
82d6e46c673f
fixed order of accessibles + other tweaks to MaSh
blanchet
parents:
48314
diff
changeset

30 
val is_too_meta : thm > bool 
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 
48302  33 
val features_of : theory > status > term list > string list 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

34 
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

35 
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

36 
val run_prover : Proof.context > params > fact list > thm > prover_result 
48308  37 
val mash_RESET : Proof.context > unit 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

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

40 
> (string * string list * string list * string list) list > unit 
48308  41 
val mash_ADD : 
48316
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 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

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

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

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

51 
val mash_learn_thy : Proof.context > params > theory > real > unit 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

53 
Proof.context > params > term > thm list > fact list > unit 
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset

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

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

59 
structure Sledgehammer_Filter_MaSh : SLEDGEHAMMER_FILTER_MASH = 

60 
struct 

48249  61 

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

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

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

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

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

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

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

68 

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

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

72 

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

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

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

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

76 

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

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

78 

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

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

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

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

83 
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

84 

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

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

86 

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

88 
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

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

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

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

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

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

94 

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

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

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

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

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

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

102 

103 
val escape_meta = String.translate meta_char 

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

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

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

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

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

108 

48311  109 
fun extract_query line = 
110 
case space_explode ":" line of 

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

111 
[goal_name, suggs] => (unescape_meta goal_name, unescape_metas suggs) 
48312  112 
 _ => ("", []) 
48311  113 

114 
fun find_suggested facts sugg = 

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

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

117 

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

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

119 
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

120 

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

121 
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

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

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

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

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

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

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

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

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

130 
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

131 
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

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

133 
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

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

135 
end 
48312  136 

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

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

138 

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

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

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

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

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

143 

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

144 
local 
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 
fun has_bool @{typ bool} = true 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

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

149 

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

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

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

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

153 

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

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

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

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

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

158 
@{const_name HOL.eq}] 
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 
val has_bool_arg_const = 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

162 
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

163 

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

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

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

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

167 
 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

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

169 

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

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

171 

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

172 
in 
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 
fun is_fo_term thy t = 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

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

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

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

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

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

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

182 
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

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

184 
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

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

186 

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

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

188 

48302  189 
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

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

191 
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

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

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

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

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

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

200 
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

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

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

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

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

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

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

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

208 
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

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

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

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

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

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

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

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

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

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

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

219 
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

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

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

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

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

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

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

227 

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

228 
fun is_likely_tautology th = 
48302  229 
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

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

231 

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

232 
(* ### FIXME: optimize *) 
82d6e46c673f
fixed order of accessibles + other tweaks to MaSh
blanchet
parents:
48314
diff
changeset

233 
fun is_too_meta th = 
82d6e46c673f
fixed order of accessibles + other tweaks to MaSh
blanchet
parents:
48314
diff
changeset

234 
fastype_of (Object_Logic.atomize_term (theory_of_thm th) (prop_of th)) 
82d6e46c673f
fixed order of accessibles + other tweaks to MaSh
blanchet
parents:
48314
diff
changeset

235 
<> @{typ bool} 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

236 

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

237 
fun theory_ord p = 
48315
82d6e46c673f
fixed order of accessibles + other tweaks to MaSh
blanchet
parents:
48314
diff
changeset

238 
if Theory.eq_thy p then 
82d6e46c673f
fixed order of accessibles + other tweaks to MaSh
blanchet
parents:
48314
diff
changeset

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

240 
else if Theory.subthy p then 
82d6e46c673f
fixed order of accessibles + other tweaks to MaSh
blanchet
parents:
48314
diff
changeset

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

242 
else if Theory.subthy (swap p) then 
82d6e46c673f
fixed order of accessibles + other tweaks to MaSh
blanchet
parents:
48314
diff
changeset

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

244 
else case int_ord (pairself (length o Theory.ancestors_of) p) of 
82d6e46c673f
fixed order of accessibles + other tweaks to MaSh
blanchet
parents:
48314
diff
changeset

245 
EQUAL => string_ord (pairself Context.theory_name p) 
82d6e46c673f
fixed order of accessibles + other tweaks to MaSh
blanchet
parents:
48314
diff
changeset

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

247 

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

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

249 

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

250 
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

251 

48297  252 
val term_max_depth = 1 
253 
val type_max_depth = 1 

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

254 

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

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

257 
thy_feature_name_of (Context.theory_name thy) :: 
48302  258 
interesting_terms_types_and_classes term_max_depth type_max_depth ts 
259 
> exists (not o is_lambda_free) ts ? cons "lambdas" 

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

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

262 
> (case status of 

263 
General => I 

264 
 Induction => cons "induction" 

265 
 Intro => cons "intro" 

266 
 Inductive => cons "inductive" 

267 
 Elim => cons "elim" 

268 
 Simp => cons "simp" 

269 
 Def => cons "def") 

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

270 

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

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

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

277 
 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

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

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

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

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

282 

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

283 
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

284 

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

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

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

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

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

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

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

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

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

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

295 

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

296 

48302  297 
(*** Lowlevel communication with MaSh ***) 
298 

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

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

300 

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

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

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

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

304 

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

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

307 
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

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

310 
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

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

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

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

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

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

316 

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

317 
fun write_file write file = 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

318 
let val path = Path.explode file in 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

319 
File.write path ""; write (File.append path) 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

320 
end 
48311  321 

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

322 
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

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

324 
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

325 
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

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

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

328 
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

329 
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

330 
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

331 
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

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

333 

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

334 
fun run_mash_commands ctxt overlord save write_cmds read_preds = 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

336 
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

337 
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

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

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

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

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

342 
("inputFile " ^ cmd_file ^ " predictions " ^ pred_file ^ 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

343 
" numberOfPredictions " ^ string_of_int max_preds ^ 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

344 
(if save then " saveModel" else "")); 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

345 
read_preds (fn () => File.read_lines (Path.explode pred_file)) 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

347 

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

348 
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

349 
"! " ^ escape_meta name ^ ": " ^ escape_metas parents ^ "; " ^ 
48311  350 
escape_metas feats ^ "; " ^ escape_metas deps ^ "\n" 
351 

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

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

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

354 

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

355 
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

356 
escape_meta name ^ ": " ^ escape_metas (get upd) ^ "\n" 
48311  357 

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

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

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

363 
path () 

364 
end 

48302  365 

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

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

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

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

369 
elide_string 1000 (space_implode " " (map #1 upds))); 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

371 
(fn append => List.app (append o init_str_of_update #2) upds) 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

372 
(fn append => List.app (append o init_str_of_update #3) upds) 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

373 
(fn append => List.app (append o init_str_of_update #4) upds)) 
48302  374 

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

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

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

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

378 
elide_string 1000 (space_implode " " (map #1 upds))); 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

380 
(fn append => List.app (append o str_of_update) upds) (K ())) 
48302  381 

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

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

383 
(trace_msg ctxt (fn () => "MaSh QUERY " ^ space_implode " " feats); 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

385 
(fn append => append (str_of_query query)) 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

386 
(fn preds => snd (extract_query (List.last (preds ())))) 
48311  387 
handle List.Empty => []) 
48302  388 

389 

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

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

391 

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

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

394 
fact_graph : unit Graph.T} 
48301  395 

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

396 
val empty_state = {thys = Symtab.empty, fact_graph = Graph.empty} 
48301  397 

398 
local 

399 

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

401 
 mash_load _ = 

48309  402 
let val path = mash_state_path () in 
48302  403 
(true, 
404 
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

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

407 
fun add_thy comp thy = Symtab.update (thy, comp) 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

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

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

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

412 
Graph.default_node (name, ()) 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

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

415 
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

416 
> fold (add_thy false) (unescape_metas incomp_thys) 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

417 
val fact_graph = Graph.empty > fold add_fact_line fact_lines 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

418 
in {thys = thys, fact_graph = fact_graph} end 
48304  419 
 _ => empty_state) 
48302  420 
end 
48249  421 

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

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

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

426 
fun line_for_thys comp = AList.find (op =) thys comp > escape_metas 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

427 
fun fact_line_for name parents = name :: parents > escape_metas 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

430 
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

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

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

433 
fact_graph () 
48301  434 
end 
435 

48302  436 
val global_state = 
48304  437 
Synchronized.var "Sledgehammer_Filter_MaSh.global_state" (false, empty_state) 
48301  438 

439 
in 

440 

48306  441 
fun mash_map f = 
48302  442 
Synchronized.change global_state (mash_load ##> (f #> tap mash_save)) 
443 

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

48308  446 
fun mash_reset ctxt = 
48302  447 
Synchronized.change global_state (fn _ => 
48309  448 
(mash_RESET ctxt; File.write (mash_state_path ()) ""; 
48308  449 
(true, empty_state))) 
48301  450 

451 
end 

452 

48308  453 
fun mash_can_suggest_facts (_ : Proof.context) = 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

454 
mash_home () <> "" andalso not (Graph.is_empty (#fact_graph (mash_get ()))) 
48249  455 

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

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

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

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

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

460 
> fold (fn (_, th) => Symtab.update (Thm.get_name_hint th, ())) facts 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

461 
in fact_graph > Graph.restrict (Symtab.defined facts) > Graph.maximals end 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

462 

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

463 
fun mash_suggest_facts ctxt ({overlord, ...} : params) prover hyp_ts concl_t 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

464 
facts = 
48301  465 
let 
48302  466 
val thy = Proof_Context.theory_of ctxt 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

468 
val parents = parents_wrt facts fact_graph 
48302  469 
val feats = features_of thy General (concl_t :: hyp_ts) 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

470 
val suggs = mash_QUERY ctxt overlord (parents, feats) 
48311  471 
in suggested_facts suggs facts end 
48249  472 

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

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

474 
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

475 
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

476 
end 
48249  477 

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

478 
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

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

480 
fun maybe_add_from from (accum as (parents, graph)) = 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

481 
(from :: parents, Graph.add_edge_acyclic (from, name) graph) 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

482 
handle Graph.CYCLES _ => 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

484 
"Cycle between " ^ quote from ^ " and " ^ quote name); accum) 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

485 
 Graph.UNDEF _ => 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

486 
(trace_msg ctxt (fn () => "Unknown node " ^ quote from); accum) 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

488 
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

489 
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

490 
in ((name, parents, feats, deps) :: upds, graph) end 
48306  491 

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

492 
fun mash_learn_thy ctxt ({overlord, ...} : params) thy timeout = 
48304  493 
let 
494 
val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt 

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

495 
val facts = all_facts_of thy css_table 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

496 
val {fact_graph, ...} = mash_get () 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

497 
fun is_old (_, th) = can (Graph.get_node fact_graph) (Thm.get_name_hint th) 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

498 
val new_facts = facts > filter_out is_old > sort (thm_ord o pairself snd) 
48308  499 
in 
500 
if null new_facts then 

501 
() 

502 
else 

48304  503 
let 
48308  504 
val ths = facts > map snd 
48315
82d6e46c673f
fixed order of accessibles + other tweaks to MaSh
blanchet
parents:
48314
diff
changeset

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

506 
ths > filter_out (is_likely_tautology orf is_too_meta) 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

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

509 
fun do_fact ((_, (_, status)), th) (parents, upds) = 
48308  510 
let 
511 
val name = Thm.get_name_hint th 

512 
val feats = features_of thy status [prop_of th] 

513 
val deps = isabelle_dependencies_of all_names th 

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

514 
val upd = (name, parents, feats, deps) 
48311  515 
in ([name], upd :: upds) end 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

516 
val parents = parents_wrt facts fact_graph 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

517 
val (_, upds) = (parents, []) > fold do_fact new_facts > rev 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

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

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

521 
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

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

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

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

525 
(mash_INIT_or_ADD ctxt overlord (rev upds); 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

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

528 
end 
48308  529 
in mash_map trans end 
530 
end 

48304  531 

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

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

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

534 
val thy = Proof_Context.theory_of ctxt 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

535 
val name = ATP_Util.timestamp () (* should be fairly fresh *) 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

536 
val feats = features_of thy General [t] 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

537 
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

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

539 
mash_map (fn {thys, fact_graph} => 
48309  540 
let 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

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

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

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

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

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

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

549 
end 
48249  550 

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

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

553 
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

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

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

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

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

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

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

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

563 
SOME ff => ff 
48315
82d6e46c673f
fixed order of accessibles + other tweaks to MaSh
blanchet
parents:
48314
diff
changeset

564 
 NONE => if mash_can_suggest_facts ctxt then meshN else iterN 
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset

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

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

570 
fun iter () = 
48298  571 
iterative_relevant_facts ctxt params prover max_facts NONE hyp_ts 
572 
concl_t facts 

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

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

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

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

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

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

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

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

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

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

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

583 

48248  584 
end; 