author  blanchet 
Mon, 06 Jun 2011 20:36:34 +0200  
changeset 43163  31babd4b1552 
parent 43085  0a2f5b86bdd7 
child 43246  01b6391a763f 
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 

42876
e336ef6313aa
more informative message when Sledgehammer finds an unsound proof
blanchet
parents:
42848
diff
changeset

6 
Abstract representation of ATP proofs and TSTP/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 
42943  13 
type 'a problem = 'a ATP_Problem.problem 
39452  14 

42965
1403595ec38c
slightly gracefuller handling of LEOII and Satallax output
blanchet
parents:
42962
diff
changeset

15 
exception UNRECOGNIZED_ATP_PROOF of unit 
1403595ec38c
slightly gracefuller handling of LEOII and Satallax output
blanchet
parents:
42962
diff
changeset

16 

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

17 
datatype failure = 
42587
4fbb1de05169
fixed SPASS fact offset calculation and report unexpected unsound proofs with socalled sound encodings
blanchet
parents:
42550
diff
changeset

18 
Unprovable  
43050
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43029
diff
changeset

19 
GaveUp  
42587
4fbb1de05169
fixed SPASS fact offset calculation and report unexpected unsound proofs with socalled sound encodings
blanchet
parents:
42550
diff
changeset

20 
ProofMissing  
42882
391e41ac038b
make sure the Vampire incomplete proof detection code kicks in
blanchet
parents:
42876
diff
changeset

21 
ProofIncomplete  
42876
e336ef6313aa
more informative message when Sledgehammer finds an unsound proof
blanchet
parents:
42848
diff
changeset

22 
UnsoundProof of bool * string list  
42587
4fbb1de05169
fixed SPASS fact offset calculation and report unexpected unsound proofs with socalled sound encodings
blanchet
parents:
42550
diff
changeset

23 
CantConnect  
4fbb1de05169
fixed SPASS fact offset calculation and report unexpected unsound proofs with socalled sound encodings
blanchet
parents:
42550
diff
changeset

24 
TimedOut  
42953
26111aafab12
detect inappropriate problems and crashes better in Waldmeister
blanchet
parents:
42943
diff
changeset

25 
Inappropriate  
42587
4fbb1de05169
fixed SPASS fact offset calculation and report unexpected unsound proofs with socalled sound encodings
blanchet
parents:
42550
diff
changeset

26 
OutOfResources  
4fbb1de05169
fixed SPASS fact offset calculation and report unexpected unsound proofs with socalled sound encodings
blanchet
parents:
42550
diff
changeset

27 
SpassTooOld  
4fbb1de05169
fixed SPASS fact offset calculation and report unexpected unsound proofs with socalled sound encodings
blanchet
parents:
42550
diff
changeset

28 
VampireTooOld  
4fbb1de05169
fixed SPASS fact offset calculation and report unexpected unsound proofs with socalled sound encodings
blanchet
parents:
42550
diff
changeset

29 
NoPerl  
4fbb1de05169
fixed SPASS fact offset calculation and report unexpected unsound proofs with socalled sound encodings
blanchet
parents:
42550
diff
changeset

30 
NoLibwwwPerl  
4fbb1de05169
fixed SPASS fact offset calculation and report unexpected unsound proofs with socalled sound encodings
blanchet
parents:
42550
diff
changeset

31 
MalformedInput  
4fbb1de05169
fixed SPASS fact offset calculation and report unexpected unsound proofs with socalled sound encodings
blanchet
parents:
42550
diff
changeset

32 
MalformedOutput  
4fbb1de05169
fixed SPASS fact offset calculation and report unexpected unsound proofs with socalled sound encodings
blanchet
parents:
42550
diff
changeset

33 
Interrupted  
4fbb1de05169
fixed SPASS fact offset calculation and report unexpected unsound proofs with socalled sound encodings
blanchet
parents:
42550
diff
changeset

34 
Crashed  
4fbb1de05169
fixed SPASS fact offset calculation and report unexpected unsound proofs with socalled sound encodings
blanchet
parents:
42550
diff
changeset

35 
InternalError  
4fbb1de05169
fixed SPASS fact offset calculation and report unexpected unsound proofs with socalled sound encodings
blanchet
parents:
42550
diff
changeset

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

37 

39455  38 
type step_name = string * string option 
39452  39 

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

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

41 
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

42 
Inference of step_name * 'a * step_name list 
39452  43 

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

44 
type 'a proof = ('a, 'a, 'a fo_term) formula step list 
39452  45 

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

46 
val short_output : bool > string > string 
41744  47 
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

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

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

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

51 
val extract_tstplike_proof_and_outcome : 
42848  52 
bool > bool > int > (string * string) list > (failure * string) list 
53 
> string > string * failure option 

