author  blanchet 
Wed, 21 Aug 2013 15:18:06 +0200  
changeset 53128  ea1b62ed5a54 
parent 53127  60801776d8af 
child 53129  f92b24047fc7 
permissions  rwrr 
48380  1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer_mash.ML 
48248  2 
Author: Jasmin Blanchette, TU Muenchen 
3 

4 
Sledgehammer's machinelearningbased relevance filter (MaSh). 

5 
*) 

6 

48381  7 
signature SLEDGEHAMMER_MASH = 
48248  8 
sig 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

9 
type stature = ATP_Problem_Generate.stature 
51004
5f2788c38127
distinguish raw and nonraw facts, using raw for 10 000s of facts and nonraw after selection of some hundreds
blanchet
parents:
51003
diff
changeset

10 
type raw_fact = Sledgehammer_Fact.raw_fact 
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 
51008  18 
val MePoN : string 
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

19 
val MaShN : string 
51008  20 
val MeShN : string 
48379
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (MengPaulson)
blanchet
parents:
48378
diff
changeset

21 
val mepoN : string 
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (MengPaulson)
blanchet
parents:
48378
diff
changeset

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

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

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

25 
val learn_isarN : string 
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset

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

27 
val relearn_isarN : string 
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset

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

29 
val fact_filters : string list 
50826  30 
val encode_str : string > string 
31 
val encode_strs : string list > string 

32 
val unencode_str : string > string 

33 
val unencode_strs : string > string list 

50356  34 
val encode_features : (string * real) list > string 
50965  35 
val extract_suggestions : string > string * string list 
50632
12c097ff3241
slightly more elegant naming convention (to keep lowlevel and highlevel APIs separated)
blanchet
parents:
50631
diff
changeset

36 

12c097ff3241
slightly more elegant naming convention (to keep lowlevel and highlevel APIs separated)
blanchet
parents:
50631
diff
changeset

37 
structure MaSh: 
12c097ff3241
slightly more elegant naming convention (to keep lowlevel and highlevel APIs separated)
blanchet
parents:
50631
diff
changeset

38 
sig 
12c097ff3241
slightly more elegant naming convention (to keep lowlevel and highlevel APIs separated)
blanchet
parents:
50631
diff
changeset

39 
val unlearn : Proof.context > unit 
12c097ff3241
slightly more elegant naming convention (to keep lowlevel and highlevel APIs separated)
blanchet
parents:
50631
diff
changeset

40 
val learn : 
12c097ff3241
slightly more elegant naming convention (to keep lowlevel and highlevel APIs separated)
blanchet
parents:
50631
diff
changeset

41 
Proof.context > bool 
53121
5f727525b1ac
only generate feature weights for queries  they're not used elsewhere
blanchet
parents:
53118
diff
changeset

42 
> (string * string list * string list * string list) list > unit 
50632
12c097ff3241
slightly more elegant naming convention (to keep lowlevel and highlevel APIs separated)
blanchet
parents:
50631
diff
changeset

43 
val relearn : 
12c097ff3241
slightly more elegant naming convention (to keep lowlevel and highlevel APIs separated)
blanchet
parents:
50631
diff
changeset

44 
Proof.context > bool > (string * string list) list > unit 
50969  45 
val query : 
53095  46 
Proof.context > bool > int 
53121
5f727525b1ac
only generate feature weights for queries  they're not used elsewhere
blanchet
parents:
53118
diff
changeset

47 
> (string * string list * string list * string list) list 
53094  48 
* string list * string list * (string * real) list 
49 
> string list 

50632
12c097ff3241
slightly more elegant naming convention (to keep lowlevel and highlevel APIs separated)
blanchet
parents:
50631
diff
changeset

50 
end 
12c097ff3241
slightly more elegant naming convention (to keep lowlevel and highlevel APIs separated)
blanchet
parents:
50631
diff
changeset

51 

50311  52 
val mash_unlearn : Proof.context > unit 
50624
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset

53 
val nickname_of_thm : thm > string 
51134  54 
val find_suggested_facts : 
55 
Proof.context > ('b * thm) list > string list > ('b * thm) list 

