author  haftmann 
Thu, 08 Jul 2010 16:19:24 +0200  
changeset 37744  3daaf23b9ab4 
parent 37575  cfc5e281740f 
child 37962  d7dbe01f48d7 
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 

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

9 
val plural_s : int > string 
35963  10 
val serial_commas : string > string list > string list 
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

11 
val timestamp : unit > string 
35963  12 
val parse_bool_option : bool > string > string > bool option 
13 
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

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

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

16 
val maybe_quote : string > string 
36555
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36496
diff
changeset

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

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

20 

35963  21 
structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = 
22 
struct 

23 

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

24 
fun plural_s n = if n = 1 then "" else "s" 
36062  25 

35963  26 
fun serial_commas _ [] = ["??"] 
27 
 serial_commas _ [s] = [s] 

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

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

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

31 

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

32 
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

33 

35963  34 
fun parse_bool_option option name s = 
35 
(case s of 

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

37 
 "false" => SOME false 

38 
 "true" => SOME true 

39 
 "" => SOME true 

40 
 _ => raise Option) 

41 
handle Option.Option => 

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

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

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

45 
end 

46 

47 
fun parse_time_option _ "none" = NONE 

48 
 parse_time_option name s = 

49 
let 

50 
val msecs = 

51 
case space_explode " " s of 

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

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

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

55 
 _ => 0 

56 
in 

57 
if msecs <= 0 then 

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

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

60 
else 

61 
SOME (Time.fromMilliseconds msecs) 

62 
end 

63 

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

64 
val subscript = implode o map (prefix "\<^isub>") o explode 
37321  65 
fun nat_subscript n = 
66 
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

67 

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

68 
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

69 
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

70 
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

71 

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

72 
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

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

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

75 
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

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

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

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

79 

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

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

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

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

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

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

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

86 

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

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

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

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

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

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

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

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

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

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

96 
(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

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

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

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

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

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

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

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

104 

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

105 

35963  106 
end; 