42968
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

54 
val is_same_atp_step : step_name > step_name > bool 
42961  55 
val scan_general_id : string list > string * string list 
56 
val parse_formula : 

57 
string list > (string, 'a, string fo_term) formula * string list 

42943  58 
val atp_proof_from_tstplike_proof : string problem > string > string proof 
42968
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

59 
val clean_up_atp_proof_dependencies : string proof > string proof 
39454  60 
val map_term_names_in_atp_proof : 
61 
(string > string) > string proof > string proof 

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

39452  63 
end; 
64 

65 
structure ATP_Proof : ATP_PROOF = 

66 
struct 

67 

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

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

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

70 

42965
1403595ec38c
slightly gracefuller handling of LEOII and Satallax output
blanchet
parents:
42962
diff
changeset

71 
exception UNRECOGNIZED_ATP_PROOF of unit 
1403595ec38c
slightly gracefuller handling of LEOII and Satallax output
blanchet
parents:
42962
diff
changeset

72 

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

73 
datatype failure = 
42587
4fbb1de05169
fixed SPASS fact offset calculation and report unexpected unsound proofs with socalled sound encodings
blanchet
parents:
42550
diff
changeset

74 
Unprovable  
43050
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43029
diff
changeset

75 
GaveUp  
42587
4fbb1de05169
fixed SPASS fact offset calculation and report unexpected unsound proofs with socalled sound encodings
blanchet
parents:
42550
diff
changeset

76 
ProofMissing  
42882
391e41ac038b
make sure the Vampire incomplete proof detection code kicks in
blanchet
parents:
42876
diff
changeset

77 
ProofIncomplete  
42876
e336ef6313aa
more informative message when Sledgehammer finds an unsound proof
blanchet
parents:
42848
diff
changeset

78 
UnsoundProof of bool * string list  
42587
4fbb1de05169
fixed SPASS fact offset calculation and report unexpected unsound proofs with socalled sound encodings
blanchet
parents:
42550
diff
changeset

79 
CantConnect  
4fbb1de05169
fixed SPASS fact offset calculation and report unexpected unsound proofs with socalled sound encodings
blanchet
parents:
42550
diff
changeset

80 
TimedOut  
42953
26111aafab12
detect inappropriate problems and crashes better in Waldmeister
blanchet
parents:
42943
diff
changeset

81 
Inappropriate  
42587
4fbb1de05169
fixed SPASS fact offset calculation and report unexpected unsound proofs with socalled sound encodings
blanchet
parents:
42550
diff
changeset

82 
OutOfResources  
4fbb1de05169
fixed SPASS fact offset calculation and report unexpected unsound proofs with socalled sound encodings
blanchet
parents:
42550
diff
changeset

83 
SpassTooOld  
4fbb1de05169
fixed SPASS fact offset calculation and report unexpected unsound proofs with socalled sound encodings
blanchet
parents:
42550
diff
changeset

84 
VampireTooOld  
4fbb1de05169
fixed SPASS fact offset calculation and report unexpected unsound proofs with socalled sound encodings
blanchet
parents:
42550
diff
changeset

85 
NoPerl  
4fbb1de05169
fixed SPASS fact offset calculation and report unexpected unsound proofs with socalled sound encodings
blanchet
parents:
42550
diff
changeset

86 
NoLibwwwPerl  
4fbb1de05169
fixed SPASS fact offset calculation and report unexpected unsound proofs with socalled sound encodings
blanchet
parents:
42550
diff
changeset

87 
MalformedInput  
4fbb1de05169
fixed SPASS fact offset calculation and report unexpected unsound proofs with socalled sound encodings
blanchet
parents:
42550
diff
changeset

88 
MalformedOutput  
4fbb1de05169
fixed SPASS fact offset calculation and report unexpected unsound proofs with socalled sound encodings
blanchet
parents:
42550
diff
changeset

89 
Interrupted  
4fbb1de05169
fixed SPASS fact offset calculation and report unexpected unsound proofs with socalled sound encodings
blanchet
parents:
42550
diff
changeset

90 
Crashed  
4fbb1de05169
fixed SPASS fact offset calculation and report unexpected unsound proofs with socalled sound encodings
blanchet
parents:
42550
diff
changeset

91 
InternalError  
4fbb1de05169
fixed SPASS fact offset calculation and report unexpected unsound proofs with socalled sound encodings
blanchet
parents:
42550
diff
changeset

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

93 

39452  94 
fun is_ident_char c = Char.isAlphaNum c orelse c = #"_" 
42961  95 
val strip_spaces_except_between_ident_chars = strip_spaces true is_ident_char 
39452  96 

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

97 
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

98 
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

99 
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

100 
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

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

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

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

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

105 
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

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

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

108 

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

111 
\remote provers." 

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

112 

42876
e336ef6313aa
more informative message when Sledgehammer finds an unsound proof
blanchet
parents:
42848
diff
changeset

113 
fun involving [] = "" 
43005
c96f06bffd90
merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents:
42998
diff
changeset

114 
 involving ss = 
43029
3e060b1c844b
use helpers and tweak Quickcheck's priority to it comes second (to give Solve Direct slightly more time before another prover runs)
blanchet
parents:
43005
diff
changeset

115 
"involving " ^ space_implode " " (Try.serial_commas "and" (map quote ss)) ^ 
3e060b1c844b
use helpers and tweak Quickcheck's priority to it comes second (to give Solve Direct slightly more time before another prover runs)
blanchet
parents:
43005
diff
changeset

116 
" " 
42876
e336ef6313aa
more informative message when Sledgehammer finds an unsound proof
blanchet
parents:
42848
diff
changeset

117 

42968
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

118 
fun string_for_failure Unprovable = "The problem is unprovable." 
43050
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43029
diff
changeset

119 
 string_for_failure GaveUp = "The prover gave up." 
41744  120 
 string_for_failure ProofMissing = 
121 
"The prover claims the conjecture is a theorem but did not provide a proof." 

42882
391e41ac038b
make sure the Vampire incomplete proof detection code kicks in
blanchet
parents:
42876
diff
changeset

122 
 string_for_failure ProofIncomplete = 
391e41ac038b
make sure the Vampire incomplete proof detection code kicks in
blanchet
parents:
42876
diff
changeset

123 
"The prover claims the conjecture is a theorem but provided an incomplete \ 
391e41ac038b
make sure the Vampire incomplete proof detection code kicks in
blanchet
parents:
42876
diff
changeset

124 
\proof." 
42876
e336ef6313aa
more informative message when Sledgehammer finds an unsound proof
blanchet
parents:
42848
diff
changeset

125 
 string_for_failure (UnsoundProof (false, ss)) = 
e336ef6313aa
more informative message when Sledgehammer finds an unsound proof
blanchet
parents:
42848
diff
changeset

126 
"The prover found a typeunsound proof " ^ involving ss ^ 
e336ef6313aa
more informative message when Sledgehammer finds an unsound proof
blanchet
parents:
42848
diff
changeset

127 
"(or, less likely, your axioms are inconsistent). Try passing the \ 
e336ef6313aa
more informative message when Sledgehammer finds an unsound proof
blanchet
parents:
42848
diff
changeset

128 
\\"full_types\" option to Sledgehammer to avoid such spurious proofs." 
e336ef6313aa
more informative message when Sledgehammer finds an unsound proof
blanchet
parents:
42848
diff
changeset

129 
 string_for_failure (UnsoundProof (true, ss)) = 
e336ef6313aa
more informative message when Sledgehammer finds an unsound proof
blanchet
parents:
42848
diff
changeset

130 
"The prover found a typeunsound proof " ^ involving ss ^ 
e336ef6313aa
more informative message when Sledgehammer finds an unsound proof
blanchet
parents:
42848
diff
changeset

131 
"even though a supposedly typesound encoding was used (or, less likely, \ 
e336ef6313aa
more informative message when Sledgehammer finds an unsound proof
blanchet
parents:
42848
diff
changeset

132 
\your axioms are inconsistent). You might want to report this to the \ 
e336ef6313aa
more informative message when Sledgehammer finds an unsound proof
blanchet
parents:
42848
diff
changeset

