author  blanchet 
Sun, 01 May 2011 18:37:24 +0200  
changeset 42536  a513730db7b0 
parent 42531  a462dbaa584f 
child 42543  f9d402d144d4 
permissions  rwrr 
39452  1 
(* Title: HOL/Tools/ATP/atp_proof.ML 
2 
Author: Lawrence C. Paulson, Cambridge University Computer Laboratory 

3 
Author: Claire Quigley, Cambridge University Computer Laboratory 

4 
Author: Jasmin Blanchette, TU Muenchen 

5 

39454  6 
Abstract representation of ATP proofs and TSTP/Vampire/SPASS syntax. 
39452  7 
*) 
8 

9 
signature ATP_PROOF = 

10 
sig 

11 
type 'a fo_term = 'a ATP_Problem.fo_term 

42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42526
diff
changeset

12 
type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula 
39452  13 

39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

14 
datatype failure = 
42449
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42060
diff
changeset

15 
Unprovable  IncompleteUnprovable  ProofMissing  UnsoundProof  
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42060
diff
changeset

16 
CantConnect  TimedOut  OutOfResources  SpassTooOld  VampireTooOld  
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42060
diff
changeset

17 
NoPerl  NoLibwwwPerl  NoRealZ3  MalformedInput  MalformedOutput  
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42060
diff
changeset

18 
Interrupted  Crashed  InternalError  UnknownError of string 
39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

19 

39455  20 
type step_name = string * string option 
39452  21 

39453
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

22 
datatype 'a step = 
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

23 
Definition of step_name * 'a * 'a  
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

24 
Inference of step_name * 'a * step_name list 
39452  25 

42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42526
diff
changeset

26 
type 'a proof = ('a, 'a, 'a fo_term) formula step list 
39452  27 

39457  28 
val strip_spaces : (char > bool) > string > string 
41259
13972ced98d9
more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
blanchet
parents:
41222
diff
changeset

29 
val short_output : bool > string > string 
41744  30 
val string_for_failure : failure > string 
39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

31 
val extract_important_message : string > string 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

32 
val extract_known_failure : 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

33 
(failure * string) list > string > failure option 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

34 
val extract_tstplike_proof_and_outcome : 
42060
889d767ce5f4
make Minimizer honor "verbose" and "debug" options better
blanchet
parents:
41944
diff
changeset

35 
bool > bool > bool > int > (string * string) list 
889d767ce5f4
make Minimizer honor "verbose" and "debug" options better
blanchet
parents:
41944
diff
changeset

36 
> (failure * string) list > string > string * failure option 
39452  37 
val is_same_step : step_name * step_name > bool 
42449
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42060
diff
changeset

38 
val atp_proof_from_tstplike_proof : string > string proof 
39454  39 
val map_term_names_in_atp_proof : 
40 
(string > string) > string proof > string proof 

41 
val nasty_atp_proof : string Symtab.table > string proof > string proof 

39452  42 
end; 
43 

44 
structure ATP_Proof : ATP_PROOF = 

45 
struct 

46 

39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

47 
open ATP_Problem 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

48 

2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

49 
datatype failure = 
42449
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42060
diff
changeset

50 
Unprovable  IncompleteUnprovable  ProofMissing  UnsoundProof  
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42060
diff
changeset

51 
CantConnect  TimedOut  OutOfResources  SpassTooOld  VampireTooOld  
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42060
diff
changeset

52 
NoPerl  NoLibwwwPerl  NoRealZ3  MalformedInput  MalformedOutput  
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42060
diff
changeset

53 
Interrupted  Crashed  InternalError  UnknownError of string 
39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

54 

39452  55 
fun strip_spaces_in_list _ [] = [] 
56 
 strip_spaces_in_list _ [c1] = if Char.isSpace c1 then [] else [str c1] 

57 
 strip_spaces_in_list is_evil [c1, c2] = 

58 
strip_spaces_in_list is_evil [c1] @ strip_spaces_in_list is_evil [c2] 

59 
 strip_spaces_in_list is_evil (c1 :: c2 :: c3 :: cs) = 

60 
if Char.isSpace c1 then 

61 
strip_spaces_in_list is_evil (c2 :: c3 :: cs) 

