158 if verbose then |
160 if verbose then |
159 if output = "" then "No details available" else elide_string 1000 output |
161 if output = "" then "No details available" else elide_string 1000 output |
160 else |
162 else |
161 "" |
163 "" |
162 |
164 |
|
165 fun from_lemmas [] = "" |
|
166 | from_lemmas ss = " from " ^ space_implode " " (Try.serial_commas "and" (map quote ss)) |
|
167 |
163 fun string_of_atp_failure MaybeUnprovable = "Problem maybe unprovable" |
168 fun string_of_atp_failure MaybeUnprovable = "Problem maybe unprovable" |
164 | string_of_atp_failure Unprovable = "Unprovable problem" |
169 | string_of_atp_failure Unprovable = "Problem unprovable" |
165 | string_of_atp_failure GaveUp = "Gave up" |
170 | string_of_atp_failure GaveUp = "Gave up" |
166 | string_of_atp_failure ProofMissing = "Proof missing" |
171 | string_of_atp_failure ProofMissing = "Proof missing" |
167 | string_of_atp_failure ProofIncomplete = "Proof incomplete" |
172 | string_of_atp_failure ProofIncomplete = "Proof incomplete" |
168 | string_of_atp_failure ProofUnparsable = "Proof unparsable" |
173 | string_of_atp_failure ProofUnparsable = "Proof unparsable" |
|
174 | string_of_atp_failure (UnsoundProof (false, ss)) = |
|
175 "Derived the lemma \"False\"" ^ from_lemmas ss ^ |
|
176 ", likely due to the use of an unsound type encoding" |
|
177 | string_of_atp_failure (UnsoundProof (true, ss)) = |
|
178 "Derived the lemma \"False\"" ^ from_lemmas ss ^ |
|
179 ", likely due to inconsistent axioms or \"sorry\"d lemmas" |
169 | string_of_atp_failure TimedOut = "Timed out" |
180 | string_of_atp_failure TimedOut = "Timed out" |
170 | string_of_atp_failure Inappropriate = "Problem outside the prover's scope" |
181 | string_of_atp_failure Inappropriate = "Problem outside the prover's scope" |
171 | string_of_atp_failure OutOfResources = "Out of resources" |
182 | string_of_atp_failure OutOfResources = "Out of resources" |
172 | string_of_atp_failure MalformedInput = "Malformed problem" |
183 | string_of_atp_failure MalformedInput = "Malformed problem" |
173 | string_of_atp_failure MalformedOutput = "Malformed output" |
184 | string_of_atp_failure MalformedOutput = "Malformed output" |