133 
\Isabelle developers." 
41744  134 
 string_for_failure CantConnect = "Cannot connect to remote server." 
135 
 string_for_failure TimedOut = "Timed out." 

42953
26111aafab12
detect inappropriate problems and crashes better in Waldmeister
blanchet
parents:
42943
diff
changeset

136 
 string_for_failure Inappropriate = 
26111aafab12
detect inappropriate problems and crashes better in Waldmeister
blanchet
parents:
42943
diff
changeset

137 
"The problem lies outside the prover's scope." 
41744  138 
 string_for_failure OutOfResources = "The prover ran out of resources." 
139 
 string_for_failure SpassTooOld = 

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

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

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

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

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

144 
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

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

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

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

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

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

151 
\ sledgehammer\")." 
41744  152 
 string_for_failure NoPerl = "Perl" ^ missing_message_tail 
153 
 string_for_failure NoLibwwwPerl = 

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

155 
 string_for_failure MalformedInput = 

156 
"The generated problem is malformed. Please report this to the Isabelle \ 

157 
\developers." 

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

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

159 
 string_for_failure Interrupted = "The prover was interrupted." 
41744  160 
 string_for_failure Crashed = "The prover crashed." 
161 
 string_for_failure InternalError = "An internal prover error occurred." 

162 
 string_for_failure (UnknownError string) = 

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

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

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