62 
else if Char.isSpace c2 then 

63 
if Char.isSpace c3 then 

64 
strip_spaces_in_list is_evil (c1 :: c3 :: cs) 

65 
else 

66 
str c1 :: (if forall is_evil [c1, c3] then [" "] else []) @ 

67 
strip_spaces_in_list is_evil (c3 :: cs) 

68 
else 

69 
str c1 :: strip_spaces_in_list is_evil (c2 :: c3 :: cs) 

70 
fun strip_spaces is_evil = 

71 
implode o strip_spaces_in_list is_evil o String.explode 

72 

73 
fun is_ident_char c = Char.isAlphaNum c orelse c = #"_" 

74 
val strip_spaces_except_between_ident_chars = strip_spaces is_ident_char 

75 

41259
13972ced98d9
more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
blanchet
parents:
41222
diff
changeset

76 
fun elide_string threshold s = 
13972ced98d9
more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
blanchet
parents:
41222
diff
changeset

77 
if size s > threshold then 
13972ced98d9
more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
blanchet
parents:
41222
diff
changeset

78 
String.extract (s, 0, SOME (threshold div 2  5)) ^ " ...... " ^ 
13972ced98d9
more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
blanchet
parents:
41222
diff
changeset

79 
String.extract (s, size s  (threshold + 1) div 2 + 6, NONE) 
13972ced98d9
more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
blanchet
parents:
41222
diff
changeset

80 
else 
13972ced98d9
more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
blanchet
parents:
41222
diff
changeset

81 
s 
13972ced98d9
more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
blanchet
parents:
41222
diff
changeset

82 
fun short_output verbose output = 
42060
889d767ce5f4
make Minimizer honor "verbose" and "debug" options better
blanchet
parents:
41944
diff
changeset

83 
if verbose then 
889d767ce5f4
make Minimizer honor "verbose" and "debug" options better
blanchet
parents:
41944
diff
changeset

84 
if output = "" then "No details available" else elide_string 1000 output 
889d767ce5f4
make Minimizer honor "verbose" and "debug" options better
blanchet
parents:
41944
diff
changeset

85 
else 
889d767ce5f4
make Minimizer honor "verbose" and "debug" options better
blanchet
parents:
41944
diff
changeset

86 
"" 
41259
13972ced98d9
more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
blanchet
parents:
41222
diff
changeset

87 

41744  88 
val missing_message_tail = 
89 
" appears to be missing. You will need to install it if you want to invoke \ 

90 
\remote provers." 

39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

91 

41744  92 
fun string_for_failure Unprovable = 
93 
"The problem is unprovable." 

94 
 string_for_failure IncompleteUnprovable = 

95 
"The prover gave up." 

96 
 string_for_failure ProofMissing = 

97 
"The prover claims the conjecture is a theorem but did not provide a proof." 

42449
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42060
diff
changeset

98 
 string_for_failure UnsoundProof = 
42450
2765d4fb2b9c
automatically retry with fulltypes upon unsound proof
blanchet
parents:
42449
diff
changeset

99 
"The prover found a typeunsound proof. (Or, very unlikely, your axioms \ 
42449
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42060
diff
changeset

100 
\are inconsistent.)" 
41744  101 
 string_for_failure CantConnect = "Cannot connect to remote server." 
102 
 string_for_failure TimedOut = "Timed out." 

103 
 string_for_failure OutOfResources = "The prover ran out of resources." 

104 
 string_for_failure SpassTooOld = 

39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

105 
"Isabelle requires a more recent version of SPASS with support for the \ 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

106 
\TPTP syntax. To install it, download and extract the package \ 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

107 
\\"http://isabelle.in.tum.de/dist/contrib/spass3.7.tar.gz\" and add the \ 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

108 
\\"spass3.7\" directory's absolute path to " ^ 
41944
b97091ae583a
Path.print is the official way to show filesystem paths to users  note that Path.implode often indicates violation of the abstract datatype;
wenzelm
parents:
41744
diff
changeset

109 
Path.print (Path.expand (Path.appends 
39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

110 
(Path.variable "ISABELLE_HOME_USER" :: 
41944
b97091ae583a
Path.print is the official way to show filesystem paths to users  note that Path.implode often indicates violation of the abstract datatype;
wenzelm
parents:
41744
diff
changeset

111 
map Path.basic ["etc", "components"]))) ^ 
39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

