author  blanchet 
Wed, 02 Jun 2010 15:18:48 +0200  
changeset 37321  9d7cfae95b30 
parent 36960  01594f816e3a 
child 37414  d0cea0796295 
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 
36555
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36496
diff
changeset

21 
val monomorphic_term : Type.tyenv > term > term 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36496
diff
changeset

22 
val specialize_type : theory > (string * typ) > term > term 
35963  23 
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

24 

35963  25 
structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = 
26 
struct 

27 

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

28 
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

29 
case getenv "SPASS_VERSION" of 
36496  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 "/spass3.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) 

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

39 

36378  40 
fun pairf f g x = (f x, g x) 
41 

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

42 
fun plural_s n = if n = 1 then "" else "s" 
36062  43 

35963  44 
fun serial_commas _ [] = ["??"] 
45 
 serial_commas _ [s] = [s] 

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

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

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

49 

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

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

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

52 
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

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

54 
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

55 
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

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

57 
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

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

59 
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

60 

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

61 
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

62 

35963  63 
fun parse_bool_option option name s = 
64 
(case s of 

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

66 
 "false" => SOME false 

67 
 "true" => SOME true 

68 
 "" => SOME true 

69 
 _ => raise Option) 

70 
handle Option.Option => 

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

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

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

74 
end 

75 

76 
fun parse_time_option _ "none" = NONE 

77 
 parse_time_option name s = 

78 
let 

79 
val msecs = 

80 
case space_explode " " s of 

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

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

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

84 
 _ => 0 

85 
in 

86 
if msecs <= 0 then 

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

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

89 
else 

90 
SOME (Time.fromMilliseconds msecs) 

91 
end 

92 

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

93 
val subscript = implode o map (prefix "\<^isub>") o explode 
37321  94 
fun nat_subscript n = 
95 
n > string_of_int > print_mode_active Symbol.xsymbolsN ? subscript 

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

96 

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

97 
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

98 
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

99 
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

100 

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

101 
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

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

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

104 
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

105 
not (is_long_identifier (perhaps (try (unprefix "?")) s))) orelse 
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36555
diff
changeset

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

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

108 

36555
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36496
diff
changeset

109 
fun monomorphic_term subst t = 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36496
diff
changeset

110 
map_types (map_type_tvar (fn v => 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36496
diff
changeset

111 
case Type.lookup subst v of 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36496
diff
changeset

112 
SOME typ => typ 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36496
diff
changeset

113 
 NONE => raise TERM ("monomorphic_term: uninstanitated schematic type \ 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36496
diff
changeset

114 
\variable", [t]))) t 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36496
diff
changeset

115 

8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36496
diff
changeset

116 
fun specialize_type thy (s, T) t = 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36496
diff
changeset

117 
let 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36496
diff
changeset

118 
fun subst_for (Const (s', T')) = 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36496
diff
changeset

119 
if s = s' then 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36496
diff
changeset

120 
SOME (Sign.typ_match thy (T', T) Vartab.empty) 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36496
diff
changeset

121 
handle Type.TYPE_MATCH => NONE 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36496
diff
changeset

122 
else 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36496
diff
changeset

123 
NONE 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36496
diff
changeset

124 
 subst_for (t1 $ t2) = 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36496
diff
changeset

125 
(case subst_for t1 of SOME x => SOME x  NONE => subst_for t2) 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36496
diff
changeset

126 
 subst_for (Abs (_, _, t')) = subst_for t' 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36496
diff
changeset

127 
 subst_for _ = NONE 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36496
diff
changeset

128 
in 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36496
diff
changeset

129 
case subst_for t of 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36496
diff
changeset

130 
SOME subst => monomorphic_term subst t 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36496
diff
changeset

131 
 NONE => raise Type.TYPE_MATCH 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36496
diff
changeset

132 
end 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36496
diff
changeset

133 

8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36496
diff
changeset

134 

35963  135 
end; 