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