112 
" on a line of its own." 
41744  113 
 string_for_failure VampireTooOld = 
39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

114 
"Isabelle requires a more recent version of Vampire. To install it, follow \ 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

115 
\the instructions from the Sledgehammer manual (\"isabelle doc\ 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

116 
\ sledgehammer\")." 
41744  117 
 string_for_failure NoPerl = "Perl" ^ missing_message_tail 
118 
 string_for_failure NoLibwwwPerl = 

119 
"The Perl module \"libwwwperl\"" ^ missing_message_tail 

120 
 string_for_failure NoRealZ3 = 

41222  121 
"The environment variable \"Z3_REAL_SOLVER\" must be set to Z3's full path." 
41744  122 
 string_for_failure MalformedInput = 
123 
"The generated problem is malformed. Please report this to the Isabelle \ 

124 
\developers." 

125 
 string_for_failure MalformedOutput = "The prover output is malformed." 

126 
 string_for_failure Crashed = "The prover crashed." 

127 
 string_for_failure InternalError = "An internal prover error occurred." 

128 
 string_for_failure (UnknownError string) = 

129 
"A prover error occurred" ^ 

41334
3cb52cbf0eed
enable E weight generation with unofficial latest version of E (tentatively called E 1.2B)  backed by Judgment Day
blanchet
parents:
41265
diff
changeset

130 
(if string = "" then ". (Pass the \"verbose\" option for details.)" 
3cb52cbf0eed
enable E weight generation with unofficial latest version of E (tentatively called E 1.2B)  backed by Judgment Day
blanchet
parents:
41265
diff
changeset

131 
else ":\n" ^ string) 
39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

132 

2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

133 
fun extract_delimited (begin_delim, end_delim) output = 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

134 
output > first_field begin_delim > the > snd 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

135 
> first_field end_delim > the > fst 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

136 
> first_field "\n" > the > snd 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

137 
handle Option.Option => "" 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

138 

2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

139 
val tstp_important_message_delims = 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

140 
("% SZS start RequiredInformation", "% SZS end RequiredInformation") 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

141 

2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

142 
fun extract_important_message output = 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

143 
case extract_delimited tstp_important_message_delims output of 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

144 
"" => "" 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

145 
 s => s > space_explode "\n" > filter_out (curry (op =) "") 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

146 
> map (perhaps (try (unprefix "%"))) 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

147 
> map (perhaps (try (unprefix " "))) 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

148 
> space_implode "\n " > quote 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

149 

2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

150 
(* Splits by the first possible of a list of delimiters. *) 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

151 
fun extract_tstplike_proof delims output = 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

152 
case pairself (find_first (fn s => String.isSubstring s output)) 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

153 
(ListPair.unzip delims) of 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

154 
(SOME begin_delim, SOME end_delim) => 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

155 
extract_delimited (begin_delim, end_delim) output 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

156 
 _ => "" 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

157 

2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

158 
fun extract_known_failure known_failures output = 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

159 
known_failures 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

160 
> find_first (fn (_, pattern) => String.isSubstring pattern output) 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

161 
> Option.map fst 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

162 

42060
889d767ce5f4
make Minimizer honor "verbose" and "debug" options better
blanchet
parents:
41944
diff
changeset

163 
fun extract_tstplike_proof_and_outcome debug verbose complete res_code 
889d767ce5f4
make Minimizer honor "verbose" and "debug" options better
blanchet
parents:
41944
diff
changeset

164 
proof_delims known_failures output = 
39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

165 
case extract_known_failure known_failures output of 
42060
889d767ce5f4
make Minimizer honor "verbose" and "debug" options better
blanchet
parents:
41944
diff
changeset

166 
NONE => 
889d767ce5f4
make Minimizer honor "verbose" and "debug" options better
blanchet
parents:
41944
diff
changeset

167 
(case extract_tstplike_proof proof_delims output of 
889d767ce5f4
make Minimizer honor "verbose" and "debug" options better
blanchet
parents:
41944
diff
changeset

168 
"" => 
889d767ce5f4
make Minimizer honor "verbose" and "debug" options better
blanchet
parents:
41944
diff
changeset

169 
("", SOME (if res_code = 0 andalso (not debug orelse output = "") then 
889d767ce5f4
make Minimizer honor "verbose" and "debug" options better
blanchet
parents:
41944
diff
changeset

170 
ProofMissing 
889d767ce5f4
make Minimizer honor "verbose" and "debug" options better
blanchet
parents:
41944
diff
changeset

171 
else 
889d767ce5f4
make Minimizer honor "verbose" and "debug" options better
blanchet
parents:
41944
diff
changeset

172 
UnknownError (short_output verbose output))) 
889d767ce5f4
make Minimizer honor "verbose" and "debug" options better
blanchet
parents:
41944
diff
changeset

173 
 tstplike_proof => 
889d767ce5f4
make Minimizer honor "verbose" and "debug" options better
blanchet
parents:
41944
diff
changeset

174 
if res_code = 0 then (tstplike_proof, NONE) 
889d767ce5f4
make Minimizer honor "verbose" and "debug" options better
blanchet
parents:
41944
diff
changeset

175 
else ("", SOME (UnknownError (short_output verbose output)))) 
39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

176 
 SOME failure => 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

177 
("", SOME (if failure = IncompleteUnprovable andalso complete then 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

178 
Unprovable 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

179 
else 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

180 
failure)) 
39452  181 

182 
fun mk_anot (AConn (ANot, [phi])) = phi 

183 
 mk_anot phi = AConn (ANot, [phi]) 

184 
fun mk_aconn c (phi1, phi2) = AConn (c, [phi1, phi2]) 

185 

39455  186 
type step_name = string * string option 
39452  187 

39455  188 
fun is_same_step p = p > pairself fst > op = 
39452  189 

190 
fun step_name_ord p = 

39455  191 
let val q = pairself fst p in 
39452  192 
(* The "unprefix" part is to cope with remote Vampire's output. The proper 
193 
solution would be to perform a topological sort, e.g. using the nice 

194 
"Graph" functor. *) 

195 
case pairself (Int.fromString o perhaps (try (unprefix "f"))) q of 

196 
(NONE, NONE) => string_ord q 

197 
 (NONE, SOME _) => LESS 

198 
 (SOME _, NONE) => GREATER 

199 
 (SOME i, SOME j) => int_ord (i, j) 

200 
end 

201 

39453
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

202 
datatype 'a step = 
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

203 
Definition of step_name * 'a * 'a  
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

204 
Inference of step_name * 'a * step_name list 
39452  205 

42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42526
diff
changeset

206 
type 'a proof = ('a, 'a, 'a fo_term) formula step list 
39452  207 

