author  blanchet 
Tue, 18 Dec 2012 02:18:45 +0100  
changeset 50590  9d2f223ab6d9 
parent 50521  bec828f3364e 
child 50704  cd1fcda1ea88 
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 

43678  11 
type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term 
50012
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50011
diff
changeset

12 
type formula_role = ATP_Problem.formula_role 
48135  13 
type ('a, 'b, 'c, 'd) formula = ('a, 'b, 'c, 'd) ATP_Problem.formula 
42943  14 
type 'a problem = 'a ATP_Problem.problem 
39452  15 

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

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

17 

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

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

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

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

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

22 
ProofIncomplete  
44915
635ae0a73688
simplified unsound proof detection by removing impossible case
blanchet
parents:
44784
diff
changeset

23 
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

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

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

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

27 
OutOfResources  
47950
9cb132898ac8
invite users to upgrade their SPASS (so we can get rid of old code)
blanchet
parents:
47947
diff
changeset

28 
OldSPASS  
42587
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 

45551  38 
type step_name = string * string list 
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 = 
47774  41 
Definition_Step of step_name * 'a * 'a  
50012
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50011
diff
changeset

42 
Inference_Step of step_name * formula_role * 'a * string * step_name list 
39452  43 

48135  44 
type 'a proof = ('a, 'a, ('a, 'a) ho_term, 'a) 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 : 
48716
1d2a12bb0640
stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents:
48700
diff
changeset

52 
bool > (string * string) list > (failure * string) list > string 
43473
fb2713b803e6
deal with ATP time slices in a more flexible/robust fashion
blanchet
parents:
43465
diff
changeset

53 
> 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 
48539  56 
val satallax_coreN : string 
57 
val z3_tptp_coreN : string 

42961  58 
val parse_formula : 
48132
9aa0fad4e864
added type arguments to "ATerm" constructor  but don't use them yet
blanchet
parents:
48130
diff
changeset

59 
string list 
48135  60 
> (string, 'a, (string, 'a) ho_term, string) formula * string list 
48130  61 
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

62 
val clean_up_atp_proof_dependencies : string proof > string proof 
39454  63 
val map_term_names_in_atp_proof : 
64 
(string > string) > string proof > string proof 

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

39452  66 
end; 
67 

68 
structure ATP_Proof : ATP_PROOF = 

69 
struct 

70 

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

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

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

73 

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

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

75 

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

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

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

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

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

80 
ProofIncomplete  
44915
635ae0a73688
simplified unsound proof detection by removing impossible case
blanchet
parents:
44784
diff
changeset

81 
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

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

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

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

85 
OutOfResources  
47950
9cb132898ac8
invite users to upgrade their SPASS (so we can get rid of old code)
blanchet
parents:
47947
diff
changeset

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

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

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

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

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

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

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

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

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

95 

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

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

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

98 
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

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

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

101 

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

104 
\remote provers." 

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

105 

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

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

107 
 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

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

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

110 

47506  111 
fun string_for_failure Unprovable = "The generated 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

112 
 string_for_failure GaveUp = "The prover gave up." 
41744  113 
 string_for_failure ProofMissing = 
114 
"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

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

116 
"The prover claims the conjecture is a theorem but provided an incomplete \ 
46427  117 
\(or unparsable) proof." 
44915
635ae0a73688
simplified unsound proof detection by removing impossible case
blanchet
parents:
44784
diff
changeset

118 
 string_for_failure (UnsoundProof (false, ss)) = 
43823  119 
"The prover found a typeunsound proof " ^ involving ss ^ 
120 
"(or, less likely, your axioms are inconsistent). Specify a sound type \ 

121 
\encoding or omit the \"type_enc\" option." 

44915
635ae0a73688
simplified unsound proof detection by removing impossible case
blanchet
parents:
44784
diff
changeset

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

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

124 
"even though a supposedly typesound encoding was used (or, less likely, \ 
43465  125 
\your axioms are inconsistent). Please report this to the Isabelle \ 
126 
\developers." 

41744  127 
 string_for_failure CantConnect = "Cannot connect to remote server." 
128 
 string_for_failure TimedOut = "Timed out." 

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

129 
 string_for_failure Inappropriate = 
47506  130 
"The generated problem lies outside the prover's scope." 
41744  131 
 string_for_failure OutOfResources = "The prover ran out of resources." 
47950
9cb132898ac8
invite users to upgrade their SPASS (so we can get rid of old code)
blanchet
parents:
47947
diff
changeset

132 
 string_for_failure OldSPASS = 
9cb132898ac8
invite users to upgrade their SPASS (so we can get rid of old code)
blanchet
parents:
47947
diff
changeset

133 
"The version of SPASS you are using is obsolete. Please upgrade to \ 
9cb132898ac8
invite users to upgrade their SPASS (so we can get rid of old code)
blanchet
parents:
47947
diff
changeset