166 

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

167 
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

168 
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

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

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

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

172 

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

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

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

175 

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

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

177 
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

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

179 
 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

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

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

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

183 

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

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

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

186 
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

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

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

189 
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

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

191 

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

192 
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

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

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

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

196 

42848  197 
fun extract_tstplike_proof_and_outcome verbose complete res_code proof_delims 
198 
known_failures output = 

42882
391e41ac038b
make sure the Vampire incomplete proof detection code kicks in
blanchet
parents:
42876
diff
changeset

199 
case (extract_tstplike_proof proof_delims output, 
391e41ac038b
make sure the Vampire incomplete proof detection code kicks in
blanchet
parents:
42876
diff
changeset

200 
extract_known_failure known_failures output) of 
391e41ac038b
make sure the Vampire incomplete proof detection code kicks in
blanchet
parents:
42876
diff
changeset

201 
(_, SOME ProofIncomplete) => ("", SOME ProofIncomplete) 
391e41ac038b
make sure the Vampire incomplete proof detection code kicks in
blanchet
parents:
42876
diff
changeset

202 
 ("", SOME failure) => 
43050
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43029
diff
changeset

203 
("", SOME (if failure = GaveUp andalso complete then Unprovable 
42882
391e41ac038b
make sure the Vampire incomplete proof detection code kicks in
blanchet
parents:
42876
diff
changeset

204 
else failure)) 
391e41ac038b
make sure the Vampire incomplete proof detection code kicks in
blanchet
parents:
42876
diff
changeset

205 
 ("", NONE) => 
391e41ac038b
make sure the Vampire incomplete proof detection code kicks in
blanchet
parents:
42876
diff
changeset

206 
("", SOME (if res_code = 0 andalso output = "" then ProofMissing 
391e41ac038b
make sure the Vampire incomplete proof detection code kicks in
blanchet
parents:
42876
diff
changeset

207 
else UnknownError (short_output verbose output))) 
391e41ac038b
make sure the Vampire incomplete proof detection code kicks in
blanchet
parents:
42876
diff
changeset

208 
 (tstplike_proof, _) => (tstplike_proof, NONE) 
39452  209 

39455  210 
type step_name = string * string option 
39452  211 

42968
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

212 
fun is_same_atp_step (s1, _) (s2, _) = s1 = s2 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

213 

74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

214 
val vampire_fact_prefix = "f" 
39452  215 

216 
fun step_name_ord p = 

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

220 
"Graph" functor. *) 

42968
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

221 
case pairself (Int.fromString 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

222 
o perhaps (try (unprefix vampire_fact_prefix))) q of 
39452  223 
(NONE, NONE) => string_ord q 
224 
 (NONE, SOME _) => LESS 

225 
 (SOME _, NONE) => GREATER 

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

227 
end 

228 

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

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

230 
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

231 
Inference of step_name * 'a * step_name list 
39452  232 

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

233 
type 'a proof = ('a, 'a, 'a fo_term) formula step list 
39452  234 

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

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

237 

238 
(**** PARSING OF TSTP FORMAT ****) 

239 

42973
6b39a2098ffd
hack to obtain potable step names from Waldmeister
blanchet
parents:
42968
diff
changeset

240 
(* FIXME: temporary hack *) 
6b39a2098ffd
hack to obtain potable step names from Waldmeister
blanchet
parents:
42968
diff
changeset

241 
fun repair_waldmeister_step_name s = 
6b39a2098ffd
hack to obtain potable step names from Waldmeister
blanchet
parents:
42968
diff
changeset

242 
case space_explode "." s of 
6b39a2098ffd
hack to obtain potable step names from Waldmeister
blanchet
parents:
42968
diff
changeset

243 
[a, b, c, d] => 
6b39a2098ffd
hack to obtain potable step names from Waldmeister
blanchet
parents:
42968
diff
changeset

244 
(case a of "0" => "X"  "1" => "Y"  _ => "Z" ^ a) ^ 
6b39a2098ffd
hack to obtain potable step names from Waldmeister
blanchet
parents:
42968
diff
changeset

245 
(if size b = 1 then "0" else "") ^ b ^ c ^ d 
6b39a2098ffd
hack to obtain potable step names from Waldmeister
blanchet
parents:
42968
diff
changeset

246 
 _ => s 
6b39a2098ffd
hack to obtain potable step names from Waldmeister
blanchet
parents:
42968
diff
changeset

247 

42536  248 
(* Strings enclosed in single quotes (e.g., file names) *) 
39452  249 
val scan_general_id = 
42973
6b39a2098ffd
hack to obtain potable step names from Waldmeister
blanchet
parents:
42968
diff
changeset

