equal
deleted
inserted
replaced
4 General-purpose functions used by the Sledgehammer modules. |
4 General-purpose functions used by the Sledgehammer modules. |
5 *) |
5 *) |
6 |
6 |
7 signature SLEDGEHAMMER_UTIL = |
7 signature SLEDGEHAMMER_UTIL = |
8 sig |
8 sig |
9 val is_new_spass_version : bool |
|
10 val pairf : ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c |
9 val pairf : ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c |
11 val plural_s : int -> string |
10 val plural_s : int -> string |
12 val serial_commas : string -> string list -> string list |
11 val serial_commas : string -> string list -> string list |
13 val replace_all : string -> string -> string -> string |
12 val replace_all : string -> string -> string -> string |
14 val remove_all : string -> string -> string |
13 val remove_all : string -> string -> string |
22 val specialize_type : theory -> (string * typ) -> term -> term |
21 val specialize_type : theory -> (string * typ) -> term -> term |
23 end; |
22 end; |
24 |
23 |
25 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = |
24 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = |
26 struct |
25 struct |
27 |
|
28 val is_new_spass_version = |
|
29 case getenv "SPASS_VERSION" of |
|
30 "" => (case getenv "SPASS_HOME" of |
|
31 "" => false |
|
32 | s => |
|
33 (* Hack: Preliminary versions of the SPASS 3.7 package don't set |
|
34 "SPASS_VERSION". *) |
|
35 String.isSubstring "/spass-3.7/" s) |
|
36 | s => (case s |> space_explode "." |> map Int.fromString of |
|
37 SOME m :: SOME n :: _ => m > 3 orelse (m = 3 andalso n >= 5) |
|
38 | _ => false) |
|
39 |
26 |
40 fun pairf f g x = (f x, g x) |
27 fun pairf f g x = (f x, g x) |
41 |
28 |
42 fun plural_s n = if n = 1 then "" else "s" |
29 fun plural_s n = if n = 1 then "" else "s" |
43 |
30 |