1use std::marker::PhantomData;
2
3use ftml_ontology::terms::Term;
4use ftml_uris::{DocumentElementUri, DocumentUri, FtmlUri, ModuleUri, SymbolUri};
5use serde_json::de;
6
7use crate::CheckLog;
8
9#[cfg(feature = "colors")]
10use crate::ColorDisplay;
11#[cfg(feature = "full")]
12use crate::{FmtTraceDisplay, TraceDisplay};
13
14#[derive(Debug, Clone, serde::Serialize, serde::Deserialize)]
15pub struct DocumentCheckResult {
16 pub uri: DocumentUri,
17 pub checks: Box<[CheckResult]>,
18}
19impl DocumentCheckResult {
20 pub fn filter_failures(&mut self) {
21 self.checks = std::mem::take(&mut self.checks)
22 .into_iter()
23 .filter(|c| !c.success())
24 .map(|mut e| {
25 e.filter_failures();
26 e
27 })
28 .collect();
29 }
30 #[must_use]
31 pub fn to_json(&self) -> String {
32 let mut s = Vec::<u8>::new();
33 let mut serializer = serde_json::Serializer::new(&mut s);
34 let serializer = serde_stacker::Serializer::new(&mut serializer);
35 let _ = <Self as serde::Serialize>::serialize(self, serializer);
36 String::from_utf8(s).unwrap_or_default()
37 }
38 pub fn from_json(s: &str) -> Result<Self, String> {
40 let mut deserializer = serde_json::Deserializer::from_str(s);
41 deserializer.disable_recursion_limit();
42 let deserializer = serde_stacker::Deserializer::new(&mut deserializer);
43 <Self as serde::Deserialize>::deserialize(deserializer).map_err(|e| e.to_string())
44 }
45 #[cfg(feature = "full")]
46 #[must_use]
47 pub fn display<D: FmtTraceDisplay>(&self) -> impl std::fmt::Display + use<'_, D> {
48 struct Displayer<'a, D: FmtTraceDisplay>(&'a DocumentCheckResult, PhantomData<D>);
49 impl<D: FmtTraceDisplay> std::fmt::Display for Displayer<'_, D> {
50 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
51 let mut d = D::new(f);
52 d.string("Checking document ", Some(crate::MessageLevel::Header))?;
53 d.uri(self.0.uri.as_uri(), Some(crate::MessageLevel::Header))?;
54 d.string("\n", None)?;
55 drop(d);
56 for c in &self.0.checks {
57 c.display::<D>().fmt(f)?;
58 }
59 Ok(())
60 }
61 }
62
63 Displayer(self, PhantomData::<D>)
65 }
66
67 #[cfg(feature = "colors")]
68 #[must_use]
69 pub fn colored(&self) -> impl std::fmt::Display {
70 self.display::<ColorDisplay>()
71 }
72
73 pub fn success(&self) -> bool {
74 self.checks.iter().all(CheckResult::success)
75 }
76}
77
78#[allow(clippy::large_enum_variant)]
79#[derive(Debug, Clone, serde::Serialize, serde::Deserialize)]
80pub enum SymbolCheckResult {
81 TypeOnly {
82 result: TypeCheckResult,
83 },
84 DefiniensOnly {
85 inferred: Option<Term>,
86 log: CheckLog,
87 },
88 Both {
89 inhabitable: TypeCheckResult,
90 matches: Option<TypeCheckResult>,
91 },
92}
93impl SymbolCheckResult {
94 pub fn filter_failures(&mut self) {
95 match self {
96 Self::TypeOnly { result } => result.filter_failures(),
97 Self::DefiniensOnly { log, .. } => log.filter_failures(),
98 Self::Both {
99 inhabitable,
100 matches,
101 } => {
102 inhabitable.filter_failures();
103 if let Some(m) = matches {
104 m.filter_failures();
105 }
106 }
107 }
108 }
109 #[cfg(feature = "full")]
110 #[must_use]
111 pub fn display<D: FmtTraceDisplay>(&self) -> impl std::fmt::Display + use<'_, D> {
112 struct Displayer<'a, D: FmtTraceDisplay>(&'a SymbolCheckResult, PhantomData<D>);
113 impl<D: FmtTraceDisplay> std::fmt::Display for Displayer<'_, D> {
114 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
115 match self.0 {
116 SymbolCheckResult::TypeOnly { result } => result.display::<D>().fmt(f),
117 SymbolCheckResult::DefiniensOnly { log, .. } => log.display::<D>().fmt(f),
118 SymbolCheckResult::Both {
119 inhabitable,
120 matches,
121 } => {
122 inhabitable.display::<D>().fmt(f)?;
123 if let Some(r) = matches.as_ref() {
124 r.display::<D>().fmt(f)?;
125 }
126 Ok(())
127 }
128 }
129 }
130 }
131 Displayer(self, PhantomData::<D>)
132 }
133
134 #[cfg(feature = "colors")]
135 #[must_use]
136 pub fn colored(&self) -> impl std::fmt::Display {
137 self.display::<ColorDisplay>()
138 }
139 #[must_use]
140 pub fn success(&self) -> bool {
141 match self {
142 Self::TypeOnly { result } => result.success,
143 Self::DefiniensOnly { inferred, .. } => inferred.is_some(),
144 Self::Both {
145 inhabitable,
146 matches,
147 } => inhabitable.success && matches.as_ref().is_some_and(|r| r.success),
148 }
149 }
150}
151
152#[allow(clippy::large_enum_variant)]
153#[derive(Debug, Clone, serde::Serialize, serde::Deserialize)]
154pub enum CheckResult {
155 Module {
156 uri: ModuleUri,
157 checks: Vec<ContentCheckResult>,
158 },
159 Variable(DocumentElementUri, SymbolCheckResult),
160 Proof(DocumentElementUri, Vec<ProofStepResult>),
161 Term {
162 uri: DocumentElementUri,
163 inferred: Option<Term>,
164 log: CheckLog,
165 },
166 Content(ContentCheckResult),
167 Missing(ModuleUri),
168}
169impl CheckResult {
170 pub fn filter_failures(&mut self) {
171 match self {
172 Self::Module { checks, .. } => {
173 *checks = std::mem::take(checks)
174 .into_iter()
175 .filter(|c| !c.success())
176 .map(|mut c| {
177 c.filter_failures();
178 c
179 })
180 .collect();
181 }
182 Self::Variable(_, check) => check.filter_failures(),
183 Self::Proof(_, checks) => {
184 *checks = std::mem::take(checks)
185 .into_iter()
186 .filter(|c| !c.success())
187 .map(|mut c| {
188 c.filter_failures();
189 c
190 })
191 .collect();
192 }
193 Self::Term { log, .. } => log.filter_failures(),
194 Self::Content(check) => check.filter_failures(),
195 _ => (),
196 }
197 }
198 #[cfg(feature = "full")]
199 #[must_use]
200 pub fn display<D: FmtTraceDisplay>(&self) -> impl std::fmt::Display + use<'_, D> {
201 struct Displayer<'a, D: FmtTraceDisplay>(&'a CheckResult, PhantomData<D>);
202 impl<D: FmtTraceDisplay> std::fmt::Display for Displayer<'_, D> {
203 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
204 match self.0 {
205 CheckResult::Missing(u) => {
206 let mut d = D::new(f);
207 d.string("\nMissing module: ", Some(crate::MessageLevel::Failure))?;
208 d.uri(u.as_uri(), Some(crate::MessageLevel::Failure))?;
209 d.string("\n", None)
210 }
211 CheckResult::Module { uri, checks } => {
212 let mut d = D::new(f);
213 d.string("\nChecking module ", Some(crate::MessageLevel::Header))?;
214 d.uri(uri.as_uri(), Some(crate::MessageLevel::Header))?;
215 d.string("\n", None)?;
216 drop(d);
217 for c in checks {
218 c.display::<D>().fmt(f)?;
219 }
220 Ok(())
221 }
222 CheckResult::Variable(uri, r) => {
223 let mut d = D::new(f);
224 d.string("\nChecking variable ", Some(crate::MessageLevel::Header))?;
225 d.uri(uri.as_uri(), Some(crate::MessageLevel::Header))?;
226 d.string("\n", None)?;
227 drop(d);
228 r.display::<D>().fmt(f)
229 }
230 CheckResult::Term { uri, log, .. } => {
231 let mut d = D::new(f);
232 d.string("\nChecking term ", Some(crate::MessageLevel::Header))?;
233 d.uri(uri.as_uri(), Some(crate::MessageLevel::Header))?;
234 d.string("\n", None)?;
235 drop(d);
236 log.display::<D>().fmt(f)
237 }
238 CheckResult::Content(c) => c.display::<D>().fmt(f),
239 CheckResult::Proof(uri, checks) => {
240 let mut d = D::new(f);
241 d.string("\nChecking proof ", Some(crate::MessageLevel::Header))?;
242 d.uri(uri.as_uri(), Some(crate::MessageLevel::Header))?;
243 d.string("\n", None)?;
244 drop(d);
245 for c in checks {
246 c.display::<D>().fmt(f)?;
247 }
248 Ok(())
249 }
250 }
251 }
252 }
253
254 Displayer(self, PhantomData::<D>)
255 }
256 #[cfg(feature = "colors")]
257 #[must_use]
258 pub fn colored(&self) -> impl std::fmt::Display {
259 self.display::<ColorDisplay>()
260 }
261
262 pub fn success(&self) -> bool {
263 match self {
264 Self::Module { checks, .. } => checks.iter().all(ContentCheckResult::success),
265 Self::Variable(_, res) => res.success(),
266 Self::Term { inferred, .. } => inferred.is_some(),
267 Self::Missing(_) => false,
268 Self::Content(c) => c.success(),
269 Self::Proof(_, s) => s.iter().all(ProofStepResult::success),
270 }
271 }
272}
273
274#[allow(clippy::large_enum_variant)]
275#[derive(Debug, Clone, serde::Serialize, serde::Deserialize)]
276pub enum ProofStepResult {
277 Assumption {
278 var: Option<DocumentElementUri>,
279 result: ProofStepCheckResult,
280 },
281 Conclusion {
282 var: Option<DocumentElementUri>,
283 result: ProofStepCheckResult,
284 },
285 Step {
286 var: Option<DocumentElementUri>,
287 result: ProofStepCheckResult,
288 },
289 Subproof {
290 uri: DocumentElementUri,
291 var: Option<DocumentElementUri>,
292 results: Vec<Self>,
293 },
294}
295impl ProofStepResult {
296 pub fn filter_failures(&mut self) {
297 match self {
298 Self::Assumption { result, .. }
299 | Self::Conclusion { result, .. }
300 | Self::Step { result, .. } => result.filter_failures(),
301 Self::Subproof { results, .. } => {
302 *results = std::mem::take(results)
303 .into_iter()
304 .filter(|s| !s.success())
305 .map(|mut c| {
306 c.filter_failures();
307 c
308 })
309 .collect();
310 }
311 }
312 }
313 pub fn success(&self) -> bool {
314 match self {
315 Self::Assumption { result, .. }
316 | Self::Conclusion { result, .. }
317 | Self::Step { result, .. } => result.success(),
318 Self::Subproof { results, .. } => results.iter().all(Self::success),
319 }
320 }
321 #[cfg(feature = "full")]
322 #[must_use]
323 pub fn display<D: FmtTraceDisplay>(&self) -> impl std::fmt::Display + use<'_, D> {
324 struct Displayer<'a, D: FmtTraceDisplay>(&'a ProofStepResult, PhantomData<D>);
325 impl<D: FmtTraceDisplay> std::fmt::Display for Displayer<'_, D> {
326 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
327 let mut d = D::new(f);
328 match self.0 {
329 ProofStepResult::Assumption { var, result } => {
330 d.string("\nChecking Assumption ", Some(crate::MessageLevel::Header))?;
331 if let Some(var) = var {
332 d.uri(var.as_uri(), Some(crate::MessageLevel::Header))?;
333 }
334 d.string("\n", None)?;
335 drop(d);
336 result.display::<D>().fmt(f)
337 }
338 ProofStepResult::Conclusion { var, result } => {
339 d.string("\nChecking Conclusion ", Some(crate::MessageLevel::Header))?;
340 if let Some(var) = var {
341 d.uri(var.as_uri(), Some(crate::MessageLevel::Header))?;
342 }
343 d.string("\n", None)?;
344 drop(d);
345 result.display::<D>().fmt(f)
346 }
347 ProofStepResult::Step { var, result } => {
348 d.string("\nChecking Step ", Some(crate::MessageLevel::Header))?;
349 if let Some(var) = var {
350 d.uri(var.as_uri(), Some(crate::MessageLevel::Header))?;
351 }
352 d.string("\n", None)?;
353 drop(d);
354 result.display::<D>().fmt(f)
355 }
356 ProofStepResult::Subproof { uri, var, results } => {
357 d.string("\nChecking Subproof ", Some(crate::MessageLevel::Header))?;
358 d.uri(uri.as_uri(), Some(crate::MessageLevel::Header))?;
359 if let Some(var) = var {
360 d.string(" = ", Some(crate::MessageLevel::Header))?;
361 d.uri(var.as_uri(), Some(crate::MessageLevel::Header))?;
362 }
363 d.string("\n", None)?;
364 drop(d);
365 for r in results {
366 r.display::<D>().fmt(f)?;
367 }
368 Ok(())
369 }
370 }
371 }
372 }
373
374 Displayer(self, PhantomData::<D>)
375 }
376 #[cfg(feature = "colors")]
377 #[must_use]
378 pub fn colored(&self) -> impl std::fmt::Display {
379 self.display::<ColorDisplay>()
380 }
381}
382
383#[derive(Debug, Clone, serde::Serialize, serde::Deserialize)]
384pub enum ContentCheckResult {
385 Symbol(SymbolUri, SymbolCheckResult),
386}
387impl ContentCheckResult {
388 pub fn filter_failures(&mut self) {
389 match self {
390 Self::Symbol(_, check) => check.filter_failures(),
391 }
392 }
393 #[cfg(feature = "full")]
394 #[must_use]
395 pub fn display<D: FmtTraceDisplay>(&self) -> impl std::fmt::Display + use<'_, D> {
396 struct Displayer<'a, D: FmtTraceDisplay>(&'a ContentCheckResult, PhantomData<D>);
397 impl<D: FmtTraceDisplay> std::fmt::Display for Displayer<'_, D> {
398 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
399 let mut d = D::new(f);
400 match self.0 {
401 ContentCheckResult::Symbol(uri, s) => {
402 d.string("\nChecking symbol ", Some(crate::MessageLevel::Header))?;
403 d.uri(uri.as_uri(), Some(crate::MessageLevel::Header))?;
404 d.string("\n", None)?;
405 drop(d);
406 s.display::<D>().fmt(f)
407 }
408 }
409 }
410 }
411
412 Displayer(self, PhantomData::<D>)
413 }
414 #[cfg(feature = "colors")]
415 #[must_use]
416 pub fn colored(&self) -> impl std::fmt::Display {
417 self.display::<ColorDisplay>()
418 }
419 #[must_use]
420 pub fn success(&self) -> bool {
421 match self {
422 Self::Symbol(_, r) => r.success(),
423 }
424 }
425}
426
427#[derive(Debug, Clone, serde::Serialize, serde::Deserialize)]
428pub struct TypeCheckResult {
429 pub success: bool,
430 pub log: CheckLog,
431}
432impl TypeCheckResult {
433 pub fn filter_failures(&mut self) {
434 self.log.filter_failures();
435 }
436 #[cfg(feature = "full")]
437 #[must_use]
438 pub fn display<D: FmtTraceDisplay>(&self) -> impl std::fmt::Display + use<'_, D> {
439 self.log.display::<D>()
440 }
441 #[cfg(feature = "colors")]
442 #[must_use]
443 pub fn colored(&self) -> impl std::fmt::Display {
444 self.display::<ColorDisplay>()
445 }
446}
447
448#[allow(clippy::large_enum_variant)]
449#[derive(Debug, Clone, serde::Serialize, serde::Deserialize)]
450pub enum ProofStepCheckResult {
451 GoalOnly {
452 result: TypeCheckResult,
453 },
454 ProofOnly {
455 inferred: Option<Term>,
456 log: CheckLog,
457 },
458 Both {
459 inhabitable: TypeCheckResult,
460 matches: Option<TypeCheckResult>,
461 },
462}
463impl ProofStepCheckResult {
464 pub fn filter_failures(&mut self) {
465 match self {
466 Self::GoalOnly { result } => result.filter_failures(),
467 Self::ProofOnly { log, .. } => log.filter_failures(),
468 Self::Both {
469 inhabitable,
470 matches,
471 } => {
472 inhabitable.filter_failures();
473 if let Some(m) = matches {
474 m.filter_failures();
475 }
476 }
477 }
478 }
479 #[cfg(feature = "full")]
480 #[must_use]
481 pub fn display<D: FmtTraceDisplay>(&self) -> impl std::fmt::Display + use<'_, D> {
482 struct Displayer<'a, D: FmtTraceDisplay>(&'a ProofStepCheckResult, PhantomData<D>);
483 impl<D: FmtTraceDisplay> std::fmt::Display for Displayer<'_, D> {
484 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
485 match self.0 {
486 ProofStepCheckResult::GoalOnly { result } => result.display::<D>().fmt(f),
487 ProofStepCheckResult::ProofOnly { log, .. } => log.display::<D>().fmt(f),
488 ProofStepCheckResult::Both {
489 inhabitable,
490 matches,
491 } => {
492 inhabitable.display::<D>().fmt(f)?;
493 if let Some(r) = matches.as_ref() {
494 r.display::<D>().fmt(f)?;
495 }
496 Ok(())
497 }
498 }
499 }
500 }
501 Displayer(self, PhantomData::<D>)
502 }
503
504 #[cfg(feature = "colors")]
505 #[must_use]
506 pub fn colored(&self) -> impl std::fmt::Display {
507 self.display::<ColorDisplay>()
508 }
509 #[must_use]
510 pub fn success(&self) -> bool {
511 match self {
512 Self::GoalOnly { result } => result.success,
513 Self::ProofOnly { inferred, .. } => inferred.is_some(),
514 Self::Both {
515 inhabitable,
516 matches,
517 } => inhabitable.success && matches.as_ref().is_some_and(|r| r.success),
518 }
519 }
520}