author  blanchet 
Tue, 21 Dec 2010 01:12:17 +0100  
changeset 41334  3cb52cbf0eed 
parent 41265  a393d6d8e198 
child 41738  eb98c60a6cf0 
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 

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

12 
type 'a uniform_formula = 'a ATP_Problem.uniform_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 = 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

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

16 
OutOfResources  SpassTooOld  VampireTooOld  NoPerl  NoLibwwwPerl  
41222  17 
NoRealZ3  MalformedInput  MalformedOutput  Interrupted  Crashed  
41259
13972ced98d9
more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
blanchet
parents:
41222
diff
changeset

18 
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 

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

26 
type 'a proof = 'a uniform_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 
40669  30 
val string_for_failure : string > 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 : 
41259
13972ced98d9
more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
blanchet
parents:
41222
diff
changeset

35 
bool > bool > int > (string * string) list > (failure * string) list 
13972ced98d9
more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
blanchet
parents:
41222
diff
changeset

36 
> string > string * failure option 
39452  37 
val is_same_step : step_name * step_name > bool 
41146  38 
val atp_proof_from_tstplike_string : bool > 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 = 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

50 
Unprovable  IncompleteUnprovable  CantConnect  TimedOut  OutOfResources  
41222  51 
SpassTooOld  VampireTooOld  NoPerl  NoLibwwwPerl  NoRealZ3  
52 
MalformedInput  MalformedOutput  Interrupted  Crashed  InternalError  

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

53 
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 = 
13972ced98d9
more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
blanchet
parents:
41222
diff
changeset

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

84 

40684
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset

85 
fun missing_message_tail prover = 
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset

86 
" appears to be missing. You will need to install it if you want to run " ^ 
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset

87 
prover ^ "s remotely." 
39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

88 

40669  89 
fun string_for_failure prover Unprovable = 
90 
"The " ^ prover ^ " problem is unprovable." 

91 
 string_for_failure prover IncompleteUnprovable = 

92 
"The " ^ prover ^ " cannot prove the problem." 

93 
 string_for_failure _ CantConnect = "Cannot connect to remote server." 

94 
 string_for_failure _ TimedOut = "Timed out." 

95 
 string_for_failure prover OutOfResources = 

96 
"The " ^ prover ^ " ran out of resources." 

97 
 string_for_failure _ SpassTooOld = 

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

98 
"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

99 
\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

100 
\\"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

101 
\\"spass3.7\" directory's absolute path to " ^ 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

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