250 
$$ "'"  Scan.repeat (~$$ "'")  $$ "'" 
6b39a2098ffd
hack to obtain potable step names from Waldmeister
blanchet
parents:
42968
diff
changeset

251 
>> implode >> repair_waldmeister_step_name 
39452  252 
 Scan.repeat ($$ "$")  Scan.many1 Symbol.is_letdig 
253 
>> (fn (ss1, ss2) => implode ss1 ^ implode ss2) 

254 

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

42594
62398fdbb528
fixed parsing of multiple negations (e.g. ~~~p) found in Vampire proofs
blanchet
parents:
42587
diff
changeset

256 
fun parse_annotation x = 
42610
def5846169ce
make sure that "file" annotations are read correctly in SInEE and E proofs
blanchet
parents:
42605
diff
changeset

257 
((scan_general_id ::: Scan.repeat ($$ " "  scan_general_id)) 
def5846169ce
make sure that "file" annotations are read correctly in SInEE and E proofs
blanchet
parents:
42605
diff
changeset

258 
 Scan.optional parse_annotation [] >> op @ 
42594
62398fdbb528
fixed parsing of multiple negations (e.g. ~~~p) found in Vampire proofs
blanchet
parents:
42587
diff
changeset

259 
 $$ "("  parse_annotations  $$ ")" 
62398fdbb528
fixed parsing of multiple negations (e.g. ~~~p) found in Vampire proofs
blanchet
parents:
42587
diff
changeset

260 
 $$ "["  parse_annotations  $$ "]") x 
62398fdbb528
fixed parsing of multiple negations (e.g. ~~~p) found in Vampire proofs
blanchet
parents:
42587
diff
changeset

261 
and parse_annotations x = 
62398fdbb528
fixed parsing of multiple negations (e.g. ~~~p) found in Vampire proofs
blanchet
parents:
42587
diff
changeset

262 
(Scan.optional (parse_annotation 
62398fdbb528
fixed parsing of multiple negations (e.g. ~~~p) found in Vampire proofs
blanchet
parents:
42587
diff
changeset

263 
::: Scan.repeat ($$ ","  parse_annotation)) [] 
39452  264 
>> flat) x 
265 

42966
4e2d6c1e5392
more work on parsing LEOII proofs without lambdas
blanchet
parents:
42965
diff
changeset

266 
fun list_app (f, args) = 
42968
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

267 
fold (fn arg => fn f => ATerm (tptp_app, [f, arg])) args f 
42966
4e2d6c1e5392
more work on parsing LEOII proofs without lambdas
blanchet
parents:
42965
diff
changeset

268 

42968
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

269 
(* We ignore TFF and THF types for now. *) 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

270 
fun parse_type_stuff x = 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

271 
Scan.repeat (($$ tptp_has_type  $$ tptp_fun_type)  parse_arg) x 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

272 
and parse_arg x = 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

273 
($$ "("  parse_term  $$ ")"  parse_type_stuff 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

274 
 scan_general_id  parse_type_stuff 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

275 
 Scan.optional ($$ "("  parse_terms  $$ ")") [] 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

276 
>> ATerm) x 
42966
4e2d6c1e5392
more work on parsing LEOII proofs without lambdas
blanchet
parents:
42965
diff
changeset

277 
and parse_app x = 
42968
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

278 
(parse_arg  Scan.repeat ($$ tptp_app  parse_arg) >> list_app) x 
42966
4e2d6c1e5392
more work on parsing LEOII proofs without lambdas
blanchet
parents:
42965
diff
changeset

279 
and parse_term x = 
42968
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

280 
(parse_app  Scan.option (Scan.option ($$ tptp_not_infix)  $$ tptp_equal 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

281 
 parse_app) 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

282 
>> (fn (u1, NONE) => u1 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

283 
 (u1, SOME (NONE, u2)) => ATerm ("equal", [u1, u2]) 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

284 
 (u1, SOME (SOME _, u2)) => 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

285 
ATerm (tptp_not, [ATerm ("equal", [u1, u2])]))) x 
42966
4e2d6c1e5392
more work on parsing LEOII proofs without lambdas
blanchet
parents:
42965
diff
changeset

286 
and parse_terms x = 
4e2d6c1e5392
more work on parsing LEOII proofs without lambdas
blanchet
parents:
42965
diff
changeset

287 
(parse_term ::: Scan.repeat ($$ ","  parse_term)) x 
39452  288 

42968
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

289 
(* TODO: Avoid duplication with "parse_term" above. *) 
39598  290 
fun parse_atom x = 
42968
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