208 
fun step_name (Definition (name, _, _)) = name 

209 
 step_name (Inference (name, _, _)) = name 

210 

211 
(**** PARSING OF TSTP FORMAT ****) 

212 

42536  213 
(* Strings enclosed in single quotes (e.g., file names) *) 
39452  214 
val scan_general_id = 
215 
$$ "'"  Scan.repeat (~$$ "'")  $$ "'" >> implode 

216 
 Scan.repeat ($$ "$")  Scan.many1 Symbol.is_letdig 

217 
>> (fn (ss1, ss2) => implode ss1 ^ implode ss2) 

218 

219 
(* Generalized firstorder terms, which include file names, numbers, etc. *) 

220 
fun parse_annotation strict x = 

221 
((scan_general_id ::: Scan.repeat ($$ " "  scan_general_id) 

222 
>> (strict ? filter (is_some o Int.fromString))) 

223 
 Scan.optional (parse_annotation strict) [] >> op @ 

224 
 $$ "("  parse_annotations strict  $$ ")" 

225 
 $$ "["  parse_annotations strict  $$ "]") x 

226 
and parse_annotations strict x = 

227 
(Scan.optional (parse_annotation strict 

228 
::: Scan.repeat ($$ ","  parse_annotation strict)) [] 

229 
>> flat) x 

230 

231 
(* Vampire proof lines sometimes contain needless information such as "(0:3)", 

232 
which can be hard to disambiguate from function application in an LL(1) 

233 
parser. As a workaround, we extend the TPTP term syntax with such detritus 

234 
and ignore it. *) 

