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