author | blanchet |
Fri, 20 Jul 2012 22:19:46 +0200 | |
changeset 48404 | 0a261b4aa093 |
parent 48403 | 1f214c653c80 |
child 48406 | b002cc16aa99 |
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 |
|
48311 | 31 |
val extract_query : string -> string * string list |
48378 | 32 |
val nickname_of : thm -> string |
48321 | 33 |
val suggested_facts : string list -> ('a * thm) list -> ('a * thm) list |
34 |
val mesh_facts : |
|
35 |
int -> (('a * thm) list * ('a * thm) list) list -> ('a * thm) list |
|
48324 | 36 |
val is_likely_tautology_or_too_meta : thm -> bool |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
37 |
val theory_ord : theory * theory -> order |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
38 |
val thm_ord : thm * thm -> order |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
39 |
val goal_of_thm : theory -> thm -> thm |
48321 | 40 |
val run_prover_for_mash : |
48318 | 41 |
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
|
42 |
val features_of : |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
43 |
Proof.context -> string -> theory -> stature -> term list -> string list |
48404 | 44 |
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
|
45 |
val atp_dependencies_of : |
48404 | 46 |
Proof.context -> params -> string -> int -> fact list -> unit Symtab.table |
47 |
-> thm -> string list option |
|
48332
271a4a6af734
optimize parent computation in MaSh + remove temporary files
blanchet
parents:
48330
diff
changeset
|
48 |
val mash_CLEAR : Proof.context -> unit |
48308 | 49 |
val mash_ADD : |
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
50 |
Proof.context -> bool |
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
51 |
-> (string * string list * string list * string list) list -> unit |
48404 | 52 |
val mash_REPROVE : |
53 |
Proof.context -> bool -> (string * string list) list -> unit |
|
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
54 |
val mash_QUERY : |
48318 | 55 |
Proof.context -> bool -> int -> string list * string list -> string list |
48332
271a4a6af734
optimize parent computation in MaSh + remove temporary files
blanchet
parents:
48330
diff
changeset
|
56 |
val mash_unlearn : Proof.context -> unit |
48318 | 57 |
val mash_could_suggest_facts : unit -> bool |
48321 | 58 |
val mash_can_suggest_facts : Proof.context -> bool |
48298 | 59 |
val mash_suggest_facts : |
48321 | 60 |
Proof.context -> params -> string -> int -> term list -> term |
61 |
-> ('a * thm) list -> ('a * thm) list * ('a * thm) list |
|
48383 | 62 |
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
|
63 |
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
|
64 |
-> unit |
48395
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset
|
65 |
val mash_learn : |
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset
|
66 |
Proof.context -> params -> fact_override -> thm list -> bool -> unit |
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset
|
67 |
val relevant_facts : |
48292 | 68 |
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
|
69 |
-> 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
|
70 |
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
|
71 |
val running_learners : unit -> unit |
48248 | 72 |
end; |
73 |
||
48381 | 74 |
structure Sledgehammer_MaSh : SLEDGEHAMMER_MASH = |
48248 | 75 |
struct |
48249 | 76 |
|
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
77 |
open ATP_Util |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
78 |
open ATP_Problem_Generate |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
79 |
open Sledgehammer_Util |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
80 |
open Sledgehammer_Fact |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
81 |
open Sledgehammer_Provers |
48318 | 82 |
open Sledgehammer_Minimize |
48381 | 83 |
open Sledgehammer_MePo |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
84 |
|
48308 | 85 |
val trace = |
48380 | 86 |
Attrib.setup_config_bool @{binding sledgehammer_mash_trace} (K false) |
48308 | 87 |
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else () |
88 |
||
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset
|
89 |
val MaShN = "MaSh" |
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset
|
90 |
|
48379
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents:
48378
diff
changeset
|
91 |
val mepoN = "mepo" |
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
92 |
val mashN = "mash" |
48379
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents:
48378
diff
changeset
|
93 |
val meshN = "mesh" |
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
94 |
|
48379
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents:
48378
diff
changeset
|
95 |
val fact_filters = [meshN, mepoN, mashN] |
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
96 |
|
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
97 |
val unlearnN = "unlearn" |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
98 |
val learn_isarN = "learn_isar" |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
99 |
val learn_atpN = "learn_atp" |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
100 |
val relearn_isarN = "relearn_isar" |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
101 |
val relearn_atpN = "relearn_atp" |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
102 |
|
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
103 |
fun mash_home () = getenv "MASH_HOME" |
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 () = |
48309 | 105 |
getenv "ISABELLE_HOME_USER" ^ "/mash" |
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
106 |
|> tap (Isabelle_System.mkdir o Path.explode) |
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 |
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
108 |
fun mash_state_path () = mash_state_dir () ^ "/state" |> Path.explode |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
109 |
|
48330 | 110 |
|
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
111 |
(*** Isabelle helpers ***) |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
112 |
|
48308 | 113 |
fun meta_char c = |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
114 |
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
|
115 |
c = #")" orelse c = #"," then |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
116 |
String.str c |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
117 |
else |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
118 |
(* fixed width, in case more digits follow *) |
48395
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset
|
119 |
"%" ^ stringN_of_int 3 (Char.ord c) |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
120 |
|
48308 | 121 |
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
|
122 |
| unmeta_chars accum (#"%" :: d1 :: d2 :: d3 :: cs) = |
48308 | 123 |
(case Int.fromString (String.implode [d1, d2, d3]) of |
124 |
SOME n => unmeta_chars (Char.chr n :: accum) cs |
|
125 |
| NONE => "" (* error *)) |
|
48395
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset
|
126 |
| unmeta_chars _ (#"%" :: _) = "" (* error *) |
48308 | 127 |
| unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs |
128 |
||
129 |
val escape_meta = String.translate meta_char |
|
48303
f1d135d0ea69
improved MaSh string escaping and make more operations string-based
blanchet
parents:
48302
diff
changeset
|
130 |
val escape_metas = map escape_meta #> space_implode " " |
48315
82d6e46c673f
fixed order of accessibles + other tweaks to MaSh
blanchet
parents:
48314
diff
changeset
|
131 |
val unescape_meta = String.explode #> unmeta_chars [] |
82d6e46c673f
fixed order of accessibles + other tweaks to MaSh
blanchet
parents:
48314
diff
changeset
|
132 |
val unescape_metas = |
82d6e46c673f
fixed order of accessibles + other tweaks to MaSh
blanchet
parents:
48314
diff
changeset
|
133 |
space_explode " " #> filter_out (curry (op =) "") #> map unescape_meta |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
134 |
|
48311 | 135 |
fun extract_query line = |
136 |
case space_explode ":" line of |
|
48315
82d6e46c673f
fixed order of accessibles + other tweaks to MaSh
blanchet
parents:
48314
diff
changeset
|
137 |
[goal_name, suggs] => (unescape_meta goal_name, unescape_metas suggs) |
48312 | 138 |
| _ => ("", []) |
48311 | 139 |
|
48378 | 140 |
fun parent_of_local_thm th = |
141 |
let |
|
142 |
val thy = th |> Thm.theory_of_thm |
|
143 |
val facts = thy |> Global_Theory.facts_of |
|
144 |
val space = facts |> Facts.space_of |
|
145 |
fun id_of s = #id (Name_Space.the_entry space s) |
|
146 |
fun max_id (s', _) (s, id) = |
|
147 |
let val id' = id_of s' in if id > id' then (s, id) else (s', id') end |
|
148 |
in ("", ~1) |> Facts.fold_static max_id facts |> fst end |
|
149 |
||
150 |
val local_prefix = "local" ^ Long_Name.separator |
|
151 |
||
152 |
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
|
153 |
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
|
154 |
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
|
155 |
(* 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
|
156 |
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
|
157 |
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
|
158 |
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
|
159 |
| 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
|
160 |
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
|
161 |
else |
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset
|
162 |
backquote_thm th |
48378 | 163 |
|
48330 | 164 |
fun suggested_facts suggs facts = |
165 |
let |
|
48378 | 166 |
fun add_fact (fact as (_, th)) = Symtab.default (nickname_of th, fact) |
48330 | 167 |
val tab = Symtab.empty |> fold add_fact facts |
168 |
in map_filter (Symtab.lookup tab) suggs end |
|
48311 | 169 |
|
48329
5781c4620245
use better score function, based on previous evaluation (cf. Deduct 2011 slides)
blanchet
parents:
48328
diff
changeset
|
170 |
(* Ad hoc score function roughly based on Blanchette's Ringberg 2011 data. *) |
5781c4620245
use better score function, based on previous evaluation (cf. Deduct 2011 slides)
blanchet
parents:
48328
diff
changeset
|
171 |
fun score x = Math.pow (1.5, 15.5 - 0.05 * Real.fromInt x) + 15.0 |
48328
ca0b7d19dd62
attempt at meshing according to more meaningful factors
blanchet
parents:
48327
diff
changeset
|
172 |
|
ca0b7d19dd62
attempt at meshing according to more meaningful factors
blanchet
parents:
48327
diff
changeset
|
173 |
fun sum_sq_avg [] = 0 |
48329
5781c4620245
use better score function, based on previous evaluation (cf. Deduct 2011 slides)
blanchet
parents:
48328
diff
changeset
|
174 |
| sum_sq_avg xs = |
5781c4620245
use better score function, based on previous evaluation (cf. Deduct 2011 slides)
blanchet
parents:
48328
diff
changeset
|
175 |
Real.ceil (100000.0 * fold (curry (op +) o score) xs 0.0) div length xs |
48313
0faafdffa662
mesh facts by taking into consideration whether a fact is known to MeSh
blanchet
parents:
48312
diff
changeset
|
176 |
|
48320
891a24a48155
improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
blanchet
parents:
48319
diff
changeset
|
177 |
fun mesh_facts max_facts [(selected, unknown)] = |
891a24a48155
improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
blanchet
parents:
48319
diff
changeset
|
178 |
take max_facts selected @ take (max_facts - length selected) unknown |
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
179 |
| mesh_facts max_facts mess = |
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
180 |
let |
48320
891a24a48155
improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
blanchet
parents:
48319
diff
changeset
|
181 |
val mess = mess |> map (apfst (`length)) |
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
182 |
val fact_eq = Thm.eq_thm o pairself 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
|
183 |
fun score_in fact ((sel_len, sels), unks) = |
891a24a48155
improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
blanchet
parents:
48319
diff
changeset
|
184 |
case find_index (curry fact_eq fact) sels of |
891a24a48155
improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
blanchet
parents:
48319
diff
changeset
|
185 |
~1 => (case find_index (curry fact_eq fact) unks of |
48329
5781c4620245
use better score function, based on previous evaluation (cf. Deduct 2011 slides)
blanchet
parents:
48328
diff
changeset
|
186 |
~1 => SOME 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
|
187 |
| _ => NONE) |
48329
5781c4620245
use better score function, based on previous evaluation (cf. Deduct 2011 slides)
blanchet
parents:
48328
diff
changeset
|
188 |
| j => SOME j |
48328
ca0b7d19dd62
attempt at meshing according to more meaningful factors
blanchet
parents:
48327
diff
changeset
|
189 |
fun score_of fact = mess |> map_filter (score_in fact) |> sum_sq_avg |
48320
891a24a48155
improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
blanchet
parents:
48319
diff
changeset
|
190 |
val facts = fold (union fact_eq 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
|
191 |
in |
48328
ca0b7d19dd62
attempt at meshing according to more meaningful factors
blanchet
parents:
48327
diff
changeset
|
192 |
facts |> map (`score_of) |> sort (int_ord o swap o pairself fst) |
ca0b7d19dd62
attempt at meshing according to more meaningful factors
blanchet
parents:
48327
diff
changeset
|
193 |
|> map snd |> take max_facts |
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
194 |
end |
48312 | 195 |
|
48395
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset
|
196 |
val thy_feature_name_of = prefix "y" |
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset
|
197 |
val const_name_of = prefix "c" |
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset
|
198 |
val type_name_of = prefix "t" |
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset
|
199 |
val class_name_of = prefix "s" |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
200 |
|
48324 | 201 |
fun is_likely_tautology_or_too_meta th = |
202 |
let |
|
203 |
val is_boring_const = member (op =) atp_widely_irrelevant_consts |
|
204 |
fun is_boring_bool t = |
|
205 |
not (exists_Const (not o is_boring_const o fst) t) orelse |
|
206 |
exists_type (exists_subtype (curry (op =) @{typ prop})) t |
|
207 |
fun is_boring_prop (@{const Trueprop} $ t) = is_boring_bool t |
|
208 |
| is_boring_prop (@{const "==>"} $ t $ u) = |
|
209 |
is_boring_prop t andalso is_boring_prop u |
|
210 |
| is_boring_prop (Const (@{const_name all}, _) $ (Abs (_, _, t)) $ u) = |
|
211 |
is_boring_prop t andalso is_boring_prop u |
|
212 |
| is_boring_prop (Const (@{const_name "=="}, _) $ t $ u) = |
|
213 |
is_boring_bool t andalso is_boring_bool u |
|
214 |
| is_boring_prop _ = true |
|
215 |
in |
|
216 |
is_boring_prop (prop_of th) andalso not (Thm.eq_thm_prop (@{thm ext}, th)) |
|
217 |
end |
|
218 |
||
219 |
fun theory_ord p = |
|
220 |
if Theory.eq_thy p then |
|
221 |
EQUAL |
|
222 |
else if Theory.subthy p then |
|
223 |
LESS |
|
224 |
else if Theory.subthy (swap p) then |
|
225 |
GREATER |
|
226 |
else case int_ord (pairself (length o Theory.ancestors_of) p) of |
|
227 |
EQUAL => string_ord (pairself Context.theory_name p) |
|
228 |
| order => order |
|
229 |
||
230 |
val thm_ord = theory_ord o pairself theory_of_thm |
|
231 |
||
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
232 |
val freezeT = Type.legacy_freeze_type |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
233 |
|
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
234 |
fun freeze (t $ u) = freeze t $ freeze u |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
235 |
| 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
|
236 |
| freeze (Var ((s, _), T)) = Free (s, freezeT T) |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
237 |
| freeze (Const (s, T)) = Const (s, freezeT T) |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
238 |
| freeze (Free (s, T)) = Free (s, freezeT T) |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
239 |
| freeze t = t |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
240 |
|
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
241 |
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
|
242 |
|
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
243 |
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
|
244 |
let |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
245 |
val problem = |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
246 |
{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
|
247 |
facts = facts |> map (apfst (apfst (fn name => name ()))) |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
248 |
|> map Untranslated_Fact} |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
249 |
in |
48399
4bacc8983b3d
learn from SMT proofs when they can be minimized by Metis
blanchet
parents:
48398
diff
changeset
|
250 |
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
|
251 |
problem |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
252 |
end |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
253 |
|
48326 | 254 |
val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}] |
255 |
||
48398 | 256 |
val logical_consts = |
257 |
[@{const_name prop}, @{const_name Pure.conjunction}] @ atp_logical_consts |
|
258 |
||
48318 | 259 |
fun interesting_terms_types_and_classes ctxt prover term_max_depth |
260 |
type_max_depth ts = |
|
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
261 |
let |
48318 | 262 |
fun is_bad_const (x as (s, _)) args = |
48398 | 263 |
member (op =) logical_consts s orelse |
48318 | 264 |
fst (is_built_in_const_for_prover ctxt prover x args) |
48304 | 265 |
fun add_classes @{sort type} = I |
266 |
| 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
|
267 |
fun do_add_type (Type (s, Ts)) = |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
268 |
(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
|
269 |
#> fold do_add_type Ts |
48304 | 270 |
| do_add_type (TFree (_, S)) = add_classes S |
271 |
| do_add_type (TVar (_, S)) = add_classes S |
|
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
272 |
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
|
273 |
fun mk_app s args = |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
274 |
if member (op <>) args "" then s ^ "(" ^ space_implode "," args ^ ")" |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
275 |
else s |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
276 |
fun patternify ~1 _ = "" |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
277 |
| patternify depth t = |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
278 |
case strip_comb t of |
48398 | 279 |
(Const (x as (s, _)), args) => |
280 |
if is_bad_const x args then "" |
|
281 |
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
|
282 |
| _ => "" |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
283 |
fun add_term_patterns ~1 _ = I |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
284 |
| add_term_patterns depth t = |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
285 |
insert (op =) (patternify depth t) |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
286 |
#> add_term_patterns (depth - 1) t |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
287 |
val add_term = add_term_patterns term_max_depth |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
288 |
fun add_patterns t = |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
289 |
let val (head, args) = strip_comb t in |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
290 |
(case head of |
48398 | 291 |
Const (_, T) => add_term t #> add_type T |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
292 |
| Free (_, T) => add_type T |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
293 |
| Var (_, T) => add_type T |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
294 |
| Abs (_, T, body) => add_type T #> add_patterns body |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
295 |
| _ => I) |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
296 |
#> fold add_patterns args |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
297 |
end |
48326 | 298 |
in [] |> fold add_patterns ts end |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
299 |
|
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
300 |
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
|
301 |
|
48297 | 302 |
val term_max_depth = 1 |
303 |
val type_max_depth = 1 |
|
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
304 |
|
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
305 |
(* TODO: Generate type classes for types? *) |
48385 | 306 |
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
|
307 |
thy_feature_name_of (Context.theory_name thy) :: |
48318 | 308 |
interesting_terms_types_and_classes ctxt prover term_max_depth type_max_depth |
309 |
ts |
|
48332
271a4a6af734
optimize parent computation in MaSh + remove temporary files
blanchet
parents:
48330
diff
changeset
|
310 |
|> forall is_lambda_free ts ? cons "no_lams" |
271a4a6af734
optimize parent computation in MaSh + remove temporary files
blanchet
parents:
48330
diff
changeset
|
311 |
|> forall (not o exists_Const is_exists) ts ? cons "no_skos" |
48385 | 312 |
|> scope <> Global ? cons "local" |
48302 | 313 |
|> (case status of |
314 |
General => I |
|
315 |
| Induction => cons "induction" |
|
316 |
| Intro => cons "intro" |
|
317 |
| Inductive => cons "inductive" |
|
318 |
| Elim => cons "elim" |
|
319 |
| Simp => cons "simp" |
|
320 |
| Def => cons "def") |
|
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
321 |
|
48404 | 322 |
(* Too many dependencies is a sign that a decision procedure is at work. There |
323 |
isn't much too learn from such proofs. *) |
|
324 |
val max_dependencies = 10 |
|
325 |
val atp_dependency_default_max_fact = 50 |
|
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
326 |
|
48404 | 327 |
fun trim_dependencies deps = |
328 |
if length deps <= max_dependencies then SOME deps else NONE |
|
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
329 |
|
48404 | 330 |
fun isar_dependencies_of all_facts = |
331 |
thms_in_proof (SOME all_facts) #> trim_dependencies |
|
332 |
||
333 |
fun atp_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover |
|
334 |
auto_level facts all_names th = |
|
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
335 |
case isar_dependencies_of all_names th of |
48404 | 336 |
SOME [] => NONE |
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
337 |
| isar_deps => |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
338 |
let |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
339 |
val thy = Proof_Context.theory_of ctxt |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
340 |
val goal = goal_of_thm thy th |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
341 |
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
|
342 |
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
|
343 |
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
|
344 |
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
|
345 |
fun add_isar_dep facts dep accum = |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
346 |
if exists (is_dep dep) accum then |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
347 |
accum |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
348 |
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
|
349 |
SOME ((name, status), th) => accum @ [((name, status), th)] |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
350 |
| NONE => accum (* shouldn't happen *) |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
351 |
val facts = |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
352 |
facts |> iterative_relevant_facts ctxt params prover |
48404 | 353 |
(max_facts |> the_default atp_dependency_default_max_fact) |
354 |
NONE hyp_ts concl_t |
|
355 |
|> 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
|
356 |
|> map fix_name |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
357 |
in |
48404 | 358 |
if verbose andalso auto_level = 0 then |
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
359 |
let val num_facts = length facts in |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
360 |
"MaSh: " ^ quote prover ^ " on " ^ quote (nickname_of th) ^ |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
361 |
" 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
|
362 |
"." |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
363 |
|> Output.urgent_message |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
364 |
end |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
365 |
else |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
366 |
(); |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
367 |
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
|
368 |
{outcome = NONE, used_facts, ...} => |
48404 | 369 |
(if verbose andalso auto_level = 0 then |
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
370 |
let val num_facts = length used_facts in |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
371 |
"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
|
372 |
plural_s num_facts ^ "." |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
373 |
|> Output.urgent_message |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
374 |
end |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
375 |
else |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
376 |
(); |
48404 | 377 |
used_facts |> map fst |> trim_dependencies) |
378 |
| _ => NONE |
|
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
379 |
end |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
380 |
|
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
381 |
|
48302 | 382 |
(*** Low-level communication with MaSh ***) |
383 |
||
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 |
(* more friendly than "try o File.rm" for those who keep the files open in their |
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 |
text editor *) |
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 |
fun wipe_out file = File.write file "" |
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 |
|
48323 | 388 |
fun write_file (xs, f) file = |
48318 | 389 |
let val path = Path.explode file in |
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
|
390 |
wipe_out path; |
48323 | 391 |
xs |> chunk_list 500 |
392 |
|> List.app (File.append path o space_implode "" o map f) |
|
48318 | 393 |
end |
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
394 |
|
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
|
395 |
fun run_mash_tool ctxt overlord save max_suggs write_cmds read_suggs = |
48311 | 396 |
let |
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
|
397 |
val (temp_dir, serial) = |
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset
|
398 |
if overlord then (getenv "ISABELLE_HOME_USER", "") |
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset
|
399 |
else (getenv "ISABELLE_TMP", serial_string ()) |
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset
|
400 |
val log_file = if overlord then temp_dir ^ "/mash_log" else "/dev/null" |
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
401 |
val err_file = temp_dir ^ "/mash_err" ^ serial |
48318 | 402 |
val sugg_file = temp_dir ^ "/mash_suggs" ^ serial |
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
403 |
val cmd_file = temp_dir ^ "/mash_commands" ^ serial |
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
|
404 |
val core = |
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset
|
405 |
"--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^ |
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset
|
406 |
" --numberOfPredictions " ^ string_of_int max_suggs ^ |
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset
|
407 |
(if save then " --saveModel" else "") |
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset
|
408 |
val command = |
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset
|
409 |
mash_home () ^ "/mash --quiet --outputDir " ^ mash_model_dir () ^ |
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset
|
410 |
" --log " ^ log_file ^ " " ^ core ^ " >& " ^ err_file |
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
411 |
in |
48323 | 412 |
write_file ([], K "") sugg_file; |
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
413 |
write_file write_cmds cmd_file; |
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
|
414 |
trace_msg ctxt (fn () => "Running " ^ command); |
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset
|
415 |
Isabelle_System.bash command; |
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset
|
416 |
read_suggs (fn () => try File.read_lines (Path.explode sugg_file) |> these) |
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 |
|> tap (fn _ => trace_msg ctxt (fn () => |
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 |
case try File.read (Path.explode err_file) 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
|
419 |
NONE => "Done" |
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 |
| SOME "" => "Done" |
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 s => "Error: " ^ elide_string 1000 s)) |
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 |
|> not overlord |
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 |
? tap (fn _ => List.app (wipe_out o Path.explode) |
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 |
[err_file, sugg_file, cmd_file]) |
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
425 |
end |
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
426 |
|
48404 | 427 |
fun str_of_add (name, parents, feats, deps) = |
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
428 |
"! " ^ escape_meta name ^ ": " ^ escape_metas parents ^ "; " ^ |
48311 | 429 |
escape_metas feats ^ "; " ^ escape_metas deps ^ "\n" |
430 |
||
48404 | 431 |
fun str_of_reprove (name, deps) = |
432 |
"p " ^ escape_meta name ^ ": " ^ escape_metas deps ^ "\n" |
|
433 |
||
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
434 |
fun str_of_query (parents, feats) = |
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
435 |
"? " ^ escape_metas parents ^ "; " ^ escape_metas feats |
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
436 |
|
48332
271a4a6af734
optimize parent computation in MaSh + remove temporary files
blanchet
parents:
48330
diff
changeset
|
437 |
fun mash_CLEAR ctxt = |
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
|
438 |
let val path = mash_model_dir () |> Path.explode in |
48332
271a4a6af734
optimize parent computation in MaSh + remove temporary files
blanchet
parents:
48330
diff
changeset
|
439 |
trace_msg ctxt (K "MaSh CLEAR"); |
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
|
440 |
File.fold_dir (fn file => fn _ => |
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset
|
441 |
try File.rm (Path.append path (Path.basic file))) |
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset
|
442 |
path NONE; |
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset
|
443 |
() |
48309 | 444 |
end |
48302 | 445 |
|
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
446 |
fun mash_ADD _ _ [] = () |
48404 | 447 |
| mash_ADD ctxt overlord adds = |
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
448 |
(trace_msg ctxt (fn () => "MaSh ADD " ^ |
48404 | 449 |
elide_string 1000 (space_implode " " (map #1 adds))); |
450 |
run_mash_tool ctxt overlord true 0 (adds, str_of_add) (K ())) |
|
451 |
||
452 |
fun mash_REPROVE _ _ [] = () |
|
453 |
| mash_REPROVE ctxt overlord reps = |
|
454 |
(trace_msg ctxt (fn () => "MaSh REPROVE " ^ |
|
455 |
elide_string 1000 (space_implode " " (map #1 reps))); |
|
456 |
run_mash_tool ctxt overlord true 0 (reps, str_of_reprove) (K ())) |
|
48302 | 457 |
|
48318 | 458 |
fun mash_QUERY ctxt overlord max_suggs (query as (_, feats)) = |
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
459 |
(trace_msg ctxt (fn () => "MaSh QUERY " ^ space_implode " " feats); |
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
|
460 |
run_mash_tool ctxt overlord false max_suggs |
48323 | 461 |
([query], str_of_query) |
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
|
462 |
(fn suggs => |
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset
|
463 |
case suggs () 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
|
464 |
[] => [] |
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset
|
465 |
| suggs => snd (extract_query (List.last suggs))) |
48311 | 466 |
handle List.Empty => []) |
48302 | 467 |
|
468 |
||
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
469 |
(*** High-level communication with MaSh ***) |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
470 |
|
48321 | 471 |
fun try_graph ctxt when def f = |
472 |
f () |
|
473 |
handle Graph.CYCLES (cycle :: _) => |
|
474 |
(trace_msg ctxt (fn () => |
|
475 |
"Cycle involving " ^ commas cycle ^ " when " ^ when); def) |
|
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
476 |
| Graph.DUP name => |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
477 |
(trace_msg ctxt (fn () => |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
478 |
"Duplicate fact " ^ quote name ^ " when " ^ when); def) |
48321 | 479 |
| Graph.UNDEF name => |
480 |
(trace_msg ctxt (fn () => |
|
481 |
"Unknown fact " ^ quote name ^ " when " ^ when); def) |
|
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
482 |
| exn => |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
483 |
if Exn.is_interrupt exn then |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
484 |
reraise exn |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
485 |
else |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
486 |
(trace_msg ctxt (fn () => |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
487 |
"Internal error when " ^ when ^ ":\n" ^ |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
488 |
ML_Compiler.exn_message exn); def) |
48321 | 489 |
|
48400 | 490 |
type mash_state = {fact_G : unit Graph.T} |
48301 | 491 |
|
48400 | 492 |
val empty_state = {fact_G = Graph.empty} |
48301 | 493 |
|
494 |
local |
|
495 |
||
48390
4147f2bc4442
add versioning to MaSh state + cleanup dead code
blanchet
parents:
48389
diff
changeset
|
496 |
val version = "*** MaSh 0.0 ***" |
4147f2bc4442
add versioning to MaSh state + cleanup dead code
blanchet
parents:
48389
diff
changeset
|
497 |
|
4147f2bc4442
add versioning to MaSh state + cleanup dead code
blanchet
parents:
48389
diff
changeset
|
498 |
fun load _ (state as (true, _)) = state |
4147f2bc4442
add versioning to MaSh state + cleanup dead code
blanchet
parents:
48389
diff
changeset
|
499 |
| load ctxt _ = |
48309 | 500 |
let val path = mash_state_path () in |
48302 | 501 |
(true, |
502 |
case try File.read_lines path of |
|
48390
4147f2bc4442
add versioning to MaSh state + cleanup dead code
blanchet
parents:
48389
diff
changeset
|
503 |
SOME (version' :: fact_lines) => |
48302 | 504 |
let |
48322
8a8d71e34297
fixed MaSh state load code so it works even if the facts are read in disorder
blanchet
parents:
48321
diff
changeset
|
505 |
fun add_edge_to name parent = |
8a8d71e34297
fixed MaSh state load code so it works even if the facts are read in disorder
blanchet
parents:
48321
diff
changeset
|
506 |
Graph.default_node (parent, ()) |
8a8d71e34297
fixed MaSh state load code so it works even if the facts are read in disorder
blanchet
parents:
48321
diff
changeset
|
507 |
#> Graph.add_edge (parent, name) |
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
508 |
fun add_fact_line line = |
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
509 |
case extract_query line of |
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
510 |
("", _) => I (* shouldn't happen *) |
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
511 |
| (name, parents) => |
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
512 |
Graph.default_node (name, ()) |
48322
8a8d71e34297
fixed MaSh state load code so it works even if the facts are read in disorder
blanchet
parents:
48321
diff
changeset
|
513 |
#> fold (add_edge_to name) parents |
48400 | 514 |
val fact_G = |
48322
8a8d71e34297
fixed MaSh state load code so it works even if the facts are read in disorder
blanchet
parents:
48321
diff
changeset
|
515 |
try_graph ctxt "loading state" Graph.empty (fn () => |
48390
4147f2bc4442
add versioning to MaSh state + cleanup dead code
blanchet
parents:
48389
diff
changeset
|
516 |
Graph.empty |> version' = version |
4147f2bc4442
add versioning to MaSh state + cleanup dead code
blanchet
parents:
48389
diff
changeset
|
517 |
? fold add_fact_line fact_lines) |
48400 | 518 |
in {fact_G = fact_G} end |
48304 | 519 |
| _ => empty_state) |
48302 | 520 |
end |
48249 | 521 |
|
48400 | 522 |
fun save {fact_G} = |
48301 | 523 |
let |
48309 | 524 |
val path = mash_state_path () |
48318 | 525 |
fun fact_line_for name parents = |
526 |
escape_meta name ^ ": " ^ escape_metas parents |
|
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
527 |
val append_fact = File.append path o suffix "\n" oo fact_line_for |
48400 | 528 |
fun append_entry (name, ((), (parents, _))) () = |
529 |
append_fact name (Graph.Keys.dest parents) |
|
48301 | 530 |
in |
48390
4147f2bc4442
add versioning to MaSh state + cleanup dead code
blanchet
parents:
48389
diff
changeset
|
531 |
File.write path (version ^ "\n"); |
48400 | 532 |
Graph.fold append_entry fact_G () |
48301 | 533 |
end |
534 |
||
48302 | 535 |
val global_state = |
48381 | 536 |
Synchronized.var "Sledgehammer_MaSh.global_state" (false, empty_state) |
48301 | 537 |
|
538 |
in |
|
539 |
||
48321 | 540 |
fun mash_map ctxt f = |
48390
4147f2bc4442
add versioning to MaSh state + cleanup dead code
blanchet
parents:
48389
diff
changeset
|
541 |
Synchronized.change global_state (load ctxt ##> (f #> tap save)) |
48302 | 542 |
|
48321 | 543 |
fun mash_get ctxt = |
48390
4147f2bc4442
add versioning to MaSh state + cleanup dead code
blanchet
parents:
48389
diff
changeset
|
544 |
Synchronized.change_result global_state (load ctxt #> `snd) |
48302 | 545 |
|
48332
271a4a6af734
optimize parent computation in MaSh + remove temporary files
blanchet
parents:
48330
diff
changeset
|
546 |
fun mash_unlearn ctxt = |
48302 | 547 |
Synchronized.change global_state (fn _ => |
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
|
548 |
(mash_CLEAR ctxt; wipe_out (mash_state_path ()); (true, empty_state))) |
48301 | 549 |
|
550 |
end |
|
551 |
||
48318 | 552 |
fun mash_could_suggest_facts () = mash_home () <> "" |
48400 | 553 |
fun mash_can_suggest_facts ctxt = not (Graph.is_empty (#fact_G (mash_get ctxt))) |
48249 | 554 |
|
48400 | 555 |
fun queue_of xs = Queue.empty |> fold Queue.enqueue xs |
556 |
||
557 |
fun max_facts_in_graph fact_G facts = |
|
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
558 |
let |
48378 | 559 |
val facts = [] |> fold (cons o nickname_of o snd) facts |
48330 | 560 |
val tab = Symtab.empty |> fold (fn name => Symtab.update (name, ())) facts |
48400 | 561 |
fun enqueue_new seen name = |
562 |
not (member (op =) seen name) ? Queue.enqueue name |
|
563 |
fun find_maxes seen maxs names = |
|
48401 | 564 |
case try Queue.dequeue names of |
565 |
NONE => map snd maxs |
|
566 |
| SOME (name, names) => |
|
567 |
if Symtab.defined tab name then |
|
568 |
let |
|
569 |
val new = (Graph.all_preds fact_G [name], name) |
|
570 |
fun not_ancestor (_, x) (yp, _) = not (member (op =) yp x) |
|
571 |
val maxs = maxs |> filter (fn max => not_ancestor max new) |
|
572 |
val maxs = maxs |> forall (not_ancestor new) maxs ? cons new |
|
573 |
in find_maxes (name :: seen) maxs names end |
|
574 |
else |
|
575 |
find_maxes (name :: seen) maxs |
|
576 |
(Graph.Keys.fold (enqueue_new seen) |
|
577 |
(Graph.imm_preds fact_G name) names) |
|
48400 | 578 |
in find_maxes [] [] (queue_of (Graph.maximals fact_G)) end |
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
579 |
|
48318 | 580 |
(* Generate more suggestions than requested, because some might be thrown out |
581 |
later for various reasons and "meshing" gives better results with some |
|
582 |
slack. *) |
|
583 |
fun max_suggs_of max_facts = max_facts + Int.min (200, max_facts) |
|
584 |
||
48400 | 585 |
fun is_fact_in_graph fact_G (_, th) = |
586 |
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
|
587 |
|
48318 | 588 |
fun mash_suggest_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts |
589 |
concl_t facts = |
|
48301 | 590 |
let |
48302 | 591 |
val thy = Proof_Context.theory_of ctxt |
48400 | 592 |
val fact_G = #fact_G (mash_get ctxt) |
593 |
val parents = max_facts_in_graph fact_G facts |
|
48385 | 594 |
val feats = features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts) |
48318 | 595 |
val suggs = |
48400 | 596 |
if Graph.is_empty fact_G then [] |
48320
891a24a48155
improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
blanchet
parents:
48319
diff
changeset
|
597 |
else mash_QUERY ctxt overlord (max_suggs_of max_facts) (parents, feats) |
891a24a48155
improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
blanchet
parents:
48319
diff
changeset
|
598 |
val selected = facts |> suggested_facts suggs |
48400 | 599 |
val unknown = facts |> filter_out (is_fact_in_graph fact_G) |
48320
891a24a48155
improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
blanchet
parents:
48319
diff
changeset
|
600 |
in (selected, unknown) end |
48249 | 601 |
|
48404 | 602 |
fun add_to_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
|
603 |
let |
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
604 |
fun maybe_add_from from (accum as (parents, graph)) = |
48321 | 605 |
try_graph ctxt "updating graph" accum (fn () => |
606 |
(from :: parents, Graph.add_edge_acyclic (from, name) graph)) |
|
607 |
val graph = graph |> Graph.default_node (name, ()) |
|
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
608 |
val (parents, graph) = ([], graph) |> fold maybe_add_from parents |
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
609 |
val (deps, graph) = ([], graph) |> fold maybe_add_from deps |
48404 | 610 |
in ((name, parents, feats, deps) :: adds, graph) end |
48306 | 611 |
|
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
|
612 |
val learn_timeout_slack = 2.0 |
48318 | 613 |
|
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
|
614 |
fun launch_thread timeout task = |
48383 | 615 |
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
|
616 |
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
|
617 |
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
|
618 |
val death_time = Time.+ (birth_time, hard_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
|
619 |
val desc = ("machine learner for Sledgehammer", "") |
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
|
620 |
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
|
621 |
|
48400 | 622 |
fun freshish_name () = |
623 |
Date.fmt ".%Y_%m_%d_%H_%M_%S__" (Date.fromTimeLocal (Time.now ())) ^ |
|
624 |
serial_string () |
|
625 |
||
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
|
626 |
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
|
627 |
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
|
628 |
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
|
629 |
() |
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
|
630 |
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
|
631 |
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
|
632 |
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
|
633 |
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
|
634 |
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
|
635 |
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
|
636 |
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
|
637 |
val {fact_G} = mash_get 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
|
638 |
val parents = max_facts_in_graph fact_G facts |
1f214c653c80
don't store fresh names in fact graph, since these cannot be the parents of any other facts
blanchet
parents:
48401
diff
changeset
|
639 |
in |
1f214c653c80
don't store fresh names in fact graph, since these cannot be the parents of any other facts
blanchet
parents:
48401
diff
changeset
|
640 |
mash_ADD ctxt overlord [(name, parents, feats, deps)]; (true, "") |
1f214c653c80
don't store fresh names in fact graph, since these cannot be the parents of any other facts
blanchet
parents:
48401
diff
changeset
|
641 |
end) |
48383 | 642 |
|
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
643 |
fun sendback sub = |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
644 |
Markup.markup Isabelle_Markup.sendback (sledgehammerN ^ " " ^ sub) |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
645 |
|
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
646 |
val commit_timeout = seconds 30.0 |
48332
271a4a6af734
optimize parent computation in MaSh + remove temporary files
blanchet
parents:
48330
diff
changeset
|
647 |
|
48318 | 648 |
(* The timeout is understood in a very slack fashion. *) |
48404 | 649 |
fun mash_learn_facts ctxt (params as {debug, verbose, overlord, ...}) prover |
650 |
auto_level atp learn_timeout facts = |
|
48304 | 651 |
let |
48318 | 652 |
val timer = Timer.startRealTimer () |
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
653 |
fun next_commit_time () = |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
654 |
Time.+ (Timer.checkRealTimer timer, commit_timeout) |
48400 | 655 |
val {fact_G} = mash_get ctxt |
656 |
val (old_facts, new_facts) = |
|
657 |
facts |> List.partition (is_fact_in_graph fact_G) |
|
658 |
||> sort (thm_ord o pairself snd) |
|
48308 | 659 |
in |
48404 | 660 |
if null new_facts andalso (not atp orelse null old_facts) then |
661 |
if auto_level < 2 then |
|
662 |
"No new " ^ (if atp then "ATP" else "Isar") ^ " proofs to learn." ^ |
|
663 |
(if auto_level = 0 andalso not atp then |
|
664 |
"\n\nHint: Try " ^ sendback learn_atpN ^ " to learn from ATP proofs." |
|
665 |
else |
|
666 |
"") |
|
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
667 |
else |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
668 |
"" |
48308 | 669 |
else |
48304 | 670 |
let |
48315
82d6e46c673f
fixed order of accessibles + other tweaks to MaSh
blanchet
parents:
48314
diff
changeset
|
671 |
val all_names = |
48400 | 672 |
facts |> map snd |
673 |
|> filter_out is_likely_tautology_or_too_meta |
|
674 |
|> map (rpair () o nickname_of) |
|
675 |
|> Symtab.make |
|
48404 | 676 |
val deps_of = |
677 |
if atp then |
|
678 |
atp_dependencies_of ctxt params prover auto_level facts all_names |
|
679 |
else |
|
680 |
isar_dependencies_of all_names |
|
681 |
fun do_commit [] [] state = state |
|
682 |
| do_commit adds reps {fact_G} = |
|
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
683 |
let |
48404 | 684 |
val (adds, fact_G) = |
685 |
([], fact_G) |> fold (add_to_fact_graph ctxt) adds |
|
686 |
in |
|
687 |
mash_ADD ctxt overlord (rev adds); |
|
688 |
mash_REPROVE ctxt overlord reps; |
|
689 |
{fact_G = fact_G} |
|
690 |
end |
|
691 |
fun commit last adds reps = |
|
692 |
(if debug andalso auto_level = 0 then |
|
693 |
Output.urgent_message "Committing..." |
|
694 |
else |
|
695 |
(); |
|
696 |
mash_map ctxt (do_commit (rev adds) reps); |
|
697 |
if not last andalso auto_level = 0 then |
|
698 |
let val num_proofs = length adds + length reps in |
|
699 |
"Learned " ^ string_of_int num_proofs ^ " " ^ |
|
700 |
(if atp then "ATP" else "Isar") ^ " proof" ^ |
|
701 |
plural_s num_proofs ^ " in the last " ^ |
|
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
702 |
string_from_time commit_timeout ^ "." |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
703 |
|> Output.urgent_message |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
704 |
end |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
705 |
else |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
706 |
()) |
48404 | 707 |
fun learn_new_fact _ (accum as (_, (_, _, _, true))) = accum |
708 |
| learn_new_fact ((_, stature), th) |
|
709 |
(adds, (parents, n, next_commit, _)) = |
|
48318 | 710 |
let |
48378 | 711 |
val name = nickname_of th |
48332
271a4a6af734
optimize parent computation in MaSh + remove temporary files
blanchet
parents:
48330
diff
changeset
|
712 |
val feats = |
48385 | 713 |
features_of ctxt prover (theory_of_thm th) stature [prop_of th] |
48404 | 714 |
val deps = deps_of 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
|
715 |
val n = n |> not (null deps) ? Integer.add 1 |
48404 | 716 |
val adds = (name, parents, feats, deps) :: adds |
717 |
val (adds, next_commit) = |
|
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
718 |
if Time.> (Timer.checkRealTimer timer, next_commit) then |
48404 | 719 |
(commit false adds []; ([], next_commit_time ())) |
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
720 |
else |
48404 | 721 |
(adds, next_commit) |
722 |
val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout) |
|
723 |
in (adds, ([name], n, next_commit, timed_out)) end |
|
724 |
val n = |
|
725 |
if null new_facts then |
|
726 |
0 |
|
727 |
else |
|
728 |
let |
|
729 |
val last_th = new_facts |> List.last |> snd |
|
730 |
(* crude approximation *) |
|
731 |
val ancestors = |
|
732 |
old_facts |
|
733 |
|> filter (fn (_, th) => thm_ord (th, last_th) <> GREATER) |
|
734 |
val parents = max_facts_in_graph fact_G ancestors |
|
735 |
val (adds, (_, n, _, _)) = |
|
736 |
([], (parents, 0, next_commit_time (), false)) |
|
737 |
|> fold learn_new_fact new_facts |
|
738 |
in commit true adds []; n end |
|
739 |
fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum |
|
740 |
| relearn_old_fact (_, th) (reps, (n, next_commit, _)) = |
|
741 |
let |
|
742 |
val name = nickname_of th |
|
743 |
val (n, reps) = |
|
744 |
case deps_of th of |
|
745 |
SOME deps => (n + 1, (name, deps) :: reps) |
|
746 |
| NONE => (n, reps) |
|
747 |
val (reps, next_commit) = |
|
748 |
if Time.> (Timer.checkRealTimer timer, next_commit) then |
|
749 |
(commit false [] reps; ([], next_commit_time ())) |
|
750 |
else |
|
751 |
(reps, next_commit) |
|
752 |
val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout) |
|
753 |
in (reps, (n, next_commit, timed_out)) end |
|
754 |
val n = |
|
755 |
if null old_facts then |
|
756 |
n |
|
757 |
else |
|
758 |
let |
|
759 |
fun score_of (_, th) = |
|
760 |
random_range 0 (1000 * max_dependencies) |
|
761 |
- 500 * (th |> isar_dependencies_of all_names |
|
762 |
|> Option.map length |
|
763 |
|> the_default max_dependencies) |
|
764 |
val old_facts = |
|
765 |
old_facts |> map (`score_of) |
|
766 |
|> sort (int_ord o pairself fst) |
|
767 |
|> map snd |
|
768 |
val (reps, (n, _, _)) = |
|
769 |
([], (n, next_commit_time (), false)) |
|
770 |
|> fold relearn_old_fact old_facts |
|
771 |
in commit true [] reps; n end |
|
48318 | 772 |
in |
48404 | 773 |
if verbose orelse auto_level < 2 then |
774 |
"Learned " ^ string_of_int n ^ " nontrivial " ^ |
|
775 |
(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
|
776 |
(if verbose then |
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset
|
777 |
" 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
|
778 |
else |
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset
|
779 |
"") ^ "." |
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset
|
780 |
else |
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset
|
781 |
"" |
48318 | 782 |
end |
48308 | 783 |
end |
48304 | 784 |
|
48404 | 785 |
fun mash_learn ctxt (params as {provers, timeout, ...}) fact_override chained |
786 |
atp = |
|
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
787 |
let |
48396 | 788 |
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
|
789 |
val ctxt = ctxt |> Config.put instantiate_inducts false |
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset
|
790 |
val facts = |
48396 | 791 |
nearly_all_facts ctxt false fact_override Symtab.empty css chained [] |
792 |
@{prop True} |
|
48404 | 793 |
val num_facts = length facts |
794 |
val prover = hd provers |
|
795 |
fun learn auto_level atp = |
|
796 |
mash_learn_facts ctxt params prover auto_level atp infinite_timeout facts |
|
797 |
|> Output.urgent_message |
|
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
798 |
in |
48404 | 799 |
(if atp then |
800 |
("MaShing through " ^ string_of_int num_facts ^ " fact" ^ |
|
801 |
plural_s num_facts ^ " for ATP proofs (" ^ quote prover ^ " timeout: " ^ |
|
802 |
string_from_time timeout ^ ").\n\nCollecting Isar proofs first..." |
|
803 |
|> Output.urgent_message; |
|
804 |
learn 1 false; |
|
805 |
"Now collecting ATP proofs. This may take several hours. You can \ |
|
806 |
\safely stop the learning process at any point." |
|
807 |
|> Output.urgent_message; |
|
808 |
learn 0 true) |
|
809 |
else |
|
810 |
("MaShing through " ^ string_of_int num_facts ^ " fact" ^ |
|
811 |
plural_s num_facts ^ " for Isar proofs..." |
|
812 |
|> Output.urgent_message; |
|
813 |
learn 0 false)) |
|
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
814 |
end |
48249 | 815 |
|
48318 | 816 |
(* The threshold should be large enough so that MaSh doesn't kick in for Auto |
817 |
Sledgehammer and Try. *) |
|
818 |
val min_secs_for_learning = 15 |
|
819 |
||
48321 | 820 |
fun relevant_facts ctxt (params as {learn, fact_filter, timeout, ...}) prover |
821 |
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
|
822 |
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
|
823 |
error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".") |
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
824 |
else if only then |
48289 | 825 |
facts |
48321 | 826 |
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
|
827 |
[] |
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset
|
828 |
else |
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset
|
829 |
let |
48327
568b3193e53e
don't include hidden facts in relevance filter + tweak MaSh learning
blanchet
parents:
48326
diff
changeset
|
830 |
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
|
831 |
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
|
832 |
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
|
833 |
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
|
834 |
launch_thread timeout |
48404 | 835 |
(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
|
836 |
timeout facts)) |
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset
|
837 |
end |
48318 | 838 |
else |
839 |
() |
|
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
840 |
val fact_filter = |
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
841 |
case fact_filter of |
48379
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents:
48378
diff
changeset
|
842 |
SOME ff => (() |> ff <> mepoN ? maybe_learn; ff) |
48318 | 843 |
| NONE => |
48386
b903ea11b3bc
use good old MePo filter for SMT solvers by default, since arithmetic is built-in for them
blanchet
parents:
48385
diff
changeset
|
844 |
if is_smt_prover ctxt prover then mepoN |
b903ea11b3bc
use good old MePo filter for SMT solvers by default, since arithmetic is built-in for them
blanchet
parents:
48385
diff
changeset
|
845 |
else if mash_can_suggest_facts ctxt then (maybe_learn (); meshN) |
48379
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents:
48378
diff
changeset
|
846 |
else if mash_could_suggest_facts () then (maybe_learn (); mepoN) |
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents:
48378
diff
changeset
|
847 |
else mepoN |
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset
|
848 |
val add_ths = Attrib.eval_thms ctxt add |
48292 | 849 |
fun prepend_facts ths accepts = |
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset
|
850 |
((facts |> filter (member Thm.eq_thm_prop ths o snd)) @ |
48292 | 851 |
(accepts |> filter_out (member Thm.eq_thm_prop ths o snd))) |
48293 | 852 |
|> take max_facts |
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
853 |
fun iter () = |
48298 | 854 |
iterative_relevant_facts ctxt params prover max_facts NONE hyp_ts |
855 |
concl_t facts |
|
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
856 |
fun mash () = |
48320
891a24a48155
improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
blanchet
parents:
48319
diff
changeset
|
857 |
mash_suggest_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
|
858 |
val mess = |
48320
891a24a48155
improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
blanchet
parents:
48319
diff
changeset
|
859 |
[] |> (if fact_filter <> mashN then cons (iter (), []) else I) |
48379
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents:
48378
diff
changeset
|
860 |
|> (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
|
861 |
in |
48313
0faafdffa662
mesh facts by taking into consideration whether a fact is known to MeSh
blanchet
parents:
48312
diff
changeset
|
862 |
mesh_facts max_facts mess |
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset
|
863 |
|> not (null add_ths) ? prepend_facts add_ths |
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset
|
864 |
end |
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset
|
865 |
|
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset
|
866 |
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
|
867 |
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
|
868 |
|
48248 | 869 |
end; |