134 
\SPASS 3.8ds. To install it, download and extract the package \ 
9cb132898ac8
invite users to upgrade their SPASS (so we can get rid of old code)
blanchet
parents:
47947
diff
changeset

135 
\\"http://www21.in.tum.de/~blanchet/spass3.8ds.tar.gz\" and add the \ 
9cb132898ac8
invite users to upgrade their SPASS (so we can get rid of old code)
blanchet
parents:
47947
diff
changeset

136 
\\"spass3.8ds\" directory's absolute path to " ^ 
9cb132898ac8
invite users to upgrade their SPASS (so we can get rid of old code)
blanchet
parents:
47947
diff
changeset

137 
quote (Path.implode (Path.expand (Path.appends 
9cb132898ac8
invite users to upgrade their SPASS (so we can get rid of old code)
blanchet
parents:
47947
diff
changeset

138 
(Path.variable "ISABELLE_HOME_USER" :: 
9cb132898ac8
invite users to upgrade their SPASS (so we can get rid of old code)
blanchet
parents:
47947
diff
changeset

139 
map Path.basic ["etc", "components"])))) ^ 
9cb132898ac8
invite users to upgrade their SPASS (so we can get rid of old code)
blanchet
parents:
47947
diff
changeset

140 
" on a line of its own." 
41744  141 
 string_for_failure NoPerl = "Perl" ^ missing_message_tail 
142 
 string_for_failure NoLibwwwPerl = 

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

144 
 string_for_failure MalformedInput = 

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

146 
\developers." 

147 
 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

148 
 string_for_failure Interrupted = "The prover was interrupted." 
41744  149 
 string_for_failure Crashed = "The prover crashed." 
150 
 string_for_failure InternalError = "An internal prover error occurred." 

151 
 string_for_failure (UnknownError string) = 

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

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

154 
else ":\n" ^ string) 
39491
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_delimited (begin_delim, end_delim) output = 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

157 
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

158 
> first_field end_delim > the > fst 
48539  159 
> perhaps (try (first_field "\n" #> the #> snd)) 
39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39457
diff
changeset

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

161 

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

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

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

164 

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

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

166 
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

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

168 
 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

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

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

171 
> space_implode "\n " > quote 
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 
(* 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

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

175 
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

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

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

178 
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

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

180 

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

181 
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

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

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

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

185 

48716
1d2a12bb0640
stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents:
48700
diff
changeset

186 
fun extract_tstplike_proof_and_outcome verbose proof_delims known_failures 
1d2a12bb0640
stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents:
48700
diff
changeset

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

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

189 
extract_known_failure known_failures output) of 
48700  190 
(_, SOME ProofIncomplete) => ("", NONE) 
43246  191 
 ("", SOME ProofMissing) => ("", NONE) 
192 
 ("", NONE) => ("", SOME (UnknownError (short_output verbose output))) 

48716
1d2a12bb0640
stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents:
48700
diff
changeset

193 
 res as ("", _) => res 
42882
391e41ac038b
make sure the Vampire incomplete proof detection code kicks in
blanchet
parents:
42876
diff
changeset

194 
 (tstplike_proof, _) => (tstplike_proof, NONE) 
39452  195 

45551  196 
type step_name = string * string list 
39452  197 

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

198 
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

199 

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

200 
val vampire_fact_prefix = "f" 
39452  201 

202 
fun step_name_ord p = 

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

206 
"Graph" functor. *) 

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

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

208 
o perhaps (try (unprefix vampire_fact_prefix))) q of 
39452  209 
(NONE, NONE) => string_ord q 
210 
 (NONE, SOME _) => LESS 

211 
 (SOME _, NONE) => GREATER 

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

213 
end 

214 

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

215 
datatype 'a step = 
47774  216 
Definition_Step of step_name * 'a * 'a  
50012
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50011
diff
changeset

217 
Inference_Step of step_name * formula_role * 'a * string * step_name list 
39452  218 

48135  219 
type 'a proof = ('a, 'a, ('a, 'a) ho_term, 'a) formula step list 
39452  220 

47774  221 
fun step_name (Definition_Step (name, _, _)) = name 
50012
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50011
diff
changeset

222 
 step_name (Inference_Step (name, _, _, _, _)) = name 
39452  223 

224 
(**** PARSING OF TSTP FORMAT ****) 

225 

42536  226 
(* Strings enclosed in single quotes (e.g., file names) *) 
39452  227 
val scan_general_id = 
47917
b287682bf917
improve parsing of Waldmeister dependencies (and kill obsolete hack)
blanchet
parents:
47787
diff
changeset

