author | blanchet |
Mon, 12 Nov 2012 12:06:56 +0100 | |
changeset 50049 | dd6a4655cd72 |
parent 50048 | fb024bbf4b65 |
child 50267 | 1da2e67242d6 |
permissions | -rw-r--r-- |
36062 | 1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_util.ML |
35963 | 2 |
Author: Jasmin Blanchette, TU Muenchen |
3 |
||
4 |
General-purpose functions used by the Sledgehammer modules. |
|
5 |
*) |
|
6 |
||
7 |
signature SLEDGEHAMMER_UTIL = |
|
8 |
sig |
|
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48383
diff
changeset
|
9 |
val sledgehammerN : string |
36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36062
diff
changeset
|
10 |
val plural_s : int -> string |
35963 | 11 |
val serial_commas : string -> string list -> string list |
38738
0ce517c1970f
make sure that "undo_ascii_of" is the inverse of "ascii_of", also for non-printable characters -- and avoid those in ``-style facts
blanchet
parents:
38698
diff
changeset
|
12 |
val simplify_spaces : string -> string |
48656
5caa414ce9a2
cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
blanchet
parents:
48392
diff
changeset
|
13 |
val with_cleanup : ('a -> unit) -> ('a -> 'b) -> 'a -> 'b |
48383 | 14 |
val infinite_timeout : Time.time |
48318 | 15 |
val time_mult : real -> Time.time -> Time.time |
35963 | 16 |
val parse_bool_option : bool -> string -> string -> bool option |
17 |
val parse_time_option : string -> string -> Time.time option |
|
38044 | 18 |
val subgoal_count : Proof.state -> int |
38696
4c6b65d6a135
quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
blanchet
parents:
38652
diff
changeset
|
19 |
val reserved_isar_keyword_table : unit -> unit Symtab.table |
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48292
diff
changeset
|
20 |
val thms_in_proof : unit Symtab.table option -> thm -> string list |
50048 | 21 |
val with_vanilla_print_mode : ('a -> 'b) -> 'a -> 'b |
35963 | 22 |
end; |
39318 | 23 |
|
35963 | 24 |
structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = |
25 |
struct |
|
26 |
||
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43043
diff
changeset
|
27 |
open ATP_Util |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43043
diff
changeset
|
28 |
|
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48383
diff
changeset
|
29 |
val sledgehammerN = "sledgehammer" |
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48383
diff
changeset
|
30 |
|
36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36062
diff
changeset
|
31 |
fun plural_s n = if n = 1 then "" else "s" |
36062 | 32 |
|
43029
3e060b1c844b
use helpers and tweak Quickcheck's priority to it comes second (to give Solve Direct slightly more time before another prover runs)
blanchet
parents:
43005
diff
changeset
|
33 |
val serial_commas = Try.serial_commas |
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43043
diff
changeset
|
34 |
val simplify_spaces = strip_spaces false (K true) |
37962
d7dbe01f48d7
keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
37575
diff
changeset
|
35 |
|
48656
5caa414ce9a2
cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
blanchet
parents:
48392
diff
changeset
|
36 |
fun with_cleanup clean_up f x = |
5caa414ce9a2
cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
blanchet
parents:
48392
diff
changeset
|
37 |
Exn.capture f x |
5caa414ce9a2
cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
blanchet
parents:
48392
diff
changeset
|
38 |
|> tap (fn _ => clean_up x) |
5caa414ce9a2
cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
blanchet
parents:
48392
diff
changeset
|
39 |
|> Exn.release |
5caa414ce9a2
cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
blanchet
parents:
48392
diff
changeset
|
40 |
|
48383 | 41 |
val infinite_timeout = seconds 31536000.0 (* one year *) |
42 |
||
48318 | 43 |
fun time_mult k t = |
44 |
Time.fromMilliseconds (Real.ceil (k * Real.fromInt (Time.toMilliseconds t))) |
|
45 |
||
35963 | 46 |
fun parse_bool_option option name s = |
47 |
(case s of |
|
48 |
"smart" => if option then NONE else raise Option |
|
49 |
| "false" => SOME false |
|
50 |
| "true" => SOME true |
|
51 |
| "" => SOME true |
|
52 |
| _ => raise Option) |
|
53 |
handle Option.Option => |
|
54 |
let val ss = map quote ((option ? cons "smart") ["true", "false"]) in |
|
55 |
error ("Parameter " ^ quote name ^ " must be assigned " ^ |
|
56 |
space_implode " " (serial_commas "or" ss) ^ ".") |
|
57 |
end |
|
58 |
||
40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
39890
diff
changeset
|
59 |
val has_junk = |
40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
40341
diff
changeset
|
60 |
exists (fn s => not (Symbol.is_digit s) andalso s <> ".") o raw_explode (* FIXME Symbol.explode (?) *) |
40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
39890
diff
changeset
|
61 |
|
35963 | 62 |
fun parse_time_option _ "none" = NONE |
63 |
| parse_time_option name s = |
|
40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
39890
diff
changeset
|
64 |
let val secs = if has_junk s then NONE else Real.fromString s in |
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
43033
diff
changeset
|
65 |
if is_none secs orelse Real.< (the secs, 0.0) then |
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
43033
diff
changeset
|
66 |
error ("Parameter " ^ quote name ^ " must be assigned a nonnegative \ |
40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
39890
diff
changeset
|
67 |
\number of seconds (e.g., \"60\", \"0.5\") or \"none\".") |
35963 | 68 |
else |
40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
39890
diff
changeset
|
69 |
SOME (seconds (the secs)) |
35963 | 70 |
end |
71 |
||
43029
3e060b1c844b
use helpers and tweak Quickcheck's priority to it comes second (to give Solve Direct slightly more time before another prover runs)
blanchet
parents:
43005
diff
changeset
|
72 |
val subgoal_count = Try.subgoal_count |
38044 | 73 |
|
38696
4c6b65d6a135
quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
blanchet
parents:
38652
diff
changeset
|
74 |
fun reserved_isar_keyword_table () = |
48292 | 75 |
Keyword.dest () |-> union (op =) |> map (rpair ()) |> Symtab.make |
38696
4c6b65d6a135
quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
blanchet
parents:
38652
diff
changeset
|
76 |
|
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
46957
diff
changeset
|
77 |
(* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
46957
diff
changeset
|
78 |
fixes that seem to be missing over there; or maybe the two code portions are |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
46957
diff
changeset
|
79 |
not doing the same? *) |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
46957
diff
changeset
|
80 |
fun fold_body_thms thm_name f = |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
46957
diff
changeset
|
81 |
let |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
46957
diff
changeset
|
82 |
fun app n (PBody {thms, ...}) = |
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48292
diff
changeset
|
83 |
thms |> fold (fn (_, (name, _, body)) => fn accum => |
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48292
diff
changeset
|
84 |
let |
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48292
diff
changeset
|
85 |
(* The second disjunct caters for the uncommon case where the proved |
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48292
diff
changeset
|
86 |
theorem occurs in its own proof (e.g., |
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48292
diff
changeset
|
87 |
"Transitive_Closure.trancl_into_trancl"). *) |
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48292
diff
changeset
|
88 |
val no_name = (name = "" orelse (n = 1 andalso name = thm_name)) |
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48292
diff
changeset
|
89 |
val accum = |
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48292
diff
changeset
|
90 |
accum |> (if n = 1 andalso not no_name then f name else I) |
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48292
diff
changeset
|
91 |
val n = n + (if no_name then 0 else 1) |
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48292
diff
changeset
|
92 |
in accum |> (if n <= 1 then app n (Future.join body) else I) end) |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
46957
diff
changeset
|
93 |
in fold (app 0) end |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
46957
diff
changeset
|
94 |
|
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
46957
diff
changeset
|
95 |
fun thms_in_proof all_names th = |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
46957
diff
changeset
|
96 |
let |
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48292
diff
changeset
|
97 |
val collect = |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
46957
diff
changeset
|
98 |
case all_names of |
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48292
diff
changeset
|
99 |
SOME names => (fn s => Symtab.defined names s ? insert (op =) s) |
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48292
diff
changeset
|
100 |
| NONE => insert (op =) |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
46957
diff
changeset
|
101 |
val names = |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
46957
diff
changeset
|
102 |
[] |> fold_body_thms (Thm.get_name_hint th) collect [Thm.proof_body_of th] |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
46957
diff
changeset
|
103 |
in names end |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
46957
diff
changeset
|
104 |
|
50048 | 105 |
fun with_vanilla_print_mode f x = |
106 |
Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) |
|
107 |
(print_mode_value ())) f x |
|
108 |
||
35963 | 109 |
end; |