author  blanchet 
Fri, 28 Dec 2012 21:03:39 +0100  
changeset 50632  12c097ff3241 
parent 50631  b69079c14665 
child 50633  87961472b404 
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 
48296
e7f01b7e244e
gracefully handle the case of empty theories when going up the accessibility chain
blanchet
parents:
48293
diff
changeset

10 
type fact = Sledgehammer_Fact.fact 
e7f01b7e244e
gracefully handle the case of empty theories when going up the accessibility chain
blanchet
parents:
48293
diff
changeset

11 
type fact_override = Sledgehammer_Fact.fact_override 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

12 
type params = Sledgehammer_Provers.params 
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset

13 
type relevance_fudge = Sledgehammer_Provers.relevance_fudge 
48251
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 
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

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

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

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

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

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

22 
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

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

24 
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

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

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

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

28 
val escape_metas : string list > string 
48308  29 
val unescape_meta : string > string 
30 
val unescape_metas : string > string list 

50356  31 
val encode_features : (string * real) list > string 
48406  32 
val extract_query : string > string * (string * real) list 
50632
12c097ff3241
slightly more elegant naming convention (to keep lowlevel and highlevel APIs separated)
blanchet
parents:
50631
diff
changeset

33 

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

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

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

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

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

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

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

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

41 
Proof.context > bool > (string * string list) list > unit 
12c097ff3241
slightly more elegant naming convention (to keep lowlevel and highlevel APIs separated)
blanchet
parents:
50631
diff
changeset

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

43 
Proof.context > bool > int > string list * (string * real) list 
12c097ff3241
slightly more elegant naming convention (to keep lowlevel and highlevel APIs separated)
blanchet
parents:
50631
diff
changeset

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

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

46 

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

