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