author  blanchet 
Wed, 08 Dec 2010 22:17:53 +0100  
changeset 41092  1b796ffa8347 
parent 40684  c7ba327eb58c 
child 41146  be78f4053bce 
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  
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
39645
diff
changeset

17 
MalformedInput  MalformedOutput  Interrupted  Crashed  InternalError  
39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

18 
UnknownError 
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 
40669  29 
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

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

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

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

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

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

35 
> string * failure option 
39452  36 
val is_same_step : step_name * step_name > bool 
39454  37 
val atp_proof_from_tstplike_string : string > string proof 
38 
val map_term_names_in_atp_proof : 

39 
(string > string) > string proof > string proof 

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

39452  41 
end; 
42 

43 
structure ATP_Proof : ATP_PROOF = 

44 
struct 

45 

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

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

47 

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

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

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

50 
SpassTooOld  VampireTooOld  NoPerl  NoLibwwwPerl  MalformedInput  
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
39645
diff
changeset

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

52 

39452  53 
fun strip_spaces_in_list _ [] = [] 
54 
 strip_spaces_in_list _ [c1] = if Char.isSpace c1 then [] else [str c1] 

55 
 strip_spaces_in_list is_evil [c1, c2] = 

56 
strip_spaces_in_list is_evil [c1] @ strip_spaces_in_list is_evil [c2] 

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

58 
if Char.isSpace c1 then 

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

60 
else if Char.isSpace c2 then 

61 
if Char.isSpace c3 then 

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

63 
else 

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

65 
strip_spaces_in_list is_evil (c3 :: cs) 

66 
else 

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

68 
fun strip_spaces is_evil = 

69 
implode o strip_spaces_in_list is_evil o String.explode 

70 

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

72 
val strip_spaces_except_between_ident_chars = strip_spaces is_ident_char 

73 

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

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

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

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

77 

40669  78 
fun string_for_failure prover Unprovable = 
79 
"The " ^ prover ^ " problem is unprovable." 

80 
 string_for_failure prover IncompleteUnprovable = 

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

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

83 
 string_for_failure _ TimedOut = "Timed out." 

84 
 string_for_failure prover OutOfResources = 

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

86 
 string_for_failure _ SpassTooOld = 

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

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

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

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

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

91 
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

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

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

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

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

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

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

99 
 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

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

101 
"The Perl module \"libwwwperl\"" ^ missing_message_tail prover 
40669  102 
 string_for_failure prover MalformedInput = 
103 
"The " ^ prover ^ " problem is malformed. Please report this to the Isabelle \ 

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

104 
\developers." 
40669  105 
 string_for_failure prover MalformedOutput = 
106 
"The " ^ prover ^ " output is malformed." 

107 
 string_for_failure prover Interrupted = "The " ^ prover ^ " was interrupted." 

108 
 string_for_failure prover Crashed = "The " ^ prover ^ " crashed." 

109 
 string_for_failure prover InternalError = 

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

111 
 string_for_failure prover UnknownError = 

41092  112 
(* "An" is correct for "ATP" and "SMT". *) 
113 
"An " ^ prover ^ " error occurred." 

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

114 

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

115 
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

116 
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

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

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

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

120 

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

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

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

123 

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

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

125 
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

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

127 
 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

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

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

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

131 

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

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

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

134 
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

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

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

137 
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

138 
 _ => "" 
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_known_failure known_failures output = 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

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

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

143 
> Option.map fst 
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 
fun extract_tstplike_proof_and_outcome complete res_code proof_delims 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

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

147 
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

148 
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

149 
"" => ("", 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

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

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

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

153 
 tstplike_proof => if res_code = 0 then (tstplike_proof, NONE) 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

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

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

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

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

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

159 
failure)) 
39452  160 

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

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

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

164 

39455  165 
type step_name = string * string option 
39452  166 

39455  167 
fun is_same_step p = p > pairself fst > op = 
39452  168 

169 
fun step_name_ord p = 

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

173 
"Graph" functor. *) 

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

175 
(NONE, NONE) => string_ord q 

176 
 (NONE, SOME _) => LESS 

177 
 (SOME _, NONE) => GREATER 

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

179 
end 

180 

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

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

182 
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

183 
Inference of step_name * 'a * step_name list 
39452  184 

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

185 
type 'a proof = 'a uniform_formula step list 
39452  186 

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

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

189 

190 
(**** PARSING OF TSTP FORMAT ****) 

191 

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

193 
val scan_general_id = 

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

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

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

197 

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

199 
fun parse_annotation strict x = 

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

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

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

203 
 $$ "("  parse_annotations strict  $$ ")" 

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

205 
and parse_annotations strict x = 

206 
(Scan.optional (parse_annotation strict 

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

208 
>> flat) x 

209 

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

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

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

213 
and ignore it. *) 

214 
fun parse_vampire_detritus x = 

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

216 

39454  217 
fun parse_term x = 
218 
(scan_general_id 

219 
 Scan.optional ($$ "("  (parse_vampire_detritus  parse_terms) 

39452  220 
 $$ ")") [] 
221 
 Scan.optional ($$ "("  parse_vampire_detritus  $$ ")") [] 

222 
>> ATerm) x 

39454  223 
and parse_terms x = (parse_term ::: Scan.repeat ($$ ","  parse_term)) x 
39452  224 