228 
$$ "'"  Scan.repeat (~$$ "'")  $$ "'" >> implode 
39452  229 
 Scan.repeat ($$ "$")  Scan.many1 Symbol.is_letdig 
230 
>> (fn (ss1, ss2) => implode ss1 ^ implode ss2) 

231 

45235
7187bce94e88
more robust parsing of TSTP sources  Vampire has nonstandard "introduced()" tags and Waldmeister(OnTPTP) has weird "theory(...)" dependencies
blanchet
parents:
45209
diff
changeset

232 
val skip_term = 
45208
9a00f9cc8707
marginally cleaner proof parsing, that doesn't stumble upon LEOII's Estep proofs
blanchet
parents:
45203
diff
changeset

233 
let 
45235
7187bce94e88
more robust parsing of TSTP sources  Vampire has nonstandard "introduced()" tags and Waldmeister(OnTPTP) has weird "theory(...)" dependencies
blanchet
parents:
45209
diff
changeset

234 
fun skip _ accum [] = (accum, []) 
7187bce94e88
more robust parsing of TSTP sources  Vampire has nonstandard "introduced()" tags and Waldmeister(OnTPTP) has weird "theory(...)" dependencies
blanchet
parents:
45209
diff
changeset

235 
 skip 0 accum (ss as "," :: _) = (accum, ss) 
7187bce94e88
more robust parsing of TSTP sources  Vampire has nonstandard "introduced()" tags and Waldmeister(OnTPTP) has weird "theory(...)" dependencies
blanchet
parents:
45209
diff
changeset

236 
 skip 0 accum (ss as ")" :: _) = (accum, ss) 
7187bce94e88
more robust parsing of TSTP sources  Vampire has nonstandard "introduced()" tags and Waldmeister(OnTPTP) has weird "theory(...)" dependencies
blanchet
parents:
45209
diff
changeset

237 
 skip 0 accum (ss as "]" :: _) = (accum, ss) 
7187bce94e88
more robust parsing of TSTP sources  Vampire has nonstandard "introduced()" tags and Waldmeister(OnTPTP) has weird "theory(...)" dependencies
blanchet
parents:
45209
diff
changeset

238 
 skip n accum ((s as "(") :: ss) = skip (n + 1) (s :: accum) ss 
7187bce94e88
more robust parsing of TSTP sources  Vampire has nonstandard "introduced()" tags and Waldmeister(OnTPTP) has weird "theory(...)" dependencies
blanchet
parents:
45209
diff
changeset

239 
 skip n accum ((s as "[") :: ss) = skip (n + 1) (s :: accum) ss 
7187bce94e88
more robust parsing of TSTP sources  Vampire has nonstandard "introduced()" tags and Waldmeister(OnTPTP) has weird "theory(...)" dependencies
blanchet
parents:
45209
diff
changeset

240 
 skip n accum ((s as "]") :: ss) = skip (n  1) (s :: accum) ss 
7187bce94e88
more robust parsing of TSTP sources  Vampire has nonstandard "introduced()" tags and Waldmeister(OnTPTP) has weird "theory(...)" dependencies
blanchet
parents:
45209
diff
changeset

241 
 skip n accum ((s as ")") :: ss) = skip (n  1) (s :: accum) ss 
7187bce94e88
more robust parsing of TSTP sources  Vampire has nonstandard "introduced()" tags and Waldmeister(OnTPTP) has weird "theory(...)" dependencies
blanchet
parents:
45209
diff
changeset

242 
 skip n accum (s :: ss) = skip n (s :: accum) ss 
7187bce94e88
more robust parsing of TSTP sources  Vampire has nonstandard "introduced()" tags and Waldmeister(OnTPTP) has weird "theory(...)" dependencies
blanchet
parents:
45209
diff
changeset

243 
in skip 0 [] #>> (rev #> implode) end 
45208
9a00f9cc8707
marginally cleaner proof parsing, that doesn't stumble upon LEOII's Estep proofs
blanchet
parents:
45203
diff
changeset

244 

9a00f9cc8707
marginally cleaner proof parsing, that doesn't stumble upon LEOII's Estep proofs
blanchet
parents:
45203
diff
changeset

245 
datatype source = 
9a00f9cc8707
marginally cleaner proof parsing, that doesn't stumble upon LEOII's Estep proofs
blanchet
parents:
45203
diff
changeset

246 
File_Source of string * string option  
45209  247 
Inference_Source of string * string list 
45208
9a00f9cc8707
marginally cleaner proof parsing, that doesn't stumble upon LEOII's Estep proofs
blanchet
parents:
45203
diff
changeset

248 

48132
9aa0fad4e864
added type arguments to "ATerm" constructor  but don't use them yet
blanchet
parents:
48130
diff
changeset

