author  blanchet 
Wed, 18 Jul 2012 08:44:04 +0200  
changeset 48303  f1d135d0ea69 
parent 48302  6cf5e58f1185 
child 48304  50e64af9c829 
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 

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

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

18 
val escape_metas : string list > string 
48299  19 
val all_non_tautological_facts_of : 
20 
theory > status Termtab.table > fact list 

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

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

22 
val thm_ord : thm * thm > order 
48303
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

23 
val thy_facts_from_thms : ('a * thm) list > string list Symtab.table 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

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

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

28 
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

29 
val run_prover : Proof.context > params > fact list > thm > prover_result 
48299  30 
val generate_accessibility : Proof.context > theory > bool > string > unit 
31 
val generate_features : Proof.context > theory > bool > string > unit 

32 
val generate_isa_dependencies : 

33 
Proof.context > theory > bool > string > unit 

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

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

35 
Proof.context > params > theory > bool > string > unit 
48302  36 
val mash_RESET : unit > unit 
37 
val mash_ADD : string > string list > string list > string list > unit 

38 
val mash_DEL : string list > string list > unit 

39 
val mash_SUGGEST : string list > string list > string list 

48298  40 
val mash_reset : unit > unit 
41 
val mash_can_suggest_facts : unit > bool 

42 
val mash_suggest_facts : 

48302  43 
Proof.context > params > string > int > term list > term > fact list 
48298  44 
> fact list * fact list 
45 
val mash_can_learn_thy : theory > bool 

46 
val mash_learn_thy : theory > real > unit 

47 
val mash_learn_proof : theory > term > thm list > unit 

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

48 
val relevant_facts : 
48292  49 
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

50 
> term > fact list > fact list 
48248  51 
end; 
52 

53 
structure Sledgehammer_Filter_MaSh : SLEDGEHAMMER_FILTER_MASH = 

54 
struct 

48249  55 

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

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

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

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

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

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

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

62 

48301  63 
val mash_dir = "mash" 
64 
val model_file = "model" 

65 
val state_file = "state" 

66 

48302  67 
fun mk_path file = 
68 
getenv "ISABELLE_HOME_USER" ^ "/" ^ mash_dir ^ "/" ^ file 

69 
> Path.explode 

48249  70 

48302  71 
val fresh_fact_prefix = Long_Name.separator 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

72 

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

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

74 

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

75 
fun escape_meta_char c = 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

76 
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

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

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

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

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

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

82 

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

83 
val escape_meta = String.translate escape_meta_char 
48303
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

84 
val escape_metas = map escape_meta #> space_implode " " 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

85 

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

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

87 

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

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

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

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

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

92 

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

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

94 

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

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

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

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

98 

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

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

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

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

102 

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

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

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

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

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

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

108 

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

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

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

111 
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

112 

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

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

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

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

116 
 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

117 

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

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

119 

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

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

121 

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

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

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

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

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

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

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

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

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

130 
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

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

132 
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

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

134 

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

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

136 

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

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

139 
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

140 
val bad_consts = atp_widely_irrelevant_consts 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

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

143 
#> fold do_add_type Ts 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

144 
 do_add_type (TFree (_, S)) = union (op =) (map class_name_of S) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

145 
 do_add_type (TVar (_, S)) = union (op =) (map class_name_of S) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

146 
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

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

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

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

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

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

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

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

154 
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

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

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

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

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

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

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

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

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

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

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

165 
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

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

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

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

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

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

171 
end 
48302  172 
in [] > fold add_patterns ts > sort string_ord end 
48251
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_likely_tautology th = 
48302  175 
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

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

177 

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

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

179 
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

180 

48299  181 
fun all_non_tautological_facts_of thy css_table = 
182 
all_facts_of thy css_table 

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

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

184 

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

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

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

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

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

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

190 

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

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

192 

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

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

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

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

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

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

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

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

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

201 

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

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

203 
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

204 

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

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

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

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

208 
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

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

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

211 
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

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

213 

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

214 
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

215 

48297  216 
val term_max_depth = 1 
217 
val type_max_depth = 1 

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

218 

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

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

221 
thy_feature_name_of (Context.theory_name thy) :: 
48302  222 
interesting_terms_types_and_classes term_max_depth type_max_depth ts 
223 
> exists (not o is_lambda_free) ts ? cons "lambdas" 

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

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

226 
> (case status of 

227 
General => I 

228 
 Induction => cons "induction" 

229 
 Intro => cons "intro" 

230 
 Inductive => cons "inductive" 

231 
 Elim => cons "elim" 

232 
 Simp => cons "simp" 

233 
 Def => cons "def") 

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

234 

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

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

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

237 

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

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

241 
 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

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

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

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

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

246 

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

247 
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

248 

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

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

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

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

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

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

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

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

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

258 
in prover params (K (K (K ""))) problem end 
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 
(* ### 
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

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

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

263 
fun add_facts (f :: fs) prevs = (f, prevs) :: add_facts fs [th] 
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

264 
fun add_thy facts = 
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

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

266 
val thy = theory_of_thm (hd facts) 
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

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

268 
in add_thms facts parents end 
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

269 
in fold (add_thy o snd) thy_facts end 
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

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

271 

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

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

273 
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

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

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

276 

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

277 
fun theory_of_fact thy fact = 
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

278 
Context.this_theory thy (hd (Long_Name.explode fact)) 
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

279 

48299  280 
fun generate_accessibility ctxt thy include_thy file_name = 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

282 
val path = file_name > Path.explode 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

283 
val _ = File.write path "" 
48303
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

284 
fun do_fact fact prevs = 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

286 
val s = escape_meta fact ^ ": " ^ escape_metas prevs ^ "\n" 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

287 
val _ = File.append path s 
48303
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

288 
in [fact] end 
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

289 
val thy_facts = 
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

290 
all_non_tautological_facts_of thy Termtab.empty 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

291 
> not include_thy ? filter_out (has_thy thy o snd) 
48303
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

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

293 
fun do_thy facts = 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

295 
val thy = theory_of_fact thy (hd facts) 
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

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

297 
in fold do_fact facts parents; () end 
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

298 
in Symtab.fold (fn (_, facts) => K (do_thy facts)) thy_facts () end 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

299 

48299  300 
fun generate_features ctxt thy include_thy file_name = 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

302 
val path = file_name > Path.explode 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

303 
val _ = File.write path "" 
48299  304 
val css_table = clasimpset_rule_table_of ctxt 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

305 
val facts = 
48299  306 
all_non_tautological_facts_of thy css_table 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

307 
> not include_thy ? filter_out (has_thy thy o snd) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

308 
fun do_fact ((_, (_, status)), th) = 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

310 
val name = Thm.get_name_hint th 
48302  311 
val feats = features_of (theory_of_thm th) status [prop_of th] 
48303
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

312 
val s = escape_meta name ^ ": " ^ escape_metas feats ^ "\n" 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

313 
in File.append path s end 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

314 
in List.app do_fact facts end 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

315 

48299  316 
fun generate_isa_dependencies ctxt thy include_thy file_name = 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

318 
val path = file_name > Path.explode 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

319 
val _ = File.write path "" 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

321 
all_non_tautological_facts_of thy Termtab.empty 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

322 
> not include_thy ? filter_out (has_thy thy o snd) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

324 
val all_names = ths > map Thm.get_name_hint 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

325 
fun do_thm th = 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

327 
val name = Thm.get_name_hint th 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

328 
val deps = isabelle_dependencies_of all_names th 
48303
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

329 
val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n" 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

330 
in File.append path s end 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

331 
in List.app do_thm ths end 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

332 

48293  333 
fun generate_atp_dependencies ctxt (params as {provers, max_facts, ...}) thy 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

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

336 
val path = file_name > Path.explode 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

337 
val _ = File.write path "" 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

339 
all_non_tautological_facts_of thy Termtab.empty 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

340 
> not include_thy ? filter_out (has_thy thy o snd) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

341 
val ths = facts > map snd 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

342 
val all_names = ths > map Thm.get_name_hint 
48303
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

343 
fun is_dep dep (_, th) = Thm.get_name_hint th = dep 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

344 
fun add_isa_dep facts dep accum = 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

345 
if exists (is_dep dep) accum then 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

347 
else case find_first (is_dep dep) facts of 
48289  348 
SOME ((name, status), th) => accum @ [((name, status), th)] 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

349 
 NONE => accum (* shouldn't happen *) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

350 
fun fix_name ((_, stature), th) = 
48303
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

351 
((fn () => th > Thm.get_name_hint, stature), th) 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

352 
fun do_thm th = 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

354 
val name = Thm.get_name_hint th 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

355 
val goal = goal_of_thm thy th 
48292  356 
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

358 
case isabelle_dependencies_of all_names th of 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

360 
 isa_dep as [_] => isa_dep (* can hardly beat that *) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

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

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

364 
facts > filter (fn (_, th') => thm_ord (th', th) = LESS) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

365 
val facts = 
48292  366 
facts > iterative_relevant_facts ctxt params (hd provers) 
48293  367 
(the max_facts) NONE hyp_ts concl_t 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

368 
> fold (add_isa_dep facts) isa_deps 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

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

371 
case run_prover ctxt params facts goal of 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

372 
{outcome = NONE, used_facts, ...} => 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

373 
used_facts > map fst > sort string_ord 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

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

376 
val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n" 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

377 
in File.append path s end 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

378 
in List.app do_thm ths end 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

379 

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

380 

48302  381 
(*** Lowlevel communication with MaSh ***) 
382 

383 
fun mash_RESET () = (warning "MaSh RESET"; File.rm (mk_path model_file)) 

384 

385 
fun mash_ADD fact access feats deps = 

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

386 
warning ("MaSh ADD " ^ fact ^ ": " ^ escape_metas access ^ "; " ^ 
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

387 
escape_metas feats ^ "; " ^ escape_metas deps) 
48302  388 

389 
fun mash_DEL facts feats = 

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

390 
warning ("MaSh DEL " ^ escape_metas facts ^ "; " ^ escape_metas feats) 
48302  391 

392 
fun mash_SUGGEST access feats = 

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

393 
(warning ("MaSh SUGGEST " ^ escape_metas access ^ "; " ^ escape_metas feats); 
48302  394 
[]) 
395 

396 

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

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

398 

48301  399 
type mash_state = 
48302  400 
{fresh : int, 
401 
completed_thys : unit Symtab.table, 

48301  402 
thy_facts : string list Symtab.table} 
403 

404 
val mash_zero = 

48302  405 
{fresh = 0, 
406 
completed_thys = Symtab.empty, 

48301  407 
thy_facts = Symtab.empty} 
408 

409 
local 

410 

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

412 
 mash_load _ = 

48302  413 
let 
414 
val path = mk_path state_file 

415 
val _ = Isabelle_System.mkdir (path > Path.dir) 

416 
in 

417 
(true, 

418 
case try File.read_lines path of 

419 
SOME (fresh_line :: comp_line :: facts_lines) => 

420 
let 

421 
fun comp_thys_of_line comp_line = 

422 
Symtab.make (comp_line > space_explode " " > map (rpair ())) 

423 
fun add_facts_line line = 

424 
case space_explode " " line of 

425 
thy :: facts => Symtab.update_new (thy, facts) 

426 
 _ => I (* shouldn't happen *) 

427 
in 

428 
{fresh = Int.fromString fresh_line > the_default 0, 

429 
completed_thys = comp_thys_of_line comp_line, 

430 
thy_facts = fold add_facts_line facts_lines Symtab.empty} 

431 
end 

432 
 _ => mash_zero) 

433 
end 

48249  434 

48302  435 
fun mash_save ({fresh, completed_thys, thy_facts} : mash_state) = 
48301  436 
let 
48302  437 
val path = mk_path state_file 
48303
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

438 
val comp_line = (completed_thys > Symtab.keys > escape_metas) ^ "\n" 
f1d135d0ea69
improved MaSh string escaping and make more operations stringbased
blanchet
parents:
48302
diff
changeset

439 
fun fact_line_for (thy, facts) = escape_metas (thy :: facts) ^ "\n" 
48301  440 
in 
48302  441 
File.write path (string_of_int fresh ^ "\n" ^ comp_line); 
48301  442 
Symtab.fold (fn thy_fact => fn () => 
443 
File.append path (fact_line_for thy_fact)) thy_facts 

444 
end 

445 

48302  446 
val global_state = 
447 
Synchronized.var "Sledgehammer_Filter_MaSh.global_state" (false, mash_zero) 

48301  448 

449 
in 

450 

451 
fun mash_change f = 

48302  452 
Synchronized.change global_state (mash_load ##> (f #> tap mash_save)) 
453 

454 
fun mash_peek f = Synchronized.change global_state (mash_load ##> tap f) 

48301  455 

48302  456 
fun mash_value () = Synchronized.change_result global_state (mash_load #> `snd) 
457 

458 
fun mash_reset () = 

459 
Synchronized.change global_state (fn _ => 

460 
(mash_RESET (); File.rm (mk_path state_file); (true, mash_zero))) 

48301  461 

462 
end 

463 

464 
fun mash_can_suggest_facts () = 

465 
not (Symtab.is_empty (#thy_facts (mash_value ()))) 

48249  466 

48298  467 
fun mash_suggest_facts ctxt params prover max_facts hyp_ts concl_t facts = 
48301  468 
let 
48302  469 
val thy = Proof_Context.theory_of ctxt 
470 
val access = accessibility_of thy (#thy_facts (mash_value ())) 

471 
val feats = features_of thy General (concl_t :: hyp_ts) 

48301  472 
val suggs = mash_SUGGEST access feats 
473 
in (facts, []) end 

48249  474 

48301  475 
fun mash_can_learn_thy thy = 
476 
not (Symtab.defined (#completed_thys (mash_value ())) 

477 
(Context.theory_name thy)) 

48249  478 

48298  479 
fun mash_learn_thy thy timeout = () 
48302  480 
(* ### *) 
48298  481 

48302  482 
fun mash_learn_proof thy t ths = 
483 
mash_change (fn {fresh, completed_thys, thy_facts} => 

484 
let 

485 
val fact = fresh_fact_prefix ^ string_of_int fresh 

486 
val access = accessibility_of thy thy_facts 

487 
val feats = features_of thy General [t] 

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

488 
val deps = ths > map Thm.get_name_hint 
48302  489 
in 
490 
mash_ADD fact access feats deps; 

491 
{fresh = fresh + 1, completed_thys = completed_thys, 

492 
thy_facts = thy_facts} 

493 
end) 

48249  494 

48293  495 
fun relevant_facts ctxt params prover max_facts 
48298  496 
({add, only, ...} : fact_override) hyp_ts concl_t facts = 
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset

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

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

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

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

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

505 
((facts > filter (member Thm.eq_thm_prop ths o snd)) @ 
48292  506 
(accepts > filter_out (member Thm.eq_thm_prop ths o snd))) 
48293  507 
> take max_facts 
48298  508 
val iter_facts = 
509 
iterative_relevant_facts ctxt params prover max_facts NONE hyp_ts 

510 
concl_t facts 

511 
val (mash_facts, mash_rejected) = 

512 
mash_suggest_facts ctxt params prover max_facts hyp_ts concl_t facts 

48302  513 
val mesh_facts = iter_facts (* ### *) 
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset

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

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

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

518 

48248  519 
end; 