291 
(parse_term  Scan.option (Scan.option ($$ tptp_not_infix)  $$ tptp_equal 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

292 
 parse_term) 
39598  293 
>> (fn (u1, NONE) => AAtom u1 
42943  294 
 (u1, SOME (NONE, u2)) => AAtom (ATerm ("equal", [u1, u2])) 
39598  295 
 (u1, SOME (SOME _, u2)) => 
42943  296 
mk_anot (AAtom (ATerm ("equal", [u1, u2]))))) x 
39452  297 

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

299 

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

301 
operator precedence. *) 

42605
8734eb0033b3
Vampire sometimes generates formulas with ~ (not) followed by a quantified subformula, without parentheses  parse these correctly
blanchet
parents:
42603
diff
changeset

302 
fun parse_literal x = 
42968
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

303 
((Scan.repeat ($$ tptp_not) >> length) 
42605
8734eb0033b3
Vampire sometimes generates formulas with ~ (not) followed by a quantified subformula, without parentheses  parse these correctly
blanchet
parents:
42603
diff
changeset

304 
 ($$ "("  parse_formula  $$ ")" 
8734eb0033b3
Vampire sometimes generates formulas with ~ (not) followed by a quantified subformula, without parentheses  parse these correctly
blanchet
parents:
42603
diff
changeset

305 
 parse_quantified_formula 
8734eb0033b3
Vampire sometimes generates formulas with ~ (not) followed by a quantified subformula, without parentheses  parse these correctly
blanchet
parents:
42603
diff
changeset

306 
 parse_atom) 
8734eb0033b3
Vampire sometimes generates formulas with ~ (not) followed by a quantified subformula, without parentheses  parse these correctly
blanchet
parents:
42603
diff
changeset

307 
>> (fn (n, phi) => phi > n mod 2 = 1 ? mk_anot)) x 
8734eb0033b3
Vampire sometimes generates formulas with ~ (not) followed by a quantified subformula, without parentheses  parse these correctly
blanchet
parents:
42603
diff
changeset

308 
and parse_formula x = 
8734eb0033b3
Vampire sometimes generates formulas with ~ (not) followed by a quantified subformula, without parentheses  parse these correctly
blanchet
parents:
42603
diff
changeset

309 
(parse_literal 
43163  310 
 Scan.option ((Scan.this_string tptp_implies 
311 
 Scan.this_string tptp_iff 

312 
 Scan.this_string tptp_not_iff 

313 
 Scan.this_string tptp_if 

314 
 $$ tptp_or 

315 
 $$ tptp_and)  parse_formula) 

39452  316 
>> (fn (phi1, NONE) => phi1 
43163  317 
 (phi1, SOME (c, phi2)) => 
318 
if c = tptp_implies then mk_aconn AImplies phi1 phi2 

319 
else if c = tptp_iff then mk_aconn AIff phi1 phi2 

320 
else if c = tptp_not_iff then mk_anot (mk_aconn AIff phi1 phi2) 

321 
else if c = tptp_if then mk_aconn AImplies phi2 phi1 

322 
else if c = tptp_or then mk_aconn AOr phi1 phi2 

323 
else if c = tptp_and then mk_aconn AAnd phi1 phi2 

324 
else raise Fail ("impossible connective " ^ quote c))) x 

42605
8734eb0033b3
Vampire sometimes generates formulas with ~ (not) followed by a quantified subformula, without parentheses  parse these correctly
blanchet
parents:
42603
diff
changeset

325 
and parse_quantified_formula x = 
42968
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

326 
(($$ tptp_forall >> K AForall  $$ tptp_exists >> K AExists) 
42605
8734eb0033b3
Vampire sometimes generates formulas with ~ (not) followed by a quantified subformula, without parentheses  parse these correctly
blanchet
parents:
42603
diff
changeset

327 
 $$ "["  parse_terms  $$ "]"  $$ ":"  parse_literal 
8734eb0033b3
Vampire sometimes generates formulas with ~ (not) followed by a quantified subformula, without parentheses  parse these correctly
blanchet
parents:
42603
diff
changeset

328 
>> (fn ((q, ts), phi) => 
42966
4e2d6c1e5392
more work on parsing LEOII proofs without lambdas
blanchet
parents:
42965
diff
changeset

329 
(* We ignore TFF and THF types for now. *) 
42605
8734eb0033b3
Vampire sometimes generates formulas with ~ (not) followed by a quantified subformula, without parentheses  parse these correctly
blanchet
parents:
42603
diff
changeset

330 
AQuant (q, map (rpair NONE o fo_term_head) ts, phi))) x 
39452  331 

42968
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

332 
fun skip_formula ss = 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

333 
let 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

334 
fun skip _ [] = [] 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

335 
 skip 0 (ss as "," :: _) = ss 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

336 
 skip 0 (ss as ")" :: _) = ss 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