235 
fun parse_vampire_detritus x = 

236 
(scan_general_id  $$ ":"  scan_general_id >> K []) x 

237 

39454  238 
fun parse_term x = 
239 
(scan_general_id 

41203
1393514094d7
fixed more issues with the Vampire output parser, and added support for Vampire's TSTP output (proof tptp)
blanchet
parents:
41201
diff
changeset

240 
 Scan.optional ($$ "("  (parse_vampire_detritus  parse_terms) 
1393514094d7
fixed more issues with the Vampire output parser, and added support for Vampire's TSTP output (proof tptp)
blanchet
parents:
41201
diff
changeset

241 
 $$ ")") [] 
1393514094d7
fixed more issues with the Vampire output parser, and added support for Vampire's TSTP output (proof tptp)
blanchet
parents:
41201
diff
changeset

242 
 Scan.optional ($$ "("  parse_vampire_detritus  $$ ")") [] 
39452  243 
>> ATerm) x 
39454  244 
and parse_terms x = (parse_term ::: Scan.repeat ($$ ","  parse_term)) x 
39452  245 

39598  246 
fun parse_atom x = 
247 
(parse_term  Scan.option (Scan.option ($$ "!")  $$ "="  parse_term) 

248 
>> (fn (u1, NONE) => AAtom u1 

249 
 (u1, SOME (NONE, u2)) => AAtom (ATerm ("c_equal", [u1, u2])) 

250 
 (u1, SOME (SOME _, u2)) => 

251 
mk_anot (AAtom (ATerm ("c_equal", [u1, u2]))))) x 

39452  252 

253 
fun fo_term_head (ATerm (s, _)) = s 

254 

255 
(* TPTP formulas are fully parenthesized, so we don't need to worry about 

256 
operator precedence. *) 

39454  257 
fun parse_formula x = 
258 
(($$ "("  parse_formula  $$ ")" 

39452  259 
 ($$ "!" >> K AForall  $$ "?" >> K AExists) 
39454  260 
 $$ "["  parse_terms  $$ "]"  $$ ":"  parse_formula 
42526  261 
>> (fn ((q, ts), phi) => 
262 
(* FIXME: TFF *) 

263 
AQuant (q, map (rpair NONE o fo_term_head) ts, phi)) 

39454  264 
 $$ "~"  parse_formula >> mk_anot 
265 
 parse_atom) 

39452  266 
 Scan.option ((Scan.this_string "=>" >> K AImplies 
267 
 Scan.this_string "<=>" >> K AIff 

268 
 Scan.this_string "<~>" >> K ANotIff 

269 
 Scan.this_string "<=" >> K AIf 

270 
 $$ "" >> K AOr  $$ "&" >> K AAnd) 

39454  271 
 parse_formula) 
39452  272 
>> (fn (phi1, NONE) => phi1 
273 
 (phi1, SOME (c, phi2)) => mk_aconn c (phi1, phi2))) x 

274 

275 
val parse_tstp_extra_arguments = 

276 
Scan.optional ($$ ","  parse_annotation false 

277 
 Scan.option ($$ ","  parse_annotations false)) [] 

278 

41203
1393514094d7
fixed more issues with the Vampire output parser, and added support for Vampire's TSTP output (proof tptp)
blanchet
parents:
41201
diff
changeset

279 
val vampire_unknown_fact = "unknown" 
42536  280 
val tofof_fact_prefix = "fof_" 
41203
1393514094d7
fixed more issues with the Vampire output parser, and added support for Vampire's TSTP output (proof tptp)
blanchet
parents:
41201
diff
changeset

281 

42525
7a506b0b644f
distinguish FOF and TFF (typed firstorder) in ATP abstract syntax tree
blanchet
parents:
42450
diff
changeset

282 
(* Syntax: (cnffoftff)\(<num>, <formula_role>, <formula> <extra_arguments>\). 
39452  283 
The <num> could be an identifier, but we assume integers. *) 
39454  284 
val parse_tstp_line = 
42525
7a506b0b644f
distinguish FOF and TFF (typed firstorder) in ATP abstract syntax tree
blanchet
parents:
42450
diff
changeset