103 
(Path.variable "ISABELLE_HOME_USER" :: 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

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

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

107 
"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

108 
\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

109 
\ sledgehammer\")." 
40684
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset

110 
 string_for_failure prover NoPerl = "Perl" ^ missing_message_tail prover 
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset

111 
 string_for_failure prover NoLibwwwPerl = 
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset

112 
"The Perl module \"libwwwperl\"" ^ missing_message_tail prover 
41265
a393d6d8e198
let each prover minimizes its own stuff (rather than taking the first prover of the list to minimize every prover's stuff)
blanchet
parents:
41259
diff
changeset

113 
 string_for_failure _ NoRealZ3 = 
41222  114 
"The environment variable \"Z3_REAL_SOLVER\" must be set to Z3's full path." 
40669  115 
 string_for_failure prover MalformedInput = 
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

116 
"The " ^ prover ^ " problem is malformed. Please report this to the \ 
1393514094d7
fixed more issues with the Vampire output parser, and added support for Vampire's TSTP output (proof tptp)
blanchet
parents:
41201
diff
changeset

117 
\Isabelle developers." 
40669  118 
 string_for_failure prover MalformedOutput = 
119 
"The " ^ prover ^ " output is malformed." 

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

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

121 
"The " ^ prover ^ " was interrupted." 
40669  122 
 string_for_failure prover Crashed = "The " ^ prover ^ " crashed." 
123 
 string_for_failure prover InternalError = 

124 
"An internal " ^ prover ^ " error occurred." 

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

125 
 string_for_failure prover (UnknownError string) = 
41092  126 
(* "An" is correct for "ATP" and "SMT". *) 
41259
13972ced98d9
more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
blanchet
parents:
41222
diff
changeset

127 
"An " ^ 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

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

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

130 

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

131 
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

132 
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

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

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

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

136 

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

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

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

139 

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

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

141 
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

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

143 
 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

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

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

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

147 

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

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

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

150 
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

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

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

153 
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

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

155 

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

156 
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

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

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

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

160 

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

161 
fun extract_tstplike_proof_and_outcome verbose complete res_code proof_delims 
39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

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

163 
case extract_known_failure known_failures output of 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

164 
NONE => (case extract_tstplike_proof proof_delims output of 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

165 
"" => ("", SOME (if res_code = 0 andalso output = "" then 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

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

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

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

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

170 
if res_code = 0 then (tstplike_proof, NONE) 
13972ced98d9
more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
blanchet
parents:
41222
diff
changeset

171 
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

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

173 
("", 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

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

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

176 
failure)) 
39452  177 

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

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

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

181 

39455  182 
type step_name = string * string option 
39452  183 

39455  184 
fun is_same_step p = p > pairself fst > op = 
39452  185 

186 
fun step_name_ord p = 

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

190 
"Graph" functor. *) 

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

192 
(NONE, NONE) => string_ord q 

193 
 (NONE, SOME _) => LESS 

194 
 (SOME _, NONE) => GREATER 

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

196 
end 

197 

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

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

199 
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

200 
Inference of step_name * 'a * step_name list 
39452  201 

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

202 
type 'a proof = 'a uniform_formula step list 
39452  203 

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

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

206 

207 
(**** PARSING OF TSTP FORMAT ****) 

208 

209 
(*Strings enclosed in single quotes, e.g. filenames*) 

210 
val scan_general_id = 

211 
$$ "'"  Scan.repeat (~$$ "'")  $$ "'" >> implode 

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

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

214 

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

216 
fun parse_annotation strict x = 

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

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

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

220 
 $$ "("  parse_annotations strict  $$ ")" 

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

222 
and parse_annotations strict x = 

223 
(Scan.optional (parse_annotation strict 

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

225 
>> flat) x 

226 

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

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

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

230 
and ignore it. *) 

231 
fun parse_vampire_detritus x = 

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

233 

39454  234 
fun parse_term x = 
235 
(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

236 
 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

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

238 
 Scan.optional ($$ "("  parse_vampire_detritus  $$ ")") [] 
39452  239 
>> ATerm) x 
39454  240 
and parse_terms x = (parse_term ::: Scan.repeat ($$ ","  parse_term)) x 
39452  241 

39598  242 
fun parse_atom x = 
243 
(parse_term  Scan.option (Scan.option ($$ "!")  $$ "="  parse_term) 

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

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

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

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

39452  248 

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

250 

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

252 
operator precedence. *) 

39454  253 
fun parse_formula x = 
254 
(($$ "("  parse_formula  $$ ")" 

39452  255 
 ($$ "!" >> K AForall  $$ "?" >> K AExists) 
39454  256 
 $$ "["  parse_terms  $$ "]"  $$ ":"  parse_formula 
39452  257 
>> (fn ((q, ts), phi) => AQuant (q, map fo_term_head ts, phi)) 
39454  258 
 $$ "~"  parse_formula >> mk_anot 
259 
 parse_atom) 

39452  260 
 Scan.option ((Scan.this_string "=>" >> K AImplies 
261 
 Scan.this_string "<=>" >> K AIff 

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

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

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

39454  265 
 parse_formula) 
39452  266 
>> (fn (phi1, NONE) => phi1 
267 
 (phi1, SOME (c, phi2)) => mk_aconn c (phi1, phi2))) x 

268 

269 
val parse_tstp_extra_arguments = 

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

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

272 

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

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

274 

39452  275 
(* Syntax: (fofcnf)\(<num>, <formula_role>, <formula> <extra_arguments>\). 
276 
The <num> could be an identifier, but we assume integers. *) 

39454  277 
val parse_tstp_line = 
278 
((Scan.this_string "fof"  Scan.this_string "cnf")  $$ "(") 

279 
 scan_general_id  $$ ","  Symbol.scan_id  $$ "," 

280 
 parse_formula  parse_tstp_extra_arguments  $$ ")"  $$ "." 

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

282 
let 

283 
val (name, deps) = 

284 
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

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

286 
((num, if s = vampire_unknown_fact then NONE else SOME s), []) 
39455  287 
 _ => ((num, NONE), deps) 
39454  288 
in 
289 
case role of 

290 
"definition" => 

291 
(case phi of 

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

293 
Definition (name, phi1, phi2) 

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

295 
(* Vampire's equality proxy axiom *) 

39455  296 
Inference (name, phi, map (rpair NONE) deps) 
39454  297 
 _ => raise Fail "malformed definition") 
39455  298 
 _ => Inference (name, phi, map (rpair NONE) deps) 
39454  299 
end) 
39452  300 

301 
(**** PARSING OF VAMPIRE OUTPUT ****) 

302 

41146  303 
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

304 
$$ "{"  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

305 
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

306 
$$ "("  parse_vampire_detritus  $$ ")" 
41146  307 

39452  308 
(* Syntax: <num>. <formula> <annotation> *) 
39454  309 
val parse_vampire_line = 
41146  310 
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

311 
 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

312 
 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

313 
 parse_annotation true 
39455  314 
>> (fn ((num, phi), deps) => 
315 
Inference ((num, NONE), phi, map (rpair NONE) deps)) 

39452  316 

317 
(**** PARSING OF SPASS OUTPUT ****) 

318 

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

320 
is not clear anyway. *) 

321 
val parse_dot_name = scan_general_id  $$ "."  scan_general_id 

322 

323 
val parse_spass_annotations = 

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

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

326 

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

328 
pluses. We ignore them. *) 

39602  329 
fun parse_decorated_atom x = 
330 
(parse_atom  Scan.repeat ($$ "*"  $$ "+"  $$ " ")) x 

39452  331 

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

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

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

335 
 mk_horn (neg_lits, pos_lits) = 

336 
mk_aconn AImplies (foldr1 (mk_aconn AAnd) neg_lits, 

337 
foldr1 (mk_aconn AOr) pos_lits) 

338 

39645  339 
fun parse_horn_clause x = 
340 
(Scan.repeat parse_decorated_atom  $$ ""  $$ "" 

341 
 Scan.repeat parse_decorated_atom  $$ ""  $$ ">" 

342 
 Scan.repeat parse_decorated_atom 

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

39452  344 

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

346 
<atoms>  <atoms> > <atoms>. *) 

39645  347 
fun parse_spass_line x = 
348 
(scan_general_id  $$ "["  $$ "0"  $$ ":"  Symbol.scan_id 

349 
 parse_spass_annotations  $$ "]"  parse_horn_clause  $$ "." 

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

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

39452  352 

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

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

358 
o raw_explode o strip_spaces_except_between_ident_chars 
39452  359 

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

361 
fun clean_up_dependencies _ [] = [] 

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

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

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

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

366 
clean_up_dependencies (name :: seen) steps 

367 

41146  368 
fun atp_proof_from_tstplike_string clean = 
39452  369 
suffix "$" (* the $ sign acts as a sentinel (FIXME: needed?) *) 
39454  370 
#> parse_proof 
41146  371 
#> clean ? (sort (step_name_ord o pairself step_name) 
372 
#> clean_up_dependencies []) 

39452  373 

39454  374 
fun map_term_names_in_term f (ATerm (s, ts)) = 
375 
ATerm (f s, map (map_term_names_in_term f) ts) 

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

377 
AQuant (q, xs, map_term_names_in_formula f phi) 

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

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

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

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

382 
Definition (name, map_term_names_in_formula f phi1, 

383 
map_term_names_in_formula f phi2) 

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

385 
Inference (name, map_term_names_in_formula f phi, deps) 

386 
fun map_term_names_in_atp_proof f = map (map_term_names_in_step f) 

387 

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

389 
fun nasty_atp_proof pool = 

390 
if Symtab.is_empty pool then I 

391 
else map_term_names_in_atp_proof (nasty_name pool) 

392 

39452  393 
end; 