48321  56 
val mesh_facts : 
50814  57 
('a * 'a > bool) > int > (real * (('a * real) list * 'a list)) list 
58 
> 'a list 

51135  59 
val crude_thm_ord : thm * thm > order 
51182
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset

60 
val thm_less : thm * thm > bool 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

61 
val goal_of_thm : theory > thm > thm 
48321  62 
val run_prover_for_mash : 
48318  63 
Proof.context > params > string > fact list > thm > prover_result 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

64 
val features_of : 
53127  65 
Proof.context > string > theory > int > int Symtab.table > stature 
66 
> term list > (string * real) list 

51177  67 
val trim_dependencies : string list > string list option 
50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50732
diff
changeset

68 
val isar_dependencies_of : 
50754
74a6adcb96ac
also generate queries for goals with too many Isar dependencies
blanchet
parents:
50751
diff
changeset

69 
string Symtab.table * string Symtab.table > thm > string list 
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset

70 
val prover_dependencies_of : 
51004
5f2788c38127
distinguish raw and nonraw facts, using raw for 10 000s of facts and nonraw after selection of some hundreds
blanchet
parents:
51003
diff
changeset

71 
Proof.context > params > string > int > raw_fact list 
50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50732
diff
changeset

72 
> string Symtab.table * string Symtab.table > thm 
50754
74a6adcb96ac
also generate queries for goals with too many Isar dependencies
blanchet
parents:
50751
diff
changeset

73 
> bool * string list 
53095  74 
val attach_parents_to_facts : 
75 
('a * thm) list > ('a * thm) list > (string list * ('a * thm)) list 

50985  76 
val weight_mepo_facts : 'a list > ('a * real) list 
50608  77 
val weight_mash_facts : 'a list > ('a * real) list 
50412  78 
val find_mash_suggestions : 
51134  79 
Proof.context > int > string list > ('b * thm) list > ('b * thm) list 
80 
> ('b * thm) list > ('b * thm) list * ('b * thm) list 

53127  81 
val add_const_counts : term > int Symtab.table > int Symtab.table 
48406  82 
val mash_suggested_facts : 
51004
5f2788c38127
distinguish raw and nonraw facts, using raw for 10 000s of facts and nonraw after selection of some hundreds
blanchet
parents:
51003
diff
changeset

83 
Proof.context > params > string > int > term list > term 
5f2788c38127
distinguish raw and nonraw facts, using raw for 10 000s of facts and nonraw after selection of some hundreds
blanchet
parents:
51003
diff
changeset

84 
> raw_fact list > fact list * fact list 
48383  85 
val mash_learn_proof : 
48384
83dc102041e6
learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents:
48383
diff
changeset

86 
Proof.context > params > string > term > ('a * thm) list > thm list 
83dc102041e6
learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents:
48383
diff
changeset

87 
> unit 
48395
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset

88 
val mash_learn : 
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset

89 
Proof.context > params > fact_override > thm list > bool > unit 
50311  90 
val is_mash_enabled : unit > bool 
91 
val mash_can_suggest_facts : Proof.context > bool 

50412  92 
val generous_max_facts : int > int 
50814  93 
val mepo_weight : real 
94 
val mash_weight : real 

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

95 
val relevant_facts : 
48292  96 
Proof.context > params > string > int > fact_override > term list 
51010  97 
> term > raw_fact list > (string * fact list) list 
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

98 
val kill_learners : unit > unit 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

99 
val running_learners : unit > unit 
48248  100 
end; 
101 

48381  102 
structure Sledgehammer_MaSh : SLEDGEHAMMER_MASH = 
48248  103 
struct 
48249  104 

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

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

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

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

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

109 
open Sledgehammer_Provers 
48318  110 
open Sledgehammer_Minimize 
48381  111 
open Sledgehammer_MePo 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

112 

48308  113 
val trace = 
48380  114 
Attrib.setup_config_bool @{binding sledgehammer_mash_trace} (K false) 
51032
69da236d7838
added option to use SNoW as machine learning algo
blanchet
parents:
51029
diff
changeset

115 

48308  116 
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else () 
117 

51008  118 
val MePoN = "MePo" 
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

119 
val MaShN = "MaSh" 
51008  120 
val MeShN = "MeSh" 
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

121 

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

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

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

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

125 

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

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

127 

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

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

129 
val learn_isarN = "learn_isar" 
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset

130 
val learn_proverN = "learn_prover" 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

131 
val relearn_isarN = "relearn_isar" 
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset

132 
val relearn_proverN = "relearn_prover" 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

133 

48394
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset

134 
fun mash_model_dir () = 
50340
72519bf5f135
simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents:
50339
diff
changeset

135 
Path.explode "$ISABELLE_HOME_USER/mash" > tap Isabelle_System.mkdir 
48394
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset

136 
val mash_state_dir = mash_model_dir 
50310  137 
fun mash_state_file () = Path.append (mash_state_dir ()) (Path.explode "state") 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

138 

48330  139 

50311  140 
(*** Lowlevel communication with MaSh ***) 
141 

53117  142 
val save_models_arg = "saveModels" 
143 
val shutdown_server_arg = "shutdownServer" 

144 

50311  145 
fun wipe_out_file file = (try (File.rm o Path.explode) file; ()) 
146 

50335
b17b05c8d4a4
proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents:
50319
diff
changeset

147 
fun write_file banner (xs, f) path = 
b17b05c8d4a4
proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents:
50319
diff
changeset

148 
(case banner of SOME s => File.write path s  NONE => (); 
53094  149 
xs > chunk_list 500 > List.app (File.append path o implode o map f)) 
50319
dddcaeb92e11
robust writing of MaSh state  better drop learning data than cause other problems in Sledgehammer
blanchet
parents:
50311
diff
changeset

150 
handle IO.Io _ => () 
50311  151 

53117  152 
fun run_mash_tool ctxt overlord extra_args write_cmds read_suggs = 
50311  153 
let 
154 
val (temp_dir, serial) = 

155 
if overlord then (getenv "ISABELLE_HOME_USER", "") 

156 
else (getenv "ISABELLE_TMP", serial_string ()) 

157 
val log_file = if overlord then temp_dir ^ "/mash_log" else "/dev/null" 

158 
val err_file = temp_dir ^ "/mash_err" ^ serial 

159 
val sugg_file = temp_dir ^ "/mash_suggs" ^ serial 

50335
b17b05c8d4a4
proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents:
50319
diff
changeset

160 
val sugg_path = Path.explode sugg_file 
50311  161 
val cmd_file = temp_dir ^ "/mash_commands" ^ serial 
50335
b17b05c8d4a4
proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents:
50319
diff
changeset

162 
val cmd_path = Path.explode cmd_file 
51001  163 
val model_dir = File.shell_path (mash_model_dir ()) 
53101  164 
val core = "inputFile " ^ cmd_file ^ " predictions " ^ sugg_file 
50311  165 
val command = 
51032
69da236d7838
added option to use SNoW as machine learning algo
blanchet
parents:
51029
diff
changeset

166 
"cd \"$ISABELLE_SLEDGEHAMMER_MASH\"/src; " ^ 
69da236d7838
added option to use SNoW as machine learning algo
blanchet
parents:
51029
diff
changeset

167 
"./mash.py quiet" ^ 
51001  168 
" outputDir " ^ model_dir ^ 
169 
" modelFile=" ^ model_dir ^ "/model.pickle" ^ 

170 
" dictsFile=" ^ model_dir ^ "/dict.pickle" ^ 

171 
" log " ^ log_file ^ " " ^ core ^ 

53117  172 
(if extra_args = [] then "" else " " ^ space_implode " " extra_args) ^ 
50311  173 
" >& " ^ err_file 
174 
fun run_on () = 

50750  175 
(Isabelle_System.bash command 
176 
> tap (fn _ => trace_msg ctxt (fn () => 

177 
case try File.read (Path.explode err_file) of 

178 
NONE => "Done" 

179 
 SOME "" => "Done" 

180 
 SOME s => "Error: " ^ elide_string 1000 s)); 

50335
b17b05c8d4a4
proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents:
50319
diff
changeset

181 
read_suggs (fn () => try File.read_lines sugg_path > these)) 
50311  182 
fun clean_up () = 
183 
if overlord then () 

184 
else List.app wipe_out_file [err_file, sugg_file, cmd_file] 

185 
in 

50335
b17b05c8d4a4
proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents:
50319
diff
changeset

186 
write_file (SOME "") ([], K "") sugg_path; 
b17b05c8d4a4
proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents:
50319
diff
changeset

187 
write_file (SOME "") write_cmds cmd_path; 
50311  188 
trace_msg ctxt (fn () => "Running " ^ command); 
189 
with_cleanup clean_up run_on () 

190 
end 

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

191 

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

193 
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

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

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

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

197 
(* fixed width, in case more digits follow *) 
48395
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset

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

199 

48308  200 
fun unmeta_chars accum [] = String.implode (rev accum) 
48395
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset

201 
 unmeta_chars accum (#"%" :: d1 :: d2 :: d3 :: cs) = 
48308  202 
(case Int.fromString (String.implode [d1, d2, d3]) of 
203 
SOME n => unmeta_chars (Char.chr n :: accum) cs 

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

48395
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset

205 
 unmeta_chars _ (#"%" :: _) = "" (* error *) 
48308  206 
 unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs 
207 

50826  208 
val encode_str = String.translate meta_char 
209 
val encode_strs = map encode_str #> space_implode " " 

210 
val unencode_str = String.explode #> unmeta_chars [] 

211 
val unencode_strs = 

212 
space_explode " " #> filter_out (curry (op =) "") #> map unencode_str 

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

213 

50858  214 
fun freshish_name () = 
215 
Date.fmt ".%Y%m%d_%H%M%S__" (Date.fromTimeLocal (Time.now ())) ^ 

216 
serial_string () 

217 

50356  218 
fun encode_feature (name, weight) = 
50826  219 
encode_str name ^ 
51990  220 
(if Real.== (weight, 1.0) then "" else "=" ^ Markup.print_real weight) 
50356  221 

222 
val encode_features = map encode_feature #> space_implode " " 

223 

50631  224 
fun str_of_learn (name, parents, feats, deps) = 
50826  225 
"! " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^ 
53121
5f727525b1ac
only generate feature weights for queries  they're not used elsewhere
blanchet
parents:
53118
diff
changeset

226 
encode_strs feats ^ "; " ^ encode_strs deps ^ "\n" 
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

227 

50631  228 
fun str_of_relearn (name, deps) = 
50826  229 
"p " ^ encode_str name ^ ": " ^ encode_strs deps ^ "\n" 
50311  230 

53099  231 
fun str_of_query max_suggs (learns, hints, parents, feats) = 
53095  232 
implode (map str_of_learn learns) ^ 
53099  233 
"? " ^ string_of_int max_suggs ^ " # " ^ encode_strs parents ^ "; " ^ 
234 
encode_features feats ^ 

53095  235 
(if null hints then "" else "; " ^ encode_strs hints) ^ "\n" 
48406  236 

53098  237 
(* The suggested weights don't make much sense. *) 
48406  238 
fun extract_suggestion sugg = 
239 
case space_explode "=" sugg of 

51177  240 
[name, _ (* weight *)] => 
50965  241 
SOME (unencode_str name (* , Real.fromString weight > the_default 1.0 *)) 
242 
 [name] => SOME (unencode_str name (* , 1.0 *)) 

48406  243 
 _ => NONE 
244 

50633  245 
fun extract_suggestions line = 
48311  246 
case space_explode ":" line of 
48406  247 
[goal, suggs] => 
50826  248 
(unencode_str goal, map_filter extract_suggestion (space_explode " " suggs)) 
48312  249 
 _ => ("", []) 
48311  250 

50632
12c097ff3241
slightly more elegant naming convention (to keep lowlevel and highlevel APIs separated)
blanchet
parents:
50631
diff
changeset

251 
structure MaSh = 
12c097ff3241
slightly more elegant naming convention (to keep lowlevel and highlevel APIs separated)
blanchet
parents:
50631
diff
changeset

252 
struct 
12c097ff3241
slightly more elegant naming convention (to keep lowlevel and highlevel APIs separated)
blanchet
parents:
50631
diff
changeset

253 

12c097ff3241
slightly more elegant naming convention (to keep lowlevel and highlevel APIs separated)
blanchet
parents:
50631
diff
changeset

254 
fun unlearn ctxt = 
50311  255 
let val path = mash_model_dir () in 
50632
12c097ff3241
slightly more elegant naming convention (to keep lowlevel and highlevel APIs separated)
blanchet
parents:
50631
diff
changeset

256 
trace_msg ctxt (K "MaSh unlearn"); 
53117  257 
run_mash_tool ctxt false [shutdown_server_arg] ([], K ""); 
50319
dddcaeb92e11
robust writing of MaSh state  better drop learning data than cause other problems in Sledgehammer
blanchet
parents:
50311
diff
changeset

258 
try (File.fold_dir (fn file => fn _ => 
dddcaeb92e11
robust writing of MaSh state  better drop learning data than cause other problems in Sledgehammer
blanchet
parents:
50311
diff
changeset

259 
try File.rm (Path.append path (Path.basic file))) 
dddcaeb92e11
robust writing of MaSh state  better drop learning data than cause other problems in Sledgehammer
blanchet
parents:
50311
diff
changeset

260 
path) NONE; 
50311  261 
() 
262 
end 

263 

50632
12c097ff3241
slightly more elegant naming convention (to keep lowlevel and highlevel APIs separated)
blanchet
parents:
50631
diff
changeset

264 
fun learn _ _ [] = () 
12c097ff3241
slightly more elegant naming convention (to keep lowlevel and highlevel APIs separated)
blanchet
parents:
50631
diff
changeset

265 
 learn ctxt overlord learns = 
12c097ff3241
slightly more elegant naming convention (to keep lowlevel and highlevel APIs separated)
blanchet
parents:
50631
diff
changeset

266 
(trace_msg ctxt (fn () => "MaSh learn " ^ 
50631  267 
elide_string 1000 (space_implode " " (map #1 learns))); 
53117  268 
run_mash_tool ctxt overlord [save_models_arg] (learns, str_of_learn) 
269 
(K ())) 

50311  270 

50632
12c097ff3241
slightly more elegant naming convention (to keep lowlevel and highlevel APIs separated)
blanchet
parents:
50631
diff
changeset

271 
fun relearn _ _ [] = () 
12c097ff3241
slightly more elegant naming convention (to keep lowlevel and highlevel APIs separated)
blanchet
parents:
50631
diff
changeset

272 
 relearn ctxt overlord relearns = 
12c097ff3241
slightly more elegant naming convention (to keep lowlevel and highlevel APIs separated)
blanchet
parents:
50631
diff
changeset

273 
(trace_msg ctxt (fn () => "MaSh relearn " ^ 
50631  274 
elide_string 1000 (space_implode " " (map #1 relearns))); 
53117  275 
run_mash_tool ctxt overlord [save_models_arg] (relearns, str_of_relearn) 
276 
(K ())) 

50311  277 

53117  278 
fun query ctxt overlord max_suggs (query as (_, _, _, feats)) = 
50969  279 
(trace_msg ctxt (fn () => "MaSh query " ^ encode_features feats); 
53117  280 
run_mash_tool ctxt overlord [] ([query], str_of_query max_suggs) 
50311  281 
(fn suggs => 
282 
case suggs () of 

283 
[] => [] 

50633  284 
 suggs => snd (extract_suggestions (List.last suggs))) 
50311  285 
handle List.Empty => []) 
286 

50632
12c097ff3241
slightly more elegant naming convention (to keep lowlevel and highlevel APIs separated)
blanchet
parents:
50631
diff
changeset

287 
end; 
12c097ff3241
slightly more elegant naming convention (to keep lowlevel and highlevel APIs separated)
blanchet
parents:
50631
diff
changeset

288 

50311  289 

290 
(*** Middlelevel communication with MaSh ***) 

291 

50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset

292 
datatype proof_kind = 
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset

293 
Isar_Proof  Automatic_Proof  Isar_Proof_wegen_Prover_Flop 
50311  294 

295 
fun str_of_proof_kind Isar_Proof = "i" 

50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset

296 
 str_of_proof_kind Automatic_Proof = "a" 
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset

297 
 str_of_proof_kind Isar_Proof_wegen_Prover_Flop = "x" 
50311  298 

299 
fun proof_kind_of_str "i" = Isar_Proof 

50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset

300 
 proof_kind_of_str "a" = Automatic_Proof 
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset

301 
 proof_kind_of_str "x" = Isar_Proof_wegen_Prover_Flop 
50311  302 

303 
(* FIXME: Here a "Graph.update_node" function would be useful *) 

50610  304 
fun update_access_graph_node (name, kind) = 
50311  305 
Graph.default_node (name, Isar_Proof) 
306 
#> kind <> Isar_Proof ? Graph.map_node name (K kind) 

307 

308 
fun try_graph ctxt when def f = 

309 
f () 

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

311 
(trace_msg ctxt (fn () => 

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

313 
 Graph.DUP name => 

314 
(trace_msg ctxt (fn () => 

315 
"Duplicate fact " ^ quote name ^ " when " ^ when); def) 

316 
 Graph.UNDEF name => 

317 
(trace_msg ctxt (fn () => 

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

319 
 exn => 

320 
if Exn.is_interrupt exn then 

321 
reraise exn 

322 
else 

323 
(trace_msg ctxt (fn () => 

324 
"Internal error when " ^ when ^ ":\n" ^ 

325 
ML_Compiler.exn_message exn); def) 

326 

327 
fun graph_info G = 

328 
string_of_int (length (Graph.keys G)) ^ " node(s), " ^ 

329 
string_of_int (fold (Integer.add o length o snd) (Graph.dest G) 0) ^ 

330 
" edge(s), " ^ 

331 
string_of_int (length (Graph.minimals G)) ^ " minimal, " ^ 

332 
string_of_int (length (Graph.maximals G)) ^ " maximal" 

333 

53095  334 
type mash_state = 
335 
{access_G : unit Graph.T, 

336 
num_known_facts : int, 

337 
dirty : string list option} 

50311  338 

53095  339 
val empty_state = {access_G = Graph.empty, num_known_facts = 0, dirty = SOME []} 
50311  340 

341 
local 

342 

53095  343 
val version = "*** MaSh version 20130820 ***" 
50357
187ae76a1757
more robustness in the face of MaSh format changes  don't overwrite new versions with old versions
blanchet
parents:
50356
diff
changeset

344 

53095  345 
exception FILE_VERSION_TOO_NEW of unit 
50311  346 

347 
fun extract_node line = 

348 
case space_explode ":" line of 

349 
[head, parents] => 

350 
(case space_explode " " head of 

351 
[kind, name] => 

50826  352 
SOME (unencode_str name, unencode_strs parents, 
50311  353 
try proof_kind_of_str kind > the_default Isar_Proof) 
354 
 _ => NONE) 

355 
 _ => NONE 

356 

357 
fun load _ (state as (true, _)) = state 

358 
 load ctxt _ = 

359 
let val path = mash_state_file () in 

360 
(true, 

361 
case try File.read_lines path of 

362 
SOME (version' :: node_lines) => 

363 
let 

364 
fun add_edge_to name parent = 

365 
Graph.default_node (parent, Isar_Proof) 

366 
#> Graph.add_edge (parent, name) 

367 
fun add_node line = 

368 
case extract_node line of 

369 
NONE => I (* shouldn't happen *) 

370 
 SOME (name, parents, kind) => 

50610  371 
update_access_graph_node (name, kind) 
50311  372 
#> fold (add_edge_to name) parents 
53095  373 
val (access_G, num_known_facts) = 
50357
187ae76a1757
more robustness in the face of MaSh format changes  don't overwrite new versions with old versions
blanchet
parents:
50356
diff
changeset

374 
case string_ord (version', version) of 
187ae76a1757
more robustness in the face of MaSh format changes  don't overwrite new versions with old versions
blanchet
parents:
50356
diff
changeset

375 
EQUAL => 
53095  376 
(try_graph ctxt "loading state" Graph.empty (fn () => 
377 
fold add_node node_lines Graph.empty), 

378 
length node_lines) 

50860  379 
 LESS => 
53095  380 
(* can't parse old file *) 
381 
(MaSh.unlearn ctxt; (Graph.empty, 0)) 

382 
 GREATER => raise FILE_VERSION_TOO_NEW () 

50311  383 
in 
384 
trace_msg ctxt (fn () => 

50610  385 
"Loaded fact graph (" ^ graph_info access_G ^ ")"); 
53095  386 
{access_G = access_G, num_known_facts = num_known_facts, 
387 
dirty = SOME []} 

50311  388 
end 
389 
 _ => empty_state) 

390 
end 

391 

392 
fun save _ (state as {dirty = SOME [], ...}) = state 

53095  393 
 save ctxt {access_G, num_known_facts, dirty} = 
50311  394 
let 
395 
fun str_of_entry (name, parents, kind) = 

50826  396 
str_of_proof_kind kind ^ " " ^ encode_str name ^ ": " ^ 
397 
encode_strs parents ^ "\n" 

50311  398 
fun append_entry (name, (kind, (parents, _))) = 
399 
cons (name, Graph.Keys.dest parents, kind) 

400 
val (banner, entries) = 

401 
case dirty of 

402 
SOME names => 

50610  403 
(NONE, fold (append_entry o Graph.get_entry access_G) names []) 
404 
 NONE => (SOME (version ^ "\n"), Graph.fold append_entry access_G []) 

50311  405 
in 
50335
b17b05c8d4a4
proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents:
50319
diff
changeset

406 
write_file banner (entries, str_of_entry) (mash_state_file ()); 
50311  407 
trace_msg ctxt (fn () => 
50610  408 
"Saved fact graph (" ^ graph_info access_G ^ 
50311  409 
(case dirty of 
410 
SOME dirty => 

411 
"; " ^ string_of_int (length dirty) ^ " dirty fact(s)" 

412 
 _ => "") ^ ")"); 

53095  413 
{access_G = access_G, num_known_facts = num_known_facts, dirty = SOME []} 
50311  414 
end 
415 

416 
val global_state = 

417 
Synchronized.var "Sledgehammer_MaSh.global_state" (false, empty_state) 

418 

419 
in 

420 

50570  421 
fun map_state ctxt f = 
50311  422 
Synchronized.change global_state (load ctxt ##> (f #> save ctxt)) 
53095  423 
handle FILE_VERSION_TOO_NEW () => () 
50311  424 

50570  425 
fun peek_state ctxt f = 
50357
187ae76a1757
more robustness in the face of MaSh format changes  don't overwrite new versions with old versions
blanchet
parents:
50356
diff
changeset

426 
Synchronized.change_result global_state 
187ae76a1757
more robustness in the face of MaSh format changes  don't overwrite new versions with old versions
blanchet
parents:
50356
diff
changeset

427 
(perhaps (try (load ctxt)) #> `snd #>> f) 
50311  428 

50570  429 
fun clear_state ctxt = 
50311  430 
Synchronized.change global_state (fn _ => 
50632
12c097ff3241
slightly more elegant naming convention (to keep lowlevel and highlevel APIs separated)
blanchet
parents:
50631
diff
changeset

431 
(MaSh.unlearn ctxt; (* also removes the state file *) 
50311  432 
(true, empty_state))) 
433 

434 
end 

435 

50570  436 
val mash_unlearn = clear_state 
437 

50311  438 

439 
(*** Isabelle helpers ***) 

440 

50722  441 
val local_prefix = "local" ^ Long_Name.separator 
48378  442 

50722  443 
fun elided_backquote_thm threshold th = 
444 
elide_string threshold 

445 
(backquote_thm (Proof_Context.init_global (Thm.theory_of_thm th)) th) 

48378  446 

51181
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset

447 
val thy_name_of_thm = Context.theory_name o Thm.theory_of_thm 
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset

448 

50624
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset

449 
fun nickname_of_thm th = 
48394
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset

450 
if Thm.has_name_hint th then 
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset

451 
let val hint = Thm.get_name_hint th in 
50722  452 
(* There must be a better way to detect local facts. *) 
48394
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset

453 
case try (unprefix local_prefix) hint of 
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset

454 
SOME suf => 
51181
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset

455 
thy_name_of_thm th ^ Long_Name.separator ^ suf ^ 
50732  456 
Long_Name.separator ^ elided_backquote_thm 50 th 
48394
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset

457 
 NONE => hint 
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset

458 
end 
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset

459 
else 
50722  460 
elided_backquote_thm 200 th 
48378  461 

51134  462 
fun find_suggested_facts ctxt facts = 
48330  463 
let 
51134  464 
fun add (fact as (_, th)) = Symtab.default (nickname_of_thm th, fact) 
465 
val tab = fold add facts Symtab.empty 

466 
fun lookup nick = 

467 
Symtab.lookup tab nick 

468 
> tap (fn NONE => trace_msg ctxt (fn () => "Cannot find " ^ quote nick) 

469 
 _ => ()) 

470 
in map_filter lookup end 

48311  471 

50383
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

472 
fun scaled_avg [] = 0 
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

473 
 scaled_avg xs = 
48407  474 
Real.ceil (100000000.0 * fold (curry (op +)) xs 0.0) div length xs 
48328
ca0b7d19dd62
attempt at meshing according to more meaningful factors
blanchet
parents:
48327
diff
changeset

475 

50383
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

476 
fun avg [] = 0.0 
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

477 
 avg xs = fold (curry (op +)) xs 0.0 / Real.fromInt (length xs) 
48313
0faafdffa662
mesh facts by taking into consideration whether a fact is known to MeSh
blanchet
parents:
48312
diff
changeset

478 

50383
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

479 
fun normalize_scores _ [] = [] 
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

480 
 normalize_scores max_facts xs = 
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

481 
let val avg = avg (map snd (take max_facts xs)) in 
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

482 
map (apsnd (curry Real.* (1.0 / avg))) xs 
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

483 
end 
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

484 

50814  485 
fun mesh_facts _ max_facts [(_, (sels, unks))] = 
48406  486 
map fst (take max_facts sels) @ take (max_facts  length sels) unks 
50861
fa4253914e98
honor unknown chained in MaSh and a few other tweaks
blanchet
parents:
50860
diff
changeset

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

488 
let 
51029  489 
val mess = mess > map (apsnd (apfst (normalize_scores max_facts))) 
490 
fun score_in fact (global_weight, (sels, unks)) = 

50383
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

491 
let 
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

492 
fun score_at j = 
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

493 
case try (nth sels) j of 
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

494 
SOME (_, score) => SOME (global_weight * score) 
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

495 
 NONE => NONE 
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

496 
in 
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

497 
case find_index (curry fact_eq fact o fst) sels of 
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

498 
~1 => (case find_index (curry fact_eq fact) unks of 
50861
fa4253914e98
honor unknown chained in MaSh and a few other tweaks
blanchet
parents:
50860
diff
changeset

499 
~1 => SOME 0.0 
50383
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

500 
 _ => NONE) 
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

501 
 rank => score_at rank 
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

502 
end 
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

503 
fun weight_of fact = mess > map_filter (score_in fact) > scaled_avg 
48406  504 
val facts = 
51029  505 
fold (union fact_eq o map fst o take max_facts o fst o snd) mess [] 
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

506 
in 
48406  507 
facts > map (`weight_of) > sort (int_ord o swap o pairself fst) 
48328
ca0b7d19dd62
attempt at meshing according to more meaningful factors
blanchet
parents:
48327
diff
changeset

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

509 
end 
48312  510 

50874
2eae85887282
adjust weights  sorts are prolific, so tone them down even more
blanchet
parents:
50869
diff
changeset

511 
fun thy_feature_of s = ("y" ^ s, 8.0 (* FUDGE *)) 
2eae85887282
adjust weights  sorts are prolific, so tone them down even more
blanchet
parents:
50869
diff
changeset

512 
fun const_feature_of s = ("c" ^ s, 32.0 (* FUDGE *)) 
2eae85887282
adjust weights  sorts are prolific, so tone them down even more
blanchet
parents:
50869
diff
changeset

513 
fun free_feature_of s = ("f" ^ s, 40.0 (* FUDGE *)) 
2eae85887282
adjust weights  sorts are prolific, so tone them down even more
blanchet
parents:
50869
diff
changeset

514 
fun type_feature_of s = ("t" ^ s, 4.0 (* FUDGE *)) 
50584
4fff0898cc0e
tuned weights  keep same relative values, but use 1.0 as the least weight
blanchet
parents:
50583
diff
changeset

515 
fun class_feature_of s = ("s" ^ s, 1.0 (* FUDGE *)) 
4fff0898cc0e
tuned weights  keep same relative values, but use 1.0 as the least weight
blanchet
parents:
50583
diff
changeset

516 
fun status_feature_of status = (string_of_status status, 2.0 (* FUDGE *)) 
4fff0898cc0e
tuned weights  keep same relative values, but use 1.0 as the least weight
blanchet
parents:
50583
diff
changeset

517 
val local_feature = ("local", 8.0 (* FUDGE *)) 
4fff0898cc0e
tuned weights  keep same relative values, but use 1.0 as the least weight
blanchet
parents:
50583
diff
changeset

518 
val lams_feature = ("lams", 2.0 (* FUDGE *)) 
4fff0898cc0e
tuned weights  keep same relative values, but use 1.0 as the least weight
blanchet
parents:
50583
diff
changeset

519 
val skos_feature = ("skos", 2.0 (* FUDGE *)) 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

520 

53127  521 
fun weighted_const_feature_of num_facts const_tab const_s s = 
522 
("c" ^ s, 

523 
if num_facts = 0 then 

524 
0.0 

525 
else 

526 
let val count = Symtab.lookup const_tab const_s > the_default 0 in 

527 
16.0 + (Real.fromInt num_facts / Real.fromInt count) 

528 
end) 

529 

51136  530 
(* The following "crude" functions should be progressively phased out, since 
531 
they create visibility edges that do not exist in Isabelle, resulting in 

532 
failed lookups later on. *) 

533 

51135  534 
fun crude_theory_ord p = 
50722  535 
if Theory.subthy p then 
536 
if Theory.eq_thy p then EQUAL else LESS 

48324  537 
else if Theory.subthy (swap p) then 
538 
GREATER 

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

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

541 
 order => order 

542 

51135  543 
fun crude_thm_ord p = 
544 
case crude_theory_ord (pairself theory_of_thm p) of 

50359
da395f0e7dea
tweaked order of theorems to avoid forward dependencies (MaSh)
blanchet
parents:
50357
diff
changeset

545 
EQUAL => 
50624
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset

546 
let val q = pairself nickname_of_thm p in 
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset

547 
(* Hack to put "xxx_def" before "xxxI" and "xxxE" *) 
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset

548 
case bool_ord (pairself (String.isSuffix "_def") (swap q)) of 
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset

549 
EQUAL => string_ord q 
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset

550 
 ord => ord 
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset

551 
end 
50359
da395f0e7dea
tweaked order of theorems to avoid forward dependencies (MaSh)
blanchet
parents:
50357
diff
changeset

552 
 ord => ord 
48324  553 

51136  554 
val thm_less_eq = Theory.subthy o pairself theory_of_thm 
555 
fun thm_less p = thm_less_eq p andalso not (thm_less_eq (swap p)) 

556 

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

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

558 

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

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

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

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

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

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

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

565 

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

566 
fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

567 

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

568 
fun run_prover_for_mash ctxt params prover facts goal = 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

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

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

571 
{state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1, 
51010  572 
factss = [("", facts)]} 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

573 
in 
51187
c344cf148e8f
avoid using "smt" for minimization  better use the prover itself, since then Sledgehammer gets to try metis again and gives the opportunity to output an Isar proof  and show Isar proof as fallback for SMT proofs
blanchet
parents:
51184
diff
changeset

574 
get_minimizing_prover ctxt MaSh (K (K ())) prover params (K (K (K ""))) 
c344cf148e8f
avoid using "smt" for minimization  better use the prover itself, since then Sledgehammer gets to try metis again and gives the opportunity to output an Isar proof  and show Isar proof as fallback for SMT proofs
blanchet
parents:
51184
diff
changeset

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

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

577 

48326  578 
val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}] 
579 

48398  580 
val logical_consts = 
581 
[@{const_name prop}, @{const_name Pure.conjunction}] @ atp_logical_consts 

582 

53086
15fe0ca088b3
MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents:
53085
diff
changeset

583 
val pat_tvar_prefix = "_" 
15fe0ca088b3
MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents:
53085
diff
changeset

584 
val pat_var_prefix = "_" 
15fe0ca088b3
MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents:
53085
diff
changeset

585 

53089  586 
(* try "Long_Name.base_name" for shorter names *) 
587 
fun massage_long_name s = s 

53083
019ecbb18e3f
generate patterns for variables as well in MaSh (cf. HOL(y)Hammer)
blanchet
parents:
53082
diff
changeset

588 

53086
15fe0ca088b3
MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents:
53085
diff
changeset

589 
val crude_str_of_sort = 
15fe0ca088b3
MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents:
53085
diff
changeset

590 
space_implode ":" o map massage_long_name o subtract (op =) @{sort type} 
15fe0ca088b3
MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents:
53085
diff
changeset

591 

15fe0ca088b3
MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents:
53085
diff
changeset

592 
fun crude_str_of_typ (Type (s, [])) = massage_long_name s 
53083
019ecbb18e3f
generate patterns for variables as well in MaSh (cf. HOL(y)Hammer)
blanchet
parents:
53082
diff
changeset

593 
 crude_str_of_typ (Type (s, Ts)) = 
53128  594 
massage_long_name s ^ implode (map crude_str_of_typ Ts) 
53083
019ecbb18e3f
generate patterns for variables as well in MaSh (cf. HOL(y)Hammer)
blanchet
parents:
53082
diff
changeset

595 
 crude_str_of_typ (TFree (_, S)) = crude_str_of_sort S 
019ecbb18e3f
generate patterns for variables as well in MaSh (cf. HOL(y)Hammer)
blanchet
parents:
53082
diff
changeset

596 
 crude_str_of_typ (TVar (_, S)) = crude_str_of_sort S 
019ecbb18e3f
generate patterns for variables as well in MaSh (cf. HOL(y)Hammer)
blanchet
parents:
53082
diff
changeset

597 

53128  598 
fun maybe_singleton_str _ "" = [] 
599 
 maybe_singleton_str pref s = [pref ^ s] 

600 

53082  601 
val max_pat_breadth = 10 
50585  602 

53127  603 
fun term_features_of ctxt prover thy_name num_facts const_tab term_max_depth 
604 
type_max_depth ts = 

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

605 
let 
50392
190053ee24ed
expand type classes into their ancestors for MaSh
blanchet
parents:
50391
diff
changeset

606 
val thy = Proof_Context.theory_of ctxt 
53082  607 

608 
val pass_args = map_product (fn p => fn "" => p  q => p ^ "(" ^ q ^ ")") 

50857
80768e28c9ee
better handlig of builtins  at the toplevel, not in subterms
blanchet
parents:
50841
diff
changeset

609 
fun is_built_in (x as (s, _)) args = 
80768e28c9ee
better handlig of builtins  at the toplevel, not in subterms
blanchet
parents:
50841
diff
changeset

610 
if member (op =) logical_consts s then (true, args) 
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51990
diff
changeset

611 
else is_built_in_const_of_prover ctxt prover x args 
53082  612 

50393  613 
val fixes = map snd (Variable.dest_fixes ctxt) 
50392
190053ee24ed
expand type classes into their ancestors for MaSh
blanchet
parents:
50391
diff
changeset

614 
val classes = Sign.classes_of thy 
53082  615 

48304  616 
fun add_classes @{sort type} = I 
50392
190053ee24ed
expand type classes into their ancestors for MaSh
blanchet
parents:
50391
diff
changeset

617 
 add_classes S = 
190053ee24ed
expand type classes into their ancestors for MaSh
blanchet
parents:
50391
diff
changeset

618 
fold (`(Sorts.super_classes classes) 
190053ee24ed
expand type classes into their ancestors for MaSh
blanchet
parents:
50391
diff
changeset

619 
#> swap #> op :: 
53086
15fe0ca088b3
MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents:
53085
diff
changeset

620 
#> subtract (op =) @{sort type} #> map massage_long_name 
50392
190053ee24ed
expand type classes into their ancestors for MaSh
blanchet
parents:
50391
diff
changeset

621 
#> map class_feature_of 
190053ee24ed
expand type classes into their ancestors for MaSh
blanchet
parents:
50391
diff
changeset

622 
#> union (op = o pairself fst)) S 
53082  623 

624 
fun pattify_type 0 _ = [] 

625 
 pattify_type _ (Type (s, [])) = 

53086
15fe0ca088b3
MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents:
53085
diff
changeset

626 
if member (op =) bad_types s then [] else [massage_long_name s] 
53082  627 
 pattify_type depth (Type (s, U :: Ts)) = 
628 
let 

629 
val T = Type (s, Ts) 

630 
val ps = take max_pat_breadth (pattify_type depth T) 

631 
val qs = take max_pat_breadth ("" :: pattify_type (depth  1) U) 

632 
in pass_args ps qs end 

53128  633 
 pattify_type _ (TFree (_, S)) = 
634 
maybe_singleton_str pat_tvar_prefix (crude_str_of_sort S) 

635 
 pattify_type _ (TVar (_, S)) = 

636 
maybe_singleton_str pat_tvar_prefix (crude_str_of_sort S) 

53082  637 
fun add_type_pat depth T = 
53083
019ecbb18e3f
generate patterns for variables as well in MaSh (cf. HOL(y)Hammer)
blanchet
parents:
53082
diff
changeset

638 
union (op = o pairself fst) (map type_feature_of (pattify_type depth T)) 
53082  639 
fun add_type_pats 0 _ = I 
640 
 add_type_pats depth t = 

641 
add_type_pat depth t #> add_type_pats (depth  1) t 

53083
019ecbb18e3f
generate patterns for variables as well in MaSh (cf. HOL(y)Hammer)
blanchet
parents:
53082
diff
changeset

642 
fun add_type T = 
019ecbb18e3f
generate patterns for variables as well in MaSh (cf. HOL(y)Hammer)
blanchet
parents:
53082
diff
changeset

643 
add_type_pats type_max_depth T 
019ecbb18e3f
generate patterns for variables as well in MaSh (cf. HOL(y)Hammer)
blanchet
parents:
53082
diff
changeset

644 
#> fold_atyps_sorts (fn (_, S) => add_classes S) T 
53084  645 
fun add_subtypes (T as Type (_, Ts)) = add_type T #> fold add_subtypes Ts 
646 
 add_subtypes T = add_type T 

53082  647 

53085  648 
fun pattify_term _ _ 0 _ = [] 
649 
 pattify_term _ args _ (Const (x as (s, _))) = 

53086
15fe0ca088b3
MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents:
53085
diff
changeset

650 
if fst (is_built_in x args) then [] else [massage_long_name s] 
53085  651 
 pattify_term _ _ _ (Free (s, T)) = 
53128  652 
maybe_singleton_str pat_var_prefix (crude_str_of_typ T) 
53090
1426c97311f2
treat frees as both consts and vars, for more hits
blanchet
parents:
53089
diff
changeset

653 
> (if member (op =) fixes s then 
1426c97311f2
treat frees as both consts and vars, for more hits
blanchet
parents:
53089
diff
changeset

654 
cons (massage_long_name (thy_name ^ Long_Name.separator ^ s)) 
1426c97311f2
treat frees as both consts and vars, for more hits
blanchet
parents:
53089
diff
changeset

655 
else 
1426c97311f2
treat frees as both consts and vars, for more hits
blanchet
parents:
53089
diff
changeset

656 
I) 
53128  657 
 pattify_term _ _ _ (Var (_, T)) = 
658 
maybe_singleton_str pat_var_prefix (crude_str_of_typ T) 

53085  659 
 pattify_term Ts _ _ (Bound j) = 
53128  660 
maybe_singleton_str pat_var_prefix (crude_str_of_typ (nth Ts j)) 
53085  661 
 pattify_term Ts args depth (t $ u) = 
50339
d8dae91f3107
MaSh improvements: deeper patterns + more respect for chained facts
blanchet
parents:
50338
diff
changeset

662 
let 
53085  663 
val ps = take max_pat_breadth (pattify_term Ts (u :: args) depth t) 
664 
val qs = take max_pat_breadth ("" :: pattify_term Ts [] (depth  1) u) 

53082  665 
in pass_args ps qs end 
53085  666 
 pattify_term _ _ _ _ = [] 
667 
fun add_term_pat Ts feature_of depth = 

668 
union (op = o pairself fst) o map feature_of o pattify_term Ts [] depth 

669 
fun add_term_pats _ _ 0 _ = I 

670 
 add_term_pats Ts feature_of depth t = 

671 
add_term_pat Ts feature_of depth t 

672 
#> add_term_pats Ts feature_of (depth  1) t 

673 
fun add_term Ts feature_of = add_term_pats Ts feature_of term_max_depth 

674 
fun add_subterms Ts t = 

50857
80768e28c9ee
better handlig of builtins  at the toplevel, not in subterms
blanchet
parents:
50841
diff
changeset

675 
case strip_comb t of 
53127  676 
(Const (x as (s, T)), args) => 
50857
80768e28c9ee
better handlig of builtins  at the toplevel, not in subterms
blanchet
parents:
50841
diff
changeset

677 
let val (built_in, args) = is_built_in x args in 
53127  678 
(not built_in 
679 
? add_term Ts (weighted_const_feature_of num_facts const_tab s) t) 

53084  680 
#> add_subtypes T 
53085  681 
#> fold (add_subterms Ts) args 
50857
80768e28c9ee
better handlig of builtins  at the toplevel, not in subterms
blanchet
parents:
50841
diff
changeset

682 
end 
80768e28c9ee
better handlig of builtins  at the toplevel, not in subterms
blanchet
parents:
50841
diff
changeset

683 
 (head, args) => 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

684 
(case head of 
53085  685 
Free (_, T) => add_term Ts free_feature_of t #> add_subtypes T 
53084  686 
 Var (_, T) => add_subtypes T 
53085  687 
 Abs (_, T, body) => add_subtypes T #> add_subterms (T :: Ts) body 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

688 
 _ => I) 
53085  689 
#> fold (add_subterms Ts) args 
690 
in [] > fold (add_subterms []) ts end 

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

691 

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

692 
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

693 

53085  694 
val term_max_depth = 2 
695 
val type_max_depth = 2 

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

696 

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

697 
(* TODO: Generate type classes for types? *) 
53127  698 
fun features_of ctxt prover thy num_facts const_tab (scope, status) ts = 
50393  699 
let val thy_name = Context.theory_name thy in 
700 
thy_feature_of thy_name :: 

53127  701 
term_features_of ctxt prover thy_name num_facts const_tab term_max_depth 
702 
type_max_depth ts 

50393  703 
> status <> General ? cons (status_feature_of status) 
704 
> scope <> Global ? cons local_feature 

705 
> exists (not o is_lambda_free) ts ? cons lams_feature 

706 
> exists (exists_Const is_exists) ts ? cons skos_feature 

707 
end 

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

708 

50434
960a3429615c
more MaSh tweaking  in particular, export the same facts in "MaSh_Export" as are later tried in "MaSh_Eval"
blanchet
parents:
50412
diff
changeset

709 
(* Too many dependencies is a sign that a decision procedure is at work. There 
960a3429615c
more MaSh tweaking  in particular, export the same facts in "MaSh_Export" as are later tried in "MaSh_Eval"
blanchet
parents:
50412
diff
changeset

710 
isn't much to learn from such proofs. *) 
960a3429615c
more MaSh tweaking  in particular, export the same facts in "MaSh_Export" as are later tried in "MaSh_Eval"
blanchet
parents:
50412
diff
changeset

711 
val max_dependencies = 20 
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset

712 

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

714 

48438
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset

715 
(* "type_definition_xxx" facts are characterized by their use of "CollectI". *) 
50755  716 
val typedef_dep = nickname_of_thm @{thm CollectI} 
717 
(* Mysterious parts of the class machinery create lots of proofs that refer 

52071  718 
exclusively to "someI_ex" (and to some internal constructions). *) 
50755  719 
val class_some_dep = nickname_of_thm @{thm someI_ex} 
48438
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset

720 

50828  721 
val fundef_ths = 
722 
@{thms fundef_ex1_existence fundef_ex1_uniqueness fundef_ex1_iff 

723 
fundef_default_value} 

724 
> map nickname_of_thm 

725 

48438
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset

726 
(* "Rep_xxx_inject", "Abs_xxx_inverse", etc., are derived using these facts. *) 
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset

727 
val typedef_ths = 
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset

728 
@{thms type_definition.Abs_inverse type_definition.Rep_inverse 
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset

729 
type_definition.Rep type_definition.Rep_inject 
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset

730 
type_definition.Abs_inject type_definition.Rep_cases 
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset

731 
type_definition.Abs_cases type_definition.Rep_induct 
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset

732 
type_definition.Abs_induct type_definition.Rep_range 
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset

733 
type_definition.Abs_image} 
50624
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset

734 
> map nickname_of_thm 
48438
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset

735 

48441  736 
fun is_size_def [dep] th = 
737 
(case first_field ".recs" dep of 

738 
SOME (pref, _) => 

50624
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset

739 
(case first_field ".size" (nickname_of_thm th) of 
48441  740 
SOME (pref', _) => pref = pref' 
741 
 NONE => false) 

742 
 NONE => false) 

743 
 is_size_def _ _ = false 

744 

53095  745 
fun no_dependencies_for_status status = 
746 
status = Non_Rec_Def orelse status = Rec_Def 

747 

51177  748 
fun trim_dependencies deps = 
50755  749 
if length deps > max_dependencies then NONE else SOME deps 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

750 

50755  751 
fun isar_dependencies_of name_tabs th = 
51020  752 
let val deps = thms_in_proof (SOME name_tabs) th in 
50828  753 
if deps = [typedef_dep] orelse 
754 
deps = [class_some_dep] orelse 

755 
exists (member (op =) fundef_ths) deps orelse 

756 
exists (member (op =) typedef_ths) deps orelse 

757 
is_size_def deps th then 

50755  758 
[] 
759 
else 

760 
deps 

761 
end 

48404  762 

50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset

763 
fun prover_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover 
50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50732
diff
changeset

764 
auto_level facts name_tabs th = 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50732
diff
changeset

765 
case isar_dependencies_of name_tabs th of 
50754
74a6adcb96ac
also generate queries for goals with too many Isar dependencies
blanchet
parents:
50751
diff
changeset

766 
[] => (false, []) 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

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

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

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

770 
val goal = goal_of_thm thy th 
52196
2281f33e8da6
redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof  have "!!a::int. Q a" sledgehammer [e])
blanchet
parents:
52125
diff
changeset

771 
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt 
51136  772 
val facts = facts > filter (fn (_, th') => thm_less (th', th)) 
51004
5f2788c38127
distinguish raw and nonraw facts, using raw for 10 000s of facts and nonraw after selection of some hundreds
blanchet
parents:
51003
diff
changeset

773 
fun nickify ((_, stature), th) = ((nickname_of_thm th, stature), th) 
50624
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset

774 
fun is_dep dep (_, th) = nickname_of_thm th = dep 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

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

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

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

778 
else case find_first (is_dep dep) facts of 
51004
5f2788c38127
distinguish raw and nonraw facts, using raw for 10 000s of facts and nonraw after selection of some hundreds
blanchet
parents:
51003
diff
changeset

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

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

781 
val facts = 
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset

782 
facts 
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset

783 
> mepo_suggested_facts ctxt params prover 
51133  784 
(max_facts > the_default prover_default_max_facts) NONE hyp_ts 
785 
concl_t 

50754
74a6adcb96ac
also generate queries for goals with too many Isar dependencies
blanchet
parents:
50751
diff
changeset

786 
> fold (add_isar_dep facts) isar_deps 
50624
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset

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

788 
in 
48404  789 
if verbose andalso auto_level = 0 then 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

790 
let val num_facts = length facts in 
50624
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset

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

792 
" with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

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

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

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

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

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

798 
case run_prover_for_mash ctxt params prover facts goal of 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

799 
{outcome = NONE, used_facts, ...} => 
48404  800 
(if verbose andalso auto_level = 0 then 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

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

802 
"Found proof with " ^ string_of_int num_facts ^ " fact" ^ 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

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

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

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

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

807 
(); 
50754
74a6adcb96ac
also generate queries for goals with too many Isar dependencies
blanchet
parents:
50751
diff
changeset

808 
(true, map fst used_facts)) 
48665  809 
 _ => (false, isar_deps) 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

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

811 

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

812 

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

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

814 

53095  815 
fun attach_crude_parents_to_facts _ [] = [] 
816 
 attach_crude_parents_to_facts parents ((fact as (_, th)) :: facts) = 

817 
(parents, fact) :: attach_crude_parents_to_facts [nickname_of_thm th] facts 

48383  818 

51182
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset

819 
(* In the following functions, chunks are risers w.r.t. "thm_less_eq". *) 
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset

820 

51181
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset

821 
fun chunks_and_parents_for chunks th = 
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset

822 
let 
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset

823 
fun insert_parent new parents = 
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset

824 
let val parents = parents > filter_out (fn p => thm_less_eq (p, new)) in 
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset

825 
parents > forall (fn p => not (thm_less_eq (new, p))) parents 
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset

826 
? cons new 
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset

827 
end 
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset

828 
fun rechunk seen (rest as th' :: ths) = 
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset

829 
if thm_less_eq (th', th) then (rev seen, rest) 
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset

830 
else rechunk (th' :: seen) ths 
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset

831 
fun do_chunk [] accum = accum 
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset

832 
 do_chunk (chunk as hd_chunk :: _) (chunks, parents) = 
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset

833 
if thm_less_eq (hd_chunk, th) then 
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset

834 
(chunk :: chunks, insert_parent hd_chunk parents) 
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset

835 
else if thm_less_eq (List.last chunk, th) then 
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset

836 
let val (front, back as hd_back :: _) = rechunk [] chunk in 
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset

837 
(front :: back :: chunks, insert_parent hd_back parents) 
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset

838 
end 
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset

839 
else 
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset

840 
(chunk :: chunks, parents) 
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset

841 
in 
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset

842 
fold_rev do_chunk chunks ([], []) 
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset

843 
>> cons [] 
51182
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset

844 
> map nickname_of_thm 
51181
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset

845 
end 
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset

846 

51182
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset

847 
fun attach_parents_to_facts _ [] = [] 
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset

848 
 attach_parents_to_facts old_facts (facts as (_, th) :: _) = 
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset

849 
let 
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset

850 
fun do_facts _ [] = [] 
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset

851 
 do_facts (_, parents) [fact] = [(parents, fact)] 
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset

852 
 do_facts (chunks, parents) 
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset

853 
((fact as (_, th)) :: (facts as (_, th') :: _)) = 
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset

854 
let 
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset

855 
val chunks = app_hd (cons th) chunks 
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset

856 
val chunks_and_parents' = 
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset

857 
if thm_less_eq (th, th') andalso 
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset

858 
thy_name_of_thm th = thy_name_of_thm th' then 
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset

859 
(chunks, [nickname_of_thm th]) 
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset

860 
else 
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset

861 
chunks_and_parents_for chunks th' 
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset

862 
in (parents, fact) :: do_facts chunks_and_parents' facts end 
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset

863 
in 
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset

864 
old_facts @ facts 
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset

865 
> do_facts (chunks_and_parents_for [[]] th) 
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset

866 
> drop (length old_facts) 
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset

867 
end 
51177  868 

53095  869 
fun maximal_wrt_graph G keys = 
870 
let 

871 
val tab = Symtab.empty > fold (fn name => Symtab.default (name, ())) keys 

872 
fun insert_new seen name = 

873 
not (Symtab.defined seen name) ? insert (op =) name 

874 
fun num_keys keys = Graph.Keys.fold (K (Integer.add 1)) keys 0 

875 
fun find_maxes _ (maxs, []) = map snd maxs 

876 
 find_maxes seen (maxs, new :: news) = 

877 
find_maxes 

878 
(seen > num_keys (Graph.imm_succs G new) > 1 

879 
? Symtab.default (new, ())) 

880 
(if Symtab.defined tab new then 

881 
let 

882 
val newp = Graph.all_preds G [new] 

883 
fun is_ancestor x yp = member (op =) yp x 

884 
val maxs = 

885 
maxs > filter (fn (_, max) => not (is_ancestor max newp)) 

886 
in 

887 
if exists (is_ancestor new o fst) maxs then 

888 
(maxs, news) 

889 
else 

890 
((newp, new) 

891 
:: filter_out (fn (_, max) => is_ancestor max newp) maxs, 

892 
news) 

893 
end 

894 
else 

895 
(maxs, Graph.Keys.fold (insert_new seen) 

896 
(Graph.imm_preds G new) news)) 

897 
in find_maxes Symtab.empty ([], Graph.maximals G) end 

898 

899 
fun maximal_wrt_access_graph access_G = 

900 
map (nickname_of_thm o snd) 

901 
#> maximal_wrt_graph access_G 

902 

903 
fun is_fact_in_graph access_G = can (Graph.get_node access_G) o nickname_of_thm 

904 

905 
(* FUDGE *) 

906 
fun weight_of_mepo_fact rank = 

907 
Math.pow (0.62, log2 (Real.fromInt (rank + 1))) 

908 

909 
fun weight_mepo_facts facts = 

910 
facts ~~ map weight_of_mepo_fact (0 upto length facts  1) 

911 

912 
val weight_raw_mash_facts = weight_mepo_facts 

913 
val weight_mash_facts = weight_raw_mash_facts 

914 

915 
(* FUDGE *) 

916 
fun weight_of_proximity_fact rank = 

917 
Math.pow (1.3, 15.5  0.2 * Real.fromInt rank) + 15.0 

918 

919 
fun weight_proximity_facts facts = 

920 
facts ~~ map weight_of_proximity_fact (0 upto length facts  1) 

921 

922 
val max_proximity_facts = 100 

923 

924 
fun find_mash_suggestions _ _ [] _ _ raw_unknown = ([], raw_unknown) 

925 
 find_mash_suggestions ctxt max_facts suggs facts chained raw_unknown = 

926 
let 

927 
val raw_mash = find_suggested_facts ctxt facts suggs 

928 
val unknown_chained = 

929 
inter (Thm.eq_thm_prop o pairself snd) chained raw_unknown 

930 
val proximity = 

931 
facts > sort (crude_thm_ord o pairself snd o swap) 

932 
> take max_proximity_facts 

933 
val mess = 

934 
[(0.90 (* FUDGE *), (map (rpair 1.0) unknown_chained, [])), 

935 
(0.08 (* FUDGE *), (weight_raw_mash_facts raw_mash, raw_unknown)), 

936 
(0.02 (* FUDGE *), (weight_proximity_facts proximity, []))] 

937 
val unknown = 

938 
raw_unknown 

939 
> fold (subtract (Thm.eq_thm_prop o pairself snd)) 

940 
[unknown_chained, proximity] 

941 
in (mesh_facts (Thm.eq_thm_prop o pairself snd) max_facts mess, unknown) end 

942 

53127  943 
fun add_const_counts t = 
944 
fold (fn s => Symtab.map_default (s, ~1) (Integer.add 1)) 

945 
(Term.add_const_names t []) 

53095  946 

53127  947 
fun mash_suggested_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts 
948 
concl_t facts = 

53095  949 
let 
950 
val thy = Proof_Context.theory_of ctxt 

951 
val chained = facts > filter (fn ((_, (scope, _)), _) => scope = Chained) 

53127  952 
val const_tab = fold (add_const_counts o prop_of o snd) facts Symtab.empty 
53095  953 
val (access_G, suggs) = 
53127  954 
peek_state ctxt (fn {access_G, ...} => 
53095  955 
if Graph.is_empty access_G then 
956 
(access_G, []) 

957 
else 

958 
let 

959 
val parents = maximal_wrt_access_graph access_G facts 

960 
val feats = 

53127  961 
features_of ctxt prover thy (length facts) const_tab 
962 
(Local, General) (concl_t :: hyp_ts) 

53095  963 
val hints = 
964 
chained > filter (is_fact_in_graph access_G o snd) 

965 
> map (nickname_of_thm o snd) 

966 
in 

967 
(access_G, MaSh.query ctxt overlord max_facts 

53118
3f290031bd9e
take out dangerous feature, now that all updates are permanent
blanchet
parents:
53117
diff
changeset

968 
([], hints, parents, feats)) 
53095  969 
end) 
970 
val unknown = facts > filter_out (is_fact_in_graph access_G o snd) 

971 
in 

972 
find_mash_suggestions ctxt max_facts suggs facts chained unknown 

973 
> pairself (map fact_of_raw_fact) 

974 
end 

975 

976 
fun learn_wrt_access_graph ctxt (name, parents, feats, deps) (learns, graph) = 

977 
let 

978 
fun maybe_learn_from from (accum as (parents, graph)) = 

979 
try_graph ctxt "updating graph" accum (fn () => 

980 
(from :: parents, Graph.add_edge_acyclic (from, name) graph)) 

981 
val graph = graph > Graph.default_node (name, Isar_Proof) 

982 
val (parents, graph) = ([], graph) > fold maybe_learn_from parents 

983 
val (deps, _) = ([], graph) > fold maybe_learn_from deps 

984 
in ((name, parents, feats, deps) :: learns, graph) end 

985 

986 
fun relearn_wrt_access_graph ctxt (name, deps) (relearns, graph) = 

987 
let 

988 
fun maybe_relearn_from from (accum as (parents, graph)) = 

989 
try_graph ctxt "updating graph" accum (fn () => 

990 
(from :: parents, Graph.add_edge_acyclic (from, name) graph)) 

991 
val graph = graph > update_access_graph_node (name, Automatic_Proof) 

992 
val (deps, _) = ([], graph) > fold maybe_relearn_from deps 

993 
in ((name, deps) :: relearns, graph) end 

994 

995 
fun flop_wrt_access_graph name = 

996 
update_access_graph_node (name, Isar_Proof_wegen_Prover_Flop) 

997 

998 
val learn_timeout_slack = 2.0 

999 

1000 
fun launch_thread timeout task = 

1001 
let 

1002 
val hard_timeout = time_mult learn_timeout_slack timeout 

1003 
val birth_time = Time.now () 

1004 
val death_time = Time.+ (birth_time, hard_timeout) 

1005 
val desc = ("Machine learner for Sledgehammer", "") 

1006 
in Async_Manager.thread MaShN birth_time death_time desc task end 

1007 

1008 
fun mash_learn_proof ctxt ({overlord, timeout, ...} : params) prover t facts 

1009 
used_ths = 

1010 
launch_thread (timeout > the_default one_day) (fn () => 

1011 
let 

1012 
val thy = Proof_Context.theory_of ctxt 

1013 
val name = freshish_name () 

53127  1014 
val feats = 
1015 
features_of ctxt prover thy 0 Symtab.empty (Local, General) [t] 

1016 
> map fst 

53095  1017 
in 
1018 
peek_state ctxt (fn {access_G, ...} => 

1019 
let 

1020 
val parents = maximal_wrt_access_graph access_G facts 

1021 
val deps = 

1022 
used_ths > filter (is_fact_in_graph access_G) 

1023 
> map nickname_of_thm 

1024 
in 

1025 
MaSh.learn ctxt overlord [(name, parents, feats, deps)] 

1026 
end); 

1027 
(true, "") 

1028 
end) 

1029 

52697
6fb98a20c349
explicit padding on command boundary for "auto" generated sendback  do not replace the corresponding goal command, but append to it;
wenzelm
parents:
52196
diff
changeset

1030 
fun sendback sub = 
6fb98a20c349
explicit padding on command boundary for "auto" generated sendback  do not replace the corresponding goal command, but append to it;
wenzelm
parents:
52196
diff
changeset

1031 
Active.sendback_markup [Markup.padding_command] (sledgehammerN ^ " " ^ sub) 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

1032 

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

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

1034 

50485
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50484
diff
changeset

1035 
(* The timeout is understood in a very relaxed fashion. *) 
48404  1036 
fun mash_learn_facts ctxt (params as {debug, verbose, overlord, ...}) prover 
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset

1037 
auto_level run_prover learn_timeout facts = 
48304  1038 
let 
48318  1039 
val timer = Timer.startRealTimer () 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

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

1041 
Time.+ (Timer.checkRealTimer timer, commit_timeout) 
50610  1042 
val {access_G, ...} = peek_state ctxt I 
53095  1043 
val is_in_access_G = is_fact_in_graph access_G o snd 
51177  1044 
val no_new_facts = forall is_in_access_G facts 
48308  1045 
in 
51177  1046 
if no_new_facts andalso not run_prover then 
48404  1047 
if auto_level < 2 then 
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset

1048 
"No new " ^ (if run_prover then "automatic" else "Isar") ^ 
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset

1049 
" proofs to learn." ^ 
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset

1050 
(if auto_level = 0 andalso not run_prover then 
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset

1051 
"\n\nHint: Try " ^ sendback learn_proverN ^ 
50751  1052 
" to learn from an automatic prover." 
48404  1053 
else 
1054 
"") 

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

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

1056 
"" 
48308  1057 
else 
48304  1058 
let 
50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50732
diff
changeset

1059 
val name_tabs = build_name_tables nickname_of_thm facts 
48439
67a6bcbd3587
removed MaSh junk arising from primrec definitions
blanchet
parents:
48438
diff
changeset

1060 
fun deps_of status th = 
53095  1061 
if no_dependencies_for_status status then 
48439
67a6bcbd3587
removed MaSh junk arising from primrec definitions
blanchet
parents:
48438
diff
changeset

1062 
SOME [] 
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset

1063 
else if run_prover then 
50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50732
diff
changeset

1064 
prover_dependencies_of ctxt params prover auto_level facts name_tabs 
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset

1065 
th 
50754
74a6adcb96ac
also generate queries for goals with too many Isar dependencies
blanchet
parents:
50751
diff
changeset

1066 
> (fn (false, _) => NONE 
51177  1067 
 (true, deps) => trim_dependencies deps) 
48404  1068 
else 
50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50732
diff
changeset

1069 
isar_dependencies_of name_tabs th 
51177  1070 
> trim_dependencies 
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

1071 
fun do_commit [] [] [] state = state 
53095  1072 
 do_commit learns relearns flops {access_G, num_known_facts, dirty} = 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

1073 
let 
50610  1074 
val was_empty = Graph.is_empty access_G 
50631  1075 
val (learns, access_G) = 
1076 
([], access_G) > fold (learn_wrt_access_graph ctxt) learns 

1077 
val (relearns, access_G) = 

1078 
([], access_G) > fold (relearn_wrt_access_graph ctxt) relearns 

50610  1079 
val access_G = access_G > fold flop_wrt_access_graph flops 
53095  1080 
val num_known_facts = num_known_facts + length learns 
48699  1081 
val dirty = 
50631  1082 
case (was_empty, dirty, relearns) of 
1083 
(false, SOME names, []) => SOME (map #1 learns @ names) 

48699  1084 
 _ => NONE 
48404  1085 
in 
50632
12c097ff3241
slightly more elegant naming convention (to keep lowlevel and highlevel APIs separated)
blanchet
parents:
50631
diff
changeset

1086 
MaSh.learn ctxt overlord (rev learns); 
12c097ff3241
slightly more elegant naming convention (to keep lowlevel and highlevel APIs separated)
blanchet
parents:
50631
diff
changeset

1087 
MaSh.relearn ctxt overlord relearns; 
53095  1088 
{access_G = access_G, num_known_facts = num_known_facts, 
1089 
dirty = dirty} 

48404  1090 
end 
50631  1091 
fun commit last learns relearns flops = 
48404  1092 
(if debug andalso auto_level = 0 then 
1093 
Output.urgent_message "Committing..." 

1094 
else 

1095 
(); 

50631  1096 
map_state ctxt (do_commit (rev learns) relearns flops); 
48404  1097 
if not last andalso auto_level = 0 then 
50631  1098 
let val num_proofs = length learns + length relearns in 
48404  1099 
"Learned " ^ string_of_int num_proofs ^ " " ^ 
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset

1100 
(if run_prover then "automatic" else "Isar") ^ " proof" ^ 
48404  1101 
plural_s num_proofs ^ " in the last " ^ 
52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

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

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

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

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

1106 
()) 
51177  1107 
fun learn_new_fact _ (accum as (_, (_, _, true))) = accum 
1108 
 learn_new_fact (parents, ((_, stature as (_, status)), th)) 

1109 
(learns, (n, next_commit, _)) = 

48318  1110 
let 
50624
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset

1111 
val name = nickname_of_thm th 
48332
271a4a6af734
optimize parent computation in MaSh + remove temporary files
blanchet
parents:
48330
diff
changeset

1112 
val feats = 
53127  1113 
features_of ctxt prover (theory_of_thm th) 0 Symtab.empty 
1114 
stature [prop_of th] 

53121
5f727525b1ac
only generate feature weights for queries  they're not used elsewhere
blanchet
parents:
53118
diff
changeset

1115 
> map fst 
48439
67a6bcbd3587
removed MaSh junk arising from primrec definitions
blanchet
parents:
48438
diff
changeset

1116 
val deps = deps_of status th > these 
48394
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset

1117 
val n = n > not (null deps) ? Integer.add 1 
50631  1118 
val learns = (name, parents, feats, deps) :: learns 
1119 
val (learns, next_commit) = 

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

1120 
if Time.> (Timer.checkRealTimer timer, next_commit) then 
50631  1121 
(commit false learns [] []; ([], next_commit_time ())) 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

1122 
else 
50631  1123 
(learns, next_commit) 
50557  1124 
val timed_out = 
1125 
case learn_timeout of 

1126 
SOME timeout => Time.> (Timer.checkRealTimer timer, timeout) 

1127 
 NONE => false 

51177  1128 
in (learns, (n, next_commit, timed_out)) end 
48404  1129 
val n = 
51177  1130 
if no_new_facts then 
48404  1131 
0 
1132 
else 

1133 
let 

51182
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset

1134 
val new_facts = 
51184
e2569dde59c8
reintroduced crucial sorting accidentally lost in 962190eab40d
blanchet
parents:
51183
diff
changeset

1135 
facts > sort (crude_thm_ord o pairself snd) 
e2569dde59c8
reintroduced crucial sorting accidentally lost in 962190eab40d
blanchet
parents:
51183
diff
changeset

1136 
> attach_parents_to_facts [] 
51177  1137 
> filter_out (is_in_access_G o snd) 
1138 
val (learns, (n, _, _)) = 

1139 
([], (0, next_commit_time (), false)) 

51182
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset

1140 
> fold learn_new_fact new_facts 
50631  1141 
in commit true learns [] []; n end 
48404  1142 
fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum 
48439
67a6bcbd3587
removed MaSh junk arising from primrec definitions
blanchet
parents:
48438
diff
changeset

1143 
 relearn_old_fact ((_, (_, status)), th) 
50631  1144 
((relearns, flops), (n, next_commit, _)) = 
48404  1145 
let 
50624
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset

1146 
val name = nickname_of_thm th 
50631  1147 
val (n, relearns, flops) = 
48439
67a6bcbd3587
removed MaSh junk arising from primrec definitions
blanchet
parents:
48438
diff
changeset

1148 
case deps_of status th of 
50631
b69079c14665
tuned ML function names
blanche&# 