author  blanchet 
Wed, 28 Apr 2010 15:34:55 +0200  
changeset 36491  6769f8eacaac 
parent 36486  c2d7e2dff59e 
child 36496  8b2dc9b4bf4c 
permissions  rwrr 
36062  1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer_util.ML 
35963  2 
Author: Jasmin Blanchette, TU Muenchen 
3 

4 
Generalpurpose functions used by the Sledgehammer modules. 

5 
*) 

6 

7 
signature SLEDGEHAMMER_UTIL = 

8 
sig 

36491
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36486
diff
changeset

9 
val is_new_spass_version : bool 
36378  10 
val pairf : ('a > 'b) > ('a > 'c) > 'a > 'b * 'c 
36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36062
diff
changeset

11 
val plural_s : int > string 
35963  12 
val serial_commas : string > string list > string list 
36169
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36142
diff
changeset

13 
val replace_all : string > string > string > string 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36142
diff
changeset

14 
val remove_all : string > string > string 
36170
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset

15 
val timestamp : unit > string 
35963  16 
val parse_bool_option : bool > string > string > bool option 
17 
val parse_time_option : string > string > Time.time option 

36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36478
diff
changeset

18 
val nat_subscript : int > string 
36478
1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36402
diff
changeset

19 
val unyxml : string > string 
1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36402
diff
changeset

20 
val maybe_quote : string > string 
35963  21 
end; 
36170
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset

22 

35963  23 
structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = 
24 
struct 

25 

36491
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36486
diff
changeset

26 
val is_new_spass_version = 
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36486
diff
changeset

27 
case getenv "SPASS_VERSION" of 
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36486
diff
changeset

28 
"" => case getenv "SPASS_HOME" of 
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36486
diff
changeset

29 
"" => false 
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36486
diff
changeset

30 
 s => 
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36486
diff
changeset

31 
(* Hack: Preliminary versions of the SPASS 3.7 package don't set 
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36486
diff
changeset

32 
"SPASS_VERSION". *) 
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36486
diff
changeset

33 
String.isSubstring "/spass3.7/" s 
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36486
diff
changeset

34 
 s => case s > space_explode "." > map Int.fromString of 
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36486
diff
changeset

35 
SOME m :: SOME n :: _ => m > 3 orelse (m = 3 andalso n >= 5) 
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36486
diff
changeset

36 
 _ => false 
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36486
diff
changeset

37 

36378  38 
fun pairf f g x = (f x, g x) 
39 

36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36062
diff
changeset

40 
fun plural_s n = if n = 1 then "" else "s" 
36062  41 

35963  42 
fun serial_commas _ [] = ["??"] 
43 
 serial_commas _ [s] = [s] 

44 
 serial_commas conj [s1, s2] = [s1, conj, s2] 

45 
 serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3] 

46 
 serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss 

47 

36169
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36142
diff
changeset

48 
fun replace_all bef aft = 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36142
diff
changeset

49 
let 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36142
diff
changeset

50 
fun aux seen "" = String.implode (rev seen) 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36142
diff
changeset

51 
 aux seen s = 
36183
f723348b2231
Sledgehammer: the empty set of fact () should mean nothing, not unchanged
blanchet
parents:
36170
diff
changeset

52 
if String.isPrefix bef s then 
36169
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36142
diff
changeset

53 
aux seen "" ^ aft ^ aux [] (unprefix bef s) 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36142
diff
changeset

54 
else 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36142
diff
changeset

55 
aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE)) 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36142
diff
changeset

56 
in aux [] end 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36142
diff
changeset

57 
fun remove_all bef = replace_all bef "" 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36142
diff
changeset

58 

36170
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset

59 
val timestamp = Date.fmt "%Y%m%d %H:%M:%S" o Date.fromTimeLocal o Time.now 
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset

60 

35963  61 
fun parse_bool_option option name s = 
62 
(case s of 

63 
"smart" => if option then NONE else raise Option 

64 
 "false" => SOME false 

65 
 "true" => SOME true 

66 
 "" => SOME true 

67 
 _ => raise Option) 

68 
handle Option.Option => 

69 
let val ss = map quote ((option ? cons "smart") ["true", "false"]) in 

70 
error ("Parameter " ^ quote name ^ " must be assigned " ^ 

71 
space_implode " " (serial_commas "or" ss) ^ ".") 

72 
end 

73 

74 
fun parse_time_option _ "none" = NONE 

75 
 parse_time_option name s = 

76 
let 

77 
val msecs = 

78 
case space_explode " " s of 

79 
[s1, "min"] => 60000 * the (Int.fromString s1) 

80 
 [s1, "s"] => 1000 * the (Int.fromString s1) 

81 
 [s1, "ms"] => the (Int.fromString s1) 

82 
 _ => 0 

83 
in 

84 
if msecs <= 0 then 

85 
error ("Parameter " ^ quote name ^ " must be assigned a positive time \ 

86 
\value (e.g., \"60 s\", \"200 ms\") or \"none\".") 

87 
else 

88 
SOME (Time.fromMilliseconds msecs) 

89 
end 

90 

36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36478
diff
changeset

91 
val subscript = implode o map (prefix "\<^isub>") o explode 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36478
diff
changeset

92 
val nat_subscript = subscript o string_of_int 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36478
diff
changeset

93 

36478
1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36402
diff
changeset

94 
fun plain_string_from_xml_tree t = 
1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36402
diff
changeset

95 
Buffer.empty > XML.add_content t > Buffer.content 
1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36402
diff
changeset

96 
val unyxml = plain_string_from_xml_tree o YXML.parse 
1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36402
diff
changeset

97 

1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36402
diff
changeset

98 
val is_long_identifier = forall Syntax.is_identifier o space_explode "." 
1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36402
diff
changeset

99 
fun maybe_quote y = 
1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36402
diff
changeset

100 
let val s = unyxml y in 
1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36402
diff
changeset

101 
y > ((not (is_long_identifier (perhaps (try (unprefix "'")) s)) andalso 
1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36402
diff
changeset

102 
not (is_long_identifier (perhaps (try (unprefix "?")) s))) orelse 
1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36402
diff
changeset

103 
OuterKeyword.is_keyword s) ? quote 
1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36402
diff
changeset

104 
end 
1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36402
diff
changeset

105 

35963  106 
end; 