author  blanchet 
Thu, 17 Oct 2013 20:20:53 +0200  
changeset 54140  564b8adb0952 
parent 54131  18b23d787062 
child 54141  f57f8e7a879f 
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 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

15 

48308  16 
val trace : bool Config.T 
51008  17 
val MePoN : string 
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

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

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

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

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

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

24 
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

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

26 
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

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

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

31 
val unencode_str : string > string 

32 
val unencode_strs : string > string list 

50356  33 
val encode_features : (string * real) list > string 
50965  34 
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

35 

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

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

37 
sig 
53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset

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

39 
val learn : 
53757
8d1a059ebcdb
reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents:
53756
diff
changeset

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

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

42 
val relearn : 
53757
8d1a059ebcdb
reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents:
53756
diff
changeset

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

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

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

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

50 

53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset

51 
val mash_unlearn : Proof.context > params > unit 
53819
e55d641d0a70
honor MaSh's zerooverhead policy  no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset

52 
val is_mash_enabled : unit > bool 
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 : 
54089
b13f6731f873
use same relevance filter for ATP and SMT solvers  attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected sideeffects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset

65 
Proof.context > theory > int > int Symtab.table > stature > term list > 
b13f6731f873
use same relevance filter for ATP and SMT solvers  attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected sideeffects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset

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

53140
a1235e90da5f
pour extra features from proximate facts into goal, in exporter
blanchet
parents:
53137
diff
changeset

76 
val num_extra_feature_facts : int 
53141
d27e99a6a679
take chained and proximate facts into consideration when computing MaSh features
blanchet
parents:
53140
diff
changeset

77 
val extra_feature_factor : real 
53140
a1235e90da5f
pour extra features from proximate facts into goal, in exporter
blanchet
parents:
53137
diff
changeset

78 
val weight_facts_smoothly : 'a list > ('a * real) list 
a1235e90da5f
pour extra features from proximate facts into goal, in exporter
blanchet
parents:
53137
diff
changeset