285 
((Scan.this_string "cnf"  Scan.this_string "fof"  Scan.this_string "tff") 
7a506b0b644f
distinguish FOF and TFF (typed firstorder) in ATP abstract syntax tree
blanchet
parents:
42450
diff
changeset

286 
 $$ "(") 
39454  287 
 scan_general_id  $$ ","  Symbol.scan_id  $$ "," 
288 
 parse_formula  parse_tstp_extra_arguments  $$ ")"  $$ "." 

289 
>> (fn (((num, role), phi), deps) => 

290 
let 

291 
val (name, deps) = 

292 
case deps of 

41203
1393514094d7
fixed more issues with the Vampire output parser, and added support for Vampire's TSTP output (proof tptp)
blanchet
parents:
41201
diff
changeset

293 
["file", _, s] => 
42536  294 
((num, 
295 
if s = vampire_unknown_fact then NONE 

296 
else SOME (s > perhaps (try (unprefix tofof_fact_prefix)))), 

297 
[]) 

39455  298 
 _ => ((num, NONE), deps) 
39454  299 
in 
300 
case role of 

301 
"definition" => 

302 
(case phi of 

303 
AConn (AIff, [phi1 as AAtom _, phi2]) => 

304 
Definition (name, phi1, phi2) 

305 
 AAtom (ATerm ("c_equal", _)) => 

306 
(* Vampire's equality proxy axiom *) 

39455  307 
Inference (name, phi, map (rpair NONE) deps) 
39454  308 
 _ => raise Fail "malformed definition") 
39455  309 
 _ => Inference (name, phi, map (rpair NONE) deps) 
39454  310 
end) 
39452  311 

312 
(**** PARSING OF VAMPIRE OUTPUT ****) 

313 

41146  314 
val parse_vampire_braced_stuff = 
41201
208bd47b6f29
generalize the Vampire parser some more to cope with things like "{2, 3\}" seen in some proofs
blanchet
parents:
41146
diff
changeset

315 
$$ "{"  Scan.repeat (scan_general_id  Scan.option ($$ ","))  $$ "}" 
41203
1393514094d7
fixed more issues with the Vampire output parser, and added support for Vampire's TSTP output (proof tptp)
blanchet
parents:
41201
diff
changeset

316 
val parse_vampire_parenthesized_detritus = 
1393514094d7
fixed more issues with the Vampire output parser, and added support for Vampire's TSTP output (proof tptp)
blanchet
parents:
41201
diff
changeset

317 
$$ "("  parse_vampire_detritus  $$ ")" 
41146  318 

39452  319 
(* Syntax: <num>. <formula> <annotation> *) 
39454  320 
val parse_vampire_line = 
41146  321 
scan_general_id  $$ "."  parse_formula 
41203
1393514094d7
fixed more issues with the Vampire output parser, and added support for Vampire's TSTP output (proof tptp)
blanchet
parents:
41201
diff
changeset

322 
 Scan.option parse_vampire_braced_stuff 
1393514094d7
fixed more issues with the Vampire output parser, and added support for Vampire's TSTP output (proof tptp)
blanchet
parents:
41201
diff
changeset

323 
 Scan.option parse_vampire_parenthesized_detritus 
1393514094d7
fixed more issues with the Vampire output parser, and added support for Vampire's TSTP output (proof tptp)
blanchet
parents:
41201
diff
changeset

324 
 parse_annotation true 
39455  325 
>> (fn ((num, phi), deps) => 
326 
Inference ((num, NONE), phi, map (rpair NONE) deps)) 

39452  327 

328 
(**** PARSING OF SPASS OUTPUT ****) 

329 

330 
(* SPASS returns clause references of the form "x.y". We ignore "y", whose role 

331 
is not clear anyway. *) 

332 
val parse_dot_name = scan_general_id  $$ "."  scan_general_id 

333 

334 
val parse_spass_annotations = 

335 
Scan.optional ($$ ":"  Scan.repeat (parse_dot_name 

336 
 Scan.option ($$ ","))) [] 

337 

338 
(* It is not clear why some literals are followed by sequences of stars and/or 

339 
pluses. We ignore them. *) 

39602  340 
fun parse_decorated_atom x = 
341 
(parse_atom  Scan.repeat ($$ "*"  $$ "+"  $$ " ")) x 

39452  342 

343 
fun mk_horn ([], []) = AAtom (ATerm ("c_False", [])) 

344 
 mk_horn ([], pos_lits) = foldr1 (mk_aconn AOr) pos_lits 

345 
 mk_horn (neg_lits, []) = mk_anot (foldr1 (mk_aconn AAnd) neg_lits) 

346 
 mk_horn (neg_lits, pos_lits) = 

347 
mk_aconn AImplies (foldr1 (mk_aconn AAnd) neg_lits, 

348 
foldr1 (mk_aconn AOr) pos_lits) 

349 

39645  350 
fun parse_horn_clause x = 
351 
(Scan.repeat parse_decorated_atom  $$ ""  $$ "" 

352 
 Scan.repeat parse_decorated_atom  $$ ""  $$ ">" 

353 
 Scan.repeat parse_decorated_atom 

354 
>> (mk_horn o apfst (op @))) x 

39452  355 

356 
(* Syntax: <num>[0:<inference><annotations>] 

357 
<atoms>  <atoms> > <atoms>. *) 

39645  358 
fun parse_spass_line x = 
359 
(scan_general_id  $$ "["  $$ "0"  $$ ":"  Symbol.scan_id 

360 
 parse_spass_annotations  $$ "]"  parse_horn_clause  $$ "." 

361 
>> (fn ((num, deps), u) => 

362 
Inference ((num, NONE), u, map (rpair NONE) deps))) x 

39452  363 

39645  364 
fun parse_line x = (parse_tstp_line  parse_vampire_line  parse_spass_line) x 
39454  365 
val parse_proof = 
39452  366 
fst o Scan.finite Symbol.stopper 
367 
(Scan.error (!! (fn _ => raise Fail "unrecognized ATP output") 

39454  368 
(Scan.repeat1 parse_line))) 
40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
40553
diff
changeset

369 
o raw_explode o strip_spaces_except_between_ident_chars 
39452  370 

371 
fun clean_up_dependency seen dep = find_first (curry is_same_step dep) seen 

372 
fun clean_up_dependencies _ [] = [] 

373 
 clean_up_dependencies seen ((step as Definition (name, _, _)) :: steps) = 

374 
step :: clean_up_dependencies (name :: seen) steps 

375 
 clean_up_dependencies seen (Inference (name, u, deps) :: steps) = 

376 
Inference (name, u, map_filter (clean_up_dependency seen) deps) :: 

377 
clean_up_dependencies (name :: seen) steps 

378 

42449
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42060
diff
changeset

379 
fun atp_proof_from_tstplike_proof "" = [] 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42060
diff
changeset

380 
 atp_proof_from_tstplike_proof s = 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42060
diff
changeset

381 
s ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *) 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42060
diff
changeset