337 
 skip 0 (ss as "]" :: _) = ss 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

338 
 skip n ("(" :: ss) = skip (n + 1) ss 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

339 
 skip n ("[" :: ss) = skip (n + 1) ss 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

340 
 skip n ("]" :: ss) = skip (n  1) ss 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

341 
 skip n (")" :: ss) = skip (n  1) ss 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

342 
 skip n (_ :: ss) = skip n ss 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

343 
in (AAtom (ATerm ("", [])), skip 0 ss) end 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

344 

39452  345 
val parse_tstp_extra_arguments = 
42594
62398fdbb528
fixed parsing of multiple negations (e.g. ~~~p) found in Vampire proofs
blanchet
parents:
42587
diff
changeset

346 
Scan.optional ($$ ","  parse_annotation 
62398fdbb528
fixed parsing of multiple negations (e.g. ~~~p) found in Vampire proofs
blanchet
parents:
42587
diff
changeset

347 
 Scan.option ($$ ","  parse_annotations)) [] 
39452  348 

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

349 
val vampire_unknown_fact = "unknown" 
42943  350 
val waldmeister_conjecture = "conjecture_1" 
351 

42536  352 
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

353 

42943  354 
fun is_same_term subst tm1 tm2 = 
355 
let 

356 
fun do_term_pair _ NONE = NONE 

357 
 do_term_pair (ATerm (s1, tm1), ATerm (s2, tm2)) (SOME subst) = 

42998
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42975
diff
changeset

358 
case pairself is_tptp_variable (s1, s2) of 
42943  359 
(true, true) => 
360 
(case AList.lookup (op =) subst s1 of 

361 
SOME s2' => if s2' = s2 then SOME subst else NONE 

362 
 NONE => 

363 
if null (AList.find (op =) subst s2) then SOME ((s1, s2) :: subst) 

364 
else NONE) 

365 
 (false, false) => 

366 
if s1 = s2 andalso length tm1 = length tm2 then 

367 
SOME subst > fold do_term_pair (tm1 ~~ tm2) 

368 
else 

369 
NONE 

370 
 _ => NONE 

371 
in SOME subst > do_term_pair (tm1, tm2) > is_some end 

372 

373 
fun is_same_formula subst (AQuant (q1, xs1, phi1)) (AQuant (q2, xs2, phi2)) = 

374 
q1 = q2 andalso length xs1 = length xs2 andalso 

375 
is_same_formula ((map fst xs1 ~~ map fst xs2) @ subst) phi1 phi2 

376 
 is_same_formula subst (AConn (c1, phis1)) (AConn (c2, phis2)) = 

377 
c1 = c2 andalso length phis1 = length phis2 andalso 

378 
forall (uncurry (is_same_formula subst)) (phis1 ~~ phis2) 

379 
 is_same_formula subst (AAtom (ATerm ("equal", [tm11, tm12]))) (AAtom tm2) = 

380 
is_same_term subst (ATerm ("equal", [tm11, tm12])) tm2 orelse 

381 
is_same_term subst (ATerm ("equal", [tm12, tm11])) tm2 

382 
 is_same_formula subst (AAtom tm1) (AAtom tm2) = is_same_term subst tm1 tm2 

383 
 is_same_formula _ _ _ = false 

384 