79 
val weight_facts_steeply : 'a list > ('a * real) list 
50412  80 
val find_mash_suggestions : 
51134  81 
Proof.context > int > string list > ('b * thm) list > ('b * thm) list 
82 
> ('b * thm) list > ('b * thm) list * ('b * thm) list 

53127  83 
val add_const_counts : term > int Symtab.table > int Symtab.table 
48406  84 
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

85 
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

86 
> raw_fact list > fact list * fact list 
48383  87 
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

88 
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

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

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

91 
Proof.context > params > fact_override > thm list > bool > unit 
53819
e55d641d0a70
honor MaSh's zerooverhead policy  no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset

92 

53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset

93 
val mash_can_suggest_facts : Proof.context > bool > bool 
50412  94 
val generous_max_facts : int > int 
50814  95 
val mepo_weight : real 
96 
val mash_weight : real 

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

97 
val relevant_facts : 
48292  98 
Proof.context > params > string > int > fact_override > term list 
51010  99 
> term > raw_fact list > (string * fact list) list 
53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset

100 
val kill_learners : Proof.context > params > unit 
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

101 
val running_learners : unit > unit 
48248  102 
end; 
103 

48381  104 
structure Sledgehammer_MaSh : SLEDGEHAMMER_MASH = 
48248  105 
struct 
48249  106 

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

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

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

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

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

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

114 

48308  115 
val trace = 
48380  116 
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

117 

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

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

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

123 

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

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

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

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

127 

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

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

129 

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

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

131 
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

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

133 
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

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

135 

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

137 
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

138 
val mash_state_dir = mash_model_dir 
50310  139 
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

140 

48330  141 

50311  142 
(*** Lowlevel communication with MaSh ***) 
143 

53117  144 
val save_models_arg = "saveModels" 
145 
val shutdown_server_arg = "shutdownServer" 

146 

50311  147 
fun wipe_out_file file = (try (File.rm o Path.explode) file; ()) 
148 

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

149 
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

150 
(case banner of SOME s => File.write path s  NONE => (); 
53094  151 
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

152 
handle IO.Io _ => () 
50311  153 

53152
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset

154 
fun run_mash_tool ctxt overlord extra_args background write_cmds read_suggs = 
50311  155 
let 
156 
val (temp_dir, serial) = 

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

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

53129  159 
val log_file = temp_dir ^ "/mash_log" ^ serial 
50311  160 
val err_file = temp_dir ^ "/mash_err" ^ serial 
161 
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

162 
val sugg_path = Path.explode sugg_file 
50311  163 
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

164 
val cmd_path = Path.explode cmd_file 
51001  165 
val model_dir = File.shell_path (mash_model_dir ()) 
50311  166 
val command = 
53556
347f743e8336
invoke Python with "no bytecode" option to avoid litering Isabelle source directory with ".pyc" files (which can be problematic for a number of reasons)
blanchet
parents:
53201
diff
changeset

167 
"cd \"$ISABELLE_SLEDGEHAMMER_MASH\"/src; \ 
53790
298774dbdde0
provide a way to override MaSh's port from configuration file
blanchet
parents:
53757
diff
changeset

168 
\PYTHONDONTWRITEBYTECODE=y ./mash.py\ 
298774dbdde0
provide a way to override MaSh's port from configuration file
blanchet
parents:
53757
diff
changeset

169 
\ quiet\ 
298774dbdde0
provide a way to override MaSh's port from configuration file
blanchet
parents:
53757
diff
changeset

170 
\ port=$MASH_PORT\ 
53556
347f743e8336
invoke Python with "no bytecode" option to avoid litering Isabelle source directory with ".pyc" files (which can be problematic for a number of reasons)
blanchet
parents:
53201
diff
changeset

171 
\ outputDir " ^ model_dir ^ 
347f743e8336
invoke Python with "no bytecode" option to avoid litering Isabelle source directory with ".pyc" files (which can be problematic for a number of reasons)
blanchet
parents:
53201
diff
changeset

172 
" modelFile=" ^ model_dir ^ "/model.pickle\ 
347f743e8336
invoke Python with "no bytecode" option to avoid litering Isabelle source directory with ".pyc" files (which can be problematic for a number of reasons)
blanchet
parents:
53201
diff
changeset

173 
\ dictsFile=" ^ model_dir ^ "/dict.pickle\ 
53790
298774dbdde0
provide a way to override MaSh's port from configuration file
blanchet
parents:
53757
diff
changeset

174 
\ log " ^ log_file ^ 
298774dbdde0
provide a way to override MaSh's port from configuration file
blanchet
parents:
53757
diff
changeset

175 
" inputFile " ^ cmd_file ^ 
298774dbdde0
provide a way to override MaSh's port from configuration file
blanchet
parents:
53757
diff
changeset

176 
" predictions " ^ sugg_file ^ 
53117  177 
(if extra_args = [] then "" else " " ^ space_implode " " extra_args) ^ 
53152
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset

178 
" >& " ^ err_file ^ 
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset

179 
(if background then " &" else "") 
50311  180 
fun run_on () = 
50750  181 
(Isabelle_System.bash command 
54100  182 
> tap (fn _ => 
183 
case try File.read (Path.explode err_file) > the_default "" of 

184 
"" => trace_msg ctxt (K "Done") 

185 
 s => warning ("MaSh error: " ^ elide_string 1000 s)); 

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

186 
read_suggs (fn () => try File.read_lines sugg_path > these)) 
50311  187 
fun clean_up () = 
188 
if overlord then () 

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

190 
in 

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

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

192 
write_file (SOME "") write_cmds cmd_path; 
50311  193 
trace_msg ctxt (fn () => "Running " ^ command); 
194 
with_cleanup clean_up run_on () 

195 
end 

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

196 

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

198 
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

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

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

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

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

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

204 

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

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

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

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

210 
 unmeta_chars _ (#"%" :: _) = "" (* error *) 
48308  211 
 unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs 
212 

50826  213 
val encode_str = String.translate meta_char 
214 
val encode_strs = map encode_str #> space_implode " " 

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

216 
val unencode_strs = 

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

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

218 

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

221 
serial_string () 

222 

53558  223 
(* Avoid scientific notation *) 
224 
fun safe_str_of_real r = 

225 
if r < 0.00001 then "0.00001" 

226 
else if r >= 1000000.0 then "1000000" 

227 
else Markup.print_real r 

228 

50356  229 
fun encode_feature (name, weight) = 
50826  230 
encode_str name ^ 
53558  231 
(if Real.== (weight, 1.0) then "" else "=" ^ safe_str_of_real weight) 
50356  232 

233 
val encode_features = map encode_feature #> space_implode " " 

234 

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

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

238 

50631  239 
fun str_of_relearn (name, deps) = 
50826  240 
"p " ^ encode_str name ^ ": " ^ encode_strs deps ^ "\n" 
50311  241 

53099  242 
fun str_of_query max_suggs (learns, hints, parents, feats) = 
53095  243 
implode (map str_of_learn learns) ^ 
53099  244 
"? " ^ string_of_int max_suggs ^ " # " ^ encode_strs parents ^ "; " ^ 
245 
encode_features feats ^ 

53095  246 
(if null hints then "" else "; " ^ encode_strs hints) ^ "\n" 
48406  247 

53098  248 
(* The suggested weights don't make much sense. *) 
48406  249 
fun extract_suggestion sugg = 
250 
case space_explode "=" sugg of 

51177  251 
[name, _ (* weight *)] => 
50965  252 
SOME (unencode_str name (* , Real.fromString weight > the_default 1.0 *)) 
253 
 [name] => SOME (unencode_str name (* , 1.0 *)) 

48406  254 
 _ => NONE 
255 

50633  256 
fun extract_suggestions line = 
48311  257 
case space_explode ":" line of 
48406  258 
[goal, suggs] => 
50826  259 
(unencode_str goal, map_filter extract_suggestion (space_explode " " suggs)) 
48312  260 
 _ => ("", []) 
48311  261 

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

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

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

264 

53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset

265 
fun shutdown ctxt overlord = 
53153  266 
(trace_msg ctxt (K "MaSh shutdown"); 
53756  267 
run_mash_tool ctxt overlord [shutdown_server_arg] false ([], K "") (K ())) 
53152
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset

268 

cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset

269 
fun save ctxt overlord = 
53153  270 
(trace_msg ctxt (K "MaSh save"); 
271 
run_mash_tool ctxt overlord [save_models_arg] true ([], K "") (K ())) 

53142
966a251efd16
have kill_all also kill MaSh server + be paranoid about reloading after clear_state, to allow for easier experimentation
blanchet
parents:
53141
diff
changeset

272 

53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset

273 
fun unlearn ctxt overlord = 
50311  274 
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

275 
trace_msg ctxt (K "MaSh unlearn"); 
53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset

276 
shutdown ctxt overlord; 
50319
dddcaeb92e11
robust writing of MaSh state  better drop learning data than cause other problems in Sledgehammer
blanchet
parents:
50311
diff
changeset

277 
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

278 
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

279 
path) NONE; 
50311  280 
() 
281 
end 

282 

53757
8d1a059ebcdb
reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents:
53756
diff
changeset

283 
fun learn _ _ _ [] = () 
8d1a059ebcdb
reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents:
53756
diff
changeset

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

285 
(trace_msg ctxt (fn () => "MaSh learn " ^ 
50631  286 
elide_string 1000 (space_implode " " (map #1 learns))); 
53757
8d1a059ebcdb
reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents:
53756
diff
changeset

287 
run_mash_tool ctxt overlord ([] > save ? cons save_models_arg) false 
8d1a059ebcdb
reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents:
53756
diff
changeset

288 
(learns, str_of_learn) (K ())) 
50311  289 

53757
8d1a059ebcdb
reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents:
53756
diff
changeset

290 
fun relearn _ _ _ [] = () 
8d1a059ebcdb
reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents:
53756
diff
changeset

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

292 
(trace_msg ctxt (fn () => "MaSh relearn " ^ 
50631  293 
elide_string 1000 (space_implode " " (map #1 relearns))); 
53757
8d1a059ebcdb
reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents:
53756
diff
changeset

294 
run_mash_tool ctxt overlord ([] > save ? cons save_models_arg) false 
8d1a059ebcdb
reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents:
53756
diff
changeset

295 
(relearns, str_of_relearn) (K ())) 
50311  296 

53117  297 
fun query ctxt overlord max_suggs (query as (_, _, _, feats)) = 
50969  298 
(trace_msg ctxt (fn () => "MaSh query " ^ encode_features feats); 
53152
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset

299 
run_mash_tool ctxt overlord [] false ([query], str_of_query max_suggs) 
50311  300 
(fn suggs => 
301 
case suggs () of 

302 
[] => [] 

50633  303 
 suggs => snd (extract_suggestions (List.last suggs))) 
50311  304 
handle List.Empty => []) 
305 

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

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

307 

50311  308 

309 
(*** Middlelevel communication with MaSh ***) 

310 

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

311 
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

312 
Isar_Proof  Automatic_Proof  Isar_Proof_wegen_Prover_Flop 
50311  313 

314 
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

315 
 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

316 
 str_of_proof_kind Isar_Proof_wegen_Prover_Flop = "x" 
50311  317 

318 
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

319 
 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

320 
 proof_kind_of_str "x" = Isar_Proof_wegen_Prover_Flop 
50311  321 

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

50610  323 
fun update_access_graph_node (name, kind) = 
50311  324 
Graph.default_node (name, Isar_Proof) 
325 
#> kind <> Isar_Proof ? Graph.map_node name (K kind) 

326 

327 
fun try_graph ctxt when def f = 

328 
f () 

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

330 
(trace_msg ctxt (fn () => 

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

332 
 Graph.DUP name => 

333 
(trace_msg ctxt (fn () => 

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

335 
 Graph.UNDEF name => 

336 
(trace_msg ctxt (fn () => 

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

338 
 exn => 

339 
if Exn.is_interrupt exn then 

340 
reraise exn 

341 
else 

342 
(trace_msg ctxt (fn () => 

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

344 
ML_Compiler.exn_message exn); def) 

345 

346 
fun graph_info G = 

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

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

349 
" edge(s), " ^ 

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

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

352 

53095  353 
type mash_state = 
354 
{access_G : unit Graph.T, 

355 
num_known_facts : int, 

356 
dirty : string list option} 

50311  357 

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

360 
local 

361 

53095  362 
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

363 

53095  364 
exception FILE_VERSION_TOO_NEW of unit 
50311  365 

366 
fun extract_node line = 

367 
case space_explode ":" line of 

368 
[head, parents] => 

369 
(case space_explode " " head of 

370 
[kind, name] => 

50826  371 
SOME (unencode_str name, unencode_strs parents, 
50311  372 
try proof_kind_of_str kind > the_default Isar_Proof) 
373 
 _ => NONE) 

374 
 _ => NONE 

375 

53152
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset

376 
fun load_state _ _ (state as (true, _)) = state 
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset

377 
 load_state ctxt overlord _ = 
50311  378 
let val path = mash_state_file () in 
379 
(true, 

380 
case try File.read_lines path of 

381 
SOME (version' :: node_lines) => 

382 
let 

383 
fun add_edge_to name parent = 

384 
Graph.default_node (parent, Isar_Proof) 

385 
#> Graph.add_edge (parent, name) 

386 
fun add_node line = 

387 
case extract_node line of 

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

389 
 SOME (name, parents, kind) => 

50610  390 
update_access_graph_node (name, kind) 
50311  391 
#> fold (add_edge_to name) parents 
53095  392 
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

393 
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

394 
EQUAL => 
53095  395 
(try_graph ctxt "loading state" Graph.empty (fn () => 
396 
fold add_node node_lines Graph.empty), 

397 
length node_lines) 

50860  398 
 LESS => 
53095  399 
(* can't parse old file *) 
53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset

400 
(MaSh.unlearn ctxt overlord; (Graph.empty, 0)) 
53095  401 
 GREATER => raise FILE_VERSION_TOO_NEW () 
50311  402 
in 
403 
trace_msg ctxt (fn () => 

50610  404 
"Loaded fact graph (" ^ graph_info access_G ^ ")"); 
53095  405 
{access_G = access_G, num_known_facts = num_known_facts, 
406 
dirty = SOME []} 

50311  407 
end 
408 
 _ => empty_state) 

409 
end 

410 

53152
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset

411 
fun save_state _ (state as {dirty = SOME [], ...}) = state 
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset

412 
 save_state ctxt {access_G, num_known_facts, dirty} = 
50311  413 
let 
414 
fun str_of_entry (name, parents, kind) = 

50826  415 
str_of_proof_kind kind ^ " " ^ encode_str name ^ ": " ^ 
416 
encode_strs parents ^ "\n" 

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

419 
val (banner, entries) = 

420 
case dirty of 

421 
SOME names => 

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

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

425 
write_file banner (entries, str_of_entry) (mash_state_file ()); 
50311  426 
trace_msg ctxt (fn () => 
50610  427 
"Saved fact graph (" ^ graph_info access_G ^ 
50311  428 
(case dirty of 
429 
SOME dirty => 

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

431 
 _ => "") ^ ")"); 

53095  432 
{access_G = access_G, num_known_facts = num_known_facts, dirty = SOME []} 
50311  433 
end 
434 

435 
val global_state = 

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

437 

438 
in 

439 

53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset

440 
fun map_state ctxt overlord f = 
53152
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset

441 
Synchronized.change global_state 
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset

442 
(load_state ctxt overlord ##> (f #> save_state ctxt)) 
53095  443 
handle FILE_VERSION_TOO_NEW () => () 
50311  444 

53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset

445 
fun peek_state ctxt overlord 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

446 
Synchronized.change_result global_state 
53152
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset

447 
(perhaps (try (load_state ctxt overlord)) #> `snd #>> f) 
50311  448 

53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset

449 
fun clear_state ctxt overlord = 
50311  450 
Synchronized.change global_state (fn _ => 
53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset

451 
(MaSh.unlearn ctxt overlord; (* also removes the state file *) 
53142
966a251efd16
have kill_all also kill MaSh server + be paranoid about reloading after clear_state, to allow for easier experimentation
blanchet
parents:
53141
diff
changeset

452 
(false, empty_state))) 
50311  453 

454 
end 

455 

53558  456 
fun mash_unlearn ctxt ({overlord, ...} : params) = 
53559
3858246c7c8f
when pouring in extra features into the goal, only consider facts from the current theory  the bottom 10 facts of the last import might be completely unrelated
blanchet
parents:
53558
diff
changeset

457 
(clear_state ctxt overlord; Output.urgent_message "Reset MaSh.") 
50570  458 

50311  459 

460 
(*** Isabelle helpers ***) 

461 

53819
e55d641d0a70
honor MaSh's zerooverhead policy  no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset

462 
fun is_mash_enabled () = (getenv "MASH" = "yes") 
e55d641d0a70
honor MaSh's zerooverhead policy  no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset

463 

50722  464 
val local_prefix = "local" ^ Long_Name.separator 
48378  465 

50722  466 
fun elided_backquote_thm threshold th = 
467 
elide_string threshold 

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

48378  469 

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

470 
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

471 

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

472 
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

473 
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

474 
let val hint = Thm.get_name_hint th in 
50722  475 
(* 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

476 
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

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

478 
thy_name_of_thm th ^ Long_Name.separator ^ suf ^ 
50732  479 
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

480 
 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

481 
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

482 
else 
50722  483 
elided_backquote_thm 200 th 
48378  484 

51134  485 
fun find_suggested_facts ctxt facts = 
48330  486 
let 
51134  487 
fun add (fact as (_, th)) = Symtab.default (nickname_of_thm th, fact) 
488 
val tab = fold add facts Symtab.empty 

489 
fun lookup nick = 

490 
Symtab.lookup tab nick 

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

492 
 _ => ()) 

493 
in map_filter lookup end 

48311  494 

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

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

496 
 scaled_avg xs = 
48407  497 
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

498 

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

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

500 
 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

501 

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

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

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

504 
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

505 
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

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

507 

50814  508 
fun mesh_facts _ max_facts [(_, (sels, unks))] = 
48406  509 
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

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

511 
let 
51029  512 
val mess = mess > map (apsnd (apfst (normalize_scores max_facts))) 
513 
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

514 
let 
54089
b13f6731f873
use same relevance filter for ATP and SMT solvers  attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected sideeffects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset

515 
val score_at = try (nth sels) #> Option.map (fn (_, score) => global_weight * score) 
50383
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

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

517 
case find_index (curry fact_eq fact o fst) sels of 
54089
b13f6731f873
use same relevance filter for ATP and SMT solvers  attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected sideeffects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset

518 
~1 => if member fact_eq unks fact then NONE else SOME 0.0 
50383
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

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

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

521 
fun weight_of fact = mess > map_filter (score_in fact) > scaled_avg 
54089
b13f6731f873
use same relevance filter for ATP and SMT solvers  attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected sideeffects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset

522 
val facts = 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

523 
in 
48406  524 
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

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

526 
end 
48312  527 

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

529 
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

530 
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

531 
fun class_feature_of s = ("s" ^ s, 1.0 (* FUDGE *)) 
53155  532 
val local_feature = ("local", 16.0 (* FUDGE *)) 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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 

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

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

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

582 

53089  583 
(* try "Long_Name.base_name" for shorter names *) 
584 
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

585 

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

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

587 
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

588 

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

589 
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

590 
 crude_str_of_typ (Type (s, Ts)) = 
53128  591 
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

592 
 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

593 
 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

594 

53128  595 
fun maybe_singleton_str _ "" = [] 
596 
 maybe_singleton_str pref s = [pref ^ s] 

597 

53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset

598 
val max_pat_breadth = 10 (* FUDGE *) 
50585  599 

54089
b13f6731f873
use same relevance filter for ATP and SMT solvers  attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected sideeffects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset

600 
fun term_features_of ctxt thy_name num_facts const_tab term_max_depth type_max_depth ts = 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

602 
val thy = Proof_Context.theory_of ctxt 
53082  603 

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

605 
val classes = Sign.classes_of thy 
53082  606 

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

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

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

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

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

612 
#> map class_feature_of 
53159  613 
#> union (eq_fst (op =))) S 
53082  614 

615 
fun pattify_type 0 _ = [] 

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

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

617 
if member (op =) bad_types s then [] else [massage_long_name s] 
53082  618 
 pattify_type depth (Type (s, U :: Ts)) = 
619 
let 

620 
val T = Type (s, Ts) 

621 
val ps = take max_pat_breadth (pattify_type depth T) 

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

53130  623 
in map_product (fn p => fn "" => p  q => p ^ "(" ^ q ^ ")") ps qs end 
53128  624 
 pattify_type _ (TFree (_, S)) = 
625 
maybe_singleton_str pat_tvar_prefix (crude_str_of_sort S) 

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

627 
maybe_singleton_str pat_tvar_prefix (crude_str_of_sort S) 

53082  628 
fun add_type_pat depth T = 
53159  629 
union (eq_fst (op =)) (map type_feature_of (pattify_type depth T)) 
53082  630 
fun add_type_pats 0 _ = I 
631 
 add_type_pats depth t = 

632 
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

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

634 
add_type_pats type_max_depth T 
53156  635 
#> fold_atyps_sorts (add_classes o snd) T 
53084  636 
fun add_subtypes (T as Type (_, Ts)) = add_type T #> fold add_subtypes Ts 
637 
 add_subtypes T = add_type T 

53082  638 

53130  639 
fun weight_of_const s = 
640 
16.0 + 

641 
(if num_facts = 0 then 

642 
0.0 

643 
else 

644 
let val count = Symtab.lookup const_tab s > the_default 1 in 

53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset

645 
Real.fromInt num_facts / Real.fromInt count (* FUDGE *) 
53130  646 
end) 
54089
b13f6731f873
use same relevance filter for ATP and SMT solvers  attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected sideeffects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset

647 
fun pattify_term _ 0 _ = [] 
b13f6731f873
use same relevance filter for ATP and SMT solvers  attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected sideeffects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset

648 
 pattify_term _ _ (Const (s, _)) = 
b13f6731f873
use same relevance filter for ATP and SMT solvers  attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected sideeffects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset

649 
if is_widely_irrelevant_const s then [] else [(massage_long_name s, weight_of_const s)] 
b13f6731f873
use same relevance filter for ATP and SMT solvers  attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected sideeffects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset

650 
 pattify_term _ _ (Free (s, T)) = 
53128  651 
maybe_singleton_str pat_var_prefix (crude_str_of_typ T) 
53130  652 
> map (rpair 0.0) 
53090
1426c97311f2
treat frees as both consts and vars, for more hits
blanchet
parents:
53089
diff
changeset

653 
> (if member (op =) fixes s then 
53130  654 
cons (free_feature_of (massage_long_name 
655 
(thy_name ^ Long_Name.separator ^ s))) 

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

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

657 
I) 
54089
b13f6731f873
use same relevance filter for ATP and SMT solvers  attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected sideeffects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset

658 
 pattify_term _ _ (Var (_, T)) = 
b13f6731f873
use same relevance filter for ATP and SMT solvers  attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected sideeffects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset

659 
maybe_singleton_str pat_var_prefix (crude_str_of_typ T) > map (rpair 0.0) 
b13f6731f873
use same relevance filter for ATP and SMT solvers  attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected sideeffects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset

660 
 pattify_term Ts _ (Bound j) = 
b13f6731f873
use same relevance filter for ATP and SMT solvers  attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected sideeffects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset

661 
maybe_singleton_str pat_var_prefix (crude_str_of_typ (nth Ts j)) > map (rpair 0.0) 
b13f6731f873
use same relevance filter for ATP and SMT solvers  attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected sideeffects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset

662 
 pattify_term Ts depth (t $ u) = 
50339
d8dae91f3107
MaSh improvements: deeper patterns + more respect for chained facts
blanchet
parents:
50338
diff
changeset

663 
let 
54089
b13f6731f873
use same relevance filter for ATP and SMT solvers  attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected sideeffects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset

664 
val ps = take max_pat_breadth (pattify_term Ts depth t) 
b13f6731f873
use same relevance filter for ATP and SMT solvers  attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected sideeffects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset

665 
val qs = take max_pat_breadth (("", 0.0) :: pattify_term Ts (depth  1) u) 
53130  666 
in 
667 
map_product (fn ppw as (p, pw) => 

668 
fn ("", _) => ppw 

669 
 (q, qw) => (p ^ "(" ^ q ^ ")", pw + qw)) ps qs 

670 
end 

54089
b13f6731f873
use same relevance filter for ATP and SMT solvers  attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected sideeffects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset

671 
 pattify_term _ _ _ = [] 
b13f6731f873
use same relevance filter for ATP and SMT solvers  attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected sideeffects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset

672 
fun add_term_pat Ts = union (eq_fst (op =)) oo pattify_term Ts 
53130  673 
fun add_term_pats _ 0 _ = I 
674 
 add_term_pats Ts depth t = 

675 
add_term_pat Ts depth t #> add_term_pats Ts (depth  1) t 

676 
fun add_term Ts = add_term_pats Ts term_max_depth 

53085  677 
fun add_subterms Ts t = 
50857
80768e28c9ee
better handlig of builtins  at the toplevel, not in subterms
blanchet
parents:
50841
diff
changeset

678 
case strip_comb t of 
54089
b13f6731f873
use same relevance filter for ATP and SMT solvers  attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected sideeffects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset

679 
(Const (s, T), args) => 
b13f6731f873
use same relevance filter for ATP and SMT solvers  attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected sideeffects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset

680 
(not (is_widely_irrelevant_const s) ? add_term Ts t) 
b13f6731f873
use same relevance filter for ATP and SMT solvers  attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected sideeffects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset

681 
#> add_subtypes T 
b13f6731f873
use same relevance filter for ATP and SMT solvers  attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected sideeffects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset

682 
#> fold (add_subterms Ts) args 
50857
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 
53130  685 
Free (_, T) => add_term Ts 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 

53085  692 
val term_max_depth = 2 
53155  693 
val type_max_depth = 1 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

694 

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

695 
(* TODO: Generate type classes for types? *) 
54089
b13f6731f873
use same relevance filter for ATP and SMT solvers  attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected sideeffects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset

696 
fun features_of ctxt thy num_facts const_tab (scope, _) ts = 
50393  697 
let val thy_name = Context.theory_name thy in 
698 
thy_feature_of thy_name :: 

54089
b13f6731f873
use same relevance filter for ATP and SMT solvers  attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected sideeffects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset

699 
term_features_of ctxt thy_name num_facts const_tab term_max_depth type_max_depth ts 
50393  700 
> scope <> Global ? cons local_feature 
701 
end 

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

702 

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

703 
(* 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

704 
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

705 
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

706 

54125
420b876ff1e2
if slicing is disabled, don't enforce last slice's "max_facts", but rather the maximum "max_facts"
blanchet
parents:
54123
diff
changeset

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

708 

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

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

52071  712 
exclusively to "someI_ex" (and to some internal constructions). *) 
50755  713 
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

714 

50828  715 
val fundef_ths = 
716 
@{thms fundef_ex1_existence fundef_ex1_uniqueness fundef_ex1_iff 

717 
fundef_default_value} 

718 
> map nickname_of_thm 

719 

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

720 
(* "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

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

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

723 
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

724 
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

725 
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

726 
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

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

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

729 

48441  730 
fun is_size_def [dep] th = 
731 
(case first_field ".recs" dep of 

732 
SOME (pref, _) => 

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

733 
(case first_field ".size" (nickname_of_thm th) of 
48441  734 
SOME (pref', _) => pref = pref' 
735 
 NONE => false) 

736 
 NONE => false) 

737 
 is_size_def _ _ = false 

738 

53095  739 
fun no_dependencies_for_status status = 
740 
status = Non_Rec_Def orelse status = Rec_Def 

741 

51177  742 
fun trim_dependencies deps = 
50755  743 
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

744 

50755  745 
fun isar_dependencies_of name_tabs th = 
51020  746 
let val deps = thms_in_proof (SOME name_tabs) th in 
50828  747 
if deps = [typedef_dep] orelse 
748 
deps = [class_some_dep] orelse 

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

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

751 
is_size_def deps th then 

50755  752 
[] 
753 
else 

754 
deps 

755 
end 

48404  756 

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

757 
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

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

759 
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

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

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

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

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

764 
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

765 
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt 
51136  766 
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

767 
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

768 
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

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

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

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

772 
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

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

774 
 NONE => accum (* shouldn't happen *) 
54123
271a8377656f
remove overloading of "max_facts"  it already controls the number of facts passed to ATPs for 'learn_prover'
blanchet
parents:
54115
diff
changeset

775 
val mepo_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

776 
facts 
54095  777 
> mepo_suggested_facts ctxt params (max_facts > the_default prover_default_max_facts) NONE 
778 
hyp_ts concl_t 

54123
271a8377656f
remove overloading of "max_facts"  it already controls the number of facts passed to ATPs for 'learn_prover'
blanchet
parents:
54115
diff
changeset

779 
val facts = 
271a8377656f
remove overloading of "max_facts"  it already controls the number of facts passed to ATPs for 'learn_prover'
blanchet
parents:
54115
diff
changeset

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

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

782 
> map nickify 
54123
271a8377656f
remove overloading of "max_facts"  it already controls the number of facts passed to ATPs for 'learn_prover'
blanchet
parents:
54115
diff
changeset

783 
val num_isar_deps = length isar_deps 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

784 
in 
48404  785 
if verbose andalso auto_level = 0 then 
54123
271a8377656f
remove overloading of "max_facts"  it already controls the number of facts passed to ATPs for 'learn_prover'
blanchet
parents:
54115
diff
changeset

786 
"MaSh: " ^ quote prover ^ " on " ^ quote (nickname_of_thm th) ^ 
271a8377656f
remove overloading of "max_facts"  it already controls the number of facts passed to ATPs for 'learn_prover'
blanchet
parents:
54115
diff
changeset

787 
" with " ^ string_of_int num_isar_deps ^ " + " ^ 
271a8377656f
remove overloading of "max_facts"  it already controls the number of facts passed to ATPs for 'learn_prover'
blanchet
parents:
54115
diff
changeset

788 
string_of_int (length facts  num_isar_deps) ^ " facts." 
271a8377656f
remove overloading of "max_facts"  it already controls the number of facts passed to ATPs for 'learn_prover'
blanchet
parents:
54115
diff
changeset

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

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

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

792 
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

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

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

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

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

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

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

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

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

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

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

805 

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

806 

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

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

808 

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

809 
(* 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

810 

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

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

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

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

814 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

836 

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

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

838 
 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

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

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

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

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

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

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

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

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

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

848 
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

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

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

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

852 
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

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

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

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

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

857 
end 
51177  858 

53095  859 
fun maximal_wrt_graph G keys = 
860 
let 

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

862 
fun insert_new seen name = 

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

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

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

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

867 
find_maxes 

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

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

870 
(if Symtab.defined tab new then 

871 
let 

872 
val newp = Graph.all_preds G [new] 

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

874 
val maxs = 

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

876 
in 

877 
if exists (is_ancestor new o fst) maxs then 

878 
(maxs, news) 

879 
else 

880 
((newp, new) 

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

882 
news) 

883 
end 

884 
else 

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

886 
(Graph.imm_preds G new) news)) 

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

888 

889 
fun maximal_wrt_access_graph access_G = 

890 
map (nickname_of_thm o snd) 

891 
#> maximal_wrt_graph access_G 

892 

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

894 

53197  895 
val chained_feature_factor = 0.5 (* FUDGE *) 
896 
val extra_feature_factor = 0.1 (* FUDGE *) 

53201
2a2dc18f3e10
reverted 6c5e7143e1f6; took a better look at evaluation data this time
blanchet
parents:
53197
diff
changeset

897 
val num_extra_feature_facts = 10 (* FUDGE *) 
53095  898 

899 
(* FUDGE *) 

900 
fun weight_of_proximity_fact rank = 

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

902 

53140
a1235e90da5f
pour extra features from proximate facts into goal, in exporter
blanchet
parents:
53137
diff
changeset

903 
fun weight_facts_smoothly facts = 
53095  904 
facts ~~ map weight_of_proximity_fact (0 upto length facts  1) 
905 

53140
a1235e90da5f
pour extra features from proximate facts into goal, in exporter
blanchet
parents:
53137
diff
changeset

906 
(* FUDGE *) 
a1235e90da5f
pour extra features from proximate facts into goal, in exporter
blanchet
parents:
53137
diff
changeset

907 
fun steep_weight_of_fact rank = 
a1235e90da5f
pour extra features from proximate facts into goal, in exporter
blanchet
parents:
53137
diff
changeset

908 
Math.pow (0.62, log2 (Real.fromInt (rank + 1))) 
a1235e90da5f
pour extra features from proximate facts into goal, in exporter
blanchet
parents:
53137
diff
changeset

909 

a1235e90da5f
pour extra features from proximate facts into goal, in exporter
blanchet
parents:
53137
diff
changeset

910 
fun weight_facts_steeply facts = 
a1235e90da5f
pour extra features from proximate facts into goal, in exporter
blanchet
parents:
53137
diff
changeset

911 
facts ~~ map steep_weight_of_fact (0 upto length facts  1) 
a1235e90da5f
pour extra features from proximate facts into goal, in exporter
blanchet
parents:
53137
diff
changeset

912 

53095  913 
val max_proximity_facts = 100 
914 

54060  915 
fun find_mash_suggestions ctxt max_facts suggs facts chained raw_unknown = 
916 
let 

917 
val inter_fact = inter (eq_snd Thm.eq_thm_prop) 

918 
val raw_mash = find_suggested_facts ctxt facts suggs 

919 
val proximate = take max_proximity_facts facts 

920 
val unknown_chained = inter_fact raw_unknown chained 

921 
val unknown_proximate = inter_fact raw_unknown proximate 

922 
val mess = 

923 
[(0.9 (* FUDGE *), (map (rpair 1.0) unknown_chained, [])), 

924 
(0.4 (* FUDGE *), (weight_facts_smoothly unknown_proximate, [])), 

925 
(0.1 (* FUDGE *), (weight_facts_steeply raw_mash, raw_unknown))] 

926 
val unknown = 

927 
raw_unknown 

928 
> fold (subtract (eq_snd Thm.eq_thm_prop)) 

929 
[unknown_chained, unknown_proximate] 

930 
in (mesh_facts (eq_snd Thm.eq_thm_prop) max_facts mess, unknown) end 

53095  931 

53127  932 
fun add_const_counts t = 
53130  933 
fold (fn s => Symtab.map_default (s, 0) (Integer.add 1)) 
53127  934 
(Term.add_const_names t []) 
53095  935 

53559
3858246c7c8f
when pouring in extra features into the goal, only consider facts from the current theory  the bottom 10 facts of the last import might be completely unrelated
blanchet
parents:
53558
diff
changeset

936 
fun mash_suggested_facts ctxt ({debug, overlord, ...} : params) prover max_facts 
3858246c7c8f
when pouring in extra features into the goal, only consider facts from the current theory  the bottom 10 facts of the last import might be completely unrelated
blanchet
parents:
53558
diff
changeset

937 
hyp_ts concl_t facts = 
53095  938 
let 
939 
val thy = Proof_Context.theory_of ctxt 

53559
3858246c7c8f
when pouring in extra features into the goal, only consider facts from the current theory  the bottom 10 facts of the last import might be completely unrelated
blanchet
parents:
53558
diff
changeset

940 
val thy_name = Context.theory_name thy 
53141
d27e99a6a679
take chained and proximate facts into consideration when computing MaSh features
blanchet
parents:
53140
diff
changeset

941 
val facts = facts > sort (crude_thm_ord o pairself snd o swap) 
53095  942 
val chained = facts > filter (fn ((_, (scope, _)), _) => scope = Chained) 
53141
d27e99a6a679
take chained and proximate facts into consideration when computing MaSh features
blanchet
parents:
53140
diff
changeset

943 
val num_facts = length facts 
53127  944 
val const_tab = fold (add_const_counts o prop_of o snd) facts Symtab.empty 
54085  945 

53559
3858246c7c8f
when pouring in extra features into the goal, only consider facts from the current theory  the bottom 10 facts of the last import might be completely unrelated
blanchet
parents:
53558
diff
changeset

946 
fun fact_has_right_theory (_, th) = 
3858246c7c8f
when pouring in extra features into the goal, only consider facts from the current theory  the bottom 10 facts of the last import might be completely unrelated
blanchet
parents:
53558
diff
changeset

947 
thy_name = Context.theory_name (theory_of_thm th) 
53141
d27e99a6a679
take chained and proximate facts into consideration when computing MaSh features
blanchet
parents:
53140
diff
changeset

948 
fun chained_or_extra_features_of factor (((_, stature), th), weight) = 
d27e99a6a679
take chained and proximate facts into consideration when computing MaSh features
blanchet
parents:
53140
diff
changeset

949 
[prop_of th] 
54089
b13f6731f873
use same relevance filter for ATP and SMT solvers  attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected sideeffects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset

950 
> features_of ctxt (theory_of_thm th) num_facts const_tab stature 
53141
d27e99a6a679
take chained and proximate facts into consideration when computing MaSh features
blanchet
parents:
53140
diff
changeset

951 
> map (apsnd (fn r => weight * factor * r)) 
54085  952 

53095  953 
val (access_G, suggs) = 
53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset

954 
peek_state ctxt overlord (fn {access_G, ...} => 
53095  955 
if Graph.is_empty access_G then 
54064  956 
(trace_msg ctxt (K "Nothing has been learned yet"); (access_G, [])) 
53095  957 
else 
958 
let 

959 
val parents = maximal_wrt_access_graph access_G facts 

53141
d27e99a6a679
take chained and proximate facts into consideration when computing MaSh features
blanchet
parents:
53140
diff
changeset

960 
val goal_feats = 
54089
b13f6731f873
use same relevance filter for ATP and SMT solvers  attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected sideeffects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset

961 
features_of ctxt thy num_facts const_tab (Local, General) (concl_t :: hyp_ts) 
53141
d27e99a6a679
take chained and proximate facts into consideration when computing MaSh features
blanchet
parents:
53140
diff
changeset

962 
val chained_feats = 
d27e99a6a679
take chained and proximate facts into consideration when computing MaSh features
blanchet
parents:
53140
diff
changeset

963 
chained 
d27e99a6a679
take chained and proximate facts into consideration when computing MaSh features
blanchet
parents:
53140
diff
changeset

964 
> map (rpair 1.0) 
d27e99a6a679
take chained and proximate facts into consideration when computing MaSh features
blanchet
parents:
53140
diff
changeset

965 
> map (chained_or_extra_features_of chained_feature_factor) 
53159  966 
> rpair [] > fold (union (eq_fst (op =))) 
53141
d27e99a6a679
take chained and proximate facts into consideration when computing MaSh features
blanchet
parents:
53140
diff
changeset

967 
val extra_feats = 
d27e99a6a679
take chained and proximate facts into consideration when computing MaSh features
blanchet
parents:
53140
diff
changeset

968 
facts 
53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset

969 
> take (Int.max (0, num_extra_feature_facts  length chained)) 
53559
3858246c7c8f
when pouring in extra features into the goal, only consider facts from the current theory  the bottom 10 facts of the last import might be completely unrelated
blanchet
parents:
53558
diff
changeset

970 
> filter fact_has_right_theory 
53141
d27e99a6a679
take chained and proximate facts into consideration when computing MaSh features
blanchet
parents:
53140
diff
changeset

971 
> weight_facts_steeply 
d27e99a6a679
take chained and proximate facts into consideration when computing MaSh features
blanchet
parents:
53140
diff
changeset

972 
> map (chained_or_extra_features_of extra_feature_factor) 
53159  973 
> rpair [] > fold (union (eq_fst (op =))) 
53095  974 
val feats = 
53159  975 
fold (union (eq_fst (op =))) [chained_feats, extra_feats] 
53141
d27e99a6a679
take chained and proximate facts into consideration when computing MaSh features
blanchet
parents:
53140
diff
changeset

976 
goal_feats 
53559
3858246c7c8f
when pouring in extra features into the goal, only consider facts from the current theory  the bottom 10 facts of the last import might be completely unrelated
blanchet
parents:
53558
diff
changeset

977 
> debug ? sort (Real.compare o swap o pairself snd) 
53095  978 
val hints = 
979 
chained > filter (is_fact_in_graph access_G o snd) 

980 
> map (nickname_of_thm o snd) 

981 
in 

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

983 
([], hints, parents, feats)) 
53095  984 
end) 
985 
val unknown = facts > filter_out (is_fact_in_graph access_G o snd) 

986 
in 

987 
find_mash_suggestions ctxt max_facts suggs facts chained unknown 

988 
> pairself (map fact_of_raw_fact) 

989 
end 

990 

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

992 
let 

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

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

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

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

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

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

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

1000 

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

1002 
let 

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

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

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

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

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

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

1009 

1010 
fun flop_wrt_access_graph name = 

1011 
update_access_graph_node (name, Isar_Proof_wegen_Prover_Flop) 

1012 

1013 
val learn_timeout_slack = 2.0 

1014 

1015 
fun launch_thread timeout task = 

1016 
let 

1017 
val hard_timeout = time_mult learn_timeout_slack timeout 

1018 
val birth_time = Time.now () 

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

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

1021 
in Async_Manager.thread MaShN birth_time death_time desc task end 

1022 

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

1024 
used_ths = 

53819
e55d641d0a70
honor MaSh's zerooverhead policy  no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset

1025 
if is_mash_enabled () then 
e55d641d0a70
honor MaSh's zerooverhead policy  no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset

1026 
launch_thread (timeout > the_default one_day) (fn () => 
e55d641d0a70
honor MaSh's zerooverhead policy  no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset

1027 
let 
e55d641d0a70
honor MaSh's zerooverhead policy  no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset

1028 
val thy = Proof_Context.theory_of ctxt 
e55d641d0a70
honor MaSh's zerooverhead policy  no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset

1029 
val name = freshish_name () 
54089
b13f6731f873
use same relevance filter for ATP and SMT solvers  attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected sideeffects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset

1030 
val feats = features_of ctxt thy 0 Symtab.empty (Local, General) [t] > map fst 
53819
e55d641d0a70
honor MaSh's zerooverhead policy  no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset

1031 
in 
e55d641d0a70
honor MaSh's zerooverhead policy  no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset

1032 
peek_state ctxt overlord (fn {access_G, ...} => 
e55d641d0a70
honor MaSh's zerooverhead policy  no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset

1033 
let 
e55d641d0a70
honor MaSh's zerooverhead policy  no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset

1034 
val parents = maximal_wrt_access_graph access_G facts 
e55d641d0a70
honor MaSh's zerooverhead policy  no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset

1035 
val deps = 
e55d641d0a70
honor MaSh's zerooverhead policy  no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset

1036 
used_ths > filter (is_fact_in_graph access_G) 
e55d641d0a70
honor MaSh's zerooverhead policy  no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset

1037 
> map nickname_of_thm 
e55d641d0a70
honor MaSh's zerooverhead policy  no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset

1038 
in 
e55d641d0a70
honor MaSh's zerooverhead policy  no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset

1039 
MaSh.learn ctxt overlord true [(name, parents, feats, deps)] 
e55d641d0a70
honor MaSh's zerooverhead policy  no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset

1040 
end); 
e55d641d0a70
honor MaSh's zerooverhead policy  no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset

1041 
(true, "") 
e55d641d0a70
honor MaSh's zerooverhead policy  no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset

1042 
end) 
e55d641d0a70
honor MaSh's zerooverhead policy  no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset

1043 
else 
e55d641d0a70
honor MaSh's zerooverhead policy  no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset

1044 
() 
53095  1045 

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

1046 
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

1047 
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

1048 

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

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

1050 

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

1051 
(* The timeout is understood in a very relaxed fashion. *) 
48404  1052 
fun mash_learn_facts ctxt (params as {debug, verbose, overlord, ...}) prover 
53152
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset

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

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

1057 
Time.+ (Timer.checkRealTimer timer, commit_timeout) 
53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset

1058 
val {access_G, ...} = peek_state ctxt overlord I 
53095  1059 
val is_in_access_G = is_fact_in_graph access_G o snd 
51177  1060 
val no_new_facts = forall is_in_access_G facts 
48308  1061 
in 
51177  1062 
if no_new_facts andalso not run_prover then 
48404  1063 
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

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

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

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

1067 
"\n\nHint: Try " ^ sendback learn_proverN ^ 
50751  1068 
" to learn from an automatic prover." 
48404  1069 
else 
1070 
"") 

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

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

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

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

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

1078 
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

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

1080 
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

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

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

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

1087 
fun do_commit [] [] [] state = state 
53095  1088 
 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

1089 
let 
50610  1090 
val was_empty = Graph.is_empty access_G 
50631  1091 
val (learns, access_G) = 
1092 
([], access_G) > fold (learn_wrt_access_graph ctxt) learns 

1093 
val (relearns, access_G) = 

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

50610  1095 
val access_G = access_G > fold flop_wrt_access_graph flops 
53095  1096 
val num_known_facts = num_known_facts + length learns 
48699  1097 
val dirty = 
50631  1098 
case (was_empty, dirty, relearns) of 
1099 
(false, SOME names, []) => SOME (map #1 learns @ names) 

48699  1100 
 _ => NONE 
48404  1101 
in 
53757
8d1a059ebcdb
reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents:
53756
diff
changeset

1102 
MaSh.learn ctxt overlord (save andalso null relearns) (rev learns); 
8d1a059ebcdb
reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents:
53756
diff
changeset

1103 
MaSh.relearn ctxt overlord save relearns; 
53095  1104 
{access_G = access_G, num_known_facts = num_known_facts, 
1105 
dirty = dirty} 

48404  1106 
end 
50631  1107 
fun commit last learns relearns flops = 
48404  1108 
(if debug andalso auto_level = 0 then 
1109 
Output.urgent_message "Committing..." 

1110 
else 

1111 
(); 

53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset

1112 
map_state ctxt overlord (do_commit (rev learns) relearns flops); 
48404  1113 
if not last andalso auto_level = 0 then 
50631  1114 
let val num_proofs = length learns + length relearns in 
48404  1115 
"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

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

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

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

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

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

1122 
()) 
51177  1123 
fun learn_new_fact _ (accum as (_, (_, _, true))) = accum 
1124 
 learn_new_fact (parents, ((_, stature as (_, status)), th)) 

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

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

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

1128 
val feats = 
54089
b13f6731f873
use same relevance filter for ATP and SMT solvers  attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected sideeffects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset

1129 
features_of ctxt (theory_of_thm th) 0 Symtab.empty stature [prop_of th] > map fst 
48439
67a6bcbd3587
removed MaSh junk arising from primrec definitions
blanchet
parents:
48438
diff
changeset

1130 
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
