author  blanchet 
Tue, 15 Oct 2013 17:21:16 +0200  
changeset 54116  ba709c934470 
parent 54062  427380d5d1d7 
child 54695  a9efdf970720 
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? *) 
54116
ba709c934470
made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverseengineering proof terms
blanchet
parents:
54062
diff
changeset

100 
fun fold_body_thm 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 
54116
ba709c934470
made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverseengineering proof terms
blanchet
parents:
54062
diff
changeset

102 
fun app_thm map_name (_, (name, _, body)) accum = 
ba709c934470
made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverseengineering proof terms
blanchet
parents:
54062
diff
changeset

103 
let 
ba709c934470
made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverseengineering proof terms
blanchet
parents:
54062
diff
changeset

104 
val (anonymous, enter_class) = 
ba709c934470
made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverseengineering proof terms
blanchet
parents:
54062
diff
changeset

105 
(* The "name = outer_name" case caters for the uncommon case where the proved theorem 
ba709c934470
made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverseengineering proof terms
blanchet
parents:
54062
diff
changeset

106 
occurs in its own proof (e.g., "Transitive_Closure.trancl_into_trancl"). *) 
ba709c934470
made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverseengineering proof terms
blanchet
parents:
54062
diff
changeset

107 
if name = "" orelse name = outer_name then (true, false) 
ba709c934470
made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverseengineering proof terms
blanchet
parents:
54062
diff
changeset

108 
else if map_inclass_name name = SOME outer_name then (true, true) 
ba709c934470
made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverseengineering proof terms
blanchet
parents:
54062
diff
changeset

109 
else (false, false) 
ba709c934470
made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverseengineering proof terms
blanchet
parents:
54062
diff
changeset

110 
in 
ba709c934470
made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverseengineering proof terms
blanchet
parents:
54062
diff
changeset

111 
if anonymous then 
ba709c934470
made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverseengineering proof terms
blanchet
parents:
54062
diff
changeset

112 
accum > app_body (if enter_class then map_inclass_name else map_name) (Future.join body) 
ba709c934470
made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverseengineering proof terms
blanchet
parents:
54062
diff
changeset

113 
else 
ba709c934470
made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverseengineering proof terms
blanchet
parents:
54062
diff
changeset

114 
accum > union (op =) (the_list (map_name name)) 
ba709c934470
made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverseengineering proof terms
blanchet
parents:
54062
diff
changeset

115 
end 
ba709c934470
made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverseengineering proof terms
blanchet
parents:
54062
diff
changeset

116 
and app_body map_name (PBody {thms, ...}) = fold (app_thm map_name) thms 
ba709c934470
made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverseengineering proof terms
blanchet
parents:
54062
diff
changeset

117 
in app_body map_plain_name end 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
46957
diff
changeset

118 

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

119 
fun thms_in_proof name_tabs th = 
54116
ba709c934470
made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverseengineering proof terms
blanchet
parents:
54062
diff
changeset

120 
let val map_names = (case name_tabs of SOME p => pairself Symtab.lookup p  NONE => `I SOME) in 
ba709c934470
made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverseengineering proof terms
blanchet
parents:
54062
diff
changeset

121 
fold_body_thm (Thm.get_name_hint th) map_names (Proofterm.strip_thm (Thm.proof_body_of th)) [] 
ba709c934470
made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverseengineering proof terms
blanchet
parents:
54062
diff
changeset

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

123 

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

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

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

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

127 
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

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

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

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

131 
> 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

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

133 
> 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

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

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

136 

50557  137 
val one_day = seconds (24.0 * 60.0 * 60.0) 
138 
val one_year = seconds (365.0 * 24.0 * 60.0 * 60.0) 

139 

140 
fun time_limit NONE = I 

141 
 time_limit (SOME delay) = TimeLimit.timeLimit delay 

142 

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

145 
(print_mode_value ())) f x 

146 

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

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

148 
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

149 

54062  150 
val spying_version = "c" 
53815
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53800
diff
changeset

151 

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

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

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

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

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

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

157 
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

158 
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

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

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

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

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

163 

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

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

165 

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

166 
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

167 

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

168 
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

169 

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

170 
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

171 

35963  172 
end; 