ftml_solver_trace/
results.rs

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

ftml_solver_trace/
results.rs
