author | wenzelm |
Fri, 16 Mar 2012 11:26:55 +0100 | |
changeset 47828 | 0c15caf47040 |
parent 43926 | 0a2f5b86bdd7 |
child 49266 | 6cdcfbddc077 |
permissions | -rw-r--r-- |
blanchet@36062 | 1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_util.ML |
blanchet@35961 | 2 |
Author: Jasmin Blanchette, TU Muenchen |
blanchet@35961 | 3 |
|
blanchet@35961 | 4 |
General-purpose functions used by the Sledgehammer modules. |
blanchet@35961 | 5 |
*) |
blanchet@35961 | 6 |
|
blanchet@35961 | 7 |
signature SLEDGEHAMMER_UTIL = |
blanchet@35961 | 8 |
sig |
blanchet@36140 | 9 |
val plural_s : int -> string |
blanchet@35961 | 10 |
val serial_commas : string -> string list -> string list |
blanchet@38977 | 11 |
val simplify_spaces : string -> string |
blanchet@35961 | 12 |
val parse_bool_option : bool -> string -> string -> bool option |
blanchet@35961 | 13 |
val parse_time_option : string -> string -> Time.time option |
blanchet@38290 | 14 |
val subgoal_count : Proof.state -> int |
blanchet@43884 | 15 |
val normalize_chained_theorems : thm list -> thm list |
blanchet@38935 | 16 |
val reserved_isar_keyword_table : unit -> unit Symtab.table |
blanchet@35961 | 17 |
end; |
blanchet@39564 | 18 |
|
blanchet@35961 | 19 |
structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = |
blanchet@35961 | 20 |
struct |
blanchet@35961 | 21 |
|
blanchet@43926 | 22 |
open ATP_Util |
blanchet@43926 | 23 |
|
blanchet@36140 | 24 |
fun plural_s n = if n = 1 then "" else "s" |
blanchet@36062 | 25 |
|
blanchet@43870 | 26 |
val serial_commas = Try.serial_commas |
blanchet@43926 | 27 |
val simplify_spaces = strip_spaces false (K true) |
blanchet@38199 | 28 |
|
blanchet@35961 | 29 |
fun parse_bool_option option name s = |
blanchet@35961 | 30 |
(case s of |
blanchet@35961 | 31 |
"smart" => if option then NONE else raise Option |
blanchet@35961 | 32 |
| "false" => SOME false |
blanchet@35961 | 33 |
| "true" => SOME true |
blanchet@35961 | 34 |
| "" => SOME true |
blanchet@35961 | 35 |
| _ => raise Option) |
blanchet@35961 | 36 |
handle Option.Option => |
blanchet@35961 | 37 |
let val ss = map quote ((option ? cons "smart") ["true", "false"]) in |
blanchet@35961 | 38 |
error ("Parameter " ^ quote name ^ " must be assigned " ^ |
blanchet@35961 | 39 |
space_implode " " (serial_commas "or" ss) ^ ".") |
blanchet@35961 | 40 |
end |
blanchet@35961 | 41 |
|
blanchet@40582 | 42 |
val has_junk = |
wenzelm@40875 | 43 |
exists (fn s => not (Symbol.is_digit s) andalso s <> ".") o raw_explode (* FIXME Symbol.explode (?) *) |
blanchet@40582 | 44 |
|
blanchet@35961 | 45 |
fun parse_time_option _ "none" = NONE |
blanchet@35961 | 46 |
| parse_time_option name s = |
blanchet@40582 | 47 |
let val secs = if has_junk s then NONE else Real.fromString s in |
blanchet@43875 | 48 |
if is_none secs orelse Real.< (the secs, 0.0) then |
blanchet@43875 | 49 |
error ("Parameter " ^ quote name ^ " must be assigned a nonnegative \ |
blanchet@40582 | 50 |
\number of seconds (e.g., \"60\", \"0.5\") or \"none\".") |
blanchet@35961 | 51 |
else |
blanchet@40582 | 52 |
SOME (seconds (the secs)) |
blanchet@35961 | 53 |
end |
blanchet@35961 | 54 |
|
blanchet@43870 | 55 |
val subgoal_count = Try.subgoal_count |
blanchet@38290 | 56 |
|
blanchet@43884 | 57 |
val normalize_chained_theorems = |
blanchet@43884 | 58 |
maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th]) |
blanchet@38935 | 59 |
fun reserved_isar_keyword_table () = |
wenzelm@47828 | 60 |
Keyword.dest () |-> union (op =) |
blanchet@38935 | 61 |
|> map (rpair ()) |> Symtab.make |
blanchet@38935 | 62 |
|
blanchet@35961 | 63 |
end; |