author | blanchet |
Tue, 19 Nov 2013 18:34:04 +0100 | |
changeset 54503 | b490e15a5e19 |
parent 54432 | 68f8bd1641da |
child 54693 | dd5874e4553f |
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 |
51004
5f2788c38127
distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds
blanchet
parents:
51003
diff
changeset
|
10 |
type raw_fact = Sledgehammer_Fact.raw_fact |
48296
e7f01b7e244e
gracefully handle the case of empty theories when going up the accessibility chain
blanchet
parents:
48293
diff
changeset
|
11 |
type fact = Sledgehammer_Fact.fact |
e7f01b7e244e
gracefully handle the case of empty theories when going up the accessibility chain
blanchet
parents:
48293
diff
changeset
|
12 |
type fact_override = Sledgehammer_Fact.fact_override |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
13 |
type params = Sledgehammer_Provers.params |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
14 |
type prover_result = Sledgehammer_Provers.prover_result |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
15 |
|
48308 | 16 |
val trace : bool Config.T |
51008 | 17 |
val MePoN : string |
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset
|
18 |
val MaShN : string |
51008 | 19 |
val MeShN : string |
48379
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents:
48378
diff
changeset
|
20 |
val mepoN : string |
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents:
48378
diff
changeset
|
21 |
val mashN : string |
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
22 |
val meshN : string |
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
23 |
val unlearnN : string |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
24 |
val learn_isarN : string |
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset
|
25 |
val learn_proverN : string |
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
26 |
val relearn_isarN : string |
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset
|
27 |
val relearn_proverN : string |
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
28 |
val fact_filters : string list |
50826 | 29 |
val encode_str : string -> string |
30 |
val encode_strs : string list -> string |
|
31 |
val unencode_str : string -> string |
|
32 |
val unencode_strs : string -> string list |
|
50356 | 33 |
val encode_features : (string * real) list -> string |
50965 | 34 |
val extract_suggestions : string -> string * string list |
50632
12c097ff3241
slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents:
50631
diff
changeset
|
35 |
|
12c097ff3241
slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents:
50631
diff
changeset
|
36 |
structure MaSh: |
12c097ff3241
slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents:
50631
diff
changeset
|
37 |
sig |
53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset
|
38 |
val unlearn : Proof.context -> bool -> unit |
50632
12c097ff3241
slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents:
50631
diff
changeset
|
39 |
val learn : |
53757
8d1a059ebcdb
reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents:
53756
diff
changeset
|
40 |
Proof.context -> bool -> bool |
53121
5f727525b1ac
only generate feature weights for queries -- they're not used elsewhere
blanchet
parents:
53118
diff
changeset
|
41 |
-> (string * string list * string list * string list) list -> unit |
50632
12c097ff3241
slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents:
50631
diff
changeset
|
42 |
val relearn : |
53757
8d1a059ebcdb
reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents:
53756
diff
changeset
|
43 |
Proof.context -> bool -> bool -> (string * string list) list -> unit |
50969 | 44 |
val query : |
53095 | 45 |
Proof.context -> bool -> int |
53121
5f727525b1ac
only generate feature weights for queries -- they're not used elsewhere
blanchet
parents:
53118
diff
changeset
|
46 |
-> (string * string list * string list * string list) list |
53094 | 47 |
* string list * string list * (string * real) list |
48 |
-> string list |
|
50632
12c097ff3241
slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents:
50631
diff
changeset
|
49 |
end |
12c097ff3241
slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents:
50631
diff
changeset
|
50 |
|
53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset
|
51 |
val mash_unlearn : Proof.context -> params -> unit |
53819
e55d641d0a70
honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset
|
52 |
val is_mash_enabled : unit -> bool |
50624
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset
|
53 |
val nickname_of_thm : thm -> string |
51134 | 54 |
val find_suggested_facts : |
55 |
Proof.context -> ('b * thm) list -> string list -> ('b * thm) list |
|
48321 | 56 |
val mesh_facts : |
50814 | 57 |
('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list |
58 |
-> 'a list |
|
51135 | 59 |
val crude_thm_ord : thm * thm -> order |
51182
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset
|
60 |
val thm_less : thm * thm -> bool |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
61 |
val goal_of_thm : theory -> thm -> thm |
48321 | 62 |
val run_prover_for_mash : |
54141
f57f8e7a879f
generate a comment storing the goal nickname in "learn_prover"
blanchet
parents:
54140
diff
changeset
|
63 |
Proof.context -> params -> string -> string -> fact list -> thm -> prover_result |
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
64 |
val features_of : |
54089
b13f6731f873
use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset
|
65 |
Proof.context -> theory -> int -> int Symtab.table -> stature -> term list -> |
b13f6731f873
use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset
|
66 |
(string * real) list |
51177 | 67 |
val trim_dependencies : string list -> string list option |
50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50732
diff
changeset
|
68 |
val isar_dependencies_of : |
50754
74a6adcb96ac
also generate queries for goals with too many Isar dependencies
blanchet
parents:
50751
diff
changeset
|
69 |
string Symtab.table * string Symtab.table -> thm -> string list |
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset
|
70 |
val prover_dependencies_of : |
51004
5f2788c38127
distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds
blanchet
parents:
51003
diff
changeset
|
71 |
Proof.context -> params -> string -> int -> raw_fact list |
50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50732
diff
changeset
|
72 |
-> string Symtab.table * string Symtab.table -> thm |
50754
74a6adcb96ac
also generate queries for goals with too many Isar dependencies
blanchet
parents:
50751
diff
changeset
|
73 |
-> bool * string list |
53095 | 74 |
val attach_parents_to_facts : |
75 |
('a * thm) list -> ('a * thm) list -> (string list * ('a * thm)) list |
|
53140
a1235e90da5f
pour extra features from proximate facts into goal, in exporter
blanchet
parents:
53137
diff
changeset
|
76 |
val num_extra_feature_facts : int |
53141
d27e99a6a679
take chained and proximate facts into consideration when computing MaSh features
blanchet
parents:
53140
diff
changeset
|
77 |
val extra_feature_factor : real |
53140
a1235e90da5f
pour extra features from proximate facts into goal, in exporter
blanchet
parents:
53137
diff
changeset
|
78 |
val weight_facts_smoothly : 'a list -> ('a * real) list |
a1235e90da5f
pour extra features from proximate facts into goal, in exporter
blanchet
parents:
53137
diff
changeset
|
79 |
val weight_facts_steeply : 'a list -> ('a * real) list |
50412 | 80 |
val find_mash_suggestions : |
51134 | 81 |
Proof.context -> int -> string list -> ('b * thm) list -> ('b * thm) list |
82 |
-> ('b * thm) list -> ('b * thm) list * ('b * thm) list |
|
53127 | 83 |
val add_const_counts : term -> int Symtab.table -> int Symtab.table |
48406 | 84 |
val mash_suggested_facts : |
54503 | 85 |
Proof.context -> params -> int -> term list -> term -> raw_fact list -> fact list * fact list |
86 |
val mash_learn_proof : Proof.context -> params -> term -> ('a * thm) list -> thm list -> unit |
|
48395
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset
|
87 |
val mash_learn : |
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset
|
88 |
Proof.context -> params -> fact_override -> thm list -> bool -> unit |
53819
e55d641d0a70
honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset
|
89 |
|
53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset
|
90 |
val mash_can_suggest_facts : Proof.context -> bool -> bool |
50412 | 91 |
val generous_max_facts : int -> int |
50814 | 92 |
val mepo_weight : real |
93 |
val mash_weight : real |
|
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset
|
94 |
val relevant_facts : |
48292 | 95 |
Proof.context -> params -> string -> int -> fact_override -> term list |
51010 | 96 |
-> term -> raw_fact list -> (string * fact list) list |
53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset
|
97 |
val kill_learners : Proof.context -> params -> unit |
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset
|
98 |
val running_learners : unit -> unit |
48248 | 99 |
end; |
100 |
||
48381 | 101 |
structure Sledgehammer_MaSh : SLEDGEHAMMER_MASH = |
48248 | 102 |
struct |
48249 | 103 |
|
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
104 |
open ATP_Util |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
105 |
open ATP_Problem_Generate |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
106 |
open Sledgehammer_Util |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
107 |
open Sledgehammer_Fact |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
108 |
open Sledgehammer_Provers |
48318 | 109 |
open Sledgehammer_Minimize |
48381 | 110 |
open Sledgehammer_MePo |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
111 |
|
48308 | 112 |
val trace = |
48380 | 113 |
Attrib.setup_config_bool @{binding sledgehammer_mash_trace} (K false) |
51032
69da236d7838
added option to use SNoW as machine learning algo
blanchet
parents:
51029
diff
changeset
|
114 |
|
48308 | 115 |
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else () |
116 |
||
51008 | 117 |
val MePoN = "MePo" |
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset
|
118 |
val MaShN = "MaSh" |
51008 | 119 |
val MeShN = "MeSh" |
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset
|
120 |
|
48379
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents:
48378
diff
changeset
|
121 |
val mepoN = "mepo" |
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
122 |
val mashN = "mash" |
48379
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents:
48378
diff
changeset
|
123 |
val meshN = "mesh" |
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
124 |
|
48379
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents:
48378
diff
changeset
|
125 |
val fact_filters = [meshN, mepoN, mashN] |
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
126 |
|
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
127 |
val unlearnN = "unlearn" |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
128 |
val learn_isarN = "learn_isar" |
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset
|
129 |
val learn_proverN = "learn_prover" |
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
130 |
val relearn_isarN = "relearn_isar" |
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset
|
131 |
val relearn_proverN = "relearn_prover" |
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
132 |
|
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
|
133 |
fun mash_model_dir () = |
50340
72519bf5f135
simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents:
50339
diff
changeset
|
134 |
Path.explode "$ISABELLE_HOME_USER/mash" |> tap Isabelle_System.mkdir |
48394
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset
|
135 |
val mash_state_dir = mash_model_dir |
50310 | 136 |
fun mash_state_file () = Path.append (mash_state_dir ()) (Path.explode "state") |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
137 |
|
48330 | 138 |
|
50311 | 139 |
(*** Low-level communication with MaSh ***) |
140 |
||
53117 | 141 |
val save_models_arg = "--saveModels" |
142 |
val shutdown_server_arg = "--shutdownServer" |
|
143 |
||
50311 | 144 |
fun wipe_out_file file = (try (File.rm o Path.explode) file; ()) |
145 |
||
50335
b17b05c8d4a4
proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents:
50319
diff
changeset
|
146 |
fun write_file banner (xs, f) path = |
b17b05c8d4a4
proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents:
50319
diff
changeset
|
147 |
(case banner of SOME s => File.write path s | NONE => (); |
53094 | 148 |
xs |> chunk_list 500 |> List.app (File.append path o implode o map f)) |
50319
dddcaeb92e11
robust writing of MaSh state -- better drop learning data than cause other problems in Sledgehammer
blanchet
parents:
50311
diff
changeset
|
149 |
handle IO.Io _ => () |
50311 | 150 |
|
53152
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset
|
151 |
fun run_mash_tool ctxt overlord extra_args background write_cmds read_suggs = |
50311 | 152 |
let |
153 |
val (temp_dir, serial) = |
|
154 |
if overlord then (getenv "ISABELLE_HOME_USER", "") |
|
155 |
else (getenv "ISABELLE_TMP", serial_string ()) |
|
53129 | 156 |
val log_file = temp_dir ^ "/mash_log" ^ serial |
50311 | 157 |
val err_file = temp_dir ^ "/mash_err" ^ serial |
158 |
val sugg_file = temp_dir ^ "/mash_suggs" ^ serial |
|
50335
b17b05c8d4a4
proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents:
50319
diff
changeset
|
159 |
val sugg_path = Path.explode sugg_file |
50311 | 160 |
val cmd_file = temp_dir ^ "/mash_commands" ^ serial |
50335
b17b05c8d4a4
proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents:
50319
diff
changeset
|
161 |
val cmd_path = Path.explode cmd_file |
51001 | 162 |
val model_dir = File.shell_path (mash_model_dir ()) |
50311 | 163 |
val command = |
53556
347f743e8336
invoke Python with "no bytecode" option to avoid litering Isabelle source directory with ".pyc" files (which can be problematic for a number of reasons)
blanchet
parents:
53201
diff
changeset
|
164 |
"cd \"$ISABELLE_SLEDGEHAMMER_MASH\"/src; \ |
53790
298774dbdde0
provide a way to override MaSh's port from configuration file
blanchet
parents:
53757
diff
changeset
|
165 |
\PYTHONDONTWRITEBYTECODE=y ./mash.py\ |
298774dbdde0
provide a way to override MaSh's port from configuration file
blanchet
parents:
53757
diff
changeset
|
166 |
\ --quiet\ |
298774dbdde0
provide a way to override MaSh's port from configuration file
blanchet
parents:
53757
diff
changeset
|
167 |
\ --port=$MASH_PORT\ |
53556
347f743e8336
invoke Python with "no bytecode" option to avoid litering Isabelle source directory with ".pyc" files (which can be problematic for a number of reasons)
blanchet
parents:
53201
diff
changeset
|
168 |
\ --outputDir " ^ model_dir ^ |
347f743e8336
invoke Python with "no bytecode" option to avoid litering Isabelle source directory with ".pyc" files (which can be problematic for a number of reasons)
blanchet
parents:
53201
diff
changeset
|
169 |
" --modelFile=" ^ model_dir ^ "/model.pickle\ |
347f743e8336
invoke Python with "no bytecode" option to avoid litering Isabelle source directory with ".pyc" files (which can be problematic for a number of reasons)
blanchet
parents:
53201
diff
changeset
|
170 |
\ --dictsFile=" ^ model_dir ^ "/dict.pickle\ |
53790
298774dbdde0
provide a way to override MaSh's port from configuration file
blanchet
parents:
53757
diff
changeset
|
171 |
\ --log " ^ log_file ^ |
298774dbdde0
provide a way to override MaSh's port from configuration file
blanchet
parents:
53757
diff
changeset
|
172 |
" --inputFile " ^ cmd_file ^ |
298774dbdde0
provide a way to override MaSh's port from configuration file
blanchet
parents:
53757
diff
changeset
|
173 |
" --predictions " ^ sugg_file ^ |
53117 | 174 |
(if extra_args = [] then "" else " " ^ space_implode " " extra_args) ^ |
53152
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset
|
175 |
" >& " ^ err_file ^ |
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset
|
176 |
(if background then " &" else "") |
50311 | 177 |
fun run_on () = |
50750 | 178 |
(Isabelle_System.bash command |
54100 | 179 |
|> tap (fn _ => |
180 |
case try File.read (Path.explode err_file) |> the_default "" of |
|
181 |
"" => trace_msg ctxt (K "Done") |
|
182 |
| s => warning ("MaSh error: " ^ elide_string 1000 s)); |
|
50335
b17b05c8d4a4
proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents:
50319
diff
changeset
|
183 |
read_suggs (fn () => try File.read_lines sugg_path |> these)) |
50311 | 184 |
fun clean_up () = |
185 |
if overlord then () |
|
186 |
else List.app wipe_out_file [err_file, sugg_file, cmd_file] |
|
187 |
in |
|
50335
b17b05c8d4a4
proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents:
50319
diff
changeset
|
188 |
write_file (SOME "") ([], K "") sugg_path; |
b17b05c8d4a4
proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents:
50319
diff
changeset
|
189 |
write_file (SOME "") write_cmds cmd_path; |
50311 | 190 |
trace_msg ctxt (fn () => "Running " ^ command); |
191 |
with_cleanup clean_up run_on () |
|
192 |
end |
|
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
193 |
|
48308 | 194 |
fun meta_char c = |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
195 |
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
|
196 |
c = #")" orelse c = #"," then |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
197 |
String.str c |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
198 |
else |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
199 |
(* fixed width, in case more digits follow *) |
48395
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset
|
200 |
"%" ^ stringN_of_int 3 (Char.ord c) |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
201 |
|
48308 | 202 |
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
|
203 |
| unmeta_chars accum (#"%" :: d1 :: d2 :: d3 :: cs) = |
48308 | 204 |
(case Int.fromString (String.implode [d1, d2, d3]) of |
205 |
SOME n => unmeta_chars (Char.chr n :: accum) cs |
|
206 |
| NONE => "" (* error *)) |
|
48395
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset
|
207 |
| unmeta_chars _ (#"%" :: _) = "" (* error *) |
48308 | 208 |
| unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs |
209 |
||
50826 | 210 |
val encode_str = String.translate meta_char |
211 |
val encode_strs = map encode_str #> space_implode " " |
|
212 |
val unencode_str = String.explode #> unmeta_chars [] |
|
213 |
val unencode_strs = |
|
214 |
space_explode " " #> filter_out (curry (op =) "") #> map unencode_str |
|
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
215 |
|
53558 | 216 |
(* Avoid scientific notation *) |
217 |
fun safe_str_of_real r = |
|
218 |
if r < 0.00001 then "0.00001" |
|
219 |
else if r >= 1000000.0 then "1000000" |
|
220 |
else Markup.print_real r |
|
221 |
||
50356 | 222 |
fun encode_feature (name, weight) = |
50826 | 223 |
encode_str name ^ |
53558 | 224 |
(if Real.== (weight, 1.0) then "" else "=" ^ safe_str_of_real weight) |
50356 | 225 |
|
226 |
val encode_features = map encode_feature #> space_implode " " |
|
227 |
||
50631 | 228 |
fun str_of_learn (name, parents, feats, deps) = |
50826 | 229 |
"! " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^ |
53121
5f727525b1ac
only generate feature weights for queries -- they're not used elsewhere
blanchet
parents:
53118
diff
changeset
|
230 |
encode_strs feats ^ "; " ^ encode_strs deps ^ "\n" |
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset
|
231 |
|
50631 | 232 |
fun str_of_relearn (name, deps) = |
50826 | 233 |
"p " ^ encode_str name ^ ": " ^ encode_strs deps ^ "\n" |
50311 | 234 |
|
53099 | 235 |
fun str_of_query max_suggs (learns, hints, parents, feats) = |
53095 | 236 |
implode (map str_of_learn learns) ^ |
53099 | 237 |
"? " ^ string_of_int max_suggs ^ " # " ^ encode_strs parents ^ "; " ^ |
238 |
encode_features feats ^ |
|
53095 | 239 |
(if null hints then "" else "; " ^ encode_strs hints) ^ "\n" |
48406 | 240 |
|
53098 | 241 |
(* The suggested weights don't make much sense. *) |
48406 | 242 |
fun extract_suggestion sugg = |
243 |
case space_explode "=" sugg of |
|
51177 | 244 |
[name, _ (* weight *)] => |
50965 | 245 |
SOME (unencode_str name (* , Real.fromString weight |> the_default 1.0 *)) |
246 |
| [name] => SOME (unencode_str name (* , 1.0 *)) |
|
48406 | 247 |
| _ => NONE |
248 |
||
50633 | 249 |
fun extract_suggestions line = |
48311 | 250 |
case space_explode ":" line of |
48406 | 251 |
[goal, suggs] => |
50826 | 252 |
(unencode_str goal, map_filter extract_suggestion (space_explode " " suggs)) |
48312 | 253 |
| _ => ("", []) |
48311 | 254 |
|
50632
12c097ff3241
slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents:
50631
diff
changeset
|
255 |
structure MaSh = |
12c097ff3241
slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents:
50631
diff
changeset
|
256 |
struct |
12c097ff3241
slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents:
50631
diff
changeset
|
257 |
|
53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset
|
258 |
fun shutdown ctxt overlord = |
53153 | 259 |
(trace_msg ctxt (K "MaSh shutdown"); |
53756 | 260 |
run_mash_tool ctxt overlord [shutdown_server_arg] false ([], K "") (K ())) |
53152
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset
|
261 |
|
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset
|
262 |
fun save ctxt overlord = |
53153 | 263 |
(trace_msg ctxt (K "MaSh save"); |
264 |
run_mash_tool ctxt overlord [save_models_arg] true ([], K "") (K ())) |
|
53142
966a251efd16
have kill_all also kill MaSh server + be paranoid about reloading after clear_state, to allow for easier experimentation
blanchet
parents:
53141
diff
changeset
|
265 |
|
53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset
|
266 |
fun unlearn ctxt overlord = |
50311 | 267 |
let val path = mash_model_dir () in |
50632
12c097ff3241
slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents:
50631
diff
changeset
|
268 |
trace_msg ctxt (K "MaSh unlearn"); |
53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset
|
269 |
shutdown ctxt overlord; |
50319
dddcaeb92e11
robust writing of MaSh state -- better drop learning data than cause other problems in Sledgehammer
blanchet
parents:
50311
diff
changeset
|
270 |
try (File.fold_dir (fn file => fn _ => |
dddcaeb92e11
robust writing of MaSh state -- better drop learning data than cause other problems in Sledgehammer
blanchet
parents:
50311
diff
changeset
|
271 |
try File.rm (Path.append path (Path.basic file))) |
dddcaeb92e11
robust writing of MaSh state -- better drop learning data than cause other problems in Sledgehammer
blanchet
parents:
50311
diff
changeset
|
272 |
path) NONE; |
50311 | 273 |
() |
274 |
end |
|
275 |
||
53757
8d1a059ebcdb
reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents:
53756
diff
changeset
|
276 |
fun learn _ _ _ [] = () |
8d1a059ebcdb
reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents:
53756
diff
changeset
|
277 |
| learn ctxt overlord save learns = |
54432
68f8bd1641da
have MaSh support nameless facts (i.e. proofs) and use that support
blanchet
parents:
54143
diff
changeset
|
278 |
let val names = elide_string 1000 (space_implode " " (map #1 learns)) in |
68f8bd1641da
have MaSh support nameless facts (i.e. proofs) and use that support
blanchet
parents:
54143
diff
changeset
|
279 |
(trace_msg ctxt (fn () => "MaSh learn" ^ (if names = "" then "" else " " ^ names)); |
68f8bd1641da
have MaSh support nameless facts (i.e. proofs) and use that support
blanchet
parents:
54143
diff
changeset
|
280 |
run_mash_tool ctxt overlord ([] |> save ? cons save_models_arg) false |
68f8bd1641da
have MaSh support nameless facts (i.e. proofs) and use that support
blanchet
parents:
54143
diff
changeset
|
281 |
(learns, str_of_learn) (K ())) |
68f8bd1641da
have MaSh support nameless facts (i.e. proofs) and use that support
blanchet
parents:
54143
diff
changeset
|
282 |
end |
50311 | 283 |
|
53757
8d1a059ebcdb
reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents:
53756
diff
changeset
|
284 |
fun relearn _ _ _ [] = () |
8d1a059ebcdb
reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents:
53756
diff
changeset
|
285 |
| relearn ctxt overlord save relearns = |
50632
12c097ff3241
slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents:
50631
diff
changeset
|
286 |
(trace_msg ctxt (fn () => "MaSh relearn " ^ |
50631 | 287 |
elide_string 1000 (space_implode " " (map #1 relearns))); |
53757
8d1a059ebcdb
reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents:
53756
diff
changeset
|
288 |
run_mash_tool ctxt overlord ([] |> save ? cons save_models_arg) false |
8d1a059ebcdb
reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents:
53756
diff
changeset
|
289 |
(relearns, str_of_relearn) (K ())) |
50311 | 290 |
|
53117 | 291 |
fun query ctxt overlord max_suggs (query as (_, _, _, feats)) = |
50969 | 292 |
(trace_msg ctxt (fn () => "MaSh query " ^ encode_features feats); |
53152
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset
|
293 |
run_mash_tool ctxt overlord [] false ([query], str_of_query max_suggs) |
50311 | 294 |
(fn suggs => |
295 |
case suggs () of |
|
296 |
[] => [] |
|
50633 | 297 |
| suggs => snd (extract_suggestions (List.last suggs))) |
50311 | 298 |
handle List.Empty => []) |
299 |
||
50632
12c097ff3241
slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents:
50631
diff
changeset
|
300 |
end; |
12c097ff3241
slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents:
50631
diff
changeset
|
301 |
|
50311 | 302 |
|
303 |
(*** Middle-level communication with MaSh ***) |
|
304 |
||
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset
|
305 |
datatype proof_kind = |
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset
|
306 |
Isar_Proof | Automatic_Proof | Isar_Proof_wegen_Prover_Flop |
50311 | 307 |
|
308 |
fun str_of_proof_kind Isar_Proof = "i" |
|
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset
|
309 |
| str_of_proof_kind Automatic_Proof = "a" |
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset
|
310 |
| str_of_proof_kind Isar_Proof_wegen_Prover_Flop = "x" |
50311 | 311 |
|
312 |
fun proof_kind_of_str "i" = Isar_Proof |
|
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset
|
313 |
| proof_kind_of_str "a" = Automatic_Proof |
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset
|
314 |
| proof_kind_of_str "x" = Isar_Proof_wegen_Prover_Flop |
50311 | 315 |
|
316 |
(* FIXME: Here a "Graph.update_node" function would be useful *) |
|
50610 | 317 |
fun update_access_graph_node (name, kind) = |
50311 | 318 |
Graph.default_node (name, Isar_Proof) |
319 |
#> kind <> Isar_Proof ? Graph.map_node name (K kind) |
|
320 |
||
321 |
fun try_graph ctxt when def f = |
|
322 |
f () |
|
323 |
handle Graph.CYCLES (cycle :: _) => |
|
324 |
(trace_msg ctxt (fn () => |
|
325 |
"Cycle involving " ^ commas cycle ^ " when " ^ when); def) |
|
326 |
| Graph.DUP name => |
|
327 |
(trace_msg ctxt (fn () => |
|
328 |
"Duplicate fact " ^ quote name ^ " when " ^ when); def) |
|
329 |
| Graph.UNDEF name => |
|
330 |
(trace_msg ctxt (fn () => |
|
331 |
"Unknown fact " ^ quote name ^ " when " ^ when); def) |
|
332 |
| exn => |
|
333 |
if Exn.is_interrupt exn then |
|
334 |
reraise exn |
|
335 |
else |
|
336 |
(trace_msg ctxt (fn () => |
|
337 |
"Internal error when " ^ when ^ ":\n" ^ |
|
338 |
ML_Compiler.exn_message exn); def) |
|
339 |
||
340 |
fun graph_info G = |
|
341 |
string_of_int (length (Graph.keys G)) ^ " node(s), " ^ |
|
342 |
string_of_int (fold (Integer.add o length o snd) (Graph.dest G) 0) ^ |
|
343 |
" edge(s), " ^ |
|
344 |
string_of_int (length (Graph.minimals G)) ^ " minimal, " ^ |
|
345 |
string_of_int (length (Graph.maximals G)) ^ " maximal" |
|
346 |
||
53095 | 347 |
type mash_state = |
348 |
{access_G : unit Graph.T, |
|
349 |
num_known_facts : int, |
|
350 |
dirty : string list option} |
|
50311 | 351 |
|
53095 | 352 |
val empty_state = {access_G = Graph.empty, num_known_facts = 0, dirty = SOME []} |
50311 | 353 |
|
354 |
local |
|
355 |
||
53095 | 356 |
val version = "*** MaSh version 20130820 ***" |
50357
187ae76a1757
more robustness in the face of MaSh format changes -- don't overwrite new versions with old versions
blanchet
parents:
50356
diff
changeset
|
357 |
|
53095 | 358 |
exception FILE_VERSION_TOO_NEW of unit |
50311 | 359 |
|
360 |
fun extract_node line = |
|
361 |
case space_explode ":" line of |
|
362 |
[head, parents] => |
|
363 |
(case space_explode " " head of |
|
364 |
[kind, name] => |
|
50826 | 365 |
SOME (unencode_str name, unencode_strs parents, |
50311 | 366 |
try proof_kind_of_str kind |> the_default Isar_Proof) |
367 |
| _ => NONE) |
|
368 |
| _ => NONE |
|
369 |
||
53152
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset
|
370 |
fun load_state _ _ (state as (true, _)) = state |
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset
|
371 |
| load_state ctxt overlord _ = |
50311 | 372 |
let val path = mash_state_file () in |
373 |
(true, |
|
374 |
case try File.read_lines path of |
|
375 |
SOME (version' :: node_lines) => |
|
376 |
let |
|
377 |
fun add_edge_to name parent = |
|
378 |
Graph.default_node (parent, Isar_Proof) |
|
379 |
#> Graph.add_edge (parent, name) |
|
380 |
fun add_node line = |
|
381 |
case extract_node line of |
|
382 |
NONE => I (* shouldn't happen *) |
|
383 |
| SOME (name, parents, kind) => |
|
50610 | 384 |
update_access_graph_node (name, kind) |
50311 | 385 |
#> fold (add_edge_to name) parents |
53095 | 386 |
val (access_G, num_known_facts) = |
50357
187ae76a1757
more robustness in the face of MaSh format changes -- don't overwrite new versions with old versions
blanchet
parents:
50356
diff
changeset
|
387 |
case string_ord (version', version) of |
187ae76a1757
more robustness in the face of MaSh format changes -- don't overwrite new versions with old versions
blanchet
parents:
50356
diff
changeset
|
388 |
EQUAL => |
53095 | 389 |
(try_graph ctxt "loading state" Graph.empty (fn () => |
390 |
fold add_node node_lines Graph.empty), |
|
391 |
length node_lines) |
|
50860 | 392 |
| LESS => |
53095 | 393 |
(* can't parse old file *) |
53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset
|
394 |
(MaSh.unlearn ctxt overlord; (Graph.empty, 0)) |
53095 | 395 |
| GREATER => raise FILE_VERSION_TOO_NEW () |
50311 | 396 |
in |
397 |
trace_msg ctxt (fn () => |
|
50610 | 398 |
"Loaded fact graph (" ^ graph_info access_G ^ ")"); |
53095 | 399 |
{access_G = access_G, num_known_facts = num_known_facts, |
400 |
dirty = SOME []} |
|
50311 | 401 |
end |
402 |
| _ => empty_state) |
|
403 |
end |
|
404 |
||
53152
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset
|
405 |
fun save_state _ (state as {dirty = SOME [], ...}) = state |
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset
|
406 |
| save_state ctxt {access_G, num_known_facts, dirty} = |
50311 | 407 |
let |
408 |
fun str_of_entry (name, parents, kind) = |
|
50826 | 409 |
str_of_proof_kind kind ^ " " ^ encode_str name ^ ": " ^ |
410 |
encode_strs parents ^ "\n" |
|
50311 | 411 |
fun append_entry (name, (kind, (parents, _))) = |
412 |
cons (name, Graph.Keys.dest parents, kind) |
|
413 |
val (banner, entries) = |
|
414 |
case dirty of |
|
415 |
SOME names => |
|
50610 | 416 |
(NONE, fold (append_entry o Graph.get_entry access_G) names []) |
417 |
| NONE => (SOME (version ^ "\n"), Graph.fold append_entry access_G []) |
|
50311 | 418 |
in |
50335
b17b05c8d4a4
proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents:
50319
diff
changeset
|
419 |
write_file banner (entries, str_of_entry) (mash_state_file ()); |
50311 | 420 |
trace_msg ctxt (fn () => |
50610 | 421 |
"Saved fact graph (" ^ graph_info access_G ^ |
50311 | 422 |
(case dirty of |
423 |
SOME dirty => |
|
424 |
"; " ^ string_of_int (length dirty) ^ " dirty fact(s)" |
|
425 |
| _ => "") ^ ")"); |
|
53095 | 426 |
{access_G = access_G, num_known_facts = num_known_facts, dirty = SOME []} |
50311 | 427 |
end |
428 |
||
429 |
val global_state = |
|
430 |
Synchronized.var "Sledgehammer_MaSh.global_state" (false, empty_state) |
|
431 |
||
432 |
in |
|
433 |
||
53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset
|
434 |
fun map_state ctxt overlord f = |
53152
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset
|
435 |
Synchronized.change global_state |
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset
|
436 |
(load_state ctxt overlord ##> (f #> save_state ctxt)) |
53095 | 437 |
handle FILE_VERSION_TOO_NEW () => () |
50311 | 438 |
|
53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset
|
439 |
fun peek_state ctxt overlord f = |
50357
187ae76a1757
more robustness in the face of MaSh format changes -- don't overwrite new versions with old versions
blanchet
parents:
50356
diff
changeset
|
440 |
Synchronized.change_result global_state |
53152
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset
|
441 |
(perhaps (try (load_state ctxt overlord)) #> `snd #>> f) |
50311 | 442 |
|
53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset
|
443 |
fun clear_state ctxt overlord = |
50311 | 444 |
Synchronized.change global_state (fn _ => |
53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset
|
445 |
(MaSh.unlearn ctxt overlord; (* also removes the state file *) |
53142
966a251efd16
have kill_all also kill MaSh server + be paranoid about reloading after clear_state, to allow for easier experimentation
blanchet
parents:
53141
diff
changeset
|
446 |
(false, empty_state))) |
50311 | 447 |
|
448 |
end |
|
449 |
||
53558 | 450 |
fun mash_unlearn ctxt ({overlord, ...} : params) = |
53559
3858246c7c8f
when pouring in extra features into the goal, only consider facts from the current theory -- the bottom 10 facts of the last import might be completely unrelated
blanchet
parents:
53558
diff
changeset
|
451 |
(clear_state ctxt overlord; Output.urgent_message "Reset MaSh.") |
50570 | 452 |
|
50311 | 453 |
|
454 |
(*** Isabelle helpers ***) |
|
455 |
||
53819
e55d641d0a70
honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset
|
456 |
fun is_mash_enabled () = (getenv "MASH" = "yes") |
e55d641d0a70
honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset
|
457 |
|
50722 | 458 |
val local_prefix = "local" ^ Long_Name.separator |
48378 | 459 |
|
50722 | 460 |
fun elided_backquote_thm threshold th = |
461 |
elide_string threshold |
|
462 |
(backquote_thm (Proof_Context.init_global (Thm.theory_of_thm th)) th) |
|
48378 | 463 |
|
51181
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset
|
464 |
val thy_name_of_thm = Context.theory_name o Thm.theory_of_thm |
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset
|
465 |
|
50624
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset
|
466 |
fun nickname_of_thm th = |
48394
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset
|
467 |
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
|
468 |
let val hint = Thm.get_name_hint th in |
50722 | 469 |
(* There must be a better way to detect local facts. *) |
48394
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset
|
470 |
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
|
471 |
SOME suf => |
51181
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset
|
472 |
thy_name_of_thm th ^ Long_Name.separator ^ suf ^ |
50732 | 473 |
Long_Name.separator ^ elided_backquote_thm 50 th |
48394
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset
|
474 |
| 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
|
475 |
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
|
476 |
else |
50722 | 477 |
elided_backquote_thm 200 th |
48378 | 478 |
|
51134 | 479 |
fun find_suggested_facts ctxt facts = |
48330 | 480 |
let |
51134 | 481 |
fun add (fact as (_, th)) = Symtab.default (nickname_of_thm th, fact) |
482 |
val tab = fold add facts Symtab.empty |
|
483 |
fun lookup nick = |
|
484 |
Symtab.lookup tab nick |
|
485 |
|> tap (fn NONE => trace_msg ctxt (fn () => "Cannot find " ^ quote nick) |
|
486 |
| _ => ()) |
|
487 |
in map_filter lookup end |
|
48311 | 488 |
|
50383
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset
|
489 |
fun scaled_avg [] = 0 |
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset
|
490 |
| scaled_avg xs = |
48407 | 491 |
Real.ceil (100000000.0 * fold (curry (op +)) xs 0.0) div length xs |
48328
ca0b7d19dd62
attempt at meshing according to more meaningful factors
blanchet
parents:
48327
diff
changeset
|
492 |
|
50383
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset
|
493 |
fun avg [] = 0.0 |
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset
|
494 |
| avg xs = fold (curry (op +)) xs 0.0 / Real.fromInt (length xs) |
48313
0faafdffa662
mesh facts by taking into consideration whether a fact is known to MeSh
blanchet
parents:
48312
diff
changeset
|
495 |
|
50383
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset
|
496 |
fun normalize_scores _ [] = [] |
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset
|
497 |
| normalize_scores max_facts xs = |
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset
|
498 |
let val avg = avg (map snd (take max_facts xs)) in |
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset
|
499 |
map (apsnd (curry Real.* (1.0 / avg))) xs |
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset
|
500 |
end |
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset
|
501 |
|
50814 | 502 |
fun mesh_facts _ max_facts [(_, (sels, unks))] = |
48406 | 503 |
map fst (take max_facts sels) @ take (max_facts - length sels) unks |
50861
fa4253914e98
honor unknown chained in MaSh and a few other tweaks
blanchet
parents:
50860
diff
changeset
|
504 |
| mesh_facts fact_eq max_facts mess = |
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
505 |
let |
51029 | 506 |
val mess = mess |> map (apsnd (apfst (normalize_scores max_facts))) |
507 |
fun score_in fact (global_weight, (sels, unks)) = |
|
50383
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset
|
508 |
let |
54089
b13f6731f873
use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset
|
509 |
val score_at = try (nth sels) #> Option.map (fn (_, score) => global_weight * score) |
50383
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset
|
510 |
in |
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset
|
511 |
case find_index (curry fact_eq fact o fst) sels of |
54089
b13f6731f873
use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset
|
512 |
~1 => if member fact_eq unks fact then NONE else SOME 0.0 |
50383
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset
|
513 |
| rank => score_at rank |
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset
|
514 |
end |
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset
|
515 |
fun weight_of fact = mess |> map_filter (score_in fact) |> scaled_avg |
54089
b13f6731f873
use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset
|
516 |
val facts = fold (union fact_eq o map fst o take max_facts o fst o snd) mess [] |
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
517 |
in |
48406 | 518 |
facts |> map (`weight_of) |> sort (int_ord o swap o pairself fst) |
48328
ca0b7d19dd62
attempt at meshing according to more meaningful factors
blanchet
parents:
48327
diff
changeset
|
519 |
|> map snd |> take max_facts |
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
520 |
end |
48312 | 521 |
|
53155 | 522 |
fun free_feature_of s = ("f" ^ s, 40.0 (* FUDGE *)) |
50874
2eae85887282
adjust weights -- sorts are prolific, so tone them down even more
blanchet
parents:
50869
diff
changeset
|
523 |
fun thy_feature_of s = ("y" ^ s, 8.0 (* FUDGE *)) |
2eae85887282
adjust weights -- sorts are prolific, so tone them down even more
blanchet
parents:
50869
diff
changeset
|
524 |
fun type_feature_of s = ("t" ^ s, 4.0 (* FUDGE *)) |
50584
4fff0898cc0e
tuned weights -- keep same relative values, but use 1.0 as the least weight
blanchet
parents:
50583
diff
changeset
|
525 |
fun class_feature_of s = ("s" ^ s, 1.0 (* FUDGE *)) |
53155 | 526 |
val local_feature = ("local", 16.0 (* FUDGE *)) |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
527 |
|
51135 | 528 |
fun crude_theory_ord p = |
50722 | 529 |
if Theory.subthy p then |
530 |
if Theory.eq_thy p then EQUAL else LESS |
|
48324 | 531 |
else if Theory.subthy (swap p) then |
532 |
GREATER |
|
533 |
else case int_ord (pairself (length o Theory.ancestors_of) p) of |
|
534 |
EQUAL => string_ord (pairself Context.theory_name p) |
|
535 |
| order => order |
|
536 |
||
51135 | 537 |
fun crude_thm_ord p = |
538 |
case crude_theory_ord (pairself theory_of_thm p) of |
|
50359
da395f0e7dea
tweaked order of theorems to avoid forward dependencies (MaSh)
blanchet
parents:
50357
diff
changeset
|
539 |
EQUAL => |
50624
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset
|
540 |
let val q = pairself nickname_of_thm p in |
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset
|
541 |
(* Hack to put "xxx_def" before "xxxI" and "xxxE" *) |
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset
|
542 |
case bool_ord (pairself (String.isSuffix "_def") (swap q)) of |
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset
|
543 |
EQUAL => string_ord q |
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset
|
544 |
| ord => ord |
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset
|
545 |
end |
50359
da395f0e7dea
tweaked order of theorems to avoid forward dependencies (MaSh)
blanchet
parents:
50357
diff
changeset
|
546 |
| ord => ord |
48324 | 547 |
|
51136 | 548 |
val thm_less_eq = Theory.subthy o pairself theory_of_thm |
549 |
fun thm_less p = thm_less_eq p andalso not (thm_less_eq (swap p)) |
|
550 |
||
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
551 |
val freezeT = Type.legacy_freeze_type |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
552 |
|
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
553 |
fun freeze (t $ u) = freeze t $ freeze u |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
554 |
| 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
|
555 |
| freeze (Var ((s, _), T)) = Free (s, freezeT T) |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
556 |
| freeze (Const (s, T)) = Const (s, freezeT T) |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
557 |
| freeze (Free (s, T)) = Free (s, freezeT T) |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
558 |
| freeze t = t |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
559 |
|
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
560 |
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
|
561 |
|
54141
f57f8e7a879f
generate a comment storing the goal nickname in "learn_prover"
blanchet
parents:
54140
diff
changeset
|
562 |
fun run_prover_for_mash ctxt params prover goal_name facts goal = |
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
563 |
let |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
564 |
val problem = |
54141
f57f8e7a879f
generate a comment storing the goal nickname in "learn_prover"
blanchet
parents:
54140
diff
changeset
|
565 |
{comment = "Goal: " ^ goal_name, state = Proof.init ctxt, goal = goal, subgoal = 1, |
f57f8e7a879f
generate a comment storing the goal nickname in "learn_prover"
blanchet
parents:
54140
diff
changeset
|
566 |
subgoal_count = 1, factss = [("", facts)]} |
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
567 |
in |
54503 | 568 |
get_minimizing_prover ctxt MaSh (K ()) prover params (K (K (K ""))) problem |
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
569 |
end |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
570 |
|
48326 | 571 |
val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}] |
572 |
||
53086
15fe0ca088b3
MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents:
53085
diff
changeset
|
573 |
val pat_tvar_prefix = "_" |
15fe0ca088b3
MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents:
53085
diff
changeset
|
574 |
val pat_var_prefix = "_" |
15fe0ca088b3
MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents:
53085
diff
changeset
|
575 |
|
53089 | 576 |
(* try "Long_Name.base_name" for shorter names *) |
577 |
fun massage_long_name s = s |
|
53083
019ecbb18e3f
generate patterns for variables as well in MaSh (cf. HOL(y)Hammer)
blanchet
parents:
53082
diff
changeset
|
578 |
|
53086
15fe0ca088b3
MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents:
53085
diff
changeset
|
579 |
val crude_str_of_sort = |
15fe0ca088b3
MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents:
53085
diff
changeset
|
580 |
space_implode ":" o map massage_long_name o subtract (op =) @{sort type} |
15fe0ca088b3
MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents:
53085
diff
changeset
|
581 |
|
15fe0ca088b3
MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents:
53085
diff
changeset
|
582 |
fun crude_str_of_typ (Type (s, [])) = massage_long_name s |
53083
019ecbb18e3f
generate patterns for variables as well in MaSh (cf. HOL(y)Hammer)
blanchet
parents:
53082
diff
changeset
|
583 |
| crude_str_of_typ (Type (s, Ts)) = |
53128 | 584 |
massage_long_name s ^ implode (map crude_str_of_typ Ts) |
53083
019ecbb18e3f
generate patterns for variables as well in MaSh (cf. HOL(y)Hammer)
blanchet
parents:
53082
diff
changeset
|
585 |
| crude_str_of_typ (TFree (_, S)) = crude_str_of_sort S |
019ecbb18e3f
generate patterns for variables as well in MaSh (cf. HOL(y)Hammer)
blanchet
parents:
53082
diff
changeset
|
586 |
| crude_str_of_typ (TVar (_, S)) = crude_str_of_sort S |
019ecbb18e3f
generate patterns for variables as well in MaSh (cf. HOL(y)Hammer)
blanchet
parents:
53082
diff
changeset
|
587 |
|
53128 | 588 |
fun maybe_singleton_str _ "" = [] |
589 |
| maybe_singleton_str pref s = [pref ^ s] |
|
590 |
||
53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset
|
591 |
val max_pat_breadth = 10 (* FUDGE *) |
50585 | 592 |
|
54089
b13f6731f873
use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset
|
593 |
fun term_features_of ctxt thy_name num_facts const_tab term_max_depth type_max_depth ts = |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
594 |
let |
50392
190053ee24ed
expand type classes into their ancestors for MaSh
blanchet
parents:
50391
diff
changeset
|
595 |
val thy = Proof_Context.theory_of ctxt |
53082 | 596 |
|
50393 | 597 |
val fixes = map snd (Variable.dest_fixes ctxt) |
50392
190053ee24ed
expand type classes into their ancestors for MaSh
blanchet
parents:
50391
diff
changeset
|
598 |
val classes = Sign.classes_of thy |
53082 | 599 |
|
48304 | 600 |
fun add_classes @{sort type} = I |
50392
190053ee24ed
expand type classes into their ancestors for MaSh
blanchet
parents:
50391
diff
changeset
|
601 |
| add_classes S = |
190053ee24ed
expand type classes into their ancestors for MaSh
blanchet
parents:
50391
diff
changeset
|
602 |
fold (`(Sorts.super_classes classes) |
190053ee24ed
expand type classes into their ancestors for MaSh
blanchet
parents:
50391
diff
changeset
|
603 |
#> swap #> op :: |
53086
15fe0ca088b3
MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents:
53085
diff
changeset
|
604 |
#> subtract (op =) @{sort type} #> map massage_long_name |
50392
190053ee24ed
expand type classes into their ancestors for MaSh
blanchet
parents:
50391
diff
changeset
|
605 |
#> map class_feature_of |
53159 | 606 |
#> union (eq_fst (op =))) S |
53082 | 607 |
|
608 |
fun pattify_type 0 _ = [] |
|
609 |
| pattify_type _ (Type (s, [])) = |
|
53086
15fe0ca088b3
MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents:
53085
diff
changeset
|
610 |
if member (op =) bad_types s then [] else [massage_long_name s] |
53082 | 611 |
| pattify_type depth (Type (s, U :: Ts)) = |
612 |
let |
|
613 |
val T = Type (s, Ts) |
|
614 |
val ps = take max_pat_breadth (pattify_type depth T) |
|
615 |
val qs = take max_pat_breadth ("" :: pattify_type (depth - 1) U) |
|
53130 | 616 |
in map_product (fn p => fn "" => p | q => p ^ "(" ^ q ^ ")") ps qs end |
53128 | 617 |
| pattify_type _ (TFree (_, S)) = |
618 |
maybe_singleton_str pat_tvar_prefix (crude_str_of_sort S) |
|
619 |
| pattify_type _ (TVar (_, S)) = |
|
620 |
maybe_singleton_str pat_tvar_prefix (crude_str_of_sort S) |
|
53082 | 621 |
fun add_type_pat depth T = |
53159 | 622 |
union (eq_fst (op =)) (map type_feature_of (pattify_type depth T)) |
53082 | 623 |
fun add_type_pats 0 _ = I |
624 |
| add_type_pats depth t = |
|
625 |
add_type_pat depth t #> add_type_pats (depth - 1) t |
|
53083
019ecbb18e3f
generate patterns for variables as well in MaSh (cf. HOL(y)Hammer)
blanchet
parents:
53082
diff
changeset
|
626 |
fun add_type T = |
019ecbb18e3f
generate patterns for variables as well in MaSh (cf. HOL(y)Hammer)
blanchet
parents:
53082
diff
changeset
|
627 |
add_type_pats type_max_depth T |
53156 | 628 |
#> fold_atyps_sorts (add_classes o snd) T |
53084 | 629 |
fun add_subtypes (T as Type (_, Ts)) = add_type T #> fold add_subtypes Ts |
630 |
| add_subtypes T = add_type T |
|
53082 | 631 |
|
53130 | 632 |
fun weight_of_const s = |
633 |
16.0 + |
|
634 |
(if num_facts = 0 then |
|
635 |
0.0 |
|
636 |
else |
|
637 |
let val count = Symtab.lookup const_tab s |> the_default 1 in |
|
53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset
|
638 |
Real.fromInt num_facts / Real.fromInt count (* FUDGE *) |
53130 | 639 |
end) |
54089
b13f6731f873
use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset
|
640 |
fun pattify_term _ 0 _ = [] |
b13f6731f873
use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset
|
641 |
| pattify_term _ _ (Const (s, _)) = |
b13f6731f873
use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset
|
642 |
if is_widely_irrelevant_const s then [] else [(massage_long_name s, weight_of_const s)] |
b13f6731f873
use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset
|
643 |
| pattify_term _ _ (Free (s, T)) = |
53128 | 644 |
maybe_singleton_str pat_var_prefix (crude_str_of_typ T) |
53130 | 645 |
|> map (rpair 0.0) |
53090
1426c97311f2
treat frees as both consts and vars, for more hits
blanchet
parents:
53089
diff
changeset
|
646 |
|> (if member (op =) fixes s then |
53130 | 647 |
cons (free_feature_of (massage_long_name |
648 |
(thy_name ^ Long_Name.separator ^ s))) |
|
53090
1426c97311f2
treat frees as both consts and vars, for more hits
blanchet
parents:
53089
diff
changeset
|
649 |
else |
1426c97311f2
treat frees as both consts and vars, for more hits
blanchet
parents:
53089
diff
changeset
|
650 |
I) |
54089
b13f6731f873
use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset
|
651 |
| pattify_term _ _ (Var (_, T)) = |
b13f6731f873
use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset
|
652 |
maybe_singleton_str pat_var_prefix (crude_str_of_typ T) |> map (rpair 0.0) |
b13f6731f873
use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset
|
653 |
| pattify_term Ts _ (Bound j) = |
b13f6731f873
use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset
|
654 |
maybe_singleton_str pat_var_prefix (crude_str_of_typ (nth Ts j)) |> map (rpair 0.0) |
b13f6731f873
use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset
|
655 |
| pattify_term Ts depth (t $ u) = |
50339
d8dae91f3107
MaSh improvements: deeper patterns + more respect for chained facts
blanchet
parents:
50338
diff
changeset
|
656 |
let |
54089
b13f6731f873
use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset
|
657 |
val ps = take max_pat_breadth (pattify_term Ts depth t) |
b13f6731f873
use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset
|
658 |
val qs = take max_pat_breadth (("", 0.0) :: pattify_term Ts (depth - 1) u) |
53130 | 659 |
in |
660 |
map_product (fn ppw as (p, pw) => |
|
661 |
fn ("", _) => ppw |
|
662 |
| (q, qw) => (p ^ "(" ^ q ^ ")", pw + qw)) ps qs |
|
663 |
end |
|
54089
b13f6731f873
use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset
|
664 |
| pattify_term _ _ _ = [] |
b13f6731f873
use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset
|
665 |
fun add_term_pat Ts = union (eq_fst (op =)) oo pattify_term Ts |
53130 | 666 |
fun add_term_pats _ 0 _ = I |
667 |
| add_term_pats Ts depth t = |
|
668 |
add_term_pat Ts depth t #> add_term_pats Ts (depth - 1) t |
|
669 |
fun add_term Ts = add_term_pats Ts term_max_depth |
|
53085 | 670 |
fun add_subterms Ts t = |
50857
80768e28c9ee
better handlig of built-ins -- at the top-level, not in subterms
blanchet
parents:
50841
diff
changeset
|
671 |
case strip_comb t of |
54089
b13f6731f873
use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset
|
672 |
(Const (s, T), args) => |
b13f6731f873
use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset
|
673 |
(not (is_widely_irrelevant_const s) ? add_term Ts t) |
b13f6731f873
use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset
|
674 |
#> add_subtypes T |
b13f6731f873
use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset
|
675 |
#> fold (add_subterms Ts) args |
50857
80768e28c9ee
better handlig of built-ins -- at the top-level, not in subterms
blanchet
parents:
50841
diff
changeset
|
676 |
| (head, args) => |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
677 |
(case head of |
53130 | 678 |
Free (_, T) => add_term Ts t #> add_subtypes T |
53084 | 679 |
| Var (_, T) => add_subtypes T |
53085 | 680 |
| Abs (_, T, body) => add_subtypes T #> add_subterms (T :: Ts) body |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
681 |
| _ => I) |
53085 | 682 |
#> fold (add_subterms Ts) args |
683 |
in [] |> fold (add_subterms []) ts end |
|
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
684 |
|
53085 | 685 |
val term_max_depth = 2 |
53155 | 686 |
val type_max_depth = 1 |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
687 |
|
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
688 |
(* TODO: Generate type classes for types? *) |
54089
b13f6731f873
use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset
|
689 |
fun features_of ctxt thy num_facts const_tab (scope, _) ts = |
50393 | 690 |
let val thy_name = Context.theory_name thy in |
691 |
thy_feature_of thy_name :: |
|
54089
b13f6731f873
use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset
|
692 |
term_features_of ctxt thy_name num_facts const_tab term_max_depth type_max_depth ts |
50393 | 693 |
|> scope <> Global ? cons local_feature |
694 |
end |
|
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
695 |
|
50434
960a3429615c
more MaSh tweaking -- in particular, export the same facts in "MaSh_Export" as are later tried in "MaSh_Eval"
blanchet
parents:
50412
diff
changeset
|
696 |
(* Too many dependencies is a sign that a decision procedure is at work. There |
960a3429615c
more MaSh tweaking -- in particular, export the same facts in "MaSh_Export" as are later tried in "MaSh_Eval"
blanchet
parents:
50412
diff
changeset
|
697 |
isn't much to learn from such proofs. *) |
960a3429615c
more MaSh tweaking -- in particular, export the same facts in "MaSh_Export" as are later tried in "MaSh_Eval"
blanchet
parents:
50412
diff
changeset
|
698 |
val max_dependencies = 20 |
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset
|
699 |
|
54125
420b876ff1e2
if slicing is disabled, don't enforce last slice's "max_facts", but rather the maximum "max_facts"
blanchet
parents:
54123
diff
changeset
|
700 |
val prover_default_max_facts = 25 |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
701 |
|
48438
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset
|
702 |
(* "type_definition_xxx" facts are characterized by their use of "CollectI". *) |
50755 | 703 |
val typedef_dep = nickname_of_thm @{thm CollectI} |
704 |
(* Mysterious parts of the class machinery create lots of proofs that refer |
|
52071 | 705 |
exclusively to "someI_ex" (and to some internal constructions). *) |
50755 | 706 |
val class_some_dep = nickname_of_thm @{thm someI_ex} |
48438
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset
|
707 |
|
50828 | 708 |
val fundef_ths = |
709 |
@{thms fundef_ex1_existence fundef_ex1_uniqueness fundef_ex1_iff |
|
710 |
fundef_default_value} |
|
711 |
|> map nickname_of_thm |
|
712 |
||
48438
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset
|
713 |
(* "Rep_xxx_inject", "Abs_xxx_inverse", etc., are derived using these facts. *) |
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset
|
714 |
val typedef_ths = |
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset
|
715 |
@{thms type_definition.Abs_inverse type_definition.Rep_inverse |
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset
|
716 |
type_definition.Rep type_definition.Rep_inject |
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset
|
717 |
type_definition.Abs_inject type_definition.Rep_cases |
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset
|
718 |
type_definition.Abs_cases type_definition.Rep_induct |
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset
|
719 |
type_definition.Abs_induct type_definition.Rep_range |
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset
|
720 |
type_definition.Abs_image} |
50624
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset
|
721 |
|> map nickname_of_thm |
48438
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48436
diff
changeset
|
722 |
|
48441 | 723 |
fun is_size_def [dep] th = |
724 |
(case first_field ".recs" dep of |
|
725 |
SOME (pref, _) => |
|
50624
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset
|
726 |
(case first_field ".size" (nickname_of_thm th) of |
48441 | 727 |
SOME (pref', _) => pref = pref' |
728 |
| NONE => false) |
|
729 |
| NONE => false) |
|
730 |
| is_size_def _ _ = false |
|
731 |
||
53095 | 732 |
fun no_dependencies_for_status status = |
733 |
status = Non_Rec_Def orelse status = Rec_Def |
|
734 |
||
51177 | 735 |
fun trim_dependencies deps = |
50755 | 736 |
if length deps > max_dependencies then NONE else SOME deps |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
737 |
|
50755 | 738 |
fun isar_dependencies_of name_tabs th = |
51020 | 739 |
let val deps = thms_in_proof (SOME name_tabs) th in |
50828 | 740 |
if deps = [typedef_dep] orelse |
741 |
deps = [class_some_dep] orelse |
|
742 |
exists (member (op =) fundef_ths) deps orelse |
|
743 |
exists (member (op =) typedef_ths) deps orelse |
|
744 |
is_size_def deps th then |
|
50755 | 745 |
[] |
746 |
else |
|
747 |
deps |
|
748 |
end |
|
48404 | 749 |
|
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset
|
750 |
fun prover_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover |
50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50732
diff
changeset
|
751 |
auto_level facts name_tabs th = |
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50732
diff
changeset
|
752 |
case isar_dependencies_of name_tabs th of |
50754
74a6adcb96ac
also generate queries for goals with too many Isar dependencies
blanchet
parents:
50751
diff
changeset
|
753 |
[] => (false, []) |
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
754 |
| isar_deps => |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
755 |
let |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
756 |
val thy = Proof_Context.theory_of ctxt |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
757 |
val goal = goal_of_thm thy th |
54141
f57f8e7a879f
generate a comment storing the goal nickname in "learn_prover"
blanchet
parents:
54140
diff
changeset
|
758 |
val name = nickname_of_thm th |
52196
2281f33e8da6
redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])
blanchet
parents:
52125
diff
changeset
|
759 |
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt |
51136 | 760 |
val facts = facts |> filter (fn (_, th') => thm_less (th', th)) |
51004
5f2788c38127
distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds
blanchet
parents:
51003
diff
changeset
|
761 |
fun nickify ((_, stature), th) = ((nickname_of_thm th, stature), th) |
50624
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset
|
762 |
fun is_dep dep (_, th) = nickname_of_thm th = dep |
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
763 |
fun add_isar_dep facts dep accum = |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
764 |
if exists (is_dep dep) accum then |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
765 |
accum |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
766 |
else case find_first (is_dep dep) facts of |
51004
5f2788c38127
distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds
blanchet
parents:
51003
diff
changeset
|
767 |
SOME ((_, status), th) => accum @ [(("", status), th)] |
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
768 |
| NONE => accum (* shouldn't happen *) |
54123
271a8377656f
remove overloading of "max_facts" -- it already controls the number of facts passed to ATPs for 'learn_prover'
blanchet
parents:
54115
diff
changeset
|
769 |
val mepo_facts = |
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset
|
770 |
facts |
54095 | 771 |
|> mepo_suggested_facts ctxt params (max_facts |> the_default prover_default_max_facts) NONE |
772 |
hyp_ts concl_t |
|
54123
271a8377656f
remove overloading of "max_facts" -- it already controls the number of facts passed to ATPs for 'learn_prover'
blanchet
parents:
54115
diff
changeset
|
773 |
val facts = |
271a8377656f
remove overloading of "max_facts" -- it already controls the number of facts passed to ATPs for 'learn_prover'
blanchet
parents:
54115
diff
changeset
|
774 |
mepo_facts |
50754
74a6adcb96ac
also generate queries for goals with too many Isar dependencies
blanchet
parents:
50751
diff
changeset
|
775 |
|> fold (add_isar_dep facts) isar_deps |
50624
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset
|
776 |
|> map nickify |
54123
271a8377656f
remove overloading of "max_facts" -- it already controls the number of facts passed to ATPs for 'learn_prover'
blanchet
parents:
54115
diff
changeset
|
777 |
val num_isar_deps = length isar_deps |
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
778 |
in |
48404 | 779 |
if verbose andalso auto_level = 0 then |
54141
f57f8e7a879f
generate a comment storing the goal nickname in "learn_prover"
blanchet
parents:
54140
diff
changeset
|
780 |
"MaSh: " ^ quote prover ^ " on " ^ quote name ^ " with " ^ string_of_int num_isar_deps ^ |
f57f8e7a879f
generate a comment storing the goal nickname in "learn_prover"
blanchet
parents:
54140
diff
changeset
|
781 |
" + " ^ string_of_int (length facts - num_isar_deps) ^ " facts." |
54123
271a8377656f
remove overloading of "max_facts" -- it already controls the number of facts passed to ATPs for 'learn_prover'
blanchet
parents:
54115
diff
changeset
|
782 |
|> Output.urgent_message |
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
783 |
else |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
784 |
(); |
54141
f57f8e7a879f
generate a comment storing the goal nickname in "learn_prover"
blanchet
parents:
54140
diff
changeset
|
785 |
case run_prover_for_mash ctxt params prover name facts goal of |
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
786 |
{outcome = NONE, used_facts, ...} => |
48404 | 787 |
(if verbose andalso auto_level = 0 then |
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
788 |
let val num_facts = length used_facts in |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
789 |
"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
|
790 |
plural_s num_facts ^ "." |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
791 |
|> Output.urgent_message |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
792 |
end |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
793 |
else |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
794 |
(); |
50754
74a6adcb96ac
also generate queries for goals with too many Isar dependencies
blanchet
parents:
50751
diff
changeset
|
795 |
(true, map fst used_facts)) |
48665 | 796 |
| _ => (false, isar_deps) |
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
797 |
end |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
798 |
|
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
799 |
|
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
800 |
(*** High-level communication with MaSh ***) |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48249
diff
changeset
|
801 |
|
51182
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset
|
802 |
(* In the following functions, chunks are risers w.r.t. "thm_less_eq". *) |
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset
|
803 |
|
51181
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset
|
804 |
fun chunks_and_parents_for chunks th = |
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset
|
805 |
let |
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset
|
806 |
fun insert_parent new parents = |
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset
|
807 |
let val parents = parents |> filter_out (fn p => thm_less_eq (p, new)) in |
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset
|
808 |
parents |> forall (fn p => not (thm_less_eq (new, p))) parents |
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset
|
809 |
? cons new |
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset
|
810 |
end |
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset
|
811 |
fun rechunk seen (rest as th' :: ths) = |
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset
|
812 |
if thm_less_eq (th', th) then (rev seen, rest) |
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset
|
813 |
else rechunk (th' :: seen) ths |
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset
|
814 |
fun do_chunk [] accum = accum |
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset
|
815 |
| do_chunk (chunk as hd_chunk :: _) (chunks, parents) = |
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset
|
816 |
if thm_less_eq (hd_chunk, th) then |
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset
|
817 |
(chunk :: chunks, insert_parent hd_chunk parents) |
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset
|
818 |
else if thm_less_eq (List.last chunk, th) then |
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset
|
819 |
let val (front, back as hd_back :: _) = rechunk [] chunk in |
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset
|
820 |
(front :: back :: chunks, insert_parent hd_back parents) |
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset
|
821 |
end |
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset
|
822 |
else |
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset
|
823 |
(chunk :: chunks, parents) |
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset
|
824 |
in |
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset
|
825 |
fold_rev do_chunk chunks ([], []) |
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset
|
826 |
|>> cons [] |
51182
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset
|
827 |
||> map nickname_of_thm |
51181
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset
|
828 |
end |
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51180
diff
changeset
|
829 |
|
51182
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset
|
830 |
fun attach_parents_to_facts _ [] = [] |
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset
|
831 |
| attach_parents_to_facts old_facts (facts as (_, th) :: _) = |
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset
|
832 |
let |
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset
|
833 |
fun do_facts _ [] = [] |
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset
|
834 |
| do_facts (_, parents) [fact] = [(parents, fact)] |
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset
|
835 |
| do_facts (chunks, parents) |
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset
|
836 |
((fact as (_, th)) :: (facts as (_, th') :: _)) = |
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset
|
837 |
let |
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset
|
838 |
val chunks = app_hd (cons th) chunks |
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset
|
839 |
val chunks_and_parents' = |
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset
|
840 |
if thm_less_eq (th, th') andalso |
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset
|
841 |
thy_name_of_thm th = thy_name_of_thm th' then |
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset
|
842 |
(chunks, [nickname_of_thm th]) |
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset
|
843 |
else |
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset
|
844 |
chunks_and_parents_for chunks th' |
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset
|
845 |
in (parents, fact) :: do_facts chunks_and_parents' facts end |
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset
|
846 |
in |
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset
|
847 |
old_facts @ facts |
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset
|
848 |
|> do_facts (chunks_and_parents_for [[]] th) |
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset
|
849 |
|> drop (length old_facts) |
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset
|
850 |
end |
51177 | 851 |
|
53095 | 852 |
fun maximal_wrt_graph G keys = |
853 |
let |
|
854 |
val tab = Symtab.empty |> fold (fn name => Symtab.default (name, ())) keys |
|
855 |
fun insert_new seen name = |
|
856 |
not (Symtab.defined seen name) ? insert (op =) name |
|
857 |
fun num_keys keys = Graph.Keys.fold (K (Integer.add 1)) keys 0 |
|
858 |
fun find_maxes _ (maxs, []) = map snd maxs |
|
859 |
| find_maxes seen (maxs, new :: news) = |
|
860 |
find_maxes |
|
861 |
(seen |> num_keys (Graph.imm_succs G new) > 1 |
|
862 |
? Symtab.default (new, ())) |
|
863 |
(if Symtab.defined tab new then |
|
864 |
let |
|
865 |
val newp = Graph.all_preds G [new] |
|
866 |
fun is_ancestor x yp = member (op =) yp x |
|
867 |
val maxs = |
|
868 |
maxs |> filter (fn (_, max) => not (is_ancestor max newp)) |
|
869 |
in |
|
870 |
if exists (is_ancestor new o fst) maxs then |
|
871 |
(maxs, news) |
|
872 |
else |
|
873 |
((newp, new) |
|
874 |
:: filter_out (fn (_, max) => is_ancestor max newp) maxs, |
|
875 |
news) |
|
876 |
end |
|
877 |
else |
|
878 |
(maxs, Graph.Keys.fold (insert_new seen) |
|
879 |
(Graph.imm_preds G new) news)) |
|
880 |
in find_maxes Symtab.empty ([], Graph.maximals G) end |
|
881 |
||
882 |
fun maximal_wrt_access_graph access_G = |
|
883 |
map (nickname_of_thm o snd) |
|
884 |
#> maximal_wrt_graph access_G |
|
885 |
||
886 |
fun is_fact_in_graph access_G = can (Graph.get_node access_G) o nickname_of_thm |
|
887 |
||
53197 | 888 |
val chained_feature_factor = 0.5 (* FUDGE *) |
889 |
val extra_feature_factor = 0.1 (* FUDGE *) |
|
53201
2a2dc18f3e10
reverted 6c5e7143e1f6; took a better look at evaluation data this time
blanchet
parents:
53197
diff
changeset
|
890 |
val num_extra_feature_facts = 10 (* FUDGE *) |
53095 | 891 |
|
892 |
(* FUDGE *) |
|
893 |
fun weight_of_proximity_fact rank = |
|
894 |
Math.pow (1.3, 15.5 - 0.2 * Real.fromInt rank) + 15.0 |
|
895 |
||
53140
a1235e90da5f
pour extra features from proximate facts into goal, in exporter
blanchet
parents:
53137
diff
changeset
|
896 |
fun weight_facts_smoothly facts = |
53095 | 897 |
facts ~~ map weight_of_proximity_fact (0 upto length facts - 1) |
898 |
||
53140
a1235e90da5f
pour extra features from proximate facts into goal, in exporter
blanchet
parents:
53137
diff
changeset
|
899 |
(* FUDGE *) |
a1235e90da5f
pour extra features from proximate facts into goal, in exporter
blanchet
parents:
53137
diff
changeset
|
900 |
fun steep_weight_of_fact rank = |
a1235e90da5f
pour extra features from proximate facts into goal, in exporter
blanchet
parents:
53137
diff
changeset
|
901 |
Math.pow (0.62, log2 (Real.fromInt (rank + 1))) |
a1235e90da5f
pour extra features from proximate facts into goal, in exporter
blanchet
parents:
53137
diff
changeset
|
902 |
|
a1235e90da5f
pour extra features from proximate facts into goal, in exporter
blanchet
parents:
53137
diff
changeset
|
903 |
fun weight_facts_steeply facts = |
a1235e90da5f
pour extra features from proximate facts into goal, in exporter
blanchet
parents:
53137
diff
changeset
|
904 |
facts ~~ map steep_weight_of_fact (0 upto length facts - 1) |
a1235e90da5f
pour extra features from proximate facts into goal, in exporter
blanchet
parents:
53137
diff
changeset
|
905 |
|
53095 | 906 |
val max_proximity_facts = 100 |
907 |
||
54060 | 908 |
fun find_mash_suggestions ctxt max_facts suggs facts chained raw_unknown = |
909 |
let |
|
910 |
val inter_fact = inter (eq_snd Thm.eq_thm_prop) |
|
911 |
val raw_mash = find_suggested_facts ctxt facts suggs |
|
912 |
val proximate = take max_proximity_facts facts |
|
913 |
val unknown_chained = inter_fact raw_unknown chained |
|
914 |
val unknown_proximate = inter_fact raw_unknown proximate |
|
915 |
val mess = |
|
916 |
[(0.9 (* FUDGE *), (map (rpair 1.0) unknown_chained, [])), |
|
917 |
(0.4 (* FUDGE *), (weight_facts_smoothly unknown_proximate, [])), |
|
918 |
(0.1 (* FUDGE *), (weight_facts_steeply raw_mash, raw_unknown))] |
|
919 |
val unknown = |
|
920 |
raw_unknown |
|
921 |
|> fold (subtract (eq_snd Thm.eq_thm_prop)) |
|
922 |
[unknown_chained, unknown_proximate] |
|
923 |
in (mesh_facts (eq_snd Thm.eq_thm_prop) max_facts mess, unknown) end |
|
53095 | 924 |
|
53127 | 925 |
fun add_const_counts t = |
53130 | 926 |
fold (fn s => Symtab.map_default (s, 0) (Integer.add 1)) |
53127 | 927 |
(Term.add_const_names t []) |
53095 | 928 |
|
54503 | 929 |
fun mash_suggested_facts ctxt ({debug, overlord, ...} : params) max_facts hyp_ts concl_t facts = |
53095 | 930 |
let |
931 |
val thy = Proof_Context.theory_of ctxt |
|
53559
3858246c7c8f
when pouring in extra features into the goal, only consider facts from the current theory -- the bottom 10 facts of the last import might be completely unrelated
blanchet
parents:
53558
diff
changeset
|
932 |
val thy_name = Context.theory_name thy |
53141
d27e99a6a679
take chained and proximate facts into consideration when computing MaSh features
blanchet
parents:
53140
diff
changeset
|
933 |
val facts = facts |> sort (crude_thm_ord o pairself snd o swap) |
53095 | 934 |
val chained = facts |> filter (fn ((_, (scope, _)), _) => scope = Chained) |
53141
d27e99a6a679
take chained and proximate facts into consideration when computing MaSh features
blanchet
parents:
53140
diff
changeset
|
935 |
val num_facts = length facts |
53127 | 936 |
val const_tab = fold (add_const_counts o prop_of o snd) facts Symtab.empty |
54085 | 937 |
|
53559
3858246c7c8f
when pouring in extra features into the goal, only consider facts from the current theory -- the bottom 10 facts of the last import might be completely unrelated
blanchet
parents:
53558
diff
changeset
|
938 |
fun fact_has_right_theory (_, th) = |
3858246c7c8f
when pouring in extra features into the goal, only consider facts from the current theory -- the bottom 10 facts of the last import might be completely unrelated
blanchet
parents:
53558
diff
changeset
|
939 |
thy_name = Context.theory_name (theory_of_thm th) |
53141
d27e99a6a679
take chained and proximate facts into consideration when computing MaSh features
blanchet
parents:
53140
diff
changeset
|
940 |
fun chained_or_extra_features_of factor (((_, stature), th), weight) = |
d27e99a6a679
take chained and proximate facts into consideration when computing MaSh features
blanchet
parents:
53140
diff
changeset
|
941 |
[prop_of th] |
54089
b13f6731f873
use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset
|
942 |
|> features_of ctxt (theory_of_thm th) num_facts const_tab stature |
53141
d27e99a6a679
take chained and proximate facts into consideration when computing MaSh features
blanchet
parents:
53140
diff
changeset
|
943 |
|> map (apsnd (fn r => weight * factor * r)) |
54085 | 944 |
|
53095 | 945 |
val (access_G, suggs) = |
53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset
|
946 |
peek_state ctxt overlord (fn {access_G, ...} => |
53095 | 947 |
if Graph.is_empty access_G then |
54064 | 948 |
(trace_msg ctxt (K "Nothing has been learned yet"); (access_G, [])) |
53095 | 949 |
else |
950 |
let |
|
951 |
val parents = maximal_wrt_access_graph access_G facts |
|
53141
d27e99a6a679
take chained and proximate facts into consideration when computing MaSh features
blanchet
parents:
53140
diff
changeset
|
952 |
val goal_feats = |
54089
b13f6731f873
use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset
|
953 |
features_of ctxt thy num_facts const_tab (Local, General) (concl_t :: hyp_ts) |
53141
d27e99a6a679
take chained and proximate facts into consideration when computing MaSh features
blanchet
parents:
53140
diff
changeset
|
954 |
val chained_feats = |
d27e99a6a679
take chained and proximate facts into consideration when computing MaSh features
blanchet
parents:
53140
diff
changeset
|
955 |
chained |
d27e99a6a679
take chained and proximate facts into consideration when computing MaSh features
blanchet
parents:
53140
diff
changeset
|
956 |
|> map (rpair 1.0) |
d27e99a6a679
take chained and proximate facts into consideration when computing MaSh features
blanchet
parents:
53140
diff
changeset
|
957 |
|> map (chained_or_extra_features_of chained_feature_factor) |
53159 | 958 |
|> rpair [] |-> fold (union (eq_fst (op =))) |
53141
d27e99a6a679
take chained and proximate facts into consideration when computing MaSh features
blanchet
parents:
53140
diff
changeset
|
959 |
val extra_feats = |
d27e99a6a679
take chained and proximate facts into consideration when computing MaSh features
blanchet
parents:
53140
diff
changeset
|
960 |
facts |
53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset
|
961 |
|> take (Int.max (0, num_extra_feature_facts - length chained)) |
53559
3858246c7c8f
when pouring in extra features into the goal, only consider facts from the current theory -- the bottom 10 facts of the last import might be completely unrelated
blanchet
parents:
53558
diff
changeset
|
962 |
|> filter fact_has_right_theory |
53141
d27e99a6a679
take chained and proximate facts into consideration when computing MaSh features
blanchet
parents:
53140
diff
changeset
|
963 |
|> weight_facts_steeply |
d27e99a6a679
take chained and proximate facts into consideration when computing MaSh features
blanchet
parents:
53140
diff
changeset
|
964 |
|> map (chained_or_extra_features_of extra_feature_factor) |
53159 | 965 |
|> rpair [] |-> fold (union (eq_fst (op =))) |
53095 | 966 |
val feats = |
53159 | 967 |
fold (union (eq_fst (op =))) [chained_feats, extra_feats] |
53141
d27e99a6a679
take chained and proximate facts into consideration when computing MaSh features
blanchet
parents:
53140
diff
changeset
|
968 |
goal_feats |
53559
3858246c7c8f
when pouring in extra features into the goal, only consider facts from the current theory -- the bottom 10 facts of the last import might be completely unrelated
blanchet
parents:
53558
diff
changeset
|
969 |
|> debug ? sort (Real.compare o swap o pairself snd) |
53095 | 970 |
val hints = |
971 |
chained |> filter (is_fact_in_graph access_G o snd) |
|
972 |
|> map (nickname_of_thm o snd) |
|
973 |
in |
|
974 |
(access_G, MaSh.query ctxt overlord max_facts |
|
53118
3f290031bd9e
take out dangerous feature, now that all updates are permanent
blanchet
parents:
53117
diff
changeset
|
975 |
([], hints, parents, feats)) |
53095 | 976 |
end) |
977 |
val unknown = facts |> filter_out (is_fact_in_graph access_G o snd) |
|
978 |
in |
|
979 |
find_mash_suggestions ctxt max_facts suggs facts chained unknown |
|
980 |
|> pairself (map fact_of_raw_fact) |
|
981 |
end |
|
982 |
||
983 |
fun learn_wrt_access_graph ctxt (name, parents, feats, deps) (learns, graph) = |
|
984 |
let |
|
985 |
fun maybe_learn_from from (accum as (parents, graph)) = |
|
986 |
try_graph ctxt "updating graph" accum (fn () => |
|
987 |
(from :: parents, Graph.add_edge_acyclic (from, name) graph)) |
|
988 |
val graph = graph |> Graph.default_node (name, Isar_Proof) |
|
989 |
val (parents, graph) = ([], graph) |> fold maybe_learn_from parents |
|
990 |
val (deps, _) = ([], graph) |> fold maybe_learn_from deps |
|
991 |
in ((name, parents, feats, deps) :: learns, graph) end |
|
992 |
||
993 |
fun relearn_wrt_access_graph ctxt (name, deps) (relearns, graph) = |
|
994 |
let |
|
995 |
fun maybe_relearn_from from (accum as (parents, graph)) = |
|
996 |
try_graph ctxt "updating graph" accum (fn () => |
|
997 |
(from :: parents, Graph.add_edge_acyclic (from, name) graph)) |
|
998 |
val graph = graph |> update_access_graph_node (name, Automatic_Proof) |
|
999 |
val (deps, _) = ([], graph) |> fold maybe_relearn_from deps |
|
1000 |
in ((name, deps) :: relearns, graph) end |
|
1001 |
||
1002 |
fun flop_wrt_access_graph name = |
|
1003 |
update_access_graph_node (name, Isar_Proof_wegen_Prover_Flop) |
|
1004 |
||
1005 |
val learn_timeout_slack = 2.0 |
|
1006 |
||
1007 |
fun launch_thread timeout task = |
|
1008 |
let |
|
1009 |
val hard_timeout = time_mult learn_timeout_slack timeout |
|
1010 |
val birth_time = Time.now () |
|
1011 |
val death_time = Time.+ (birth_time, hard_timeout) |
|
1012 |
val desc = ("Machine learner for Sledgehammer", "") |
|
1013 |
in Async_Manager.thread MaShN birth_time death_time desc task end |
|
1014 |
||
54503 | 1015 |
fun mash_learn_proof ctxt ({overlord, timeout, ...} : params) t facts used_ths = |
53819
e55d641d0a70
honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset
|
1016 |
if is_mash_enabled () then |
e55d641d0a70
honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset
|
1017 |
launch_thread (timeout |> the_default one_day) (fn () => |
e55d641d0a70
honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset
|
1018 |
let |
e55d641d0a70
honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset
|
1019 |
val thy = Proof_Context.theory_of ctxt |
54089
b13f6731f873
use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset
|
1020 |
val feats = features_of ctxt thy 0 Symtab.empty (Local, General) [t] |> map fst |
53819
e55d641d0a70
honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset
|
1021 |
in |
e55d641d0a70
honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset
|
1022 |
peek_state ctxt overlord (fn {access_G, ...} => |
e55d641d0a70
honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset
|
1023 |
let |
e55d641d0a70
honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset
|
1024 |
val parents = maximal_wrt_access_graph access_G facts |
e55d641d0a70
honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset
|
1025 |
val deps = |
e55d641d0a70
honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset
|
1026 |
used_ths |> filter (is_fact_in_graph access_G) |
e55d641d0a70
honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset
|
1027 |
|> map nickname_of_thm |
e55d641d0a70
honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset
|
1028 |
in |
54432
68f8bd1641da
have MaSh support nameless facts (i.e. proofs) and use that support
blanchet
parents:
54143
diff
changeset
|
1029 |
MaSh.learn ctxt overlord true [("", parents, feats, deps)] |
53819
e55d641d0a70
honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset
|
1030 |
end); |
e55d641d0a70
honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset
|
1031 |
(true, "") |
e55d641d0a70
honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset
|
1032 |
end) |
e55d641d0a70
honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset
|
1033 |
else |
e55d641d0a70
honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset
|
1034 |
() |
53095 | 1035 |
|
52697
6fb98a20c349
explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
wenzelm
parents:
52196
diff
changeset
|
1036 |
fun sendback sub = |
6fb98a20c349
explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
wenzelm
parents:
52196
diff
changeset
|
1037 |
Active.sendback_markup [Markup.padding_command] (sledgehammerN ^ " " ^ sub) |
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
1038 |
|
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
1039 |
val commit_timeout = seconds 30.0 |
48332
271a4a6af734
optimize parent computation in MaSh + remove temporary files
blanchet
parents:
48330
diff
changeset
|
1040 |
|
50485
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50484
diff
changeset
|
1041 |
(* The timeout is understood in a very relaxed fashion. *) |
48404 | 1042 |
fun mash_learn_facts ctxt (params as {debug, verbose, overlord, ...}) prover |
53152
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset
|
1043 |
save auto_level run_prover learn_timeout facts = |
48304 | 1044 |
let |
48318 | 1045 |
val timer = Timer.startRealTimer () |
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
1046 |
fun next_commit_time () = |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
1047 |
Time.+ (Timer.checkRealTimer timer, commit_timeout) |
53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset
|
1048 |
val {access_G, ...} = peek_state ctxt overlord I |
53095 | 1049 |
val is_in_access_G = is_fact_in_graph access_G o snd |
51177 | 1050 |
val no_new_facts = forall is_in_access_G facts |
48308 | 1051 |
in |
51177 | 1052 |
if no_new_facts andalso not run_prover then |
48404 | 1053 |
if auto_level < 2 then |
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset
|
1054 |
"No new " ^ (if run_prover then "automatic" else "Isar") ^ |
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset
|
1055 |
" proofs to learn." ^ |
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset
|
1056 |
(if auto_level = 0 andalso not run_prover then |
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset
|
1057 |
"\n\nHint: Try " ^ sendback learn_proverN ^ |
50751 | 1058 |
" to learn from an automatic prover." |
48404 | 1059 |
else |
1060 |
"") |
|
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
1061 |
else |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
1062 |
"" |
48308 | 1063 |
else |
48304 | 1064 |
let |
50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50732
diff
changeset
|
1065 |
val name_tabs = build_name_tables nickname_of_thm facts |
48439
67a6bcbd3587
removed MaSh junk arising from primrec definitions
blanchet
parents:
48438
diff
changeset
|
1066 |
fun deps_of status th = |
53095 | 1067 |
if no_dependencies_for_status status then |
48439
67a6bcbd3587
removed MaSh junk arising from primrec definitions
blanchet
parents:
48438
diff
changeset
|
1068 |
SOME [] |
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset
|
1069 |
else if run_prover then |
50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50732
diff
changeset
|
1070 |
prover_dependencies_of ctxt params prover auto_level facts name_tabs |
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset
|
1071 |
th |
50754
74a6adcb96ac
also generate queries for goals with too many Isar dependencies
blanchet
parents:
50751
diff
changeset
|
1072 |
|> (fn (false, _) => NONE |
51177 | 1073 |
| (true, deps) => trim_dependencies deps) |
48404 | 1074 |
else |
50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50732
diff
changeset
|
1075 |
isar_dependencies_of name_tabs th |
51177 | 1076 |
|> trim_dependencies |
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset
|
1077 |
fun do_commit [] [] [] state = state |
53095 | 1078 |
| do_commit learns relearns flops {access_G, num_known_facts, dirty} = |
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
1079 |
let |
50610 | 1080 |
val was_empty = Graph.is_empty access_G |
50631 | 1081 |
val (learns, access_G) = |
1082 |
([], access_G) |> fold (learn_wrt_access_graph ctxt) learns |
|
1083 |
val (relearns, access_G) = |
|
1084 |
([], access_G) |> fold (relearn_wrt_access_graph ctxt) relearns |
|
50610 | 1085 |
val access_G = access_G |> fold flop_wrt_access_graph flops |
53095 | 1086 |
val num_known_facts = num_known_facts + length learns |
48699 | 1087 |
val dirty = |
50631 | 1088 |
case (was_empty, dirty, relearns) of |
1089 |
(false, SOME names, []) => SOME (map #1 learns @ names) |
|
48699 | 1090 |
| _ => NONE |
48404 | 1091 |
in |
53757
8d1a059ebcdb
reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents:
53756
diff
changeset
|
1092 |
MaSh.learn ctxt overlord (save andalso null relearns) (rev learns); |
8d1a059ebcdb
reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents:
53756
diff
changeset
|
1093 |
MaSh.relearn ctxt overlord save relearns; |
53095 | 1094 |
{access_G = access_G, num_known_facts = num_known_facts, |
1095 |
dirty = dirty} |
|
48404 | 1096 |
end |
50631 | 1097 |
fun commit last learns relearns flops = |
48404 | 1098 |
(if debug andalso auto_level = 0 then |
1099 |
Output.urgent_message "Committing..." |
|
1100 |
else |
|
1101 |
(); |
|
53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset
|
1102 |
map_state ctxt overlord (do_commit (rev learns) relearns flops); |
48404 | 1103 |
if not last andalso auto_level = 0 then |
50631 | 1104 |
let val num_proofs = length learns + length relearns in |
48404 | 1105 |
"Learned " ^ string_of_int num_proofs ^ " " ^ |
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset
|
1106 |
(if run_prover then "automatic" else "Isar") ^ " proof" ^ |
48404 | 1107 |
plural_s num_proofs ^ " in the last " ^ |
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset
|
1108 |
string_of_time commit_timeout ^ "." |
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
1109 |
|> Output.urgent_message |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
1110 |
end |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
1111 |
else |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
1112 |
()) |
51177 | 1113 |
fun learn_new_fact _ (accum as (_, (_, _, true))) = accum |
1114 |
| learn_new_fact (parents, ((_, stature as (_, status)), th)) |
|
1115 |
(learns, (n, next_commit, _)) = |
|
48318 | 1116 |
let |
50624
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset
|
1117 |
val name = nickname_of_thm th |
48332
271a4a6af734
optimize parent computation in MaSh + remove temporary files
blanchet
parents:
48330
diff
changeset
|
1118 |
val feats = |
54089
b13f6731f873
use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents:
54085
diff
changeset
|
1119 |
features_of ctxt (theory_of_thm th) 0 Symtab.empty stature [prop_of th] |> map fst |
48439
67a6bcbd3587
removed MaSh junk arising from primrec definitions
blanchet
parents:
48438
diff
changeset
|
1120 |
val deps = deps_of status th |> these |
48394
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48392
diff
changeset
|
1121 |
val n = n |> not (null deps) ? Integer.add 1 |
50631 | 1122 |
val learns = (name, parents, feats, deps) :: learns |
1123 |
val (learns, next_commit) = |
|
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
1124 |
if Time.> (Timer.checkRealTimer timer, next_commit) then |
50631 | 1125 |
(commit false learns [] []; ([], next_commit_time ())) |
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48390
diff
changeset
|
1126 |
else |
50631 | 1127 |
(learns, next_commit) |
50557 | 1128 |
val timed_out = |
1129 |
case learn_timeout of |
|
1130 |
SOME timeout => Time.> (Timer.checkRealTimer timer, timeout) |
|
1131 |
| NONE => false |
|
51177 | 1132 |
in (learns, (n, next_commit, timed_out)) end |
48404 | 1133 |
val n = |
51177 | 1134 |
if no_new_facts then |
48404 | 1135 |
0 |
1136 |
else |
|
1137 |
let |
|
51182
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset
|
1138 |
val new_facts = |
51184
e2569dde59c8
reintroduced crucial sorting accidentally lost in 962190eab40d
blanchet
parents:
51183
diff
changeset
|
1139 |
facts |> sort (crude_thm_ord o pairself snd) |
e2569dde59c8
reintroduced crucial sorting accidentally lost in 962190eab40d
blanchet
parents:
51183
diff
changeset
|
1140 |
|> attach_parents_to_facts [] |
51177 | 1141 |
|> filter_out (is_in_access_G o snd) |
1142 |
val (learns, (n, _, _)) = |
|
1143 |
([], (0, next_commit_time (), false)) |
|
51182
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
51181
diff
changeset
|
1144 |
|> fold learn_new_fact new_facts |
50631 | 1145 |
in commit true learns [] []; n end |
48404 | 1146 |
fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum |
48439
67a6bcbd3587
removed MaSh junk arising from primrec definitions
blanchet
parents:
48438
diff
changeset
|
1147 |
| relearn_old_fact ((_, (_, status)), th) |
50631 | 1148 |
((relearns, flops), (n, next_commit, _)) = |
48404 | 1149 |
let |
50624
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset
|
1150 |
val name = nickname_of_thm th |
50631 | 1151 |
val (n, relearns, flops) = |
48439
67a6bcbd3587
removed MaSh junk arising from primrec definitions
blanchet
parents:
48438
diff
changeset
|
1152 |
case deps_of status th of |
50631 | 1153 |
SOME deps => (n + 1, (name, deps) :: relearns, flops) |
1154 |
| NONE => (n, relearns, name :: flops) |
|
1155 |
val (relearns, flops, next_commit) = |
|
48404 | 1156 |
if Time.> (Timer.checkRealTimer timer, next_commit) then |
50631 | 1157 |
(commit false [] relearns flops; |
1158 |
([], [], next_commit_time ())) |
|
48404 | 1159 |
else |
50631 | 1160 |
(relearns, flops, next_commit) |
50557 | 1161 |
val timed_out = |
1162 |
case learn_timeout of |
|
1163 |
SOME timeout => Time.> (Timer.checkRealTimer timer, timeout) |
|
1164 |
| NONE => false |
|
50631 | 1165 |
in ((relearns, flops), (n, next_commit, timed_out)) end |
48404 | 1166 |
val n = |
51177 | 1167 |
if not run_prover then |
48404 | 1168 |
n |
1169 |
else |
|
1170 |
let |
|
48668
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset
|
1171 |
val max_isar = 1000 * max_dependencies |
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset
|
1172 |
fun kind_of_proof th = |
50624
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50623
diff
changeset
|
1173 |
try (Graph.get_node access_G) (nickname_of_thm th) |
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset
|
1174 |
|> the_default Isar_Proof |
48406 | 1175 |
fun priority_of (_, th) = |
48668
5d63c23b4042
remember which MaSh proofs were found using ATPs
blanchet
parents:
48667
diff
changeset
|
1176 |
random_range 0 max_isar |
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset
|
1177 |
+ (case kind_of_proof th of |
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset
|
1178 |
Isar_Proof => 0 |
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset
|
1179 |
| Automatic_Proof => 2 * max_isar |
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset
|
1180 |
| Isar_Proof_wegen_Prover_Flop => max_isar) |
54131
18b23d787062
choose facts to reprove more randomly, to avoid getting stuck with impossible problems at first
blanchet
parents:
54125
diff
changeset
|
1181 |
- 100 * length (isar_dependencies_of name_tabs th) |
48404 | 1182 |
val old_facts = |
51177 | 1183 |
facts |> filter is_in_access_G |
1184 |
|> map (`priority_of) |
|
1185 |
|> sort (int_ord o pairself fst) |
|
1186 |
|> map snd |
|
50631 | 1187 |
val ((relearns, flops), (n, _, _)) = |
48669
cdcdb0547f29
remember ATP flops to avoid repeating them too quickly
blanchet
parents:
48668
diff
changeset
|
1188 |
(([], []), (n, next_commit_time (), false)) |
48404 | 1189 |
|> fold relearn_old_fact old_facts |
50631 | 1190 |
in commit true [] relearns flops; n end |
48318 | 1191 |
in |
48404 | 1192 |
if verbose orelse auto_level < 2 then |
1193 |
"Learned " ^ string_of_int n ^ " nontrivial " ^ |
|
54140 | 1194 |
(if run_prover then "automatic and " else "") ^ "Isar proof" ^ plural_s n ^ |
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset
|
1195 |
(if verbose then " in " ^ string_of_time (Timer.checkRealTimer timer) |
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset
|
1196 |
else "") ^ "." |
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset
|
1197 |
else |
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset
|
1198 |
"" |
48318 | 1199 |
end |
48308 | 1200 |
end |
48304 | 1201 |
|
54123
271a8377656f
remove overloading of "max_facts" -- it already controls the number of facts passed to ATPs for 'learn_prover'
blanchet
parents:
54115
diff
changeset
|
1202 |
fun mash_learn ctxt (params as {provers, timeout, ...}) fact_override chained run_prover = |
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
1203 |
let |
48396 | 1204 |
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
|
1205 |
val ctxt = ctxt |> Config.put instantiate_inducts false |
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48394
diff
changeset
|
1206 |
val facts = |
48396 | 1207 |
nearly_all_facts ctxt false fact_override Symtab.empty css chained [] |
1208 |
@{prop True} |
|
54115
2b7e063c7abc
improved duplicate detection in "build_name_tables" by ensuring that the earliest occurrence of a duplicate (if it exists) gets picked as the canonical instance
blanchet
parents:
54100
diff
changeset
|
1209 |
|> sort (crude_thm_ord o pairself snd o swap) |
48404 | 1210 |
val num_facts = length facts |
1211 |
val prover = hd provers |
|
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset
|
1212 |
fun learn auto_level run_prover = |
53152
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset
|
1213 |
mash_learn_facts ctxt params prover true auto_level run_prover NONE facts |
48404 | 1214 |
|> Output.urgent_message |
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
1215 |
in |
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset
|
1216 |
if run_prover then |
50340
72519bf5f135
simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents:
50339
diff
changeset
|
1217 |
("MaShing through " ^ string_of_int num_facts ^ " fact" ^ |
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset
|
1218 |
plural_s num_facts ^ " for automatic proofs (" ^ quote prover ^ |
50557 | 1219 |
(case timeout of |
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset
|
1220 |
SOME timeout => " timeout: " ^ string_of_time timeout |
50557 | 1221 |
| NONE => "") ^ ").\n\nCollecting Isar proofs first..." |
50340
72519bf5f135
simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents:
50339
diff
changeset
|
1222 |
|> Output.urgent_message; |
72519bf5f135
simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents:
50339
diff
changeset
|
1223 |
learn 1 false; |
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50450
diff
changeset
|
1224 |
"Now collecting automatic proofs. This may take several hours. You can \ |
50340
72519bf5f135
simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents:
50339
diff
changeset
|
1225 |
\safely stop the learning process at any point." |
72519bf5f135
simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents:
50339
diff
changeset
|
1226 |
|> Output.urgent_message; |
72519bf5f135
simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents:
50339
diff
changeset
|
1227 |
learn 0 true) |
72519bf5f135
simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents:
50339
diff
changeset
|
1228 |
else |
72519bf5f135
simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents:
50339
diff
changeset
|
1229 |
("MaShing through " ^ string_of_int num_facts ^ " fact" ^ |
72519bf5f135
simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents:
50339
diff
changeset
|
1230 |
plural_s num_facts ^ " for Isar proofs..." |
72519bf5f135
simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents:
50339
diff
changeset
|
1231 |
|> Output.urgent_message; |
72519bf5f135
simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents:
50339
diff
changeset
|
1232 |
learn 0 false) |
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
1233 |
end |
48249 | 1234 |
|
53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset
|
1235 |
fun mash_can_suggest_facts ctxt overlord = |
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset
|
1236 |
not (Graph.is_empty (#access_G (peek_state ctxt overlord I))) |
50311 | 1237 |
|
50383
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset
|
1238 |
(* Generate more suggestions than requested, because some might be thrown out |
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset
|
1239 |
later for various reasons. *) |
50965 | 1240 |
fun generous_max_facts max_facts = max_facts + Int.min (50, max_facts) |
50383
4274b25ff4e7
take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents:
50382
diff
changeset
|
1241 |
|
50814 | 1242 |
val mepo_weight = 0.5 |
1243 |
val mash_weight = 0.5 |
|
1244 |
||
53152
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset
|
1245 |
val max_facts_to_learn_before_query = 100 |
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset
|
1246 |
|
48318 | 1247 |
(* The threshold should be large enough so that MaSh doesn't kick in for Auto |
1248 |
Sledgehammer and Try. *) |
|
1249 |
val min_secs_for_learning = 15 |
|
1250 |
||
53153 | 1251 |
fun relevant_facts ctxt |
1252 |
(params as {overlord, blocking, learn, fact_filter, timeout, ...}) |
|
53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset
|
1253 |
prover max_facts ({add, only, ...} : fact_override) hyp_ts concl_t |
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset
|
1254 |
facts = |
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
1255 |
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
|
1256 |
error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".") |
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
1257 |
else if only then |
51004
5f2788c38127
distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds
blanchet
parents:
51003
diff
changeset
|
1258 |
let val facts = facts |> map fact_of_raw_fact in |
51010 | 1259 |
[("", facts)] |
51004
5f2788c38127
distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds
blanchet
parents:
51003
diff
changeset
|
1260 |
end |
48321 | 1261 |
else if max_facts <= 0 orelse null facts then |
51010 | 1262 |
[("", [])] |
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset
|
1263 |
else |
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset
|
1264 |
let |
53152
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset
|
1265 |
fun maybe_launch_thread () = |
53153 | 1266 |
if not blocking andalso |
1267 |
not (Async_Manager.has_running_threads MaShN) andalso |
|
50557 | 1268 |
(timeout = NONE orelse |
1269 |
Time.toSeconds (the timeout) >= min_secs_for_learning) then |
|
1270 |
let |
|
1271 |
val timeout = Option.map (time_mult learn_timeout_slack) timeout |
|
1272 |
in |
|
1273 |
launch_thread (timeout |> the_default one_day) |
|
53152
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset
|
1274 |
(fn () => (true, mash_learn_facts ctxt params prover true 2 |
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset
|
1275 |
false timeout facts)) |
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset
|
1276 |
end |
48318 | 1277 |
else |
1278 |
() |
|
53152
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset
|
1279 |
fun maybe_learn () = |
53819
e55d641d0a70
honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents:
53790
diff
changeset
|
1280 |
if is_mash_enabled () andalso learn then |
53152
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset
|
1281 |
let |
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset
|
1282 |
val {access_G, num_known_facts, ...} = peek_state ctxt overlord I |
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset
|
1283 |
val is_in_access_G = is_fact_in_graph access_G o snd |
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset
|
1284 |
in |
54012
7a8263843acb
removed spurious save if nothing needs to bee learned
blanchet
parents:
53819
diff
changeset
|
1285 |
if length facts - num_known_facts |
7a8263843acb
removed spurious save if nothing needs to bee learned
blanchet
parents:
53819
diff
changeset
|
1286 |
<= max_facts_to_learn_before_query then |
7a8263843acb
removed spurious save if nothing needs to bee learned
blanchet
parents:
53819
diff
changeset
|
1287 |
case length (filter_out is_in_access_G facts) of |
7a8263843acb
removed spurious save if nothing needs to bee learned
blanchet
parents:
53819
diff
changeset
|
1288 |
0 => false |
7a8263843acb
removed spurious save if nothing needs to bee learned
blanchet
parents:
53819
diff
changeset
|
1289 |
| num_facts_to_learn => |
7a8263843acb
removed spurious save if nothing needs to bee learned
blanchet
parents:
53819
diff
changeset
|
1290 |
if num_facts_to_learn <= max_facts_to_learn_before_query then |
7a8263843acb
removed spurious save if nothing needs to bee learned
blanchet
parents:
53819
diff
changeset
|
1291 |
(mash_learn_facts ctxt params prover false 2 false timeout facts |
7a8263843acb
removed spurious save if nothing needs to bee learned
blanchet
parents:
53819
diff
changeset
|
1292 |
|> (fn "" => () | s => Output.urgent_message (MaShN ^ ": " ^ s)); |
7a8263843acb
removed spurious save if nothing needs to bee learned
blanchet
parents:
53819
diff
changeset
|
1293 |
true) |
7a8263843acb
removed spurious save if nothing needs to bee learned
blanchet
parents:
53819
diff
changeset
|
1294 |
else |
7a8263843acb
removed spurious save if nothing needs to bee learned
blanchet
parents:
53819
diff
changeset
|
1295 |
(maybe_launch_thread (); false) |
53152
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset
|
1296 |
else |
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset
|
1297 |
(maybe_launch_thread (); false) |
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset
|
1298 |
end |
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset
|
1299 |
else |
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset
|
1300 |
false |
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset
|
1301 |
val (save, effective_fact_filter) = |
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
1302 |
case fact_filter of |
53152
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset
|
1303 |
SOME ff => (ff <> mepoN andalso maybe_learn (), ff) |
48318 | 1304 |
| NONE => |
51024
98fb341d32e3
distinguish MeSh and smart -- with smart, allow combinations of MaSh, MeSh, and MePo in different slices -- and use MaSh also with SMT solvers, based on evaluation
blanchet
parents:
51020
diff
changeset
|
1305 |
if is_mash_enabled () then |
53152
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset
|
1306 |
(maybe_learn (), |
53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset
|
1307 |
if mash_can_suggest_facts ctxt overlord then meshN else mepoN) |
48407 | 1308 |
else |
53152
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset
|
1309 |
(false, mepoN) |
54143
18def1c73c79
make sure add: doesn't add duplicates, and works for [no_atp] facts
blanchet
parents:
54141
diff
changeset
|
1310 |
|
18def1c73c79
make sure add: doesn't add duplicates, and works for [no_atp] facts
blanchet
parents:
54141
diff
changeset
|
1311 |
val unique_facts = drop_duplicate_facts facts |
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset
|
1312 |
val add_ths = Attrib.eval_thms ctxt add |
54143
18def1c73c79
make sure add: doesn't add duplicates, and works for [no_atp] facts
blanchet
parents:
54141
diff
changeset
|
1313 |
|
51004
5f2788c38127
distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds
blanchet
parents:
51003
diff
changeset
|
1314 |
fun in_add (_, th) = member Thm.eq_thm_prop add_ths th |
51003
198cb05fb35b
report (MeSh, MePo, MaSh) triple, to be able to use different filters in different slices
blanchet
parents:
51001
diff
changeset
|
1315 |
fun add_and_take accepts = |
198cb05fb35b
report (MeSh, MePo, MaSh) triple, to be able to use different filters in different slices
blanchet
parents:
51001
diff
changeset
|
1316 |
(case add_ths of |
198cb05fb35b
report (MeSh, MePo, MaSh) triple, to be able to use different filters in different slices
blanchet
parents:
51001
diff
changeset
|
1317 |
[] => accepts |
54143
18def1c73c79
make sure add: doesn't add duplicates, and works for [no_atp] facts
blanchet
parents:
54141
diff
changeset
|
1318 |
| _ => (unique_facts |> filter in_add |> map fact_of_raw_fact) @ |
51004
5f2788c38127
distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds
blanchet
parents:
51003
diff
changeset
|
1319 |
(accepts |> filter_out in_add)) |
48293 | 1320 |
|> take max_facts |
48406 | 1321 |
fun mepo () = |
54143
18def1c73c79
make sure add: doesn't add duplicates, and works for [no_atp] facts
blanchet
parents:
54141
diff
changeset
|
1322 |
(mepo_suggested_facts ctxt params max_facts NONE hyp_ts concl_t unique_facts |
54091 | 1323 |
|> weight_facts_steeply, []) |
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
1324 |
fun mash () = |
54503 | 1325 |
mash_suggested_facts ctxt params (generous_max_facts max_facts) hyp_ts concl_t facts |
53140
a1235e90da5f
pour extra features from proximate facts into goal, in exporter
blanchet
parents:
53137
diff
changeset
|
1326 |
|>> weight_facts_steeply |
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48313
diff
changeset
|
1327 |
val mess = |
51003
198cb05fb35b
report (MeSh, MePo, MaSh) triple, to be able to use different filters in different slices
blanchet
parents:
51001
diff
changeset
|
1328 |
(* the order is important for the "case" expression below *) |
54091 | 1329 |
[] |> effective_fact_filter <> mepoN ? cons (mash_weight, mash) |
1330 |
|> effective_fact_filter <> mashN ? cons (mepo_weight, mepo) |
|
1331 |
|> Par_List.map (apsnd (fn f => f ())) |
|
1332 |
val mesh = mesh_facts (eq_snd Thm.eq_thm_prop) max_facts mess |> add_and_take |
|
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset
|
1333 |
in |
53152
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53150
diff
changeset
|
1334 |
if save then MaSh.save ctxt overlord else (); |
51024
98fb341d32e3
distinguish MeSh and smart -- with smart, allow combinations of MaSh, MeSh, and MePo in different slices -- and use MaSh also with SMT solvers, based on evaluation
blanchet
parents:
51020
diff
changeset
|
1335 |
case (fact_filter, mess) of |
98fb341d32e3
distinguish MeSh and smart -- with smart, allow combinations of MaSh, MeSh, and MePo in different slices -- and use MaSh also with SMT solvers, based on evaluation
blanchet
parents:
51020
diff
changeset
|
1336 |
(NONE, [(_, (mepo, _)), (_, (mash, _))]) => |
51010 | 1337 |
[(meshN, mesh), (mepoN, mepo |> map fst |> add_and_take), |
1338 |
(mashN, mash |> map fst |> add_and_take)] |
|
54096
8ab8794410cd
repaired confusion between the stated and effective fact filter -- the mismatch could result in "Match" exceptions
blanchet
parents:
54095
diff
changeset
|
1339 |
| _ => [(effective_fact_filter, mesh)] |
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset
|
1340 |
end |
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48251
diff
changeset
|
1341 |
|
53148
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset
|
1342 |
fun kill_learners ctxt ({overlord, ...} : params) = |
c898409d8630
fixed subtle bug with "take" + thread overlord through
blanchet
parents:
53142
diff
changeset
|
1343 |
(Async_Manager.kill_threads MaShN "learner"; MaSh.shutdown ctxt overlord) |
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48318
diff
changeset
|
1344 |
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
|
1345 |
|
48248 | 1346 |
end; |