1 (* Title: HOL/Tools/Sledgehammer/sledgehammer_util.ML
2 Author: Jasmin Blanchette, TU Muenchen
4 General-purpose functions used by the Sledgehammer modules.
7 signature SLEDGEHAMMER_UTIL =
9 val sledgehammerN : string
10 val plural_s : int -> string
11 val serial_commas : string -> string list -> string list
12 val simplify_spaces : string -> string
13 val with_cleanup : ('a -> unit) -> ('a -> 'b) -> 'a -> 'b
14 val infinite_timeout : Time.time
15 val time_mult : real -> Time.time -> Time.time
16 val parse_bool_option : bool -> string -> string -> bool option
17 val parse_time_option : string -> string -> Time.time option
18 val subgoal_count : Proof.state -> int
19 val reserved_isar_keyword_table : unit -> unit Symtab.table
20 val thms_in_proof : unit Symtab.table option -> thm -> string list
23 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
28 val sledgehammerN = "sledgehammer"
30 fun plural_s n = if n = 1 then "" else "s"
32 val serial_commas = Try.serial_commas
33 val simplify_spaces = strip_spaces false (K true)
35 fun with_cleanup clean_up f x =
37 |> tap (fn _ => clean_up x)
40 val infinite_timeout = seconds 31536000.0 (* one year *)
43 Time.fromMilliseconds (Real.ceil (k * Real.fromInt (Time.toMilliseconds t)))
45 fun parse_bool_option option name s =
47 "smart" => if option then NONE else raise Option
48 | "false" => SOME false
52 handle Option.Option =>
53 let val ss = map quote ((option ? cons "smart") ["true", "false"]) in
54 error ("Parameter " ^ quote name ^ " must be assigned " ^
55 space_implode " " (serial_commas "or" ss) ^ ".")
59 exists (fn s => not (Symbol.is_digit s) andalso s <> ".") o raw_explode (* FIXME Symbol.explode (?) *)
61 fun parse_time_option _ "none" = NONE
62 | parse_time_option name s =
63 let val secs = if has_junk s then NONE else Real.fromString s in
64 if is_none secs orelse Real.< (the secs, 0.0) then
65 error ("Parameter " ^ quote name ^ " must be assigned a nonnegative \
66 \number of seconds (e.g., \"60\", \"0.5\") or \"none\".")
68 SOME (seconds (the secs))
71 val subgoal_count = Try.subgoal_count
73 fun reserved_isar_keyword_table () =
74 Keyword.dest () |-> union (op =) |> map (rpair ()) |> Symtab.make
76 (* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few
77 fixes that seem to be missing over there; or maybe the two code portions are
78 not doing the same? *)
79 fun fold_body_thms thm_name f =
81 fun app n (PBody {thms, ...}) =
82 thms |> fold (fn (_, (name, _, body)) => fn accum =>
84 (* The second disjunct caters for the uncommon case where the proved
85 theorem occurs in its own proof (e.g.,
86 "Transitive_Closure.trancl_into_trancl"). *)
87 val no_name = (name = "" orelse (n = 1 andalso name = thm_name))
89 accum |> (if n = 1 andalso not no_name then f name else I)
90 val n = n + (if no_name then 0 else 1)
91 in accum |> (if n <= 1 then app n (Future.join body) else I) end)
94 fun thms_in_proof all_names th =
98 SOME names => (fn s => Symtab.defined names s ? insert (op =) s)
99 | NONE => insert (op =)
101 [] |> fold_body_thms (Thm.get_name_hint th) collect [Thm.proof_body_of th]