author | blanchet |
Mon, 03 Dec 2012 20:55:34 +0100 | |
changeset 50335 | b17b05c8d4a4 |
parent 50319 | dddcaeb92e11 |
child 50338 | 73f2f0cd4aea |
permissions | -rw-r--r-- |
48380 | 1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_mash.ML |
48248 | 2 |
Author: Jasmin Blanchette, TU Muenchen |
3 |
||
4 |
Sledgehammer's machine-learning-based 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" (Meng--Paulson)
blanchet
parents:
48378
diff
changeset
|
18 |
val mepoN : string |
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (Meng--Paulson)
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 |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
23 |
val learn_atpN : string |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
24 |
val relearn_isarN : string |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
25 |
val relearn_atpN : 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 string-based
blanchet
parents:
48302
diff
changeset
|
27 |
val escape_meta : string -> string |
f1d135d0ea69
improved MaSh string escaping and make more operations string-based
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 |
|
48406 | 31 |
val extract_query : string -> string * (string * real) list |
50311 | 32 |
val mash_CLEAR : Proof.context -> unit |
33 |
val mash_ADD : |
|
34 |
Proof.context -> bool |
|
35 |
-> (string * string list * string list * string list) list -> unit |
|
36 |
val mash_REPROVE : |
|
37 |
Proof.context -> bool -> (string * string list) list -> unit |
|
38 |
val mash_QUERY : |
|
39 |
Proof.context -> bool -> int -> string list * string list |
|
40 |
-> (string * real) list |
|
41 |
val mash_unlearn : Proof.context -> unit |
|
48378 | 42 |
val nickname_of : thm -> string |
48406 | 43 |
val suggested_facts : |
44 |
(string * 'a) list -> ('b * thm) list -> (('b * thm) * 'a) list |
|
48321 | 45 |
val mesh_facts : |
48406 | 46 |
int -> ((('a * thm) * real) list * ('a * thm) list) list -> ('a * thm) list |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
47 |
val theory_ord : theory * theory -> order |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
48 |
val thm_ord : thm * thm -> order |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
49 |
val goal_of_thm : theory -> thm -> thm |
48321 | 50 |
val run_prover_for_mash : |
48318 | 51 |
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
|
52 |
val features_of : |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
53 |
Proof.context -> string -> theory -> stature -> term list -> string list |
48404 | 54 |
val isar_dependencies_of : unit Symtab.table -> thm -> string list option |
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
55 |
val atp_dependencies_of : |
48404 | 56 |
Proof.context -> params -> string -> int -> fact list -> unit Symtab.table |
48665 | 57 |
-> thm -> bool * string list option |
48406 | 58 |
val mash_suggested_facts : |
48321 | 59 |
Proof.context -> params -> string -> int -> term list -> term |
48435 | 60 |
-> fact list -> (fact * real) list * fact list |
48383 | 61 |
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
|
62 |
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
|
63 |
-> unit |
48395
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset
|
64 |
val mash_learn : |
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset
|
65 |
Proof.context -> params -> fact_override -> thm list -> bool -> unit |
50311 | 66 |
val is_mash_enabled : unit -> bool |
67 |
val mash_can_suggest_facts : Proof.context -> bool |
|
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset
|
68 |
val relevant_facts : |
48292 | 69 |
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
|
70 |
-> 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
|
71 |
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
|
72 |
val running_learners : unit -> unit |
48248 | 73 |
end; |
74 |
||
48381 | 75 |
structure Sledgehammer_MaSh : SLEDGEHAMMER_MASH = |
48248 | 76 |
struct |
48249 | 77 |
|
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
78 |
open ATP_Util |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
79 |
open ATP_Problem_Generate |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
80 |
open Sledgehammer_Util |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
81 |
open Sledgehammer_Fact |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
82 |
open Sledgehammer_Provers |
48318 | 83 |
open Sledgehammer_Minimize |
48381 | 84 |
open Sledgehammer_MePo |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
85 |
|
48308 | 86 |
val trace = |
48380 | 87 |
Attrib.setup_config_bool @{binding sledgehammer_mash_trace} (K false) |
48308 | 88 |
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else () |
89 |
||
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset
|
90 |
val MaShN = "MaSh" |
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset
|
91 |
|
48379
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents:
48378
diff
changeset
|
92 |
val mepoN = "mepo" |
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
93 |
val mashN = "mash" |
48379
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents:
48378
diff
changeset
|
94 |
val meshN = "mesh" |
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
95 |
|
48379
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents:
48378
diff
changeset
|
96 |
val fact_filters = [meshN, mepoN, mashN] |
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
97 |
|
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
98 |
val unlearnN = "unlearn" |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
99 |
val learn_isarN = "learn_isar" |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
100 |
val learn_atpN = "learn_atp" |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
101 |
val relearn_isarN = "relearn_isar" |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
102 |
val relearn_atpN = "relearn_atp" |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
103 |
|
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
|
104 |
fun mash_model_dir () = |
50310 | 105 |
Path.explode "$ISABELLE_HOME_USER/mash" |
106 |
|> 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
|
107 |
val mash_state_dir = mash_model_dir |
50310 | 108 |
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
|
109 |
|
48330 | 110 |
|
50311 | 111 |
(*** Low-level communication with MaSh ***) |
112 |
||
113 |
fun wipe_out_file file = (try (File.rm o Path.explode) file; ()) |
|
114 |
||
50335
b17b05c8d4a4
proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents:
50319
diff
changeset
|
115 |
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
|
116 |
(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
|
117 |
xs |> chunk_list 500 |
b17b05c8d4a4
proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents:
50319
diff
changeset
|
118 |
|> 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
|
119 |
handle IO.Io _ => () |
50311 | 120 |
|
121 |
fun run_mash_tool ctxt overlord save max_suggs write_cmds read_suggs = |
|
122 |
let |
|
123 |
val (temp_dir, serial) = |
|
124 |
if overlord then (getenv "ISABELLE_HOME_USER", "") |
|
125 |
else (getenv "ISABELLE_TMP", serial_string ()) |
|
126 |
val log_file = if overlord then temp_dir ^ "/mash_log" else "/dev/null" |
|
127 |
val err_file = temp_dir ^ "/mash_err" ^ serial |
|
128 |
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
|
129 |
val sugg_path = Path.explode sugg_file |
50311 | 130 |
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
|
131 |
val cmd_path = Path.explode cmd_file |
50311 | 132 |
val core = |
133 |
"--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^ |
|
134 |
" --numberOfPredictions " ^ string_of_int max_suggs ^ |
|
135 |
(if save then " --saveModel" else "") |
|
136 |
val command = |
|
50335
b17b05c8d4a4
proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents:
50319
diff
changeset
|
137 |
"\"$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
|
138 |
File.shell_path (mash_model_dir ()) ^ " --log " ^ log_file ^ " " ^ core ^ |
50311 | 139 |
" >& " ^ err_file |
140 |
|> tap (fn _ => trace_msg ctxt (fn () => |
|
141 |
case try File.read (Path.explode err_file) of |
|
142 |
NONE => "Done" |
|
143 |
| SOME "" => "Done" |
|
144 |
| SOME s => "Error: " ^ elide_string 1000 s)) |
|
145 |
fun run_on () = |
|
146 |
(Isabelle_System.bash command; |
|
50335
b17b05c8d4a4
proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents:
50319
diff
changeset
|
147 |
read_suggs (fn () => try File.read_lines sugg_path |> these)) |
50311 | 148 |
fun clean_up () = |
149 |
if overlord then () |
|
150 |
else List.app wipe_out_file [err_file, sugg_file, cmd_file] |
|
151 |
in |
|
50335
b17b05c8d4a4
proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents:
50319
diff
changeset
|
152 |
write_file (SOME "") ([], K "") sugg_path; |
b17b05c8d4a4
proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents:
50319
diff
changeset
|
153 |
write_file (SOME "") write_cmds cmd_path; |
50311 | 154 |
trace_msg ctxt (fn () => "Running " ^ command); |
155 |
with_cleanup clean_up run_on () |
|
156 |
end |
|
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
157 |
|
48308 | 158 |
fun meta_char c = |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
159 |
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
|
160 |
c = #")" orelse c = #"," then |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
161 |
String.str c |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
162 |
else |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
163 |
(* fixed width, in case more digits follow *) |
48395
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset
|
164 |
"%" ^ stringN_of_int 3 (Char.ord c) |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
165 |
|
48308 | 166 |
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
|
167 |
| unmeta_chars accum (#"%" :: d1 :: d2 :: d3 :: cs) = |
48308 | 168 |
(case Int.fromString (String.implode [d1, d2, d3]) of |
169 |
SOME n => unmeta_chars (Char.chr n :: accum) cs |
|
170 |
| NONE => "" (* error *)) |
|
48395
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset
|
171 |
| unmeta_chars _ (#"%" :: _) = "" (* error *) |
48308 | 172 |
| unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs |
173 |
||
174 |
val escape_meta = String.translate meta_char |
|
48303
f1d135d0ea69
improved MaSh string escaping and make more operations string-based
blanchet
parents:
48302
diff
changeset
|
175 |
val escape_metas = map escape_meta #> space_implode " " |
48315
82d6e46c673f
fixed order of accessibles + other tweaks to MaSh
blanchet
parents:
48314
diff
changeset
|
176 |
val unescape_meta = String.explode #> unmeta_chars [] |
82d6e46c673f
fixed order of accessibles + other tweaks to MaSh
blanchet
parents:
48314
diff
changeset
|
177 |
val unescape_metas = |
82d6e46c673f
fixed order of accessibles + other tweaks to MaSh
blanchet
parents:
48314
diff
changeset
|
178 |
space_explode " " #> filter_out (curry (op =) "") #> map unescape_meta |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
179 |
|
50311 | 180 |
fun str_of_add (name, parents, feats, deps) = |
181 |
"! " ^ escape_meta name ^ ": " ^ escape_metas parents ^ "; " ^ |
|
182 |
escape_metas feats ^ "; " ^ escape_metas deps ^ "\n" |
|
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset
|
183 |
|
50311 | 184 |
fun str_of_reprove (name, deps) = |
185 |
"p " ^ escape_meta name ^ ": " ^ escape_metas deps ^ "\n" |
|
186 |
||
187 |
fun str_of_query (parents, feats) = |
|
188 |
"? " ^ escape_metas parents ^ "; " ^ escape_metas feats ^ "\n" |
|
48406 | 189 |
|
190 |
fun extract_suggestion sugg = |
|
191 |
case space_explode "=" sugg of |
|
192 |
[name, weight] => |
|
193 |
SOME (unescape_meta name, Real.fromString weight |> the_default 0.0) |
|
194 |
| _ => NONE |
|
195 |
||
48311 | 196 |
fun extract_query line = |
197 |
case space_explode ":" line of |
|
48406 | 198 |
[goal, suggs] => |
199 |
(unescape_meta goal, |
|
200 |
map_filter extract_suggestion (space_explode " " suggs)) |
|
48312 | 201 |
| _ => ("", []) |
48311 | 202 |
|
50311 | 203 |
fun mash_CLEAR ctxt = |
204 |
let val path = mash_model_dir () in |
|
205 |
trace_msg ctxt (K "MaSh CLEAR"); |
|
50319
dddcaeb92e11
robust writing of MaSh state -- better drop learning data than cause other problems in Sledgehammer
blanchet
parents:
50311
diff
changeset
|
206 |
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
|
207 |
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
|
208 |
path) NONE; |
50311 | 209 |
() |
210 |
end |
|
211 |
||
212 |
fun mash_ADD _ _ [] = () |
|
213 |
| mash_ADD ctxt overlord adds = |
|
214 |
(trace_msg ctxt (fn () => "MaSh ADD " ^ |
|
215 |
elide_string 1000 (space_implode " " (map #1 adds))); |
|
216 |
run_mash_tool ctxt overlord true 0 (adds, str_of_add) (K ())) |
|
217 |
||
218 |
fun mash_REPROVE _ _ [] = () |
|
219 |
| mash_REPROVE ctxt overlord reps = |
|
220 |
(trace_msg ctxt (fn () => "MaSh REPROVE " ^ |
|
221 |
elide_string 1000 (space_implode " " (map #1 reps))); |
|
222 |
run_mash_tool ctxt overlord true 0 (reps, str_of_reprove) (K ())) |
|
223 |
||
224 |
fun mash_QUERY ctxt overlord max_suggs (query as (_, feats)) = |
|
225 |
(trace_msg ctxt (fn () => "MaSh QUERY " ^ space_implode " " feats); |
|
226 |
run_mash_tool ctxt overlord false max_suggs |
|
227 |
([query], str_of_query) |
|
228 |
(fn suggs => |
|
229 |
case suggs () of |
|
230 |
[] => [] |
|
231 |
| suggs => snd (extract_query (List.last suggs))) |
|
232 |
handle List.Empty => []) |
|
233 |
||
234 |
||
235 |
(*** Middle-level communication with MaSh ***) |
|
236 |
||
237 |
datatype proof_kind = Isar_Proof | ATP_Proof | Isar_Proof_wegen_ATP_Flop |
|
238 |
||
239 |
fun str_of_proof_kind Isar_Proof = "i" |
|
240 |
| str_of_proof_kind ATP_Proof = "a" |
|
241 |
| str_of_proof_kind Isar_Proof_wegen_ATP_Flop = "x" |
|
242 |
||
243 |
fun proof_kind_of_str "i" = Isar_Proof |
|
244 |
| proof_kind_of_str "a" = ATP_Proof |
|
245 |
| proof_kind_of_str "x" = Isar_Proof_wegen_ATP_Flop |
|
246 |
||
247 |
(* FIXME: Here a "Graph.update_node" function would be useful *) |
|
248 |
fun update_fact_graph_node (name, kind) = |
|
249 |
Graph.default_node (name, Isar_Proof) |
|
250 |
#> kind <> Isar_Proof ? Graph.map_node name (K kind) |
|
251 |
||
252 |
fun try_graph ctxt when def f = |
|
253 |
f () |
|
254 |
handle Graph.CYCLES (cycle :: _) => |
|
255 |
(trace_msg ctxt (fn () => |
|
256 |
"Cycle involving " ^ commas cycle ^ " when " ^ when); def) |
|
257 |
| Graph.DUP name => |
|
258 |
(trace_msg ctxt (fn () => |
|
259 |
"Duplicate fact " ^ quote name ^ " when " ^ when); def) |
|
260 |
| Graph.UNDEF name => |
|
261 |
(trace_msg ctxt (fn () => |
|
262 |
"Unknown fact " ^ quote name ^ " when " ^ when); def) |
|
263 |
| exn => |
|
264 |
if Exn.is_interrupt exn then |
|
265 |
reraise exn |
|
266 |
else |
|
267 |
(trace_msg ctxt (fn () => |
|
268 |
"Internal error when " ^ when ^ ":\n" ^ |
|
269 |
ML_Compiler.exn_message exn); def) |
|
270 |
||
271 |
fun graph_info G = |
|
272 |
string_of_int (length (Graph.keys G)) ^ " node(s), " ^ |
|
273 |
string_of_int (fold (Integer.add o length o snd) (Graph.dest G) 0) ^ |
|
274 |
" edge(s), " ^ |
|
275 |
string_of_int (length (Graph.minimals G)) ^ " minimal, " ^ |
|
276 |
string_of_int (length (Graph.maximals G)) ^ " maximal" |
|
277 |
||
278 |
type mash_state = {fact_G : unit Graph.T, dirty : string list option} |
|
279 |
||
280 |
val empty_state = {fact_G = Graph.empty, dirty = SOME []} |
|
281 |
||
282 |
local |
|
283 |
||
284 |
val version = "*** MaSh 0.0 ***" |
|
285 |
||
286 |
fun extract_node line = |
|
287 |
case space_explode ":" line of |
|
288 |
[head, parents] => |
|
289 |
(case space_explode " " head of |
|
290 |
[kind, name] => |
|
291 |
SOME (unescape_meta name, unescape_metas parents, |
|
292 |
try proof_kind_of_str kind |> the_default Isar_Proof) |
|
293 |
| _ => NONE) |
|
294 |
| _ => NONE |
|
295 |
||
296 |
fun load _ (state as (true, _)) = state |
|
297 |
| load ctxt _ = |
|
298 |
let val path = mash_state_file () in |
|
299 |
(true, |
|
300 |
case try File.read_lines path of |
|
301 |
SOME (version' :: node_lines) => |
|
302 |
let |
|
303 |
fun add_edge_to name parent = |
|
304 |
Graph.default_node (parent, Isar_Proof) |
|
305 |
#> Graph.add_edge (parent, name) |
|
306 |
fun add_node line = |
|
307 |
case extract_node line of |
|
308 |
NONE => I (* shouldn't happen *) |
|
309 |
| SOME (name, parents, kind) => |
|
310 |
update_fact_graph_node (name, kind) |
|
311 |
#> fold (add_edge_to name) parents |
|
312 |
val fact_G = |
|
313 |
try_graph ctxt "loading state" Graph.empty (fn () => |
|
314 |
Graph.empty |> version' = version ? fold add_node node_lines) |
|
315 |
in |
|
316 |
trace_msg ctxt (fn () => |
|
317 |
"Loaded fact graph (" ^ graph_info fact_G ^ ")"); |
|
318 |
{fact_G = fact_G, dirty = SOME []} |
|
319 |
end |
|
320 |
| _ => empty_state) |
|
321 |
end |
|
322 |
||
323 |
fun save _ (state as {dirty = SOME [], ...}) = state |
|
324 |
| save ctxt {fact_G, dirty} = |
|
325 |
let |
|
326 |
fun str_of_entry (name, parents, kind) = |
|
327 |
str_of_proof_kind kind ^ " " ^ escape_meta name ^ ": " ^ |
|
328 |
escape_metas parents ^ "\n" |
|
329 |
fun append_entry (name, (kind, (parents, _))) = |
|
330 |
cons (name, Graph.Keys.dest parents, kind) |
|
331 |
val (banner, entries) = |
|
332 |
case dirty of |
|
333 |
SOME names => |
|
334 |
(NONE, fold (append_entry o Graph.get_entry fact_G) names []) |
|
335 |
| NONE => (SOME (version ^ "\n"), Graph.fold append_entry fact_G []) |
|
336 |
in |
|
50335
b17b05c8d4a4
proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents:
50319
diff
changeset
|
337 |
write_file banner (entries, str_of_entry) (mash_state_file ()); |
50311 | 338 |
trace_msg ctxt (fn () => |
339 |
"Saved fact graph (" ^ graph_info fact_G ^ |
|
340 |
(case dirty of |
|
341 |
SOME dirty => |
|
342 |
"; " ^ string_of_int (length dirty) ^ " dirty fact(s)" |
|
343 |
| _ => "") ^ ")"); |
|
344 |
{fact_G = fact_G, dirty = SOME []} |
|
345 |
end |
|
346 |
||
347 |
val global_state = |
|
348 |
Synchronized.var "Sledgehammer_MaSh.global_state" (false, empty_state) |
|
349 |
||
350 |
in |
|
351 |
||
352 |
fun mash_map ctxt f = |
|
353 |
Synchronized.change global_state (load ctxt ##> (f #> save ctxt)) |
|
354 |
||
355 |
fun mash_peek ctxt f = |
|
356 |
Synchronized.change_result global_state (load ctxt #> `snd #>> f) |
|
357 |
||
358 |
fun mash_get ctxt = |
|
359 |
Synchronized.change_result global_state (load ctxt #> `snd) |
|
360 |
||
361 |
fun mash_unlearn ctxt = |
|
362 |
Synchronized.change global_state (fn _ => |
|
363 |
(mash_CLEAR ctxt; (* also removes the state file *) |
|
364 |
(true, empty_state))) |
|
365 |
||
366 |
end |
|
367 |
||
368 |
||
369 |
(*** Isabelle helpers ***) |
|
370 |
||
48378 | 371 |
fun parent_of_local_thm th = |
372 |
let |
|
373 |
val thy = th |> Thm.theory_of_thm |
|
374 |
val facts = thy |> Global_Theory.facts_of |
|
375 |
val space = facts |> Facts.space_of |
|
376 |
fun id_of s = #id (Name_Space.the_entry space s) |
|
377 |
fun max_id (s', _) (s, id) = |
|
378 |
let val id' = id_of s' in if id > id' then (s, id) else (s', id') end |
|
379 |
in ("", ~1) |> Facts.fold_static max_id facts |> fst end |
|
380 |
||
381 |
val local_prefix = "local" ^ Long_Name.separator |
|
382 |
||
383 |
fun nickname_of 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
|
384 |
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
|
385 |
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
|
386 |
(* 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
|
387 |
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
|
388 |
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
|
389 |
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
|
390 |
| 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
|
391 |
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
|
392 |
else |
50047
45684acf0b94
thread context correctly when printing backquoted facts
blanchet
parents:
49997
diff
changeset
|
393 |
backquote_thm (Proof_Context.init_global (Thm.theory_of_thm th)) th |
48378 | 394 |
|
48330 | 395 |
fun suggested_facts suggs facts = |
396 |
let |
|
48378 | 397 |
fun add_fact (fact as (_, th)) = Symtab.default (nickname_of th, fact) |
48330 | 398 |
val tab = Symtab.empty |> fold add_fact facts |
48406 | 399 |
fun find_sugg (name, weight) = |
400 |
Symtab.lookup tab name |> Option.map (rpair weight) |
|
401 |
in map_filter find_sugg suggs end |
|
48311 | 402 |
|
48406 | 403 |
fun sum_avg [] = 0 |
48407 | 404 |
| sum_avg xs = |
405 |
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
|
406 |
|
48406 | 407 |
fun normalize_scores [] = [] |
408 |
| normalize_scores ((fact, score) :: tail) = |
|
409 |
(fact, 1.0) :: map (apsnd (curry Real.* (1.0 / score))) tail |
|
48313
0faafdffa662
mesh facts by taking into consideration whether a fact is known to MeSh
blanchet
parents:
48312
diff
changeset
|
410 |
|
48406 | 411 |
fun mesh_facts max_facts [(sels, unks)] = |
412 |
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
|
413 |
| mesh_facts max_facts mess = |
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
414 |
let |
48406 | 415 |
val mess = mess |> map (apfst (normalize_scores #> `length)) |
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
416 |
val fact_eq = Thm.eq_thm o pairself snd |
48406 | 417 |
fun score_at sels = try (nth sels) #> Option.map snd |
48320
891a24a48155
improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
blanchet
parents:
48319
diff
changeset
|
418 |
fun score_in fact ((sel_len, sels), unks) = |
48406 | 419 |
case find_index (curry fact_eq fact o fst) sels of |
48320
891a24a48155
improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
blanchet
parents:
48319
diff
changeset
|
420 |
~1 => (case find_index (curry fact_eq fact) unks of |
48406 | 421 |
~1 => score_at sels sel_len |
48320
891a24a48155
improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
blanchet
parents:
48319
diff
changeset
|
422 |
| _ => NONE) |
48406 | 423 |
| rank => score_at sels rank |
424 |
fun weight_of fact = mess |> map_filter (score_in fact) |> sum_avg |
|
425 |
val facts = |
|
426 |
fold (union fact_eq o map fst o take max_facts o snd o fst) mess [] |
|
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
427 |
in |
48406 | 428 |
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
|
429 |
|> map snd |> take max_facts |
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
430 |
end |
48312 | 431 |
|
48395
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset
|
432 |
val thy_feature_name_of = prefix "y" |
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset
|
433 |
val const_name_of = prefix "c" |
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset
|
434 |
val type_name_of = prefix "t" |
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset
|
435 |
val class_name_of = prefix "s" |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
436 |
|
48324 | 437 |
fun theory_ord p = |
438 |
if Theory.eq_thy p then |
|
439 |
EQUAL |
|
440 |
else if Theory.subthy p then |
|
441 |
LESS |
|
442 |
else if Theory.subthy (swap p) then |
|
443 |
GREATER |
|
444 |
else case int_ord (pairself (length o Theory.ancestors_of) p) of |
|
445 |
EQUAL => string_ord (pairself Context.theory_name p) |
|
446 |
| order => order |
|
447 |
||
448 |
val thm_ord = theory_ord o pairself theory_of_thm |
|
449 |
||
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
450 |
val freezeT = Type.legacy_freeze_type |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
451 |
|
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
452 |
fun freeze (t $ u) = freeze t $ freeze u |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
453 |
| 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
|
454 |
| freeze (Var ((s, _), T)) = Free (s, freezeT T) |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
455 |
| freeze (Const (s, T)) = Const (s, freezeT T) |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
456 |
| freeze (Free (s, T)) = Free (s, freezeT T) |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
457 |
| freeze t = t |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
458 |
|
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
459 |
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
|
460 |
|
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
461 |
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
|
462 |
let |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
463 |
val problem = |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
464 |
{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
|
465 |
facts = facts |> map (apfst (apfst (fn name => name ()))) |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
466 |
|> map Untranslated_Fact} |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
467 |
in |
48399
4bacc8983b3d
learn from SMT proofs when they can be minimized by Metis
blanchet
parents:
48398
diff
changeset
|
468 |
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
|
469 |
problem |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
470 |
end |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
471 |
|
48326 | 472 |
val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}] |
473 |
||
48398 | 474 |
val logical_consts = |
475 |
[@{const_name prop}, @{const_name Pure.conjunction}] @ atp_logical_consts |
|
476 |
||
48318 | 477 |
fun interesting_terms_types_and_classes ctxt prover term_max_depth |
478 |
type_max_depth ts = |
|
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
479 |
let |
48318 | 480 |
fun is_bad_const (x as (s, _)) args = |
48398 | 481 |
member (op =) logical_consts s orelse |
48318 | 482 |
fst (is_built_in_const_for_prover ctxt prover x args) |
48304 | 483 |
fun add_classes @{sort type} = I |
484 |
| add_classes S = union (op =) (map class_name_of S) |
|
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
485 |
fun do_add_type (Type (s, Ts)) = |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
486 |
(not (member (op =) bad_types s) ? insert (op =) (type_name_of s)) |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
487 |
#> fold do_add_type Ts |
48304 | 488 |
| do_add_type (TFree (_, S)) = add_classes S |
489 |
| do_add_type (TVar (_, S)) = add_classes S |
|
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
490 |
fun add_type T = type_max_depth >= 0 ? do_add_type T |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
491 |
fun mk_app s args = |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
492 |
if member (op <>) args "" then s ^ "(" ^ space_implode "," args ^ ")" |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
493 |
else s |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
494 |
fun patternify ~1 _ = "" |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
495 |
| patternify depth t = |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
496 |
case strip_comb t of |
48398 | 497 |
(Const (x as (s, _)), args) => |
498 |
if is_bad_const x args then "" |
|
499 |
else mk_app (const_name_of s) (map (patternify (depth - 1)) args) |
|
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
500 |
| _ => "" |
48406 | 501 |
fun add_pattern depth t = |
502 |
case patternify depth t of "" => I | s => insert (op =) s |
|
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
503 |
fun add_term_patterns ~1 _ = I |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
504 |
| add_term_patterns depth t = |
48406 | 505 |
add_pattern depth t #> add_term_patterns (depth - 1) t |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
506 |
val add_term = add_term_patterns term_max_depth |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
507 |
fun add_patterns t = |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
508 |
let val (head, args) = strip_comb t in |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
509 |
(case head of |
48398 | 510 |
Const (_, T) => add_term t #> add_type T |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
511 |
| Free (_, T) => add_type T |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
512 |
| Var (_, T) => add_type T |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
513 |
| Abs (_, T, body) => add_type T #> add_patterns body |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
514 |
| _ => I) |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
515 |
#> fold add_patterns args |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
516 |
end |
48326 | 517 |
in [] |> fold add_patterns ts end |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
518 |
|
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
519 |
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
|
520 |
|
48297 | 521 |
val term_max_depth = 1 |
522 |
val type_max_depth = 1 |
|
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
523 |
|
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
524 |
(* TODO: Generate type classes for types? *) |
48385 | 525 |
fun features_of ctxt prover thy (scope, status) ts = |
48303
f1d135d0ea69
improved MaSh string escaping and make more operations string-based
blanchet
parents:
48302
diff
changeset
|
526 |
thy_feature_name_of (Context.theory_name thy) :: |
48318 | 527 |
interesting_terms_types_and_classes ctxt prover term_max_depth type_max_depth |
528 |
ts |
|
48332
271a4a6af734
optimize parent computation in MaSh + remove temporary files
blanchet
parents:
48330
diff
changeset
|
529 |
|> forall is_lambda_free ts ? cons "no_lams" |
271a4a6af734
optimize parent computation in MaSh + remove temporary files
blanchet
parents:
48330
diff
changeset
|
530 |
|> forall (not o exists_Const is_exists) ts ? cons "no_skos" |
48385 | 531 |
|> scope <> Global ? cons "local" |
48438
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset
|
532 |
|> (case string_of_status status of "" => I | s => cons s) |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
533 |
|
48665 | 534 |
(* Too many dependencies is a sign that a crazy decision procedure is at work. |
535 |
There isn't much to learn from such proofs. *) |
|
536 |
val max_dependencies = 100 |
|
537 |
val atp_dependency_default_max_facts = 50 |
|
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
538 |
|
48438
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset
|
539 |
(* "type_definition_xxx" facts are characterized by their use of "CollectI". *) |
48441 | 540 |
val typedef_deps = [@{thm CollectI} |> nickname_of] |
48438
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset
|
541 |
|
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset
|
542 |
(* "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
|
543 |
val typedef_ths = |
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset
|
544 |
@{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
|
545 |
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
|
546 |
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
|
547 |
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
|
548 |
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
|
549 |
type_definition.Abs_image} |
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset
|
550 |
|> map nickname_of |
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset
|
551 |
|
48441 | 552 |
fun is_size_def [dep] th = |
553 |
(case first_field ".recs" dep of |
|
554 |
SOME (pref, _) => |
|
555 |
(case first_field ".size" (nickname_of th) of |
|
556 |
SOME (pref', _) => pref = pref' |
|
557 |
| NONE => false) |
|
558 |
| NONE => false) |
|
559 |
| is_size_def _ _ = false |
|
560 |
||
561 |
fun trim_dependencies th deps = |
|
48668
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset
|
562 |
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
|
563 |
NONE |
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset
|
564 |
else |
48668
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset
|
565 |
SOME (if deps = typedef_deps orelse |
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset
|
566 |
exists (member (op =) typedef_ths) deps orelse |
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset
|
567 |
is_size_def deps th then |
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset
|
568 |
[] |
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset
|
569 |
else |
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset
|
570 |
deps) |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
571 |
|
48441 | 572 |
fun isar_dependencies_of all_names th = |
573 |
th |> thms_in_proof (SOME all_names) |> trim_dependencies th |
|
48404 | 574 |
|
575 |
fun atp_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover |
|
576 |
auto_level facts all_names th = |
|
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
577 |
case isar_dependencies_of all_names th of |
48665 | 578 |
SOME [] => (false, SOME []) |
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
579 |
| isar_deps => |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
580 |
let |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
581 |
val thy = Proof_Context.theory_of ctxt |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
582 |
val goal = goal_of_thm thy th |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
583 |
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
|
584 |
val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
585 |
fun fix_name ((_, stature), th) = ((fn () => nickname_of th, stature), th) |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
586 |
fun is_dep dep (_, th) = nickname_of th = dep |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
587 |
fun add_isar_dep facts dep accum = |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
588 |
if exists (is_dep dep) accum then |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
589 |
accum |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
590 |
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
|
591 |
SOME ((name, status), th) => accum @ [((name, status), th)] |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
592 |
| NONE => accum (* shouldn't happen *) |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
593 |
val facts = |
48406 | 594 |
facts |> mepo_suggested_facts ctxt params prover |
48665 | 595 |
(max_facts |> the_default atp_dependency_default_max_facts) |
48404 | 596 |
NONE hyp_ts concl_t |
597 |
|> fold (add_isar_dep facts) (these isar_deps) |
|
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
598 |
|> map fix_name |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
599 |
in |
48404 | 600 |
if verbose andalso auto_level = 0 then |
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
601 |
let val num_facts = length facts in |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
602 |
"MaSh: " ^ quote prover ^ " on " ^ quote (nickname_of th) ^ |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
603 |
" 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
|
604 |
"." |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
605 |
|> Output.urgent_message |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
606 |
end |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
607 |
else |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
608 |
(); |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
609 |
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
|
610 |
{outcome = NONE, used_facts, ...} => |
48404 | 611 |
(if verbose andalso auto_level = 0 then |
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
612 |
let val num_facts = length used_facts in |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
613 |
"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
|
614 |
plural_s num_facts ^ "." |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
615 |
|> Output.urgent_message |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
616 |
end |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
617 |
else |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
618 |
(); |
48665 | 619 |
case used_facts |> map fst |> trim_dependencies th of |
620 |
NONE => (false, isar_deps) |
|
621 |
| atp_deps => (true, atp_deps)) |
|
622 |
| _ => (false, isar_deps) |
|
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
623 |
end |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
624 |
|
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
625 |
|
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
626 |
(*** High-level communication with MaSh ***) |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
627 |
|
48407 | 628 |
fun num_keys keys = Graph.Keys.fold (K (Integer.add 1)) keys 0 |
48400 | 629 |
|
48407 | 630 |
fun maximal_in_graph fact_G facts = |
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
631 |
let |
48378 | 632 |
val facts = [] |> fold (cons o nickname_of o snd) facts |
48407 | 633 |
val tab = Symtab.empty |> fold (fn name => Symtab.default (name, ())) facts |
634 |
fun insert_new seen name = |
|
635 |
not (Symtab.defined seen name) ? insert (op =) name |
|
636 |
fun find_maxes _ (maxs, []) = map snd maxs |
|
637 |
| find_maxes seen (maxs, new :: news) = |
|
638 |
find_maxes |
|
639 |
(seen |> num_keys (Graph.imm_succs fact_G new) > 1 |
|
640 |
? Symtab.default (new, ())) |
|
641 |
(if Symtab.defined tab new then |
|
642 |
let |
|
643 |
val newp = Graph.all_preds fact_G [new] |
|
644 |
fun is_ancestor x yp = member (op =) yp x |
|
645 |
val maxs = |
|
646 |
maxs |> filter (fn (_, max) => not (is_ancestor max newp)) |
|
647 |
in |
|
648 |
if exists (is_ancestor new o fst) maxs then |
|
649 |
(maxs, news) |
|
650 |
else |
|
651 |
((newp, new) |
|
652 |
:: filter_out (fn (_, max) => is_ancestor max newp) maxs, |
|
653 |
news) |
|
654 |
end |
|
655 |
else |
|
656 |
(maxs, Graph.Keys.fold (insert_new seen) |
|
657 |
(Graph.imm_preds fact_G new) news)) |
|
658 |
in find_maxes Symtab.empty ([], Graph.maximals fact_G) end |
|
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
659 |
|
48318 | 660 |
(* Generate more suggestions than requested, because some might be thrown out |
661 |
later for various reasons and "meshing" gives better results with some |
|
662 |
slack. *) |
|
48434
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset
|
663 |
fun max_suggs_of max_facts = max_facts + Int.min (50, max_facts) |
48318 | 664 |
|
48400 | 665 |
fun is_fact_in_graph fact_G (_, th) = |
666 |
can (Graph.get_node fact_G) (nickname_of th) |
|
48320
891a24a48155
improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
blanchet
parents:
48319
diff
changeset
|
667 |
|
48442 | 668 |
fun interleave 0 _ _ = [] |
669 |
| interleave n [] ys = take n ys |
|
670 |
| interleave n xs [] = take n xs |
|
671 |
| interleave 1 (x :: _) _ = [x] |
|
672 |
| interleave n (x :: xs) (y :: ys) = x :: y :: interleave (n - 2) xs ys |
|
48435 | 673 |
|
48406 | 674 |
fun mash_suggested_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts |
675 |
concl_t facts = |
|
48301 | 676 |
let |
48302 | 677 |
val thy = Proof_Context.theory_of ctxt |
48434
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset
|
678 |
val (fact_G, suggs) = |
48699 | 679 |
mash_peek ctxt (fn {fact_G, ...} => |
48434
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset
|
680 |
if Graph.is_empty fact_G then |
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset
|
681 |
(fact_G, []) |
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset
|
682 |
else |
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset
|
683 |
let |
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset
|
684 |
val parents = maximal_in_graph fact_G facts |
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset
|
685 |
val feats = |
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset
|
686 |
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
|
687 |
in |
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset
|
688 |
(fact_G, mash_QUERY ctxt overlord (max_suggs_of max_facts) |
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset
|
689 |
(parents, feats)) |
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset
|
690 |
end) |
48435 | 691 |
val sels = |
48408 | 692 |
facts |> suggested_facts suggs |
693 |
(* The weights currently returned by "mash.py" are too extreme to |
|
694 |
make any sense. *) |
|
48435 | 695 |
|> map fst |
696 |
val (unk_global, unk_local) = |
|
697 |
facts |> filter_out (is_fact_in_graph fact_G) |
|
48442 | 698 |
|> List.partition (fn ((_, (scope, _)), _) => scope = Global) |
699 |
in (interleave max_facts unk_local sels |> weight_mepo_facts, unk_global) end |
|
48249 | 700 |
|
48668
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset
|
701 |
fun add_wrt_fact_graph ctxt (name, parents, feats, deps) (adds, graph) = |
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
702 |
let |
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
703 |
fun maybe_add_from from (accum as (parents, graph)) = |
48321 | 704 |
try_graph ctxt "updating graph" accum (fn () => |
705 |
(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
|
706 |
val graph = graph |> Graph.default_node (name, Isar_Proof) |
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
707 |
val (parents, graph) = ([], graph) |> fold maybe_add_from parents |
48407 | 708 |
val (deps, _) = ([], graph) |> fold maybe_add_from deps |
48404 | 709 |
in ((name, parents, feats, deps) :: adds, graph) end |
48306 | 710 |
|
48668
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset
|
711 |
fun reprove_wrt_fact_graph ctxt (name, deps) (reps, graph) = |
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset
|
712 |
let |
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset
|
713 |
fun maybe_rep_from from (accum as (parents, graph)) = |
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset
|
714 |
try_graph ctxt "updating graph" accum (fn () => |
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset
|
715 |
(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
|
716 |
val graph = graph |> update_fact_graph_node (name, ATP_Proof) |
48668
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset
|
717 |
val (deps, _) = ([], graph) |> fold maybe_rep_from deps |
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset
|
718 |
in ((name, deps) :: reps, graph) end |
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset
|
719 |
|
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset
|
720 |
fun flop_wrt_fact_graph name = |
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset
|
721 |
update_fact_graph_node (name, Isar_Proof_wegen_ATP_Flop) |
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset
|
722 |
|
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
|
723 |
val learn_timeout_slack = 2.0 |
48318 | 724 |
|
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
|
725 |
fun launch_thread timeout task = |
48383 | 726 |
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
|
727 |
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
|
728 |
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
|
729 |
val death_time = Time.+ (birth_time, hard_timeout) |
48442 | 730 |
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
|
731 |
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
|
732 |
|
48400 | 733 |
fun freshish_name () = |
734 |
Date.fmt ".%Y_%m_%d_%H_%M_%S__" (Date.fromTimeLocal (Time.now ())) ^ |
|
735 |
serial_string () |
|
736 |
||
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
|
737 |
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
|
738 |
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
|
739 |
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
|
740 |
() |
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
|
741 |
else |
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
|
742 |
launch_thread timeout (fn () => |
1f214c653c80
don't store fresh names in fact graph, since these cannot be the parents of any other facts
blanchet
parents:
48401
diff
changeset
|
743 |
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
|
744 |
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
|
745 |
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
|
746 |
val feats = features_of ctxt prover thy (Local, General) [t] |
1f214c653c80
don't store fresh names in fact graph, since these cannot be the parents of any other facts
blanchet
parents:
48401
diff
changeset
|
747 |
val deps = used_ths |> map nickname_of |
1f214c653c80
don't store fresh names in fact graph, since these cannot be the parents of any other facts
blanchet
parents:
48401
diff
changeset
|
748 |
in |
48699 | 749 |
mash_peek ctxt (fn {fact_G, ...} => |
48434
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset
|
750 |
let val parents = maximal_in_graph fact_G facts in |
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset
|
751 |
mash_ADD ctxt overlord [(name, parents, feats, deps)] |
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset
|
752 |
end); |
aaaec69db3db
ensure all calls to "mash" program are synchronous
blanchet
parents:
48433
diff
changeset
|
753 |
(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
|
754 |
end) |
48383 | 755 |
|
50163
c62ce309dc26
more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
50047
diff
changeset
|
756 |
fun sendback sub = Sendback.markup (sledgehammerN ^ " " ^ sub) |
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
757 |
|
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
758 |
val commit_timeout = seconds 30.0 |
48332
271a4a6af734
optimize parent computation in MaSh + remove temporary files
blanchet
parents:
48330
diff
changeset
|
759 |
|
48318 | 760 |
(* The timeout is understood in a very slack fashion. *) |
48404 | 761 |
fun mash_learn_facts ctxt (params as {debug, verbose, overlord, ...}) prover |
762 |
auto_level atp learn_timeout facts = |
|
48304 | 763 |
let |
48318 | 764 |
val timer = Timer.startRealTimer () |
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
765 |
fun next_commit_time () = |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
766 |
Time.+ (Timer.checkRealTimer timer, commit_timeout) |
48699 | 767 |
val {fact_G, ...} = mash_get ctxt |
48400 | 768 |
val (old_facts, new_facts) = |
48667
ac58317ef11f
rule out same "technical" theories for MePo as for MaSh
blanchet
parents:
48665
diff
changeset
|
769 |
facts |> List.partition (is_fact_in_graph fact_G) |
48400 | 770 |
||> sort (thm_ord o pairself snd) |
48308 | 771 |
in |
48404 | 772 |
if null new_facts andalso (not atp orelse null old_facts) then |
773 |
if auto_level < 2 then |
|
774 |
"No new " ^ (if atp then "ATP" else "Isar") ^ " proofs to learn." ^ |
|
775 |
(if auto_level = 0 andalso not atp then |
|
776 |
"\n\nHint: Try " ^ sendback learn_atpN ^ " to learn from ATP proofs." |
|
777 |
else |
|
778 |
"") |
|
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
779 |
else |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
780 |
"" |
48308 | 781 |
else |
48304 | 782 |
let |
48315
82d6e46c673f
fixed order of accessibles + other tweaks to MaSh
blanchet
parents:
48314
diff
changeset
|
783 |
val all_names = |
49997
dbbf9578e712
made MaSh more robust in the face of duplicate "nicknames" (which can happen e.g. if you have a lemma called foo(1) and another called foo_1 in the same theory)
blanchet
parents:
48699
diff
changeset
|
784 |
Symtab.empty |
dbbf9578e712
made MaSh more robust in the face of duplicate "nicknames" (which can happen e.g. if you have a lemma called foo(1) and another called foo_1 in the same theory)
blanchet
parents:
48699
diff
changeset
|
785 |
|> fold Symtab.update (facts |> map (rpair () o nickname_of o snd)) |
48439
67a6bcbd3587
removed MaSh junk arising from primrec definitions
blanchet
parents:
48438
diff
changeset
|
786 |
fun deps_of status th = |
67a6bcbd3587
removed MaSh junk arising from primrec definitions
blanchet
parents:
48438
diff
changeset
|
787 |
if status = Non_Rec_Def orelse status = Rec_Def then |
67a6bcbd3587
removed MaSh junk arising from primrec definitions
blanchet
parents:
48438
diff
changeset
|
788 |
SOME [] |
67a6bcbd3587
removed MaSh junk arising from primrec definitions
blanchet
parents:
48438
diff
changeset
|
789 |
else if atp then |
67a6bcbd3587
removed MaSh junk arising from primrec definitions
blanchet
parents:
48438
diff
changeset
|
790 |
atp_dependencies_of ctxt params prover auto_level facts all_names th |
48665 | 791 |
|> (fn (false, _) => NONE | (true, deps) => deps) |
48404 | 792 |
else |
48439
67a6bcbd3587
removed MaSh junk arising from primrec definitions
blanchet
parents:
48438
diff
changeset
|
793 |
isar_dependencies_of all_names th |
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset
|
794 |
fun do_commit [] [] [] state = state |
48699 | 795 |
| do_commit adds reps flops {fact_G, dirty} = |
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
796 |
let |
48699 | 797 |
val was_empty = Graph.is_empty fact_G |
48404 | 798 |
val (adds, fact_G) = |
48668
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset
|
799 |
([], fact_G) |> fold (add_wrt_fact_graph ctxt) adds |
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset
|
800 |
val (reps, fact_G) = |
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset
|
801 |
([], fact_G) |> fold (reprove_wrt_fact_graph ctxt) reps |
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset
|
802 |
val fact_G = fact_G |> fold flop_wrt_fact_graph flops |
48699 | 803 |
val dirty = |
804 |
case (was_empty, dirty, reps) of |
|
805 |
(false, SOME names, []) => SOME (map #1 adds @ names) |
|
806 |
| _ => NONE |
|
48404 | 807 |
in |
808 |
mash_ADD ctxt overlord (rev adds); |
|
809 |
mash_REPROVE ctxt overlord reps; |
|
48699 | 810 |
{fact_G = fact_G, dirty = dirty} |
48404 | 811 |
end |
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset
|
812 |
fun commit last adds reps flops = |
48404 | 813 |
(if debug andalso auto_level = 0 then |
814 |
Output.urgent_message "Committing..." |
|
815 |
else |
|
816 |
(); |
|
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset
|
817 |
mash_map ctxt (do_commit (rev adds) reps flops); |
48404 | 818 |
if not last andalso auto_level = 0 then |
819 |
let val num_proofs = length adds + length reps in |
|
820 |
"Learned " ^ string_of_int num_proofs ^ " " ^ |
|
821 |
(if atp then "ATP" else "Isar") ^ " proof" ^ |
|
822 |
plural_s num_proofs ^ " in the last " ^ |
|
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
823 |
string_from_time commit_timeout ^ "." |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
824 |
|> Output.urgent_message |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
825 |
end |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
826 |
else |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
827 |
()) |
48404 | 828 |
fun learn_new_fact _ (accum as (_, (_, _, _, true))) = accum |
48439
67a6bcbd3587
removed MaSh junk arising from primrec definitions
blanchet
parents:
48438
diff
changeset
|
829 |
| learn_new_fact ((_, stature as (_, status)), th) |
48404 | 830 |
(adds, (parents, n, next_commit, _)) = |
48318 | 831 |
let |
48378 | 832 |
val name = nickname_of th |
48332
271a4a6af734
optimize parent computation in MaSh + remove temporary files
blanchet
parents:
48330
diff
changeset
|
833 |
val feats = |
48385 | 834 |
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
|
835 |
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
|
836 |
val n = n |> not (null deps) ? Integer.add 1 |
48404 | 837 |
val adds = (name, parents, feats, deps) :: adds |
838 |
val (adds, next_commit) = |
|
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
839 |
if Time.> (Timer.checkRealTimer timer, next_commit) then |
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset
|
840 |
(commit false adds [] []; ([], next_commit_time ())) |
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
841 |
else |
48404 | 842 |
(adds, next_commit) |
843 |
val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout) |
|
844 |
in (adds, ([name], n, next_commit, timed_out)) end |
|
845 |
val n = |
|
846 |
if null new_facts then |
|
847 |
0 |
|
848 |
else |
|
849 |
let |
|
850 |
val last_th = new_facts |> List.last |> snd |
|
851 |
(* crude approximation *) |
|
852 |
val ancestors = |
|
853 |
old_facts |
|
854 |
|> filter (fn (_, th) => thm_ord (th, last_th) <> GREATER) |
|
48407 | 855 |
val parents = maximal_in_graph fact_G ancestors |
48404 | 856 |
val (adds, (_, n, _, _)) = |
857 |
([], (parents, 0, next_commit_time (), false)) |
|
858 |
|> fold learn_new_fact new_facts |
|
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset
|
859 |
in commit true adds [] []; n end |
48404 | 860 |
fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum |
48439
67a6bcbd3587
removed MaSh junk arising from primrec definitions
blanchet
parents:
48438
diff
changeset
|
861 |
| relearn_old_fact ((_, (_, status)), th) |
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset
|
862 |
((reps, flops), (n, next_commit, _)) = |
48404 | 863 |
let |
864 |
val name = nickname_of th |
|
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset
|
865 |
val (n, reps, flops) = |
48439
67a6bcbd3587
removed MaSh junk arising from primrec definitions
blanchet
parents:
48438
diff
changeset
|
866 |
case deps_of status th of |
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset
|
867 |
SOME deps => (n + 1, (name, deps) :: reps, flops) |
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset
|
868 |
| NONE => (n, reps, name :: flops) |
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset
|
869 |
val (reps, flops, next_commit) = |
48404 | 870 |
if Time.> (Timer.checkRealTimer timer, next_commit) then |
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset
|
871 |
(commit false [] reps flops; ([], [], next_commit_time ())) |
48404 | 872 |
else |
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset
|
873 |
(reps, flops, next_commit) |
48404 | 874 |
val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout) |
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset
|
875 |
in ((reps, flops), (n, next_commit, timed_out)) end |
48404 | 876 |
val n = |
48433 | 877 |
if not atp orelse null old_facts then |
48404 | 878 |
n |
879 |
else |
|
880 |
let |
|
48668
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset
|
881 |
val max_isar = 1000 * max_dependencies |
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset
|
882 |
fun kind_of_proof th = |
48668
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset
|
883 |
try (Graph.get_node fact_G) (nickname_of th) |
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset
|
884 |
|> the_default Isar_Proof |
48406 | 885 |
fun priority_of (_, th) = |
48668
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset
|
886 |
random_range 0 max_isar |
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset
|
887 |
+ (case kind_of_proof th of |
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset
|
888 |
Isar_Proof => 0 |
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset
|
889 |
| ATP_Proof => 2 * max_isar |
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset
|
890 |
| Isar_Proof_wegen_ATP_Flop => max_isar) |
48404 | 891 |
- 500 * (th |> isar_dependencies_of all_names |
892 |
|> Option.map length |
|
893 |
|> the_default max_dependencies) |
|
894 |
val old_facts = |
|
48406 | 895 |
old_facts |> map (`priority_of) |
48404 | 896 |
|> sort (int_ord o pairself fst) |
897 |
|> map snd |
|
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset
|
898 |
val ((reps, flops), (n, _, _)) = |
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset
|
899 |
(([], []), (n, next_commit_time (), false)) |
48404 | 900 |
|> fold relearn_old_fact old_facts |
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset
|
901 |
in commit true [] reps flops; n end |
48318 | 902 |
in |
48404 | 903 |
if verbose orelse auto_level < 2 then |
904 |
"Learned " ^ string_of_int n ^ " nontrivial " ^ |
|
905 |
(if atp then "ATP" 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
|
906 |
(if verbose then |
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset
|
907 |
" 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
|
908 |
else |
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset
|
909 |
"") ^ "." |
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset
|
910 |
else |
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset
|
911 |
"" |
48318 | 912 |
end |
48308 | 913 |
end |
48304 | 914 |
|
48404 | 915 |
fun mash_learn ctxt (params as {provers, timeout, ...}) fact_override chained |
916 |
atp = |
|
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
917 |
let |
48396 | 918 |
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
|
919 |
val ctxt = ctxt |> Config.put instantiate_inducts false |
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset
|
920 |
val facts = |
48396 | 921 |
nearly_all_facts ctxt false fact_override Symtab.empty css chained [] |
922 |
@{prop True} |
|
48404 | 923 |
val num_facts = length facts |
924 |
val prover = hd provers |
|
925 |
fun learn auto_level atp = |
|
926 |
mash_learn_facts ctxt params prover auto_level atp infinite_timeout facts |
|
927 |
|> Output.urgent_message |
|
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
928 |
in |
48404 | 929 |
(if atp then |
930 |
("MaShing through " ^ string_of_int num_facts ^ " fact" ^ |
|
931 |
plural_s num_facts ^ " for ATP proofs (" ^ quote prover ^ " timeout: " ^ |
|
932 |
string_from_time timeout ^ ").\n\nCollecting Isar proofs first..." |
|
933 |
|> Output.urgent_message; |
|
934 |
learn 1 false; |
|
935 |
"Now collecting ATP proofs. This may take several hours. You can \ |
|
936 |
\safely stop the learning process at any point." |
|
937 |
|> Output.urgent_message; |
|
938 |
learn 0 true) |
|
939 |
else |
|
940 |
("MaShing through " ^ string_of_int num_facts ^ " fact" ^ |
|
941 |
plural_s num_facts ^ " for Isar proofs..." |
|
942 |
|> Output.urgent_message; |
|
943 |
learn 0 false)) |
|
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
944 |
end |
48249 | 945 |
|
50311 | 946 |
fun is_mash_enabled () = (getenv "MASH" = "yes") |
947 |
fun mash_can_suggest_facts ctxt = not (Graph.is_empty (#fact_G (mash_get ctxt))) |
|
948 |
||
48318 | 949 |
(* The threshold should be large enough so that MaSh doesn't kick in for Auto |
950 |
Sledgehammer and Try. *) |
|
951 |
val min_secs_for_learning = 15 |
|
952 |
||
48321 | 953 |
fun relevant_facts ctxt (params as {learn, fact_filter, timeout, ...}) prover |
954 |
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
|
955 |
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
|
956 |
error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".") |
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
957 |
else if only then |
48289 | 958 |
facts |
48321 | 959 |
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
|
960 |
[] |
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset
|
961 |
else |
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset
|
962 |
let |
48327
568b3193e53e
don't include hidden facts in relevance filter + tweak MaSh learning
blanchet
parents:
48326
diff
changeset
|
963 |
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
|
964 |
if learn andalso not (Async_Manager.has_running_threads MaShN) andalso |
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
|
965 |
Time.toSeconds timeout >= min_secs_for_learning 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
|
966 |
let val timeout = time_mult learn_timeout_slack timeout in |
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
|
967 |
launch_thread timeout |
48404 | 968 |
(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
|
969 |
timeout facts)) |
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset
|
970 |
end |
48318 | 971 |
else |
972 |
() |
|
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
973 |
val fact_filter = |
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
974 |
case fact_filter of |
48379
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents:
48378
diff
changeset
|
975 |
SOME ff => (() |> ff <> mepoN ? maybe_learn; ff) |
48318 | 976 |
| NONE => |
48407 | 977 |
if is_smt_prover ctxt prover then |
978 |
mepoN |
|
50229 | 979 |
else if is_mash_enabled () then |
48407 | 980 |
(maybe_learn (); |
981 |
if mash_can_suggest_facts ctxt then meshN else mepoN) |
|
982 |
else |
|
983 |
mepoN |
|
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset
|
984 |
val add_ths = Attrib.eval_thms ctxt add |
48292 | 985 |
fun prepend_facts ths accepts = |
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset
|
986 |
((facts |> filter (member Thm.eq_thm_prop ths o snd)) @ |
48292 | 987 |
(accepts |> filter_out (member Thm.eq_thm_prop ths o snd))) |
48293 | 988 |
|> take max_facts |
48406 | 989 |
fun mepo () = |
990 |
facts |> mepo_suggested_facts ctxt params prover max_facts NONE hyp_ts |
|
991 |
concl_t |
|
992 |
|> weight_mepo_facts |
|
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
993 |
fun mash () = |
48406 | 994 |
mash_suggested_facts ctxt params prover max_facts hyp_ts concl_t facts |
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
995 |
val mess = |
48406 | 996 |
[] |> (if fact_filter <> mashN then cons (mepo (), []) else I) |
48379
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents:
48378
diff
changeset
|
997 |
|> (if fact_filter <> mepoN then cons (mash ()) else I) |
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset
|
998 |
in |
48313
0faafdffa662
mesh facts by taking into consideration whether a fact is known to MeSh
blanchet
parents:
48312
diff
changeset
|
999 |
mesh_facts max_facts mess |
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset
|
1000 |
|> not (null add_ths) ? prepend_facts add_ths |
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset
|
1001 |
end |
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset
|
1002 |
|
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset
|
1003 |
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
|
1004 |
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
|
1005 |
|
48248 | 1006 |
end; |