249 
val dummy_phi = AAtom (ATerm (("", []), [])) 
45235
7187bce94e88
more robust parsing of TSTP sources  Vampire has nonstandard "introduced()" tags and Waldmeister(OnTPTP) has weird "theory(...)" dependencies
blanchet
parents:
45209
diff
changeset

250 
val dummy_inference = Inference_Source ("", []) 
7187bce94e88
more robust parsing of TSTP sources  Vampire has nonstandard "introduced()" tags and Waldmeister(OnTPTP) has weird "theory(...)" dependencies
blanchet
parents:
45209
diff
changeset

251 

47917
b287682bf917
improve parsing of Waldmeister dependencies (and kill obsolete hack)
blanchet
parents:
47787
diff
changeset

252 
(* "skip_term" is there to cope with Waldmeister nonsense such as 
b287682bf917
improve parsing of Waldmeister dependencies (and kill obsolete hack)
blanchet
parents:
47787
diff
changeset

253 
"theory(equality)". *) 
50011  254 
fun parse_dependency x = 
255 
(parse_inference_source >> snd 

256 
 scan_general_id  skip_term >> single) x 

257 
and parse_dependencies x = 

258 
(parse_dependency ::: Scan.repeat ($$ ","  parse_dependency) 

259 
>> flat) x 

260 
and parse_file_source x = 

261 
(Scan.this_string "file"  $$ "("  scan_general_id 

262 
 Scan.option ($$ ","  scan_general_id)  $$ ")") x 

263 
and parse_inference_source x = 

264 
(Scan.this_string "inference"  $$ "("  scan_general_id 

265 
 skip_term  $$ ","  skip_term  $$ ","  $$ "[" 

266 
 parse_dependencies  $$ "]"  $$ ")") x 

267 
and parse_source x = 

268 
(parse_file_source >> File_Source 

269 
 parse_inference_source >> Inference_Source 

45235
7187bce94e88
more robust parsing of TSTP sources  Vampire has nonstandard "introduced()" tags and Waldmeister(OnTPTP) has weird "theory(...)" dependencies
blanchet
parents:
45209
diff
changeset

270 
 skip_term >> K dummy_inference) x 
39452  271 

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

272 
fun list_app (f, args) = 
48132
9aa0fad4e864
added type arguments to "ATerm" constructor  but don't use them yet
blanchet
parents:
48130
diff
changeset

273 
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

274 

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

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

277 
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

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

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

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

281 
 Scan.optional ($$ "("  parse_terms  $$ ")") [] 
48132
9aa0fad4e864
added type arguments to "ATerm" constructor  but don't use them yet
blanchet
parents:
48130
diff
changeset

282 
>> (ATerm o apfst (rpair []))) x 
45881  283 
and parse_term x = 
42968
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

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

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

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

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

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

290 
 parse_term) 
39598  291 
>> (fn (u1, NONE) => AAtom u1 
45881  292 
 (u1, SOME (neg, u2)) => 
48132
9aa0fad4e864
added type arguments to "ATerm" constructor  but don't use them yet
blanchet
parents:
48130
diff
changeset

293 
AAtom (ATerm (("equal", []), [u1, u2])) > is_some neg ? mk_anot)) x 
39452  294 

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

296 
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

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

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

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

300 
 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

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

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

303 
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