382 
> parse_proof 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42060
diff
changeset

383 
> sort (step_name_ord o pairself step_name) 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42060
diff
changeset

384 
> clean_up_dependencies [] 
39452  385 

39454  386 
fun map_term_names_in_term f (ATerm (s, ts)) = 
387 
ATerm (f s, map (map_term_names_in_term f) ts) 

388 
fun map_term_names_in_formula f (AQuant (q, xs, phi)) = 

389 
AQuant (q, xs, map_term_names_in_formula f phi) 

390 
 map_term_names_in_formula f (AConn (c, phis)) = 

391 
AConn (c, map (map_term_names_in_formula f) phis) 

392 
 map_term_names_in_formula f (AAtom t) = AAtom (map_term_names_in_term f t) 

393 
fun map_term_names_in_step f (Definition (name, phi1, phi2)) = 

394 
Definition (name, map_term_names_in_formula f phi1, 

395 
map_term_names_in_formula f phi2) 

396 
 map_term_names_in_step f (Inference (name, phi, deps)) = 

397 
Inference (name, map_term_names_in_formula f phi, deps) 

398 
fun map_term_names_in_atp_proof f = map (map_term_names_in_step f) 

399 

400 
fun nasty_name pool s = s > Symtab.lookup pool > the_default s 

401 
fun nasty_atp_proof pool = 

402 
if Symtab.is_empty pool then I 

403 
else map_term_names_in_atp_proof (nasty_name pool) 

404 

39452  405 
end; 