author  blanchet 
Tue, 24 Sep 2013 11:02:42 +0200  
changeset 53815  e8aa538e959e 
parent 53800  ac1ec5065316 
child 54062  427380d5d1d7 
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 

48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48383
diff
changeset

9 
val sledgehammerN : string 
50608  10 
val log2 : real > real 
51181
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51010
diff
changeset

11 
val app_hd : ('a > 'a) > 'a list > 'a list 
36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36062
diff
changeset

12 
val plural_s : int > string 
35963  13 
val serial_commas : string > string list > string list 
38738
0ce517c1970f
make sure that "undo_ascii_of" is the inverse of "ascii_of", also for nonprintable characters  and avoid those in ``style facts
blanchet
parents:
38698
diff
changeset

14 
val simplify_spaces : string > string 
48656
5caa414ce9a2
cleaner temporary file cleanup for MaSh, based on triedandtrusted code
blanchet
parents:
48392
diff
changeset

15 
val with_cleanup : ('a > unit) > ('a > 'b) > 'a > 'b 
48383  16 
val infinite_timeout : Time.time 
48318  17 
val time_mult : real > Time.time > Time.time 
35963  18 
val parse_bool_option : bool > string > string > bool option 
19 
val parse_time_option : string > string > Time.time option 

38044  20 
val subgoal_count : Proof.state > int 
38696
4c6b65d6a135
quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
blanchet
parents:
38652
diff
changeset

21 
val reserved_isar_keyword_table : unit > unit Symtab.table 
50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

22 
val thms_in_proof : 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

23 
(string Symtab.table * string Symtab.table) option > thm > string list 
50267
1da2e67242d6
moved thms_of_name to Sledgehammer_Util and removed copies, updated references
smolkas
parents:
50049
diff
changeset

24 
val thms_of_name : Proof.context > string > thm list 
50557  25 
val one_day : Time.time 
26 
val one_year : Time.time 

27 
val time_limit : Time.time option > ('a > 'b) > 'a > 'b 

50048  28 
val with_vanilla_print_mode : ('a > 'b) > 'a > 'b 
53815
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53800
diff
changeset

29 
val hackish_string_of_term : Proof.context > term > string 
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53800
diff
changeset

30 
val spying : bool > (unit > Proof.state * int * string * string) > unit 
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
51930
diff
changeset

31 

c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
51930
diff
changeset

32 
(** extrema **) 
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
51930
diff
changeset

33 
val max : ('a * 'a > order) > 'a > 'a > 'a 
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
51930
diff
changeset

34 
val max_option : ('a * 'a > order) > 'a option > 'a option > 'a option 
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
51930
diff
changeset

35 
val max_list : ('a * 'a > order) > 'a list > 'a option 
35963  36 
end; 
39318  37 

35963  38 
structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = 
39 
struct 

40 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43043
diff
changeset

41 
open ATP_Util 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43043
diff
changeset

42 

48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48383
diff
changeset

43 
val sledgehammerN = "sledgehammer" 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48383
diff
changeset

44 

50608  45 
val log10_2 = Math.log10 2.0 
46 

47 
fun log2 n = Math.log10 n / log10_2 

48 

51181
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51010
diff
changeset

49 
fun app_hd f (x :: xs) = f x :: xs 
d0fa18638478
implement (more) accurate computation of parents
blanchet
parents:
51010
diff
changeset

50 

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

51 
fun plural_s n = if n = 1 then "" else "s" 
36062  52 

43029
3e060b1c844b
use helpers and tweak Quickcheck's priority to it comes second (to give Solve Direct slightly more time before another prover runs)
blanchet
parents:
43005
diff
changeset

53 
val serial_commas = Try.serial_commas 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43043
diff
changeset

54 
val simplify_spaces = strip_spaces false (K true) 
37962
d7dbe01f48d7
keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
37575
diff
changeset

55 

48656
5caa414ce9a2
cleaner temporary file cleanup for MaSh, based on triedandtrusted code
blanchet
parents:
48392
diff
changeset

56 
fun with_cleanup clean_up f x = 
5caa414ce9a2
cleaner temporary file cleanup for MaSh, based on triedandtrusted code
blanchet
parents:
48392
diff
changeset

57 
Exn.capture f x 
5caa414ce9a2
cleaner temporary file cleanup for MaSh, based on triedandtrusted code
blanchet
parents:
48392
diff
changeset

58 
> tap (fn _ => clean_up x) 
5caa414ce9a2
cleaner temporary file cleanup for MaSh, based on triedandtrusted code
blanchet
parents:
48392
diff
changeset

59 
> Exn.release 
5caa414ce9a2
cleaner temporary file cleanup for MaSh, based on triedandtrusted code
blanchet
parents:
48392
diff
changeset

60 

48383  61 
val infinite_timeout = seconds 31536000.0 (* one year *) 
62 

48318  63 
fun time_mult k t = 
64 
Time.fromMilliseconds (Real.ceil (k * Real.fromInt (Time.toMilliseconds t))) 

65 

35963  66 
fun parse_bool_option option name s = 
67 
(case s of 

51930
52fd62618631
prefer explicitly qualified exceptions, which is particular important for robust handlers;
wenzelm
parents:
51181
diff
changeset

68 
"smart" => if option then NONE else raise Option.Option 
35963  69 
 "false" => SOME false 
70 
 "true" => SOME true 

71 
 "" => SOME true 

51930
52fd62618631
prefer explicitly qualified exceptions, which is particular important for robust handlers;
wenzelm
parents:
51181
diff
changeset

72 
 _ => raise Option.Option) 
35963  73 
handle Option.Option => 
74 
let val ss = map quote ((option ? cons "smart") ["true", "false"]) in 

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

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

77 
end 

78 

40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
39890
diff
changeset

79 
val has_junk = 
40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
40341
diff
changeset

80 
exists (fn s => not (Symbol.is_digit s) andalso s <> ".") o raw_explode (* FIXME Symbol.explode (?) *) 
40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
39890
diff
changeset

81 

35963  82 
fun parse_time_option _ "none" = NONE 
83 
 parse_time_option name s = 

40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
39890
diff
changeset

84 
let val secs = if has_junk s then NONE else Real.fromString s in 
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
43033
diff
changeset

85 
if is_none secs orelse Real.< (the secs, 0.0) then 
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
43033
diff
changeset

86 
error ("Parameter " ^ quote name ^ " must be assigned a nonnegative \ 
40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
39890
diff
changeset

87 
\number of seconds (e.g., \"60\", \"0.5\") or \"none\".") 
35963  88 
else 
40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
39890
diff
changeset

89 
SOME (seconds (the secs)) 
35963  90 
end 
91 

43029
3e060b1c844b
use helpers and tweak Quickcheck's priority to it comes second (to give Solve Direct slightly more time before another prover runs)
blanchet
parents:
43005
diff
changeset

92 
val subgoal_count = Try.subgoal_count 
38044  93 

38696
4c6b65d6a135
quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
blanchet
parents:
38652
diff
changeset

94 
fun reserved_isar_keyword_table () = 
48292  95 
Keyword.dest () > union (op =) > map (rpair ()) > Symtab.make 
38696
4c6b65d6a135
quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
blanchet
parents:
38652
diff
changeset

96 

48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
46957
diff
changeset

97 
(* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
46957
diff
changeset

98 
fixes that seem to be missing over there; or maybe the two code portions are 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
46957
diff
changeset

99 
not doing the same? *) 
50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

100 
fun fold_body_thms outer_name (map_plain_name, map_inclass_name) = 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
46957
diff
changeset

101 
let 
50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

102 
fun app map_name n (PBody {thms, ...}) = 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48292
diff
changeset

103 
thms > fold (fn (_, (name, _, body)) => fn accum => 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48292
diff
changeset

104 
let 
50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

105 
val collect = union (op =) o the_list o map_name 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

106 
(* The "name = outer_name" case caters for the uncommon case where 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

107 
the proved theorem occurs in its own proof (e.g., 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

108 
"Transitive_Closure.trancl_into_trancl"). *) 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

109 
val (anonymous, enter_class) = 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

110 
if name = "" orelse (n = 1 andalso name = outer_name) then 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

111 
(true, false) 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

112 
else if n = 1 andalso map_inclass_name name = SOME outer_name then 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

113 
(true, true) 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

114 
else 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

115 
(false, false) 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48292
diff
changeset

116 
val accum = 
50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

117 
accum > (if n = 1 andalso not anonymous then collect name else I) 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

118 
val n = n + (if anonymous then 0 else 1) 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

119 
in 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

120 
accum 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

121 
> (if n <= 1 then 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

122 
app (if enter_class then map_inclass_name else map_name) n 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

123 
(Future.join body) 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

124 
else 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

125 
I) 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

126 
end) 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

127 
in fold (app map_plain_name 0) end 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
46957
diff
changeset

128 

50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

129 
fun thms_in_proof name_tabs th = 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
46957
diff
changeset

130 
let 
50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

131 
val map_names = 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

132 
case name_tabs of 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

133 
SOME p => pairself Symtab.lookup p 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

134 
 NONE => `I SOME 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
46957
diff
changeset

135 
val names = 
50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

136 
fold_body_thms (Thm.get_name_hint th) map_names [Thm.proof_body_of th] [] 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
46957
diff
changeset

137 
in names end 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
46957
diff
changeset

138 

50267
1da2e67242d6
moved thms_of_name to Sledgehammer_Util and removed copies, updated references
smolkas
parents:
50049
diff
changeset

139 
fun thms_of_name ctxt name = 
1da2e67242d6
moved thms_of_name to Sledgehammer_Util and removed copies, updated references
smolkas
parents:
50049
diff
changeset

140 
let 
1da2e67242d6
moved thms_of_name to Sledgehammer_Util and removed copies, updated references
smolkas
parents:
50049
diff
changeset

141 
val lex = Keyword.get_lexicons 
1da2e67242d6
moved thms_of_name to Sledgehammer_Util and removed copies, updated references
smolkas
parents:
50049
diff
changeset

142 
val get = maps (Proof_Context.get_fact ctxt o fst) 
1da2e67242d6
moved thms_of_name to Sledgehammer_Util and removed copies, updated references
smolkas
parents:
50049
diff
changeset

143 
in 
1da2e67242d6
moved thms_of_name to Sledgehammer_Util and removed copies, updated references
smolkas
parents:
50049
diff
changeset

144 
Source.of_string name 
1da2e67242d6
moved thms_of_name to Sledgehammer_Util and removed copies, updated references
smolkas
parents:
50049
diff
changeset

145 
> Symbol.source 
1da2e67242d6
moved thms_of_name to Sledgehammer_Util and removed copies, updated references
smolkas
parents:
50049
diff
changeset

146 
> Token.source {do_recover = SOME false} lex Position.start 
1da2e67242d6
moved thms_of_name to Sledgehammer_Util and removed copies, updated references
smolkas
parents:
50049
diff
changeset

147 
> Token.source_proper 
1da2e67242d6
moved thms_of_name to Sledgehammer_Util and removed copies, updated references
smolkas
parents:
50049
diff
changeset

148 
> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE 
1da2e67242d6
moved thms_of_name to Sledgehammer_Util and removed copies, updated references
smolkas
parents:
50049
diff
changeset

149 
> Source.exhaust 
1da2e67242d6
moved thms_of_name to Sledgehammer_Util and removed copies, updated references
smolkas
parents:
50049
diff
changeset

150 
end 
1da2e67242d6
moved thms_of_name to Sledgehammer_Util and removed copies, updated references
smolkas
parents:
50049
diff
changeset

151 

50557  152 
val one_day = seconds (24.0 * 60.0 * 60.0) 
153 
val one_year = seconds (365.0 * 24.0 * 60.0 * 60.0) 

154 

155 
fun time_limit NONE = I 

156 
 time_limit (SOME delay) = TimeLimit.timeLimit delay 

157 

50048  158 
fun with_vanilla_print_mode f x = 
159 
Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) 

160 
(print_mode_value ())) f x 

161 

53815
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53800
diff
changeset

162 
fun hackish_string_of_term ctxt = 
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53800
diff
changeset

163 
with_vanilla_print_mode (Syntax.string_of_term ctxt) #> simplify_spaces 
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53800
diff
changeset

164 

e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53800
diff
changeset

165 
val spying_version = "b" 
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53800
diff
changeset

166 

e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53800
diff
changeset

167 
fun spying false _ = () 
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53800
diff
changeset

168 
 spying true f = 
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53800
diff
changeset

169 
let 
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53800
diff
changeset

170 
val (state, i, tool, message) = f () 
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53800
diff
changeset

171 
val ctxt = Proof.context_of state 
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53800
diff
changeset

172 
val goal = Logic.get_goal (prop_of (#goal (Proof.goal state))) i 
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53800
diff
changeset

173 
val hash = String.substring (SHA1.rep (SHA1.digest (hackish_string_of_term ctxt goal)), 0, 12) 
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53800
diff
changeset

174 
in 
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53800
diff
changeset

175 
File.append (Path.explode "$ISABELLE_HOME_USER/spy_sledgehammer") 
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53800
diff
changeset

176 
(spying_version ^ " " ^ timestamp () ^ ": " ^ hash ^ ": " ^ tool ^ ": " ^ message ^ "\n") 
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53800
diff
changeset

177 
end 
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53800
diff
changeset

178 

52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
51930
diff
changeset

179 
(** extrema **) 
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
51930
diff
changeset

180 

c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
51930
diff
changeset

181 
fun max ord x y = case ord(x,y) of LESS => y  _ => x 
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
51930
diff
changeset

182 

c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
51930
diff
changeset

183 
fun max_option ord = max (option_ord ord) 
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
51930
diff
changeset

184 

c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
51930
diff
changeset

185 
fun max_list ord xs = fold (SOME #> max_option ord) xs NONE 
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
51930
diff
changeset

186 

35963  187 
end; 