48 
val nickname_of_thm : thm > string 
50412  49 
val find_suggested_facts : 
48406  50 
(string * 'a) list > ('b * thm) list > (('b * thm) * 'a) list 
48321  51 
val mesh_facts : 
50383
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

52 
int > (real * ((('a * thm) * real) list * ('a * thm) list)) list 
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

53 
> ('a * thm) list 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

55 
val thm_ord : thm * thm > order 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

56 
val goal_of_thm : theory > thm > thm 
48321  57 
val run_prover_for_mash : 
48318  58 
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

59 
val features_of : 
50356  60 
Proof.context > string > theory > stature > term list 
61 
> (string * real) list 

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

62 
val isar_dependencies_of : string Symtab.table > thm > string list option 
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

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

64 
Proof.context > params > string > int > fact list > string Symtab.table 
48665  65 
> thm > bool * string list option 
50608  66 
val weight_mash_facts : 'a list > ('a * real) list 
50412  67 
val find_mash_suggestions : 
68 
int > (Symtab.key * 'a) list > ('b * thm) list > ('b * thm) list 

50440
ca99c269ca3a
don't have MaSh pretend it knows facts it doesn't know
blanchet
parents:
50438
diff
changeset

69 
> ('b * thm) list > ('b * thm) list * ('b * thm) list 
48406  70 
val mash_suggested_facts : 
50383
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

71 
Proof.context > params > string > int > term list > term > fact list 
50440
ca99c269ca3a
don't have MaSh pretend it knows facts it doesn't know
blanchet
parents:
50438
diff
changeset

72 
> fact list * fact list 
48383  73 
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

74 
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

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

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

77 
Proof.context > params > fact_override > thm list > bool > unit 
50311  78 
val is_mash_enabled : unit > bool 
79 
val mash_can_suggest_facts : Proof.context > bool 

50412  80 
val generous_max_facts : int > int 
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset

81 
val relevant_facts : 
48292  82 
Proof.context > params > string > int > fact_override > term list 
48296
e7f01b7e244e
gracefully handle the case of empty theories when going up the accessibility chain
blanchet
parents:
48293
diff
changeset

83 
> term > fact list > fact list 
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

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

85 
val running_learners : unit > unit 
48248  86 
end; 
87 

48381  88 
structure Sledgehammer_MaSh : SLEDGEHAMMER_MASH = 
48248  89 
struct 
48249  90 

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

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

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

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

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

95 
open Sledgehammer_Provers 
48318  96 
open Sledgehammer_Minimize 
48381  97 
open Sledgehammer_MePo 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

98 

48308  99 
val trace = 
48380  100 
Attrib.setup_config_bool @{binding sledgehammer_mash_trace} (K false) 
48308  101 
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else () 
102 

48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

103 
val MaShN = "MaSh" 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

104 

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

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

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

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

108 

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

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

110 

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

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

112 
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

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

114 
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

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

116 

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

117 
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

118 
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

119 
val mash_state_dir = mash_model_dir 
50310  120 
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

121 

48330  122 

50311  123 
(*** Lowlevel communication with MaSh ***) 
124 

125 
fun wipe_out_file file = (try (File.rm o Path.explode) file; ()) 

126 

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

127 
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

128 
(case banner of SOME s => File.write path s  NONE => (); 
b17b05c8d4a4
proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents:
50319
diff
changeset

129 
xs > chunk_list 500 
b17b05c8d4a4
proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents:
50319
diff
changeset

130 
> List.app (File.append path o space_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

131 
handle IO.Io _ => () 
50311  132 

133 
fun run_mash_tool ctxt overlord save max_suggs write_cmds read_suggs = 

134 
let 

135 
val (temp_dir, serial) = 

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

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

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

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

140 
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

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

143 
val cmd_path = Path.explode cmd_file 
50311  144 
val core = 
145 
"inputFile " ^ cmd_file ^ " predictions " ^ sugg_file ^ 

146 
" numberOfPredictions " ^ string_of_int max_suggs ^ 

50623  147 
" learnTheories" ^ 
50311  148 
(if save then " saveModel" else "") 
149 
val command = 

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

150 
"\"$ISABELLE_SLEDGEHAMMER_MASH/src/mash.py\" quiet outputDir " ^ 
b17b05c8d4a4
proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents:
50319
diff
changeset

151 
File.shell_path (mash_model_dir ()) ^ " log " ^ log_file ^ " " ^ core ^ 
50311  152 
" >& " ^ err_file 
153 
> tap (fn _ => trace_msg ctxt (fn () => 

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

155 
NONE => "Done" 

156 
 SOME "" => "Done" 

157 
 SOME s => "Error: " ^ elide_string 1000 s)) 

158 
fun run_on () = 

159 
(Isabelle_System.bash command; 

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

160 
read_suggs (fn () => try File.read_lines sugg_path > these)) 
50311  161 
fun clean_up () = 
162 
if overlord then () 

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

164 
in 

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

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

166 
write_file (SOME "") write_cmds cmd_path; 
50311  167 
trace_msg ctxt (fn () => "Running " ^ command); 
168 
with_cleanup clean_up run_on () 

169 
end 

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

170 

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

172 
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

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

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

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

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

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

178 

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

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

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

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

184 
 unmeta_chars _ (#"%" :: _) = "" (* error *) 
48308  185 
 unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs 
186 

187 
val escape_meta = String.translate meta_char 

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

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

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

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

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

192 

50356  193 
fun encode_feature (name, weight) = 
50389
ad0ac9112d2c
simplify code now that "mash.py" supports weights
blanchet
parents:
50383
diff
changeset

194 
escape_meta name ^ 
ad0ac9112d2c
simplify code now that "mash.py" supports weights
blanchet
parents:
50383
diff
changeset

195 
(if Real.== (weight, 1.0) then "" else "=" ^ Real.toString weight) 
50356  196 

197 
val encode_features = map encode_feature #> space_implode " " 

198 

50631  199 
fun str_of_learn (name, parents, feats, deps) = 
50311  200 
"! " ^ escape_meta name ^ ": " ^ escape_metas parents ^ "; " ^ 
50356  201 
encode_features feats ^ "; " ^ escape_metas deps ^ "\n" 
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

202 

50631  203 
fun str_of_relearn (name, deps) = 
50311  204 
"p " ^ escape_meta name ^ ": " ^ escape_metas deps ^ "\n" 
205 

206 
fun str_of_query (parents, feats) = 

50356  207 
"? " ^ escape_metas parents ^ "; " ^ encode_features feats ^ "\n" 
48406  208 

209 
fun extract_suggestion sugg = 

210 
case space_explode "=" sugg of 

211 
[name, weight] => 

50401
8e5d7ef3da76
parse more liberal MaSh suggestion syntax (for the eval driver)
blanchet
parents:
50398
diff
changeset

212 
SOME (unescape_meta name, Real.fromString weight > the_default 1.0) 
8e5d7ef3da76
parse more liberal MaSh suggestion syntax (for the eval driver)
blanchet
parents:
50398
diff
changeset

213 
 [name] => SOME (unescape_meta name, 1.0) 
48406  214 
 _ => NONE 
215 

48311  216 
fun extract_query line = 
217 
case space_explode ":" line of 

48406  218 
[goal, suggs] => 
219 
(unescape_meta goal, 

220 
map_filter extract_suggestion (space_explode " " suggs)) 

48312  221 
 _ => ("", []) 
48311  222 

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

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

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

225 

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

226 
fun unlearn ctxt = 
50311  227 
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

228 
trace_msg ctxt (K "MaSh unlearn"); 
50319
dddcaeb92e11
robust writing of MaSh state  better drop learning data than cause other problems in Sledgehammer
blanchet
parents:
50311
diff
changeset

229 
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

230 
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

231 
path) NONE; 
50311  232 
() 
233 
end 

234 

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

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

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

237 
(trace_msg ctxt (fn () => "MaSh learn " ^ 
50631  238 
elide_string 1000 (space_implode " " (map #1 learns))); 
239 
run_mash_tool ctxt overlord true 0 (learns, str_of_learn) (K ())) 

50311  240 

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

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

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

243 
(trace_msg ctxt (fn () => "MaSh relearn " ^ 
50631  244 
elide_string 1000 (space_implode " " (map #1 relearns))); 
245 
run_mash_tool ctxt overlord true 0 (relearns, str_of_relearn) (K ())) 

50311  246 

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

247 
fun query ctxt overlord max_suggs (query as (_, feats)) = 
12c097ff3241
slightly more elegant naming convention (to keep lowlevel and highlevel APIs separated)
blanchet
parents:
50631
diff
changeset

248 
(trace_msg ctxt (fn () => "MaSh query " ^ encode_features feats); 
50311  249 
run_mash_tool ctxt overlord false max_suggs 
250 
([query], str_of_query) 

251 
(fn suggs => 

252 
case suggs () of 

253 
[] => [] 

254 
 suggs => snd (extract_query (List.last suggs))) 

255 
handle List.Empty => []) 

256 

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

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

258 

50311  259 

260 
(*** Middlelevel communication with MaSh ***) 

261 

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

262 
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

263 
Isar_Proof  Automatic_Proof  Isar_Proof_wegen_Prover_Flop 
50311  264 

265 
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

266 
 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

267 
 str_of_proof_kind Isar_Proof_wegen_Prover_Flop = "x" 
50311  268 

269 
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

270 
 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

271 
 proof_kind_of_str "x" = Isar_Proof_wegen_Prover_Flop 
50311  272 

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

50610  274 
fun update_access_graph_node (name, kind) = 
50311  275 
Graph.default_node (name, Isar_Proof) 
276 
#> kind <> Isar_Proof ? Graph.map_node name (K kind) 

277 

278 
fun try_graph ctxt when def f = 

279 
f () 

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

281 
(trace_msg ctxt (fn () => 

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

283 
 Graph.DUP name => 

284 
(trace_msg ctxt (fn () => 

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

286 
 Graph.UNDEF name => 

287 
(trace_msg ctxt (fn () => 

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

289 
 exn => 

290 
if Exn.is_interrupt exn then 

291 
reraise exn 

292 
else 

293 
(trace_msg ctxt (fn () => 

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

295 
ML_Compiler.exn_message exn); def) 

296 

297 
fun graph_info G = 

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

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

300 
" edge(s), " ^ 

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

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

303 

50610  304 
type mash_state = {access_G : unit Graph.T, dirty : string list option} 
50311  305 

50610  306 
val empty_state = {access_G = Graph.empty, dirty = SOME []} 
50311  307 

308 
local 

309 

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

311 

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

312 
exception Too_New of unit 
50311  313 

314 
fun extract_node line = 

315 
case space_explode ":" line of 

316 
[head, parents] => 

317 
(case space_explode " " head of 

318 
[kind, name] => 

319 
SOME (unescape_meta name, unescape_metas parents, 

320 
try proof_kind_of_str kind > the_default Isar_Proof) 

321 
 _ => NONE) 

322 
 _ => NONE 

323 

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

325 
 load ctxt _ = 

326 
let val path = mash_state_file () in 

327 
(true, 

328 
case try File.read_lines path of 

329 
SOME (version' :: node_lines) => 

330 
let 

331 
fun add_edge_to name parent = 

332 
Graph.default_node (parent, Isar_Proof) 

333 
#> Graph.add_edge (parent, name) 

334 
fun add_node line = 

335 
case extract_node line of 

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

337 
 SOME (name, parents, kind) => 

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

341 
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

342 
EQUAL => 
187ae76a1757
more robustness in the face of MaSh format changes  don't overwrite new versions with old versions
blanchet
parents:
50356
diff
changeset

343 
try_graph ctxt "loading state" Graph.empty (fn () => 
187ae76a1757
more robustness in the face of MaSh format changes  don't overwrite new versions with old versions
blanchet
parents:
50356
diff
changeset

344 
fold add_node node_lines Graph.empty) 
187ae76a1757
more robustness in the face of MaSh format changes  don't overwrite new versions with old versions
blanchet
parents:
50356
diff
changeset

345 
 LESS => Graph.empty (* can't parse old file *) 
187ae76a1757
more robustness in the face of MaSh format changes  don't overwrite new versions with old versions
blanchet
parents:
50356
diff
changeset

346 
 GREATER => raise Too_New () 
50311  347 
in 
348 
trace_msg ctxt (fn () => 

50610  349 
"Loaded fact graph (" ^ graph_info access_G ^ ")"); 
350 
{access_G = access_G, dirty = SOME []} 

50311  351 
end 
352 
 _ => empty_state) 

353 
end 

354 

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

50610  356 
 save ctxt {access_G, dirty} = 
50311  357 
let 
358 
fun str_of_entry (name, parents, kind) = 

359 
str_of_proof_kind kind ^ " " ^ escape_meta name ^ ": " ^ 

360 
escape_metas parents ^ "\n" 

361 
fun append_entry (name, (kind, (parents, _))) = 

362 
cons (name, Graph.Keys.dest parents, kind) 

363 
val (banner, entries) = 

364 
case dirty of 

365 
SOME names => 

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

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

369 
write_file banner (entries, str_of_entry) (mash_state_file ()); 
50311  370 
trace_msg ctxt (fn () => 
50610  371 
"Saved fact graph (" ^ graph_info access_G ^ 
50311  372 
(case dirty of 
373 
SOME dirty => 

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

375 
 _ => "") ^ ")"); 

50610  376 
{access_G = access_G, dirty = SOME []} 
50311  377 
end 
378 

379 
val global_state = 

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

381 

382 
in 

383 

50570  384 
fun map_state ctxt f = 
50311  385 
Synchronized.change global_state (load ctxt ##> (f #> save ctxt)) 
50357
187ae76a1757
more robustness in the face of MaSh format changes  don't overwrite new versions with old versions
blanchet
parents:
50356
diff
changeset

386 
handle Too_New () => () 
50311  387 

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

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

390 
(perhaps (try (load ctxt)) #> `snd #>> f) 
50311  391 

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

394 
(MaSh.unlearn ctxt; (* also removes the state file *) 
50311  395 
(true, empty_state))) 
396 

397 
end 

398 

50570  399 
val mash_unlearn = clear_state 
400 

50311  401 

402 
(*** Isabelle helpers ***) 

403 

48378  404 
fun parent_of_local_thm th = 
405 
let 

406 
val thy = th > Thm.theory_of_thm 

407 
val facts = thy > Global_Theory.facts_of 

408 
val space = facts > Facts.space_of 

409 
fun id_of s = #id (Name_Space.the_entry space s) 

410 
fun max_id (s', _) (s, id) = 

411 
let val id' = id_of s' in if id > id' then (s, id) else (s', id') end 

412 
in ("", ~1) > Facts.fold_static max_id facts > fst end 

413 

414 
val local_prefix = "local" ^ Long_Name.separator 

415 

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

416 
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

417 
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

418 
let val hint = Thm.get_name_hint th in 
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset

419 
(* FIXME: There must be a better way to detect local facts. *) 
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset

420 
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

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

422 
parent_of_local_thm th ^ Long_Name.separator ^ Long_Name.separator ^ suf 
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset

423 
 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

424 
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

425 
else 
50047
45684acf0b94
thread context correctly when printing backquoted facts
blanchet
parents:
49997
diff
changeset

426 
backquote_thm (Proof_Context.init_global (Thm.theory_of_thm th)) th 
48378  427 

50412  428 
fun find_suggested_facts suggs facts = 
48330  429 
let 
50624
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset

430 
fun add_fact (fact as (_, th)) = Symtab.default (nickname_of_thm th, fact) 
48330  431 
val tab = Symtab.empty > fold add_fact facts 
48406  432 
fun find_sugg (name, weight) = 
433 
Symtab.lookup tab name > Option.map (rpair weight) 

434 
in map_filter find_sugg suggs end 

48311  435 

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

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

437 
 scaled_avg xs = 
48407  438 
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

439 

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

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

441 
 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

442 

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

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

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

445 
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

446 
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

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

448 

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

449 
fun mesh_facts max_facts [(_, (sels, unks))] = 
48406  450 
map fst (take max_facts sels) @ take (max_facts  length sels) unks 
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

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

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

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

454 
mess > map (apsnd (apfst (normalize_scores max_facts #> `length))) 
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

455 
val fact_eq = Thm.eq_thm o pairself snd 
50383
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

456 
fun score_in fact (global_weight, ((sel_len, sels), unks)) = 
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

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

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

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

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

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

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

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

464 
~1 => (case find_index (curry fact_eq fact) unks of 
50438
9bb7868a4c20
fixed embarrassing offbyone bug in MaSh's Mesh
blanchet
parents:
50435
diff
changeset

465 
~1 => score_at (sel_len  1) 
50383
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

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

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

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

469 
fun weight_of fact = mess > map_filter (score_in fact) > scaled_avg 
48406  470 
val facts = 
50383
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

471 
fold (union fact_eq o map fst o take max_facts o snd o fst o snd) mess 
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

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

473 
in 
48406  474 
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

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

476 
end 
48312  477 

50584
4fff0898cc0e
tuned weights  keep same relative values, but use 1.0 as the least weight
blanchet
parents:
50583
diff
changeset

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

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

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

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

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

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

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

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

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

487 

48324  488 
fun theory_ord p = 
489 
if Theory.eq_thy p then 

490 
EQUAL 

491 
else if Theory.subthy p then 

492 
LESS 

493 
else if Theory.subthy (swap p) then 

494 
GREATER 

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

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

497 
 order => order 

498 

50382  499 
fun thm_ord p = 
500 
case theory_ord (pairself theory_of_thm p) of 

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

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

502 
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

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

504 
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

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

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

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

508 
 ord => ord 
48324  509 

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

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

511 

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

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

513 
 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

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

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

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

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

518 

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

519 
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

520 

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

521 
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

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

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

524 
{state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1, 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

525 
facts = facts > map (apfst (apfst (fn name => name ()))) 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

526 
> map Untranslated_Fact} 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

527 
in 
48399
4bacc8983b3d
learn from SMT proofs when they can be minimized by Metis
blanchet
parents:
48398
diff
changeset

528 
get_minimizing_prover ctxt MaSh (K (K ())) prover params (K (K (K ""))) 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

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

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

531 

48326  532 
val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}] 
533 

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

536 

50585  537 
val max_pattern_breadth = 10 
538 

539 
fun interesting_terms_types_and_classes ctxt prover thy_name term_max_depth 

48318  540 
type_max_depth ts = 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

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

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

544 
val classes = Sign.classes_of thy 
48318  545 
fun is_bad_const (x as (s, _)) args = 
48398  546 
member (op =) logical_consts s orelse 
48318  547 
fst (is_built_in_const_for_prover ctxt prover x args) 
48304  548 
fun add_classes @{sort type} = I 
50392
190053ee24ed
expand type classes into their ancestors for MaSh
blanchet
parents:
50391
diff
changeset

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

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

551 
#> swap #> op :: 
190053ee24ed
expand type classes into their ancestors for MaSh
blanchet
parents:
50391
diff
changeset

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

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

554 
#> union (op = o pairself fst)) S 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

555 
fun do_add_type (Type (s, Ts)) = 
50356  556 
(not (member (op =) bad_types s) 
557 
? insert (op = o pairself fst) (type_feature_of s)) 

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

558 
#> fold do_add_type Ts 
48304  559 
 do_add_type (TFree (_, S)) = add_classes S 
560 
 do_add_type (TVar (_, S)) = add_classes S 

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

561 
fun add_type T = type_max_depth >= 0 ? do_add_type T 
50583
681edd111e9b
really honor pattern depth, and use 2 by default
blanchet
parents:
50570
diff
changeset

562 
fun patternify_term _ 0 _ = [] 
50339
d8dae91f3107
MaSh improvements: deeper patterns + more respect for chained facts
blanchet
parents:
50338
diff
changeset

563 
 patternify_term args _ (Const (x as (s, _))) = 
50356  564 
if is_bad_const x args then [] else [s] 
50393  565 
 patternify_term _ depth (Free (s, _)) = 
566 
if depth = term_max_depth andalso member (op =) fixes s then 

567 
[thy_name ^ Long_Name.separator ^ s] 

568 
else 

569 
[] 

50339
d8dae91f3107
MaSh improvements: deeper patterns + more respect for chained facts
blanchet
parents:
50338
diff
changeset

570 
 patternify_term args depth (t $ u) = 
d8dae91f3107
MaSh improvements: deeper patterns + more respect for chained facts
blanchet
parents:
50338
diff
changeset

571 
let 
50585  572 
val ps = 
573 
take max_pattern_breadth (patternify_term (u :: args) depth t) 

574 
val qs = 

575 
take max_pattern_breadth ("" :: patternify_term [] (depth  1) u) 

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

576 
in map_product (fn p => fn "" => p  q => p ^ "(" ^ q ^ ")") ps qs end 
50339
d8dae91f3107
MaSh improvements: deeper patterns + more respect for chained facts
blanchet
parents:
50338
diff
changeset

577 
 patternify_term _ _ _ = [] 
50393  578 
fun add_term_pattern feature_of = 
579 
union (op = o pairself fst) o map feature_of oo patternify_term [] 

50583
681edd111e9b
really honor pattern depth, and use 2 by default
blanchet
parents:
50570
diff
changeset

580 
fun add_term_patterns _ 0 _ = I 
50393  581 
 add_term_patterns feature_of depth t = 
582 
add_term_pattern feature_of depth t 

583 
#> add_term_patterns feature_of (depth  1) t 

584 
fun add_term feature_of = add_term_patterns feature_of term_max_depth 

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

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

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

587 
(case head of 
50393  588 
Const (_, T) => add_term const_feature_of t #> add_type T 
589 
 Free (_, T) => add_term free_feature_of t #> add_type T 

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

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

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

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

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

594 
end 
48326  595 
in [] > fold add_patterns ts end 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

596 

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

597 
fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1}) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

598 

50583
681edd111e9b
really honor pattern depth, and use 2 by default
blanchet
parents:
50570
diff
changeset

599 
val term_max_depth = 2 
681edd111e9b
really honor pattern depth, and use 2 by default
blanchet
parents:
50570
diff
changeset

600 
val type_max_depth = 2 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset

601 

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

602 
(* TODO: Generate type classes for types? *) 
48385  603 
fun features_of ctxt prover thy (scope, status) ts = 
50393  604 
let val thy_name = Context.theory_name thy in 
605 
thy_feature_of thy_name :: 

50585  606 
interesting_terms_types_and_classes ctxt prover thy_name term_max_depth 
50393  607 
type_max_depth ts 
608 
> status <> General ? cons (status_feature_of status) 

609 
> scope <> Global ? cons local_feature 

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

611 
> exists (exists_Const is_exists) ts ? cons skos_feature 

612 
end 

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

613 

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

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

615 
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

616 
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

617 

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

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

619 

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

620 
(* "type_definition_xxx" facts are characterized by their use of "CollectI". *) 
50624
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset

621 
val typedef_deps = [@{thm CollectI} > nickname_of_thm] 
48438
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset

622 

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

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

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

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

626 
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

627 
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

628 
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

629 
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

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

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

632 

48441  633 
fun is_size_def [dep] th = 
634 
(case first_field ".recs" dep of 

635 
SOME (pref, _) => 

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

636 
(case first_field ".size" (nickname_of_thm th) of 
48441  637 
SOME (pref', _) => pref = pref' 
638 
 NONE => false) 

639 
 NONE => false) 

640 
 is_size_def _ _ = false 

641 

642 
fun trim_dependencies th deps = 

48668
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset

643 
if length deps > max_dependencies then 
48438
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset

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

645 
else 
48668
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset

646 
SOME (if deps = typedef_deps orelse 
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset

647 
exists (member (op =) typedef_ths) deps orelse 
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset

648 
is_size_def deps th then 
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset

649 
[] 
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset

650 
else 
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset

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

652 

48441  653 
fun isar_dependencies_of all_names th = 
654 
th > thms_in_proof (SOME all_names) > trim_dependencies th 

48404  655 

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

656 
fun prover_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover 
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

657 
auto_level facts all_names th = 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

658 
case isar_dependencies_of all_names th of 
48665  659 
SOME [] => (false, SOME []) 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

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

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

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

663 
val goal = goal_of_thm thy th 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

664 
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

665 
val facts = facts > filter (fn (_, th') => thm_ord (th', th) = LESS) 
50624
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset

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

667 
((fn () => nickname_of_thm th, stature), th) 
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset

668 
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

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

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

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

672 
else case find_first (is_dep dep) facts of 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

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

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

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

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

677 
> mepo_suggested_facts ctxt params prover 
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

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

679 
NONE hyp_ts concl_t 
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

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

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

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

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

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

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

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

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

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

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

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

692 
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

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

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

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

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

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

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

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

701 
(); 
48665  702 
case used_facts > map fst > trim_dependencies th of 
703 
NONE => (false, isar_deps) 

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

704 
 prover_deps => (true, prover_deps)) 
48665  705 
 _ => (false, isar_deps) 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

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

707 

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

708 

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

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

710 

48407  711 
fun num_keys keys = Graph.Keys.fold (K (Integer.add 1)) keys 0 
48400  712 

50610  713 
fun maximal_in_graph access_G facts = 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

715 
val facts = [] > fold (cons o nickname_of_thm o snd) facts 
48407  716 
val tab = Symtab.empty > fold (fn name => Symtab.default (name, ())) facts 
717 
fun insert_new seen name = 

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

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

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

721 
find_maxes 

50610  722 
(seen > num_keys (Graph.imm_succs access_G new) > 1 
48407  723 
? Symtab.default (new, ())) 
724 
(if Symtab.defined tab new then 

725 
let 

50610  726 
val newp = Graph.all_preds access_G [new] 
48407  727 
fun is_ancestor x yp = member (op =) yp x 
728 
val maxs = 

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

730 
in 

731 
if exists (is_ancestor new o fst) maxs then 

732 
(maxs, news) 

733 
else 

734 
((newp, new) 

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

736 
news) 

737 
end 

738 
else 

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

50610  740 
(Graph.imm_preds access_G new) news)) 
741 
in find_maxes Symtab.empty ([], Graph.maximals access_G) end 

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

742 

50610  743 
fun is_fact_in_graph access_G (_, th) = 
50624
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset

744 
can (Graph.get_node access_G) (nickname_of_thm th) 
48320
891a24a48155
improved meshing of MaSh and MengPaulson if some MaSh suggestions are cutoff (the common case)
blanchet
parents:
48319
diff
changeset

745 

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

746 
val weight_raw_mash_facts = weight_mepo_facts 
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

747 
val weight_mash_facts = weight_raw_mash_facts 
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

748 

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

749 
(* FUDGE *) 
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

750 
fun weight_of_proximity_fact rank = 
50398  751 
Math.pow (1.3, 15.5  0.2 * Real.fromInt rank) + 15.0 
50383
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

752 

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

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

754 
facts ~~ map weight_of_proximity_fact (0 upto length facts  1) 
50382  755 

50440
ca99c269ca3a
don't have MaSh pretend it knows facts it doesn't know
blanchet
parents:
50438
diff
changeset

756 
val max_proximity_facts = 100 
ca99c269ca3a
don't have MaSh pretend it knows facts it doesn't know
blanchet
parents:
50438
diff
changeset

757 

ca99c269ca3a
don't have MaSh pretend it knows facts it doesn't know
blanchet
parents:
50438
diff
changeset

758 
fun find_mash_suggestions max_facts suggs facts chained raw_unknown = 
50412  759 
let 
760 
val raw_mash = 

761 
facts > find_suggested_facts suggs 

762 
(* The weights currently returned by "mash.py" are too spaced out to 

763 
make any sense. *) 

764 
> map fst 

50440
ca99c269ca3a
don't have MaSh pretend it knows facts it doesn't know
blanchet
parents:
50438
diff
changeset

765 
val proximity = 
ca99c269ca3a
don't have MaSh pretend it knows facts it doesn't know
blanchet
parents:
50438
diff
changeset

766 
facts > sort (thm_ord o pairself snd o swap) 
ca99c269ca3a
don't have MaSh pretend it knows facts it doesn't know
blanchet
parents:
50438
diff
changeset

767 
> take max_proximity_facts 
50412  768 
val mess = 
50435  769 
[(0.80 (* FUDGE *), (map (rpair 1.0) chained, [])), 
50440
ca99c269ca3a
don't have MaSh pretend it knows facts it doesn't know
blanchet
parents:
50438
diff
changeset

770 
(0.16 (* FUDGE *), (weight_raw_mash_facts raw_mash, raw_unknown)), 
50435  771 
(0.04 (* FUDGE *), (weight_proximity_facts proximity, []))] 
50440
ca99c269ca3a
don't have MaSh pretend it knows facts it doesn't know
blanchet
parents:
50438
diff
changeset

772 
val unknown = 
ca99c269ca3a
don't have MaSh pretend it knows facts it doesn't know
blanchet
parents:
50438
diff
changeset

773 
raw_unknown 
ca99c269ca3a
don't have MaSh pretend it knows facts it doesn't know
blanchet
parents:
50438
diff
changeset

774 
> fold (subtract (Thm.eq_thm_prop o pairself snd)) [chained, proximity] 
ca99c269ca3a
don't have MaSh pretend it knows facts it doesn't know
blanchet
parents:
50438
diff
changeset

775 
in (mesh_facts max_facts mess, unknown) end 
50412  776 

48406  777 
fun mash_suggested_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts 
778 
concl_t facts = 

48301  779 
let 
48302  780 
val thy = Proof_Context.theory_of ctxt 
50610  781 
val (access_G, suggs) = 
782 
peek_state ctxt (fn {access_G, ...} => 

783 
if Graph.is_empty access_G then 

784 
(access_G, []) 

48434
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset

785 
else 
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset

786 
let 
50610  787 
val parents = maximal_in_graph access_G facts 
48434
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset

788 
val feats = 
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset

789 
features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts) 
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset

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

791 
(access_G, MaSh.query ctxt overlord max_facts (parents, feats)) 
48434
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset

792 
end) 
50397
d84a5ab736bb
reduce max number of dependencies for MaSh to get rid of junk
blanchet
parents:
50396
diff
changeset

793 
val chained = facts > filter (fn ((_, (scope, _)), _) => scope = Chained) 
50610  794 
val unknown = facts > filter_out (is_fact_in_graph access_G) 
50412  795 
in find_mash_suggestions max_facts suggs facts chained unknown end 
48249  796 

50631  797 
fun learn_wrt_access_graph ctxt (name, parents, feats, deps) (learns, graph) = 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

798 
let 
50631  799 
fun maybe_learn_from from (accum as (parents, graph)) = 
48321  800 
try_graph ctxt "updating graph" accum (fn () => 
801 
(from :: parents, Graph.add_edge_acyclic (from, name) graph)) 

48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

802 
val graph = graph > Graph.default_node (name, Isar_Proof) 
50631  803 
val (parents, graph) = ([], graph) > fold maybe_learn_from parents 
804 
val (deps, _) = ([], graph) > fold maybe_learn_from deps 

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

48306  806 

50631  807 
fun relearn_wrt_access_graph ctxt (name, deps) (relearns, graph) = 
48668
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset

808 
let 
50631  809 
fun maybe_relearn_from from (accum as (parents, graph)) = 
48668
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset

810 
try_graph ctxt "updating graph" accum (fn () => 
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset

811 
(from :: parents, Graph.add_edge_acyclic (from, name) graph)) 
50610  812 
val graph = graph > update_access_graph_node (name, Automatic_Proof) 
50631  813 
val (deps, _) = ([], graph) > fold maybe_relearn_from deps 
814 
in ((name, deps) :: relearns, graph) end 

48668
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset

815 

50610  816 
fun flop_wrt_access_graph name = 
817 
update_access_graph_node (name, Isar_Proof_wegen_Prover_Flop) 

48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

818 

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

819 
val learn_timeout_slack = 2.0 
48318  820 

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

821 
fun launch_thread timeout task = 
48383  822 
let 
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

823 
val hard_timeout = time_mult learn_timeout_slack timeout 
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

824 
val birth_time = Time.now () 
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

825 
val death_time = Time.+ (birth_time, hard_timeout) 
48442  826 
val desc = ("Machine learner for Sledgehammer", "") 
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

827 
in Async_Manager.launch MaShN birth_time death_time desc task end 
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

828 

48400  829 
fun freshish_name () = 
830 
Date.fmt ".%Y_%m_%d_%H_%M_%S__" (Date.fromTimeLocal (Time.now ())) ^ 

831 
serial_string () 

832 

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

833 
fun mash_learn_proof ctxt ({overlord, timeout, ...} : params) prover t facts 
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

834 
used_ths = 
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

835 
if is_smt_prover ctxt prover then 
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

836 
() 
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

837 
else 
50557  838 
launch_thread (timeout > the_default one_day) (fn () => 
48403
1f214c653c80
don't store fresh names in fact graph, since these cannot be the parents of any other facts
blanchet
parents:
48401
diff
changeset

839 
let 
1f214c653c80
don't store fresh names in fact graph, since these cannot be the parents of any other facts
blanchet
parents:
48401
diff
changeset

840 
val thy = Proof_Context.theory_of ctxt 
1f214c653c80
don't store fresh names in fact graph, since these cannot be the parents of any other facts
blanchet
parents:
48401
diff
changeset

841 
val name = freshish_name () 
1f214c653c80
don't store fresh names in fact graph, since these cannot be the parents of any other facts
blanchet
parents:
48401
diff
changeset

842 
val feats = features_of ctxt prover thy (Local, General) [t] 
50624
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset

843 
val deps = used_ths > map nickname_of_thm 
48403
1f214c653c80
don't store fresh names in fact graph, since these cannot be the parents of any other facts
blanchet
parents:
48401
diff
changeset

844 
in 
50610  845 
peek_state ctxt (fn {access_G, ...} => 
846 
let val parents = maximal_in_graph access_G facts in 

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

847 
MaSh.learn ctxt overlord [(name, parents, feats, deps)] 
48434
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset

848 
end); 
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset

849 
(true, "") 
48403
1f214c653c80
don't store fresh names in fact graph, since these cannot be the parents of any other facts
blanchet
parents:
48401
diff
changeset

850 
end) 
48383  851 

50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50440
diff
changeset

852 
fun sendback sub = Active.sendback_markup (sledgehammerN ^ " " ^ sub) 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

853 

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

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

855 

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

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

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

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

862 
Time.+ (Timer.checkRealTimer timer, commit_timeout) 
50610  863 
val {access_G, ...} = peek_state ctxt I 
50485
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50484
diff
changeset

864 
val facts = facts > sort (thm_ord o pairself snd) 
48400  865 
val (old_facts, new_facts) = 
50610  866 
facts > List.partition (is_fact_in_graph access_G) 
48308  867 
in 
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

868 
if null new_facts andalso (not run_prover orelse null old_facts) then 
48404  869 
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

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

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

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

873 
"\n\nHint: Try " ^ sendback learn_proverN ^ 
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

874 
" to learn from automatic provers." 
48404  875 
else 
876 
"") 

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

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

878 
"" 
48308  879 
else 
48304  880 
let 
50624
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset

881 
val all_names = build_all_names nickname_of_thm facts 
48439
67a6bcbd3587
removed MaSh junk arising from primrec definitions
blanchet
parents:
48438
diff
changeset

882 
fun deps_of status th = 
67a6bcbd3587
removed MaSh junk arising from primrec definitions
blanchet
parents:
48438
diff
changeset

883 
if status = Non_Rec_Def orelse status = Rec_Def then 
67a6bcbd3587
removed MaSh junk arising from primrec definitions
blanchet
parents:
48438
diff
changeset

884 
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

885 
else if 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

886 
prover_dependencies_of ctxt params prover auto_level facts all_names 
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

887 
th 
48665  888 
> (fn (false, _) => NONE  (true, deps) => deps) 
48404  889 
else 
48439
67a6bcbd3587
removed MaSh junk arising from primrec definitions
blanchet
parents:
48438
diff
changeset

890 
isar_dependencies_of all_names th 
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

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

893 
let 
50610  894 
val was_empty = Graph.is_empty access_G 
50631  895 
val (learns, access_G) = 
896 
([], access_G) > fold (learn_wrt_access_graph ctxt) learns 

897 
val (relearns, access_G) = 

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

50610  899 
val access_G = access_G > fold flop_wrt_access_graph flops 
48699  900 
val dirty = 
50631  901 
case (was_empty, dirty, relearns) of 
902 
(false, SOME names, []) => SOME (map #1 learns @ names) 

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

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

906 
MaSh.relearn ctxt overlord relearns; 
50610  907 
{access_G = access_G, dirty = dirty} 
48404  908 
end 
50631  909 
fun commit last learns relearns flops = 
48404  910 
(if debug andalso auto_level = 0 then 
911 
Output.urgent_message "Committing..." 

912 
else 

913 
(); 

50631  914 
map_state ctxt (do_commit (rev learns) relearns flops); 
48404  915 
if not last andalso auto_level = 0 then 
50631  916 
let val num_proofs = length learns + length relearns in 
48404  917 
"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

918 
(if run_prover then "automatic" else "Isar") ^ " proof" ^ 
48404  919 
plural_s num_proofs ^ " in the last " ^ 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

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

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

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

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

924 
()) 
48404  925 
fun learn_new_fact _ (accum as (_, (_, _, _, true))) = accum 
48439
67a6bcbd3587
removed MaSh junk arising from primrec definitions
blanchet
parents:
48438
diff
changeset

926 
 learn_new_fact ((_, stature as (_, status)), th) 
50631  927 
(learns, (parents, n, next_commit, _)) = 
48318  928 
let 
50624
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset

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

930 
val feats = 
48385  931 
features_of ctxt prover (theory_of_thm th) stature [prop_of th] 
48439
67a6bcbd3587
removed MaSh junk arising from primrec definitions
blanchet
parents:
48438
diff
changeset

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

933 
val n = n > not (null deps) ? Integer.add 1 
50631  934 
val learns = (name, parents, feats, deps) :: learns 
935 
val (learns, next_commit) = 

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

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

938 
else 
50631  939 
(learns, next_commit) 
50557  940 
val timed_out = 
941 
case learn_timeout of 

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

943 
 NONE => false 

50631  944 
in (learns, ([name], n, next_commit, timed_out)) end 
48404  945 
val n = 
946 
if null new_facts then 

947 
0 

948 
else 

949 
let 

950 
val last_th = new_facts > List.last > snd 

951 
(* crude approximation *) 

952 
val ancestors = 

953 
old_facts 

954 
> filter (fn (_, th) => thm_ord (th, last_th) <> GREATER) 

50610  955 
val parents = maximal_in_graph access_G ancestors 
50631  956 
val (learns, (_, n, _, _)) = 
48404  957 
([], (parents, 0, next_commit_time (), false)) 
958 
> fold learn_new_fact new_facts 

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

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

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

966 
case deps_of status th of 
50631  967 
SOME deps => (n + 1, (name, deps) :: relearns, flops) 
968 
 NONE => (n, relearns, name :: flops) 

969 
val (relearns, flops, next_commit) = 

48404  970 
if Time.> (Timer.checkRealTimer timer, next_commit) then 
50631  971 
(commit false [] relearns flops; 
972 
([], [], next_commit_time ())) 

48404  973 
else 
50631  974 
(relearns, flops, next_commit) 
50557  975 
val timed_out = 
976 
case learn_timeout of 

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

978 
 NONE => false 

50631  979 
in ((relearns, flops), (n, next_commit, timed_out)) end 
48404  980 
val n = 
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

981 
if not run_prover orelse null old_facts then 
48404  982 
n 
983 
else 

984 
let 

48668
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset

985 
val max_isar = 1000 * max_dependencies 
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

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

987 
try (Graph.get_node access_G) (nickname_of_thm th) 
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

988 
> the_default Isar_Proof 
48406  989 
fun priority_of (_, th) = 
48668
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset

990 
random_range 0 max_isar 
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

991 
+ (case kind_of_proof th of 
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

992 
Isar_Proof => 0 
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

993 
 Automatic_Proof => 2 * max_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

994 
 Isar_Proof_wegen_Prover_Flop => max_isar) 
48404  995 
 500 * (th > isar_dependencies_of all_names 
996 
> Option.map length 

997 
> the_default max_dependencies) 

998 
val old_facts = 

48406  999 
old_facts > map (`priority_of) 
48404  1000 
> sort (int_ord o pairself fst) 
1001 
> map snd 

50631  1002 
val ((relearns, flops), (n, _, _)) = 
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset

1003 
(([], []), (n, next_commit_time (), false)) 
48404  1004 
> fold relearn_old_fact old_facts 
50631  1005 
in commit true [] relearns flops; n end 
48318  1006 
in 
48404  1007 
if verbose orelse auto_level < 2 then 
1008 
"Learned " ^ string_of_int n ^ " nontrivial " ^ 

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

1009 
(if run_prover then "automatic" else "Isar") ^ " proof" ^ plural_s n ^ 
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

1010 
(if verbose then 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

1011 
" in " ^ string_from_time (Timer.checkRealTimer timer) 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

1012 
else 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

1013 
"") ^ "." 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

1014 
else 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

1015 
"" 
48318  1016 
end 
48308  1017 
end 
48304  1018 

48404  1019 
fun mash_learn ctxt (params as {provers, timeout, ...}) fact_override chained 
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

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

1021 
let 
48396  1022 
val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt 
48395
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset

1023 
val ctxt = ctxt > Config.put instantiate_inducts false 
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset

1024 
val facts = 
48396  1025 
nearly_all_facts ctxt false fact_override Symtab.empty css chained [] 
1026 
@{prop True} 

48404  1027 
val num_facts = length facts 
1028 
val prover = hd provers 

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

1029 
fun learn auto_level run_prover = 
50557  1030 
mash_learn_facts ctxt params prover auto_level run_prover NONE facts 
48404  1031 
> Output.urgent_message 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset

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

1033 
if run_prover then 
50340
72519bf5f135
simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents:
50339
diff
changeset

1034 
("MaShing through " ^ string_of_int num_facts ^ " fact" ^ 
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

1035 
plural_s num_facts ^ " for automatic proofs (" ^ quote prover ^ 
50557  1036 
(case timeout of 
1037 
SOME timeout => " timeout: " ^ string_from_time timeout 

1038 
 NONE => "") ^ ").\n\nCollecting Isar proofs first..." 

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

1039 
> Output.urgent_message; 
72519bf5f135
simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents:
50339
diff
changeset

1040 
learn 1 false; 
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

1041 
"Now collecting automatic proofs. This may take several hours. You can \ 
50340
72519bf5f135
simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents:
50339
diff
changeset

1042 
\safely stop the learning process at any point." 
72519bf5f135
simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents:
50339
diff
changeset

1043 
> Output.urgent_message; 
72519bf5f135
simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents:
50339
diff
changeset

1044 
learn 0 true) 
72519bf5f135
simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents:
50339
diff
changeset

1045 
else 
72519bf5f135
simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents:
50339
diff
changeset

1046 
("MaShing through " ^ string_of_int num_facts ^ " fact" ^ 
72519bf5f135
simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents:
50339
diff
changeset

1047 
plural_s num_facts ^ " for Isar proofs..." 
72519bf5f135
simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents:
50339
diff
changeset

1048 
> Output.urgent_message; 
72519bf5f135
simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents:
50339
diff
changeset

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

1050 
end 
48249  1051 

50311  1052 
fun is_mash_enabled () = (getenv "MASH" = "yes") 
50570  1053 
fun mash_can_suggest_facts ctxt = 
50610  1054 
not (Graph.is_empty (#access_G (peek_state ctxt I))) 
50311  1055 

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

1056 
(* Generate more suggestions than requested, because some might be thrown out 
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

1057 
later for various reasons. *) 
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

1058 
fun generous_max_facts max_facts = max_facts + Int.min (50, max_facts) 
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

1059 

48318  1060 
(* The threshold should be large enough so that MaSh doesn't kick in for Auto 
1061 
Sledgehammer and Try. *) 

1062 
val min_secs_for_learning = 15 

1063 

48321  1064 
fun relevant_facts ctxt (params as {learn, fact_filter, timeout, ...}) prover 
1065 
max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts = 

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

1066 
if not (subset (op =) (the_list fact_filter, fact_filters)) then 
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset

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

1068 
else if only then 
48289  1069 
facts 
48321  1070 
else if max_facts <= 0 orelse null facts then 
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset

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

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

1073 
let 
48327
568b3193e53e
don't include hidden facts in relevance filter + tweak MaSh learning
blanchet
parents:
48326
diff
changeset

1074 
fun maybe_learn () = 
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

1075 
if learn andalso not (Async_Manager.has_running_threads MaShN) andalso 
50557  1076 
(timeout = NONE orelse 
1077 
Time.toSeconds (the timeout) >= min_secs_for_learning) then 

1078 
let 

1079 
val timeout = Option.map (time_mult learn_timeout_slack) timeout 

1080 
in 

1081 
launch_thread (timeout > the_default one_day) 

48404  1082 
(fn () => (true, mash_learn_facts ctxt params prover 2 false 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset

1083 
timeout facts)) 
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

1084 
end 
48318  1085 
else 
1086 
() 

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

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

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

1089 
SOME ff => (() > ff <> mepoN ? maybe_learn; ff) 
48318  1090 
 NONE => 
48407  1091 
if is_smt_prover ctxt prover then 
1092 
mepoN 

50229  1093 
else if is_mash_enabled () then 
48407  1094 
(maybe_learn (); 
1095 
if mash_can_suggest_facts ctxt then meshN else mepoN) 

1096 
else 

1097 
mepoN 

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

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

1100 
((facts > filter (member Thm.eq_thm_prop ths o snd)) @ 
48292  1101 
(accepts > filter_out (member Thm.eq_thm_prop ths o snd))) 
48293  1102 
> take max_facts 
48406  1103 
fun mepo () = 
50382  1104 
mepo_suggested_facts ctxt params prover max_facts NONE hyp_ts concl_t 
1105 
facts 

1106 
> weight_mepo_facts 

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

1107 
fun mash () = 
50383
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

1108 
mash_suggested_facts ctxt params prover (generous_max_facts max_facts) 
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset

1109 
hyp_ts concl_t facts 
50440
ca99c269ca3a
don't have MaSh pretend it knows facts it doesn't know
blanchet
parents:
50438
diff
changeset

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

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

1112 
[] > (if fact_filter <> mashN then cons (0.5, (mepo (), [])) else I) 
50440
ca99c269ca3a
don't have MaSh pretend it knows facts it doesn't know
blanchet
parents:
50438
diff
changeset

1113 
> (if fact_filter <> mepoN then cons (0.5, (mash ())) else I) 
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset

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

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

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

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

1118 

48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

1119 
fun kill_learners () = Async_Manager.kill_threads MaShN "learner" 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

1120 
fun running_learners () = Async_Manager.running_threads MaShN "learner" 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset

1121 

48248  1122 
end; 