304 
(parse_literal 
43163  305 
 Scan.option ((Scan.this_string tptp_implies 
306 
 Scan.this_string tptp_iff 

307 
 Scan.this_string tptp_not_iff 

308 
 Scan.this_string tptp_if 

309 
 $$ tptp_or 

310 
 $$ tptp_and)  parse_formula) 

39452  311 
>> (fn (phi1, NONE) => phi1 
43163  312 
 (phi1, SOME (c, phi2)) => 
313 
if c = tptp_implies then mk_aconn AImplies phi1 phi2 

314 
else if c = tptp_iff then mk_aconn AIff phi1 phi2 

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

316 
else if c = tptp_if then mk_aconn AImplies phi2 phi1 

317 
else if c = tptp_or then mk_aconn AOr phi1 phi2 

318 
else if c = tptp_and then mk_aconn AAnd phi1 phi2 

319 
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

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

321 
(($$ 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

322 
 $$ "["  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

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

324 
(* We ignore TFF and THF types for now. *) 
48132
9aa0fad4e864
added type arguments to "ATerm" constructor  but don't use them yet
blanchet
parents:
48130
diff
changeset

325 
AQuant (q, map (fn ATerm ((s, []), _) => (s, NONE)) ts, phi))) x 
39452  326 

327 
val parse_tstp_extra_arguments = 

45235
7187bce94e88
more robust parsing of TSTP sources  Vampire has nonstandard "introduced()" tags and Waldmeister(OnTPTP) has weird "theory(...)" dependencies
blanchet
parents:
45209
diff
changeset

328 
Scan.optional ($$ ","  parse_source  Scan.option ($$ ","  skip_term)) 
7187bce94e88
more robust parsing of TSTP sources  Vampire has nonstandard "introduced()" tags and Waldmeister(OnTPTP) has weird "theory(...)" dependencies
blanchet
parents:
45209
diff
changeset

329 
dummy_inference 
39452  330 

47927
c35238d19bb9
repair the Waldmeister endgame only for Waldmeister proofs
blanchet
parents:
47926
diff
changeset

331 
val waldmeister_conjecture_name = "conjecture_1" 
42943  332 

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

334 

42943  335 
fun is_same_term subst tm1 tm2 = 
336 
let 

337 
fun do_term_pair _ NONE = NONE 

48132
9aa0fad4e864
added type arguments to "ATerm" constructor  but don't use them yet
blanchet
parents:
48130
diff
changeset

338 
 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

339 
case pairself is_tptp_variable (s1, s2) of 
42943  340 
(true, true) => 
341 
(case AList.lookup (op =) subst s1 of 

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

343 
 NONE => 

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

345 
else NONE) 

346 
 (false, false) => 

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

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

349 
else 

350 
NONE 

351 
 _ => NONE 

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

353 

47921
fc26d5538868
ensure the "show" equation is not reoriented by Waldmeister
blanchet
parents:
47917
diff
changeset

354 
fun is_same_formula comm subst (AQuant (q1, xs1, phi1)) (AQuant (q2, xs2, phi2)) = 
42943  355 
q1 = q2 andalso length xs1 = length xs2 andalso 
47921
fc26d5538868
ensure the "show" equation is not reoriented by Waldmeister
blanchet
parents:
47917
diff
changeset

356 
is_same_formula comm ((map fst xs1 ~~ map fst xs2) @ subst) phi1 phi2 
fc26d5538868
ensure the "show" equation is not reoriented by Waldmeister
blanchet
parents:
47917
diff
changeset

357 
 is_same_formula comm subst (AConn (c1, phis1)) (AConn (c2, phis2)) = 
42943  358 
c1 = c2 andalso length phis1 = length phis2 andalso 
47921
fc26d5538868
ensure the "show" equation is not reoriented by Waldmeister
blanchet
parents:
47917
diff
changeset

359 
forall (uncurry (is_same_formula comm subst)) (phis1 ~~ phis2) 
48132
9aa0fad4e864
added type arguments to "ATerm" constructor  but don't use them yet
blanchet
parents:
48130
diff
changeset

360 
 is_same_formula comm subst 
9aa0fad4e864
added type arguments to "ATerm" constructor  but don't use them yet
blanchet
parents:
48130
diff
changeset

361 
(AAtom (tm1 as ATerm (("equal", []), [tm11, tm12]))) (AAtom tm2) = 
47926  362 
is_same_term subst tm1 tm2 orelse 
48132
9aa0fad4e864
added type arguments to "ATerm" constructor  but don't use them yet
blanchet
parents:
48130
diff
changeset

363 
(comm andalso is_same_term subst (ATerm (("equal", []), [tm12, tm11])) tm2) 
47921
fc26d5538868
ensure the "show" equation is not reoriented by Waldmeister
blanchet
parents:
47917
diff
changeset

364 
 is_same_formula _ subst (AAtom tm1) (AAtom tm2) = is_same_term subst tm1 tm2 
fc26d5538868
ensure the "show" equation is not reoriented by Waldmeister
blanchet
parents:
47917
diff
changeset

365 
 is_same_formula _ _ _ _ = false 
42943  366 

50521
bec828f3364e
generate comments with original names for debugging
blanchet
parents:
50236
diff
changeset

367 
fun matching_formula_line_identifier phi (Formula ((ident, _), _, phi', _, _)) = 
47921
fc26d5538868
ensure the "show" equation is not reoriented by Waldmeister
blanchet
parents:
47917
diff
changeset

368 
if is_same_formula true [] phi phi' then SOME (ident, phi') else NONE 
42943  369 
 matching_formula_line_identifier _ _ = NONE 
370 

371 
fun find_formula_in_problem problem phi = 

372 
problem > maps snd > map_filter (matching_formula_line_identifier phi) 

45551  373 
> try (single o hd) > the_default [] 
42943  374 

48132
9aa0fad4e864
added type arguments to "ATerm" constructor  but don't use them yet
blanchet
parents:
48130
diff
changeset

375 
fun commute_eq (AAtom (ATerm ((s, []), tms))) = AAtom (ATerm ((s, []), rev tms)) 
47946
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
47927
diff
changeset

376 
 commute_eq _ = raise Fail "expected equation" 
47921
fc26d5538868
ensure the "show" equation is not reoriented by Waldmeister
blanchet
parents:
47917
diff
changeset

377 

50012
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50011
diff
changeset

378 
fun role_of_tptp_string "axiom" = Axiom 
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50011
diff
changeset

379 
 role_of_tptp_string "definition" = Definition 
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50011
diff
changeset

380 
 role_of_tptp_string "lemma" = Lemma 
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50011
diff
changeset

381 
 role_of_tptp_string "hypothesis" = Hypothesis 
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50011
diff
changeset

382 
 role_of_tptp_string "conjecture" = Conjecture 
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50011
diff
changeset

383 
 role_of_tptp_string "negated_conjecture" = Negated_Conjecture 
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50011
diff
changeset

384 
 role_of_tptp_string "plain" = Plain 
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50011
diff
changeset

385 
 role_of_tptp_string _ = Unknown 
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50011
diff
changeset

386 

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

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

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

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

392 
 Scan.this_string tptp_tff  Scan.this_string tptp_thf)  $$ "(") 
50236  393 
 scan_general_id  $$ ","  Symbol.scan_ascii_id  $$ "," 
45235
7187bce94e88
more robust parsing of TSTP sources  Vampire has nonstandard "introduced()" tags and Waldmeister(OnTPTP) has weird "theory(...)" dependencies
blanchet
parents:
45209
diff
changeset

394 
 (parse_formula  skip_term >> K dummy_phi)  parse_tstp_extra_arguments 
7187bce94e88
more robust parsing of TSTP sources  Vampire has nonstandard "introduced()" tags and Waldmeister(OnTPTP) has weird "theory(...)" dependencies
blanchet
parents:
45209
diff
changeset

395 
 $$ ")"  $$ "." 
42943  396 
>> (fn (((num, role), phi), deps) => 
397 
let 

47921
fc26d5538868
ensure the "show" equation is not reoriented by Waldmeister
blanchet
parents:
47917
diff
changeset

398 
val ((name, phi), rule, deps) = 
42943  399 
(* Waldmeister isn't exactly helping. *) 
400 
case deps of 

45208
9a00f9cc8707
marginally cleaner proof parsing, that doesn't stumble upon LEOII's Estep proofs
blanchet
parents:
45203
diff
changeset

401 
File_Source (_, SOME s) => 
47927
c35238d19bb9
repair the Waldmeister endgame only for Waldmeister proofs
blanchet
parents:
47926
diff
changeset

402 
(if s = waldmeister_conjecture_name then 
47921
fc26d5538868
ensure the "show" equation is not reoriented by Waldmeister
blanchet
parents:
47917
diff
changeset

403 
case find_formula_in_problem problem (mk_anot phi) of 
fc26d5538868
ensure the "show" equation is not reoriented by Waldmeister
blanchet
parents:
47917
diff
changeset

404 
(* Waldmeister hack: Get the original orientation of the 
fc26d5538868
ensure the "show" equation is not reoriented by Waldmeister
blanchet
parents:
47917
diff
changeset

405 
equation to avoid confusing Isar. *) 
fc26d5538868
ensure the "show" equation is not reoriented by Waldmeister
blanchet
parents:
47917
diff
changeset

406 
[(s, phi')] => 
fc26d5538868
ensure the "show" equation is not reoriented by Waldmeister
blanchet
parents:
47917
diff
changeset

407 
((num, [s]), 
47926  408 
phi > not (is_same_formula false [] (mk_anot phi) phi') 
47921
fc26d5538868
ensure the "show" equation is not reoriented by Waldmeister
blanchet
parents:
47917
diff
changeset

409 
? commute_eq) 
fc26d5538868
ensure the "show" equation is not reoriented by Waldmeister
blanchet
parents:
47917
diff
changeset

410 
 _ => ((num, []), phi) 
fc26d5538868
ensure the "show" equation is not reoriented by Waldmeister
blanchet
parents:
47917
diff
changeset

411 
else 
fc26d5538868
ensure the "show" equation is not reoriented by Waldmeister
blanchet
parents:
47917
diff
changeset

412 
((num, [s > perhaps (try (unprefix tofof_fact_prefix))]), 
fc26d5538868
ensure the "show" equation is not reoriented by Waldmeister
blanchet
parents:
47917
diff
changeset

413 
phi), 
fc26d5538868
ensure the "show" equation is not reoriented by Waldmeister
blanchet
parents:
47917
diff
changeset

414 
"", []) 
45208
9a00f9cc8707
marginally cleaner proof parsing, that doesn't stumble upon LEOII's Estep proofs
blanchet
parents:
45203
diff
changeset

415 
 File_Source _ => 
47921
fc26d5538868
ensure the "show" equation is not reoriented by Waldmeister
blanchet
parents:
47917
diff
changeset

416 
(((num, phi > find_formula_in_problem problem > map fst), 
fc26d5538868
ensure the "show" equation is not reoriented by Waldmeister
blanchet
parents:
47917
diff
changeset

417 
phi), "", []) 
fc26d5538868
ensure the "show" equation is not reoriented by Waldmeister
blanchet
parents:
47917
diff
changeset

418 
 Inference_Source (rule, deps) => (((num, []), phi), rule, deps) 
47787  419 
fun mk_step () = 
50012
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50011
diff
changeset

420 
Inference_Step (name, role_of_tptp_string role, phi, rule, 
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50011
diff
changeset

421 
map (rpair []) deps) 
42943  422 
in 
50012
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50011
diff
changeset

423 
case role_of_tptp_string role of 
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50011
diff
changeset

424 
Definition => 
42943  425 
(case phi of 
426 
AConn (AIff, [phi1 as AAtom _, phi2]) => 

47774  427 
Definition_Step (name, phi1, phi2) 
48132
9aa0fad4e864
added type arguments to "ATerm" constructor  but don't use them yet
blanchet
parents:
48130
diff
changeset

428 
 AAtom (ATerm (("equal", []), _)) => 
42943  429 
(* Vampire's equality proxy axiom *) 
50012
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50011
diff
changeset

430 
Inference_Step (name, Definition, phi, rule, 
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50011
diff
changeset

431 
map (rpair []) deps) 
47787  432 
 _ => mk_step ()) 
433 
 _ => mk_step () 

42943  434 
end) 
39452  435 

436 
(**** PARSING OF SPASS OUTPUT ****) 

437 

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

439 
is not clear anyway. *) 

440 
val parse_dot_name = scan_general_id  $$ "."  scan_general_id 

441 

442 
val parse_spass_annotations = 

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

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

445 

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

447 
pluses. We ignore them. *) 

39602  448 
fun parse_decorated_atom x = 
449 
(parse_atom  Scan.repeat ($$ "*"  $$ "+"  $$ " ")) x 

39452  450 

48132
9aa0fad4e864
added type arguments to "ATerm" constructor  but don't use them yet
blanchet
parents:
48130
diff
changeset

451 
fun mk_horn ([], []) = AAtom (ATerm (("c_False", []), [])) 
42943  452 
 mk_horn ([], pos_lits) = foldr1 (uncurry (mk_aconn AOr)) pos_lits 
453 
 mk_horn (neg_lits, []) = mk_anot (foldr1 (uncurry (mk_aconn AAnd)) neg_lits) 

39452  454 
 mk_horn (neg_lits, pos_lits) = 
42943  455 
mk_aconn AImplies (foldr1 (uncurry (mk_aconn AAnd)) neg_lits) 
456 
(foldr1 (uncurry (mk_aconn AOr)) pos_lits) 

39452  457 

39645  458 
fun parse_horn_clause x = 
459 
(Scan.repeat parse_decorated_atom  $$ ""  $$ "" 

460 
 Scan.repeat parse_decorated_atom  $$ ""  $$ ">" 

461 
 Scan.repeat parse_decorated_atom 

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

39452  463 

46390  464 
val parse_spass_debug = 
465 
Scan.option ($$ "("  Scan.repeat (scan_general_id  Scan.option ($$ ",")) 

466 
 $$ ")") 

467 

46427  468 
(* Syntax: <num>[0:<inference><annotations>] <atoms>  <atoms> > <atoms>. 
469 
derived from formulae <ident>* *) 

48005
eeede26f2721
killed SPASS 3.5/3.7 FLOTTER hack  requires users to upgrade to SPASS 3.8
blanchet
parents:
47972
diff
changeset

470 
fun parse_spass_line x = 
eeede26f2721
killed SPASS 3.5/3.7 FLOTTER hack  requires users to upgrade to SPASS 3.8
blanchet
parents:
47972
diff
changeset

471 
(parse_spass_debug  scan_general_id  $$ "["  $$ "0"  $$ ":" 
50236  472 
 Symbol.scan_ascii_id  parse_spass_annotations  $$ "]" 
48005
eeede26f2721
killed SPASS 3.5/3.7 FLOTTER hack  requires users to upgrade to SPASS 3.8
blanchet
parents:
47972
diff
changeset

473 
 parse_horn_clause  $$ "." 
eeede26f2721
killed SPASS 3.5/3.7 FLOTTER hack  requires users to upgrade to SPASS 3.8
blanchet
parents:
47972
diff
changeset

474 
 Scan.option (Scan.this_string "derived from formulae " 
eeede26f2721
killed SPASS 3.5/3.7 FLOTTER hack  requires users to upgrade to SPASS 3.8
blanchet
parents:
47972
diff
changeset

475 
 Scan.repeat (scan_general_id  Scan.option ($$ " "))) 
eeede26f2721
killed SPASS 3.5/3.7 FLOTTER hack  requires users to upgrade to SPASS 3.8
blanchet
parents:
47972
diff
changeset

476 
>> (fn ((((num, rule), deps), u), names) => 
50012
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50011
diff
changeset

477 
Inference_Step ((num, these names), Unknown, u, rule, 
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50011
diff
changeset

478 
map (rpair []) deps))) x 
45162  479 

48539  480 
val satallax_coreN = "__satallax_core" (* arbitrary *) 
481 
val z3_tptp_coreN = "__z3_tptp_core" (* arbitrary *) 

482 

483 
(* Syntax: core(<name>,[<name>,...,<name>]). *) 

484 
fun parse_z3_tptp_line x = 

485 
(scan_general_id  $$ ","  $$ "["  parse_dependencies  $$ "]" 

486 
>> (fn (name, names) => 

50012
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50011
diff
changeset

487 
Inference_Step (("", name :: names), Unknown, dummy_phi, 
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50011
diff
changeset

488 
z3_tptp_coreN, []))) x 
47947  489 

45162  490 
(* Syntax: <name> *) 
45203  491 
fun parse_satallax_line x = 
492 
(scan_general_id  Scan.option ($$ " ") 

50012
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50011
diff
changeset

493 
>> (fn s => Inference_Step ((s, [s]), Unknown, dummy_phi, satallax_coreN, 
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50011
diff
changeset

494 
[]))) x 
43481  495 

48005
eeede26f2721
killed SPASS 3.5/3.7 FLOTTER hack  requires users to upgrade to SPASS 3.8
blanchet
parents:
47972
diff
changeset

496 
fun parse_line problem = 
48539  497 
parse_tstp_line problem  parse_spass_line  parse_z3_tptp_line 
498 
 parse_satallax_line 

50590  499 
fun parse_proof problem = 
500 
strip_spaces_except_between_idents 

501 
#> raw_explode 

502 
#> Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ()) 

503 
(Scan.finite Symbol.stopper 

504 
(Scan.repeat1 (parse_line problem)))) 

505 
#> fst 

43481  506 

48130  507 
fun atp_proof_from_tstplike_proof _ "" = [] 
508 
 atp_proof_from_tstplike_proof problem tstp = 

43481  509 
tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *) 
48005
eeede26f2721
killed SPASS 3.5/3.7 FLOTTER hack  requires users to upgrade to SPASS 3.8
blanchet
parents:
47972
diff
changeset

510 
> parse_proof problem 
47972  511 
> sort (step_name_ord o pairself step_name) (* FIXME: needed? *) 
42968
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

512 

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

513 
fun clean_up_dependencies _ [] = [] 
47774  514 
 clean_up_dependencies seen 
515 
((step as Definition_Step (name, _, _)) :: steps) = 

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

516 
step :: clean_up_dependencies (name :: seen) steps 
50012
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50011
diff
changeset

517 
 clean_up_dependencies seen 
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50011
diff
changeset

518 
(Inference_Step (name, role, u, rule, deps) :: steps) = 
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50011
diff
changeset

519 
Inference_Step (name, role, u, rule, 
47774  520 
map_filter (fn dep => find_first (is_same_atp_step dep) seen) deps) :: 
42968
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

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

522 

42975  523 
fun clean_up_atp_proof_dependencies proof = clean_up_dependencies [] proof 
39452  524 

48132
9aa0fad4e864
added type arguments to "ATerm" constructor  but don't use them yet
blanchet
parents:
48130
diff
changeset

525 
fun map_term_names_in_term f (ATerm ((s, tys), ts)) = 
9aa0fad4e864
added type arguments to "ATerm" constructor  but don't use them yet
blanchet
parents:
48130
diff
changeset

526 
ATerm ((f s, tys), map (map_term_names_in_term f) ts) 
39454  527 
fun map_term_names_in_formula f (AQuant (q, xs, phi)) = 
528 
AQuant (q, xs, map_term_names_in_formula f phi) 

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

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

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

47774  532 
fun map_term_names_in_step f (Definition_Step (name, phi1, phi2)) = 
533 
Definition_Step (name, map_term_names_in_formula f phi1, 

534 
map_term_names_in_formula f phi2) 

50012
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50011
diff
changeset

535 
 map_term_names_in_step f (Inference_Step (name, role, phi, rule, deps)) = 
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50011
diff
changeset

536 
Inference_Step (name, role, map_term_names_in_formula f phi, rule, deps) 
39454  537 
fun map_term_names_in_atp_proof f = map (map_term_names_in_step f) 
538 

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

540 
fun nasty_atp_proof pool = 

541 
if Symtab.is_empty pool then I 

542 
else map_term_names_in_atp_proof (nasty_name pool) 

543 

39452  544 
end; 