author  smolkas 
Wed, 28 Nov 2012 12:25:43 +0100  
changeset 50267  1da2e67242d6 
parent 50049  dd6a4655cd72 
child 50485  3c6ac2da2f45 
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 
36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36062
diff
changeset

10 
val plural_s : int > string 
35963  11 
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

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

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

38044  18 
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

19 
val reserved_isar_keyword_table : unit > unit Symtab.table 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48292
diff
changeset

20 
val thms_in_proof : unit 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

21 
val thms_of_name : Proof.context > string > thm list 
50048  22 
val with_vanilla_print_mode : ('a > 'b) > 'a > 'b 
35963  23 
end; 
39318  24 

35963  25 
structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = 
26 
struct 

27 

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

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

29 

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

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

31 

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

32 
fun plural_s n = if n = 1 then "" else "s" 
36062  33 

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

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

35 
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

36 

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

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

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

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

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

41 

48383  42 
val infinite_timeout = seconds 31536000.0 (* one year *) 
43 

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

46 

35963  47 
fun parse_bool_option option name s = 
48 
(case s of 

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

50 
 "false" => SOME false 

51 
 "true" => SOME true 

52 
 "" => SOME true 

53 
 _ => raise Option) 

54 
handle Option.Option => 

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

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

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

58 
end 

59 

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

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

61 
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

62 

35963  63 
fun parse_time_option _ "none" = NONE 
64 
 parse_time_option name s = 

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

65 
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

66 
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

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

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

70 
SOME (seconds (the secs)) 
35963  71 
end 
72 

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

73 
val subgoal_count = Try.subgoal_count 
38044  74 

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

75 
fun reserved_isar_keyword_table () = 
48292  76 
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

77 

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

78 
(* 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

79 
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

80 
not doing the same? *) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
46957
diff
changeset

81 
fun fold_body_thms thm_name f = 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
46957
diff
changeset

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

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

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

85 
let 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48292
diff
changeset

86 
(* The second disjunct caters for the uncommon case where the proved 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48292
diff
changeset

87 
theorem occurs in its own proof (e.g., 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48292
diff
changeset

88 
"Transitive_Closure.trancl_into_trancl"). *) 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48292
diff
changeset

89 
val no_name = (name = "" orelse (n = 1 andalso name = thm_name)) 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48292
diff
changeset

90 
val accum = 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48292
diff
changeset

91 
accum > (if n = 1 andalso not no_name then f name else I) 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48292
diff
changeset

92 
val n = n + (if no_name then 0 else 1) 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48292
diff
changeset

93 
in accum > (if n <= 1 then app n (Future.join body) else I) end) 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
46957
diff
changeset

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

95 

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

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

97 
let 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48292
diff
changeset

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

99 
case all_names of 
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48292
diff
changeset

100 
SOME names => (fn s => Symtab.defined names s ? insert (op =) s) 
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48292
diff
changeset

101 
 NONE => insert (op =) 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
46957
diff
changeset

102 
val names = 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
46957
diff
changeset

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

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

105 

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

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

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

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

109 
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

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

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

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

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

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

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

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

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

118 

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

121 
(print_mode_value ())) f x 

122 

35963  123 
end; 