385 
fun matching_formula_line_identifier phi (Formula (ident, _, phi', _, _)) = 

386 
if is_same_formula [] phi phi' then SOME ident else NONE 

387 
 matching_formula_line_identifier _ _ = NONE 

388 

389 
fun find_formula_in_problem problem phi = 

390 
problem > maps snd > map_filter (matching_formula_line_identifier phi) 

391 
> try hd 

392 

42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42961
diff
changeset

393 
(* Syntax: (cnffoftffthf)\(<num>, <formula_role>, 
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42961
diff
changeset

394 
<formula> <extra_arguments>\). 
39452  395 
The <num> could be an identifier, but we assume integers. *) 
42943  396 
fun parse_tstp_line problem = 
42968
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

397 
((Scan.this_string tptp_cnf  Scan.this_string tptp_fof 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

398 
 Scan.this_string tptp_tff  Scan.this_string tptp_thf)  $$ "(") 
42943  399 
 scan_general_id  $$ ","  Symbol.scan_id  $$ "," 
42968
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

400 
 (parse_formula  skip_formula)  parse_tstp_extra_arguments  $$ ")" 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

401 
 $$ "." 
42943  402 
>> (fn (((num, role), phi), deps) => 
403 
let 

404 
val (name, deps) = 

405 
(* Waldmeister isn't exactly helping. *) 

406 
case deps of 

407 
["file", _, s] => 

408 
((num, 

409 
if s = vampire_unknown_fact then 

410 
NONE 

411 
else if s = waldmeister_conjecture then 

412 
find_formula_in_problem problem (mk_anot phi) 

413 
else 

414 
SOME (s > perhaps (try (unprefix tofof_fact_prefix)))), 

415 
[]) 

416 
 ["file", _] => ((num, find_formula_in_problem problem phi), []) 

417 
 _ => ((num, NONE), deps) 

418 
in 

419 
case role of 

420 
"definition" => 

421 
(case phi of 

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

423 
Definition (name, phi1, phi2) 

424 
 AAtom (ATerm ("equal", _)) => 

425 
(* Vampire's equality proxy axiom *) 

426 
Inference (name, phi, map (rpair NONE) deps) 

42968
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

427 
 _ => raise UNRECOGNIZED_ATP_PROOF ()) 
42943  428 
 _ => Inference (name, phi, map (rpair NONE) deps) 
429 
end) 

39452  430 

431 
(**** PARSING OF SPASS OUTPUT ****) 

432 

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

434 
is not clear anyway. *) 

435 
val parse_dot_name = scan_general_id  $$ "."  scan_general_id 

436 

437 
val parse_spass_annotations = 

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

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

440 

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

442 
pluses. We ignore them. *) 

39602  443 
fun parse_decorated_atom x = 
444 
(parse_atom  Scan.repeat ($$ "*"  $$ "+"  $$ " ")) x 

39452  445 

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

42943  447 
 mk_horn ([], pos_lits) = foldr1 (uncurry (mk_aconn AOr)) pos_lits 
448 
 mk_horn (neg_lits, []) = mk_anot (foldr1 (uncurry (mk_aconn AAnd)) neg_lits) 

39452  449 
 mk_horn (neg_lits, pos_lits) = 
42943  450 
mk_aconn AImplies (foldr1 (uncurry (mk_aconn AAnd)) neg_lits) 
451 
(foldr1 (uncurry (mk_aconn AOr)) pos_lits) 

39452  452 

39645  453 
fun parse_horn_clause x = 
454 
(Scan.repeat parse_decorated_atom  $$ ""  $$ "" 

455 
 Scan.repeat parse_decorated_atom  $$ ""  $$ ">" 

456 
 Scan.repeat parse_decorated_atom 

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

39452  458 

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

460 
<atoms>  <atoms> > <atoms>. *) 

39645  461 
fun parse_spass_line x = 
462 
(scan_general_id  $$ "["  $$ "0"  $$ ":"  Symbol.scan_id 

463 
 parse_spass_annotations  $$ "]"  parse_horn_clause  $$ "." 

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

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

39452  466 

42943  467 
fun parse_line problem = parse_tstp_line problem  parse_spass_line 
468 
fun parse_proof problem s = 

42648  469 
s > strip_spaces_except_between_ident_chars 
470 
> raw_explode 

471 
> Scan.finite Symbol.stopper 

42965
1403595ec38c
slightly gracefuller handling of LEOII and Satallax output
blanchet
parents:
42962
diff
changeset

472 
(Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ()) 
42943  473 
(Scan.repeat1 (parse_line problem)))) 
42648  474 
> fst 
39452  475 

42943  476 
fun atp_proof_from_tstplike_proof _ "" = [] 
477 
 atp_proof_from_tstplike_proof problem s = 

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

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

480 
> sort (step_name_ord o pairself step_name) 
42968
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

481 

74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

482 
fun clean_up_dependencies _ [] = [] 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

483 
 clean_up_dependencies seen ((step as Definition (name, _, _)) :: steps) = 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

484 
step :: clean_up_dependencies (name :: seen) steps 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

485 
 clean_up_dependencies seen (Inference (name, u, deps) :: steps) = 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

486 
Inference (name, u, 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

487 
map_filter (fn dep => find_first (is_same_atp_step dep) seen) 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

488 
deps) :: 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

489 
clean_up_dependencies (name :: seen) steps 
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

490 

42975  491 
fun clean_up_atp_proof_dependencies proof = clean_up_dependencies [] proof 
39452  492 

39454  493 
fun map_term_names_in_term f (ATerm (s, ts)) = 
494 
ATerm (f s, map (map_term_names_in_term f) ts) 

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

496 
AQuant (q, xs, map_term_names_in_formula f phi) 

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

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

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

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

501 
Definition (name, map_term_names_in_formula f phi1, 

502 
map_term_names_in_formula f phi2) 

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

504 
Inference (name, map_term_names_in_formula f phi, deps) 

505 
fun map_term_names_in_atp_proof f = map (map_term_names_in_step f) 

506 

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

508 
fun nasty_atp_proof pool = 

509 
if Symtab.is_empty pool then I 

510 
else map_term_names_in_atp_proof (nasty_name pool) 

511 

39452  512 
end; 