39598  225 
fun parse_atom x = 
226 
(parse_term  Scan.option (Scan.option ($$ "!")  $$ "="  parse_term) 

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

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

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

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

39452  231 

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

233 

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

235 
operator precedence. *) 

39454  236 
fun parse_formula x = 
237 
(($$ "("  parse_formula  $$ ")" 

39452  238 
 ($$ "!" >> K AForall  $$ "?" >> K AExists) 
39454  239 
 $$ "["  parse_terms  $$ "]"  $$ ":"  parse_formula 
39452  240 
>> (fn ((q, ts), phi) => AQuant (q, map fo_term_head ts, phi)) 
39454  241 
 $$ "~"  parse_formula >> mk_anot 
242 
 parse_atom) 

39452  243 
 Scan.option ((Scan.this_string "=>" >> K AImplies 
244 
 Scan.this_string "<=>" >> K AIff 

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

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

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

39454  248 
 parse_formula) 
39452  249 
>> (fn (phi1, NONE) => phi1 
250 
 (phi1, SOME (c, phi2)) => mk_aconn c (phi1, phi2))) x 

251 

252 
val parse_tstp_extra_arguments = 

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

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

255 

256 
(* Syntax: (fofcnf)\(<num>, <formula_role>, <formula> <extra_arguments>\). 

257 
The <num> could be an identifier, but we assume integers. *) 

39454  258 
val parse_tstp_line = 
259 
((Scan.this_string "fof"  Scan.this_string "cnf")  $$ "(") 

260 
 scan_general_id  $$ ","  Symbol.scan_id  $$ "," 

261 
 parse_formula  parse_tstp_extra_arguments  $$ ")"  $$ "." 

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

263 
let 

264 
val (name, deps) = 

265 
case deps of 

39455  266 
["file", _, s] => ((num, SOME s), []) 
267 
 _ => ((num, NONE), deps) 

39454  268 
in 
269 
case role of 

270 
"definition" => 

271 
(case phi of 

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

273 
Definition (name, phi1, phi2) 

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

275 
(* Vampire's equality proxy axiom *) 

39455  276 
Inference (name, phi, map (rpair NONE) deps) 
39454  277 
 _ => raise Fail "malformed definition") 
39455  278 
 _ => Inference (name, phi, map (rpair NONE) deps) 
39454  279 
end) 
39452  280 

281 
(**** PARSING OF VAMPIRE OUTPUT ****) 

282 

283 
(* Syntax: <num>. <formula> <annotation> *) 

39454  284 
val parse_vampire_line = 
285 
scan_general_id  $$ "."  parse_formula  parse_annotation true 

39455  286 
>> (fn ((num, phi), deps) => 
287 
Inference ((num, NONE), phi, map (rpair NONE) deps)) 

39452  288 

289 
(**** PARSING OF SPASS OUTPUT ****) 

290 

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

292 
is not clear anyway. *) 

293 
val parse_dot_name = scan_general_id  $$ "."  scan_general_id 

294 

295 
val parse_spass_annotations = 

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

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

298 

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

300 
pluses. We ignore them. *) 

39602  301 
fun parse_decorated_atom x = 
302 
(parse_atom  Scan.repeat ($$ "*"  $$ "+"  $$ " ")) x 

39452  303 

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

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

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

307 
 mk_horn (neg_lits, pos_lits) = 

308 
mk_aconn AImplies (foldr1 (mk_aconn AAnd) neg_lits, 

309 
foldr1 (mk_aconn AOr) pos_lits) 

310 

39645  311 
fun parse_horn_clause x = 
312 
(Scan.repeat parse_decorated_atom  $$ ""  $$ "" 

313 
 Scan.repeat parse_decorated_atom  $$ ""  $$ ">" 

314 
 Scan.repeat parse_decorated_atom 

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

39452  316 

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

318 
<atoms>  <atoms> > <atoms>. *) 

39645  319 
fun parse_spass_line x = 
320 
(scan_general_id  $$ "["  $$ "0"  $$ ":"  Symbol.scan_id 

321 
 parse_spass_annotations  $$ "]"  parse_horn_clause  $$ "." 

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

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

39452  324 

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

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

330 
o raw_explode o strip_spaces_except_between_ident_chars 
39452  331 

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

333 
fun clean_up_dependencies _ [] = [] 

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

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

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

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

338 
clean_up_dependencies (name :: seen) steps 

339 

39454  340 
val atp_proof_from_tstplike_string = 
39452  341 
suffix "$" (* the $ sign acts as a sentinel (FIXME: needed?) *) 
39454  342 
#> parse_proof 
39452  343 
#> sort (step_name_ord o pairself step_name) 
344 
#> clean_up_dependencies [] 

345 

39454  346 
fun map_term_names_in_term f (ATerm (s, ts)) = 
347 
ATerm (f s, map (map_term_names_in_term f) ts) 

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

349 
AQuant (q, xs, map_term_names_in_formula f phi) 

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

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

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

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

354 
Definition (name, map_term_names_in_formula f phi1, 

355 
map_term_names_in_formula f phi2) 

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

357 
Inference (name, map_term_names_in_formula f phi, deps) 

358 
fun map_term_names_in_atp_proof f = map (map_term_names_in_step f) 

359 

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

361 
fun nasty_atp_proof pool = 

362 
if Symtab.is_empty pool then I 

363 
else map_term_names_in_atp_proof (nasty_name pool) 

364 

39452  365 
end; 