ftml_solver_trace/
lib.rs

1pub mod results;
2
3use ftml_ontology::terms::{ComponentVar, Term, Variable};
4use ftml_uris::{FtmlUri, Uri, UriRef};
5#[cfg(feature = "colors")]
6use owo_colors::OwoColorize;
7use std::borrow::Cow;
8use std::{fmt::Write, marker::PhantomData};
9
10#[cfg(feature = "full")]
11pub trait CheckerRule: std::fmt::Debug + Send + Sync + std::any::Any {
12    fn priority(&self) -> isize {
13        0
14    }
15    fn display(&self) -> Vec<Displayable>;
16    fn as_box_dyn(&self) -> Box<dyn CheckerRule>;
17    fn as_dyn(&self) -> &dyn CheckerRule;
18    fn as_any(&self) -> &dyn std::any::Any;
19    fn eq(&self, o: &dyn CheckerRule) -> bool;
20}
21
22#[cfg(feature = "full")]
23pub trait SizedSolverRule:
24    std::fmt::Debug + Send + Sync + std::any::Any + Clone + Sized + PartialEq + Eq
25{
26    fn priority(&self) -> isize {
27        0
28    }
29    fn display(&self) -> Vec<Displayable>;
30}
31
32#[cfg(feature = "full")]
33impl<T: SizedSolverRule> CheckerRule for T {
34    #[allow(clippy::inline_always)]
35    #[inline(always)]
36    fn priority(&self) -> isize {
37        <Self as SizedSolverRule>::priority(self)
38    }
39
40    #[inline]
41    fn display(
42        &self,
43        //f: &mut std::fmt::Formatter,
44    ) -> Vec<Displayable> {
45        <T as SizedSolverRule>::display(self)
46    }
47
48    fn as_box_dyn(&self) -> Box<dyn CheckerRule> {
49        Box::new(self.clone()) as _
50    }
51    fn as_dyn(&self) -> &dyn CheckerRule {
52        self as _
53    }
54    fn as_any(&self) -> &dyn std::any::Any {
55        self as _
56    }
57    fn eq(&self, o: &dyn CheckerRule) -> bool {
58        o.as_any().downcast_ref::<T>().is_some_and(|v| v == self)
59    }
60}
61
62#[cfg(feature = "full")]
63#[derive(Debug, Copy, Clone, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
64pub enum MessageLevel {
65    Failure,
66    Comment,
67    Header,
68    Emph,
69}
70
71#[cfg(feature = "full")]
72#[derive(Clone, Copy, Default)]
73pub struct Indent(pub usize);
74#[cfg(feature = "full")]
75impl Indent {
76    pub const fn increase(&mut self) {
77        self.0 += 1;
78    }
79    pub const fn decrease(&mut self) {
80        self.0 = self.0.saturating_sub(1);
81    }
82}
83#[cfg(feature = "full")]
84impl std::fmt::Display for Indent {
85    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
86        if self.0 == 0 {
87            return Ok(());
88        }
89        for _ in 0..self.0 - 1 {
90            f.write_str("  │")?;
91        }
92        f.write_str("  ├─")?;
93        Ok(())
94    }
95}
96
97#[cfg(feature = "full")]
98#[derive(Debug)]
99pub enum CheckLogCow<'t> {
100    Owned(PreCheckLog),
101    Borrowed(RefCheckLog<'t>),
102}
103#[cfg(feature = "full")]
104impl<'t> From<RefCheckLog<'t>> for CheckLogCow<'t> {
105    #[inline]
106    fn from(value: RefCheckLog<'t>) -> Self {
107        Self::Borrowed(value)
108    }
109}
110#[cfg(feature = "full")]
111impl From<PreCheckLog> for CheckLogCow<'_> {
112    #[inline]
113    fn from(value: PreCheckLog) -> Self {
114        Self::Owned(value)
115    }
116}
117
118macro_rules! tasks {
119    (
120        $(
121            $name:ident($($field:ident : $tp:ident),*) => $res:tt
122        ),* $(,)?
123    ) => {
124
125        #[cfg(feature = "full")]
126        #[derive(Debug)]
127        pub enum RefCheckLog<'t> {
128            $(
129                $name {
130                    $($field: tasks!(@TPBORROW $tp),)*
131                    steps:Box<[CheckLogCow<'t>]>,
132                    context: Box<[Cow<'t, ComponentVar>]>,
133                    result: Option<$res>,
134                },
135            )*
136            Rule{
137                rule: &'t dyn CheckerRule,
138                steps:Box<[CheckLogCow<'t>]>,
139            },
140            Strategy{
141                name: &'static str,
142                steps:Box<[CheckLogCow<'t>]>,
143                success:bool
144            },
145            Msg(Vec<DisplayableRef<'t>>, MessageLevel),
146        }
147        #[cfg(feature = "full")]
148        impl RefCheckLog<'_> {
149            pub fn into_owned(self,term:&impl Fn(Term) -> Term) -> PreCheckLog {
150                match self {
151                    $(
152                        Self::$name{$($field,)* steps,context,result} => PreCheckLog::$name{
153                            $($field:tasks!(@CONV $tp $field term),)*
154                            steps: steps.into_iter().map(|t| CheckLogCow::into_owned(t,term)).collect(),
155                            context: context.into_iter().map(Cow::into_owned).collect(),
156                            result,
157
158                        },
159                    )*
160                    Self::Msg(txt,lvl) => PreCheckLog::Msg(txt.into_iter().map(|s| s.into_owned(term)).collect(),lvl),
161                    Self::Rule{rule,steps} => PreCheckLog::Rule{
162                        rule:rule.as_box_dyn(),
163                        steps: steps.into_iter().map(|t| CheckLogCow::into_owned(t,term)).collect(),
164                    },
165                    Self::Strategy{name,steps,success} => PreCheckLog::Strategy{
166                        name,
167                        steps: steps.into_iter().map(|t| CheckLogCow::into_owned(t,term)).collect(),
168                        success
169                    }
170                }
171            }
172        }
173        #[cfg(feature = "full")]
174        #[derive(Debug)]
175        pub enum PreCheckLog {
176            $(
177                $name {
178                    $($field: tasks!(@TPOWN $tp),)*
179                    steps:Vec<Self>,
180                    context:Box<[ComponentVar]>,
181                    result:Option<$res>
182                },
183            )*
184            Rule{
185                rule:Box<dyn CheckerRule>,
186                steps:Vec<Self>,
187            },
188            Strategy{
189                name: &'static str,
190                steps:Vec<Self>,
191                success:bool
192            },
193            //Dyn(Box<dyn CheckTraceDisplayable>)
194            Msg(Vec<Displayable>, MessageLevel),
195            //Count(&'static str,usize)
196            //Interpolated(Box<[DisplayableElem]>, MessageLevel),
197        }
198
199        #[cfg(feature = "full")]
200        impl CheckLog {
201            pub fn from_pre(v:PreCheckLog,terms:&mut impl FnMut(Term) -> Term) -> Self {
202                use PreCheckLog as P;
203                match v {
204                    $(
205                        P::$name{
206                            $($field,)*steps,context,result
207                        } => Self::$name{
208                            $( $field:tasks!(@FROMPRE $tp $field terms),)*
209                            context,result:result.map(|r| tasks!(@FROMPRE $res r terms)),
210                            steps:steps.into_iter().map(|e| Self::from_pre(e,terms)).collect()
211                        },
212                    )*
213                    P::Rule{ rule, steps } => Self::Rule {
214                        header:Displayable::map(rule.display(),terms),
215                        steps:steps.into_iter().map(|e| Self::from_pre(e,terms)).collect()
216                    },
217                    P::Strategy{ name, steps, success } => Self::Strategy {
218                        name:name.to_string(),
219                        steps:steps.into_iter().map(|e| Self::from_pre(e,terms)).collect(),
220                        success
221                    },
222                    P::Msg(s, MessageLevel::Comment) => Self::Comment(s),
223                    P::Msg(s, MessageLevel::Emph) => Self::Emph(s),
224                    P::Msg(s, MessageLevel::Header) => Self::Header(s),
225                    P::Msg(s, MessageLevel::Failure) => Self::Fail(s),
226                    //P::Count(s, u) =>
227                    //    Self::Comment(format!("{s} {u}"))
228                }
229            }
230        }
231        #[cfg(feature = "full")]
232        impl<'t> CheckingTask<'t> {
233            pub fn close<R:Clone>(self,res:Option<&R>,steps:Box<[CheckLogCow<'t>]>,context:&[Cow<'t,ComponentVar>]) -> RefCheckLog<'t> {
234                let context = context.iter().map(Cow::clone).collect();
235                match self {
236                    $(
237                        Self::$name( $($field),* ) => RefCheckLog::$name {
238                            $($field,)*
239                            steps,
240                            context,
241                            result: res.map(|r| unsafe{&*std::ptr::from_ref(r).cast::<$res>()}.clone() )
242                        },
243                    )*
244                    Self::Strategy(name) => RefCheckLog::Strategy {
245                        name,
246                        steps,success:res.is_some_and(|v| {
247                            if std::mem::size_of::<R>() == 1 {
248                                // SAFETY: => boolean
249                                unsafe{
250                                    std::mem::transmute_copy::<R,bool>(v)
251                                }
252                            } else {
253                                true
254                            }
255                        })
256                    },
257                    Self::Rule(rule) => RefCheckLog::Rule { rule, steps }
258                }
259            }
260        }
261        #[cfg(feature = "full")]
262        impl<'t> CheckLogCow<'t> {
263            pub fn into_owned(self,term:&impl Fn(Term) -> Term) -> PreCheckLog {
264                match self {
265                    Self::Owned(o) => o,
266                    Self::Borrowed(b) => b.into_owned(term)
267                }
268            }
269        }
270
271        #[cfg(feature = "full")]
272        #[derive(Copy,Clone,Debug)]
273        pub enum CheckingTask<'t> {
274            $(
275                $name($(tasks!(@TPBORROW $tp)),*)
276            ),*,
277            Rule(&'t dyn CheckerRule),
278            Strategy(&'static str),
279        }
280
281        #[derive(Debug, serde::Serialize, serde::Deserialize, Clone)]
282        pub enum CheckLog {
283            $(
284                $name {
285                    $($field: tasks!(@TPOWN $tp),)*
286                    steps:Vec<Self>,
287                    context:Box<[ComponentVar]>,
288                    result:Option<$res>
289                },
290            )*
291            Comment(Vec<Displayable>),
292            Emph(Vec<Displayable>),
293            Header(Vec<Displayable>),
294            Fail(Vec<Displayable>),
295            Strategy {
296                name: String,
297                steps: Vec<Self>,
298                success: bool,
299            },
300            Rule {
301                header: Vec<Displayable>,
302                steps: Vec<Self>,
303            },
304        }
305        #[cfg(feature = "full")]
306        impl CheckLog {
307            pub(crate) fn display_i(&self,displayer:&mut impl TraceDisplay) -> std::fmt::Result {
308                let mut curr = std::slice::from_ref(self).iter();
309                let mut stack = Vec::new();
310                let mut indent = Indent::default();
311                loop {
312                    while let Some(next) = curr.next() {
313                        if displayer.line(next,indent)? == std::ops::ControlFlow::Continue(()) {
314                            match next {
315                                $(
316                                    Self::$name{ $($field,)* steps, context,result } => {
317                                        displayer.task(CheckingTask::$name($($field),*),context,result.is_some())?;
318                                        tasks!(@DISPL result displayer $res);
319                                        indent.increase();
320                                        stack.push(std::mem::replace(&mut curr,steps.iter()));
321                                    }
322                                )*
323                                Self::Rule{header,steps} => {
324                                    for e in header {
325                                        displayer.displayable(e,None)?;
326                                    }
327                                    indent.increase();
328                                    stack.push(std::mem::replace(&mut curr,steps.iter()));
329                                }
330                                Self::Strategy{name,steps,success} => {
331                                    displayer.strategy(name,&[],*success)?;
332                                    indent.increase();
333                                    stack.push(std::mem::replace(&mut curr,steps.iter()));
334                                }
335                                Self::Comment(s) => {
336                                    for s in s {
337                                        displayer.displayable(s,Some(MessageLevel::Comment))?;
338                                    }
339                                }
340                                Self::Emph(s) => {
341                                    for s in s {
342                                        displayer.displayable(s,Some(MessageLevel::Emph))?;
343                                    }
344                                }
345                                Self::Header(s) => {
346                                    for s in s {
347                                        displayer.displayable(s,Some(MessageLevel::Header))?;
348                                    }
349                                }
350                                Self::Fail(s) => {
351                                    for s in s {
352                                        displayer.displayable(s,Some(MessageLevel::Failure))?;
353                                    }
354                                }
355                            }
356                        }
357                    }
358                    if let Some(next) = stack.pop() {
359                        indent.decrease();
360                        curr = next;
361                    } else {
362                        break
363                    }
364                }
365                Ok(())
366            }
367        }
368
369    };
370    (@DISPL $res:ident $disp:ident Term) => {
371        if let Some(t) = $res {
372            $disp.string(": ",None)?;
373            $disp.term(t,None)?;
374        }
375    };
376    (@DISPL $res:ident $disp:ident bool) => {};
377    (@TPBORROW Term) => {&'t Term};
378    (@TPOWN Term) => {Term};
379    (@TPBORROW str) => {&'t str};
380    (@TPOWN str) => {Box<str>};
381    (@FROMPRE Term $name:ident $f:ident) => {$f($name)};
382    (@FROMPRE str $name:ident $f:ident) => {$name};
383    (@FROMPRE bool $name:ident $f:ident) => {$name};
384    (@CONV Term $name:ident $f:ident) => {$name.clone()};//{ $f($name.clone()) };
385    (@CONV str $name:ident $f:ident) => { $name.to_string().into_boxed_str() };
386    //(@TPBORROW SolverRule) => {&'t dyn SolverRule};
387    //(@TPOWN SolverRule) => {Box<dyn SolverRule>};
388    (@CONV SolverRule $name:ident $f:ident) => { $name.as_box_dyn() };
389}
390
391#[cfg(feature = "full")]
392impl PreCheckLog {
393    pub fn push(&mut self, msg: Self) {
394        if let Some(steps) = self.steps_mut() {
395            steps.push(msg);
396        }
397    }
398    pub const fn steps_mut(&mut self) -> Option<&mut Vec<Self>> {
399        match self {
400            Self::Equality { steps, .. }
401            | Self::HasType { steps, .. }
402            | Self::Inference { steps, .. }
403            | Self::Inhabitable { steps, .. }
404            | Self::Rule { steps, .. }
405            | Self::Simplify { steps, .. }
406            | Self::Strategy { steps, .. }
407            | Self::Subtype { steps, .. }
408            | Self::Universe { steps, .. }
409            | Self::VariableInference { steps, .. }
410            | Self::Proving { steps, .. } => Some(steps),
411            Self::Msg(_, _) /*| Self::Count(_, _)*/ => None,
412        }
413    }
414}
415
416impl CheckLog {
417    pub fn filter_failures(&mut self) {
418        let Some(steps) = self.steps_mut() else {
419            return;
420        };
421        *steps = std::mem::take(steps)
422            .into_iter()
423            .filter(|s| !s.success())
424            .map(|mut s| {
425                s.filter_failures();
426                s
427            })
428            .collect();
429    }
430    pub const fn steps_mut(&mut self) -> Option<&mut Vec<Self>> {
431        match self {
432            Self::Equality { steps, .. }
433            | Self::HasType { steps, .. }
434            | Self::Inference { steps, .. }
435            | Self::Inhabitable { steps, .. }
436            | Self::Rule { steps, .. }
437            | Self::Simplify { steps, .. }
438            | Self::Strategy { steps, .. }
439            | Self::Subtype { steps, .. }
440            | Self::Universe { steps, .. }
441            | Self::VariableInference { steps, .. }
442            | Self::Proving { steps, .. } => Some(steps),
443            Self::Comment(_) | Self::Emph(_) | Self::Header(_) | Self::Fail(_) => None,
444        }
445    }
446    pub fn success(&self) -> bool {
447        match self {
448            Self::Equality { result, .. }
449            | Self::HasType { result, .. }
450            | Self::Inhabitable { result, .. }
451            | Self::Subtype { result, .. }
452            | Self::Universe { result, .. } => *result == Some(true),
453            Self::Rule { steps, .. } => steps.iter().all(Self::success),
454            Self::Inference { result, .. }
455            | Self::VariableInference { result, .. }
456            | Self::Simplify { result, .. }
457            | Self::Proving { result, .. } => result.is_some(),
458            Self::Strategy { success, .. } => *success,
459            Self::Comment(_) | Self::Header(_) | Self::Emph(_) | Self::Fail(_) => false,
460        }
461    }
462    pub fn add_failure(&mut self, s: &'static str) {
463        if let Some(steps) = self.steps_mut() {
464            steps.push(Self::Fail(vec![s.to_string().into()]));
465        }
466    }
467}
468
469#[cfg(feature = "full")]
470#[derive(Debug, Clone)]
471pub enum DisplayableRef<'r> {
472    Num(i128),
473    //Space,
474    String(Cow<'static, str>),
475    Term(Cow<'r, Term>),
476    Uri(either::Either<UriRef<'r>, Uri>),
477    Var(Cow<'r, Variable>),
478}
479#[cfg(feature = "full")]
480impl DisplayableRef<'_> {
481    pub fn into_owned(self, term: &impl Fn(Term) -> Term) -> Displayable {
482        match self {
483            Self::Num(i) => Displayable::Num(i),
484            Self::String(s) => Displayable::String(s.to_string()),
485            Self::Term(t) => Displayable::Term(term(t.into_owned())),
486            Self::Uri(u) => Displayable::Uri(match u {
487                either::Left(u) => u.owned(),
488                either::Right(u) => u,
489            }),
490            Self::Var(v) => Displayable::Var(v.into_owned()),
491        }
492    }
493}
494
495#[allow(clippy::large_enum_variant)]
496#[derive(Debug, serde::Serialize, serde::Deserialize, Clone)]
497pub enum Displayable {
498    //Log(CheckLog),
499    Num(i128),
500    //Space,
501    String(String),
502    Term(Term),
503    Uri(Uri),
504    Var(Variable),
505}
506impl Displayable {
507    fn map(v: Vec<Self>, terms: &mut impl FnMut(Term) -> Term) -> Vec<Self> {
508        v.into_iter()
509            .map(|e| {
510                if let Self::Term(t) = e {
511                    Self::Term(terms(t))
512                } else {
513                    e
514                }
515            })
516            .collect()
517    }
518}
519
520tasks! {
521    Simplify(term:Term) => Term,
522    Proving(term:Term) => Term,
523    Inference(term: Term) => Term,
524    VariableInference(var: str) => Term,
525    //Simplify(term:Term) => Term,
526    Inhabitable(term: Term) => bool,
527    Universe(term:Term) => bool,
528    Subtype(sub:Term,sup:Term) => bool,
529    HasType(tm:Term,tp:Term) => bool,
530    Equality(lhs:Term,rhs:Term) => bool,
531}
532
533#[cfg(feature = "full")]
534impl CheckLog {
535    #[must_use]
536    pub fn display<D: FmtTraceDisplay>(&self) -> impl std::fmt::Display + use<'_, D> {
537        TraceDisplayer::<'_, D> {
538            trace: self,
539            d: PhantomData,
540        }
541    }
542    #[cfg(feature = "colors")]
543    #[must_use]
544    pub fn colored(&self) -> impl std::fmt::Display {
545        TraceDisplayer {
546            d: PhantomData::<ColorDisplay>,
547            trace: self,
548        }
549    }
550}
551#[cfg(feature = "full")]
552impl std::fmt::Display for CheckLog {
553    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
554        self.display::<()>().fmt(f)
555    }
556}
557
558#[cfg(feature = "full")]
559pub trait FmtTraceDisplay {
560    fn new(f: &mut std::fmt::Formatter<'_>) -> impl TraceDisplay;
561}
562
563#[cfg(feature = "full")]
564pub trait TraceDisplay {
565    // /// ### Errors
566    //fn rule(&mut self, rule: &dyn CheckerRule) -> std::fmt::Result;
567
568    /// ### Errors
569    fn displayable(&mut self, d: &Displayable, lvl: Option<MessageLevel>) -> std::fmt::Result {
570        match d {
571            Displayable::Num(i) => self.num(*i, lvl),
572            //Displayable::Space => self.space(),
573            Displayable::String(s) => self.string(s, lvl),
574            Displayable::Term(t) => self.term(t, lvl),
575            Displayable::Uri(u) => self.uri(u.as_uri(), lvl),
576            Displayable::Var(v) => self.variable(v, lvl),
577        }
578    }
579
580    /// ### Errors
581    fn line(
582        &mut self,
583        _: &CheckLog,
584        indent: Indent,
585    ) -> Result<std::ops::ControlFlow<()>, std::fmt::Error>; /* {
586    f.write_char('\n')?;
587    self.indent(indent, None, f)?;
588    Ok(std::ops::ControlFlow::Continue(()))
589    }*/
590
591    /// ### Errors
592    fn task(
593        &mut self,
594        task: CheckingTask<'_>,
595        context: &[ComponentVar],
596        success: bool,
597    ) -> std::fmt::Result;
598
599    /// ### Errors
600    fn strategy(&mut self, name: &str, context: &[ComponentVar], success: bool)
601    -> std::fmt::Result;
602
603    /// ### Errors
604    fn uri(&mut self, uri: ftml_uris::UriRef, lvl: Option<MessageLevel>) -> std::fmt::Result;
605
606    /// ### Errors
607    fn term(&mut self, term: &Term, lvl: Option<MessageLevel>) -> std::fmt::Result;
608
609    /// ### Errors
610    fn string(&mut self, s: &str, lvl: Option<MessageLevel>) -> std::fmt::Result;
611
612    /// ### Errors
613    fn variable(&mut self, var: &Variable, lvl: Option<MessageLevel>) -> std::fmt::Result;
614
615    /// ### Errors
616    fn num(&mut self, num: i128, lvl: Option<MessageLevel>) -> std::fmt::Result;
617
618    /// ### Errors
619    fn indent(&mut self, indent: Indent, lvl: Option<MessageLevel>) -> std::fmt::Result;
620
621    /// ### Errors
622    fn space(&mut self) -> std::fmt::Result;
623}
624#[cfg(feature = "full")]
625impl FmtTraceDisplay for () {
626    #[allow(clippy::inline_always)]
627    #[inline(always)]
628    fn new(f: &mut std::fmt::Formatter<'_>) -> impl TraceDisplay {
629        f
630    }
631}
632#[cfg(feature = "full")]
633impl TraceDisplay for &mut std::fmt::Formatter<'_> {
634    fn line(
635        &mut self,
636        _: &CheckLog,
637        indent: Indent,
638        //f: &mut std::fmt::Formatter<'_>,
639    ) -> Result<std::ops::ControlFlow<()>, std::fmt::Error> {
640        self.write_char('\n')?;
641        self.indent(indent, None)?;
642        Ok(std::ops::ControlFlow::Continue(()))
643    }
644    fn space(&mut self) -> std::fmt::Result {
645        self.write_char(' ')
646    }
647    /*
648    fn rule(&mut self, rule: &dyn CheckerRule) -> std::fmt::Result {
649        self.write_str("Using rule: ")?;
650        rule.display(self, None)
651    }
652     */
653
654    fn strategy(&mut self, name: &str, _: &[ComponentVar], _: bool) -> std::fmt::Result {
655        write!(self, "Strategy: {name}")
656    }
657    fn task(
658        &mut self,
659        task: CheckingTask<'_>,
660        context: &[ComponentVar],
661        success: bool,
662        //f: &mut std::fmt::Formatter<'_>,
663    ) -> std::fmt::Result {
664        fn do_context(
665            context: &[ComponentVar],
666            mut f: &mut std::fmt::Formatter<'_>,
667        ) -> std::fmt::Result {
668            if context.is_empty() {
669                return Ok(());
670            }
671            f.write_str("{... ")?;
672            let mut first = true;
673            for ComponentVar { var, tp, df } in context {
674                if first {
675                    first = false;
676                } else {
677                    f.write_str(", ")?;
678                }
679                f.variable(var, None)?;
680                if let Some(tp) = tp {
681                    f.write_str(" : ")?;
682                    f.term(tp, None)?;
683                }
684                if let Some(df) = df {
685                    f.write_str(" : ")?;
686                    f.term(df, None)?;
687                }
688            }
689            f.write_str(" } ")
690        }
691        if success {
692            self.write_str("[SUCCESS] ")?;
693        } else {
694            self.write_str("[FAILED] ")?;
695        }
696        match task {
697            CheckingTask::Simplify(t) => {
698                self.write_str("Simplifying ")?;
699                do_context(context, self)?;
700                self.term(t, None)
701            }
702            CheckingTask::Proving(t) => {
703                self.write_str("Proving ")?;
704                do_context(context, self)?;
705                self.term(t, None)
706            }
707            CheckingTask::Inference(t) => {
708                self.write_str("Inferring type of ")?;
709                do_context(context, self)?;
710                self.term(t, None)
711            }
712            CheckingTask::VariableInference(t) => {
713                self.write_str("Inferring type of variable ")?;
714                do_context(context, self)?;
715                self.write_str(t)
716            }
717            CheckingTask::Inhabitable(tm) => {
718                self.write_str("Checking inhabitability ")?;
719                do_context(context, self)?;
720                self.write_str("⊢ INH ")?;
721                self.term(tm, None)
722            }
723            CheckingTask::Universe(tm) => {
724                self.write_str("Checking universe ")?;
725                do_context(context, self)?;
726                self.write_str("⊢ UNIV ")?;
727                self.term(tm, None)
728            }
729            CheckingTask::Subtype(sub, sup) => {
730                self.write_str("Checking subtyping ")?;
731                do_context(context, self)?;
732                self.write_str("⊢ ")?;
733                self.term(sub, None)?;
734                self.write_str(" <: ")?;
735                self.term(sup, None)
736            }
737            CheckingTask::HasType(tm, tp) => {
738                self.write_str("Checking typing ")?;
739                do_context(context, self)?;
740                self.write_str("⊢ ")?;
741                self.term(tm, None)?;
742                self.write_str(" : ")?;
743                self.term(tp, None)
744            }
745            CheckingTask::Equality(lhs, rhs) => {
746                self.write_str("Checking equality ")?;
747                do_context(context, self)?;
748                self.write_str("⊢ ")?;
749                self.term(lhs, None)?;
750                self.write_str(" == ")?;
751                self.term(rhs, None)
752            }
753            CheckingTask::Rule(rl) => {
754                for e in rl.display() {
755                    self.displayable(&e, None)?;
756                }
757                Ok(())
758            }
759            CheckingTask::Strategy(s) => self.strategy(s, context, success),
760        }
761    }
762    fn uri(&mut self, uri: ftml_uris::UriRef, _: Option<MessageLevel>) -> std::fmt::Result {
763        match uri {
764            ftml_uris::UriRef::Symbol(s) => {
765                std::fmt::Display::fmt(&s.module.name, self)?;
766                self.write_char('?')?;
767                std::fmt::Display::fmt(&s.name, self)
768            }
769            _ => std::fmt::Display::fmt(&uri, self),
770        }
771    }
772    fn indent(&mut self, indent: Indent, _: Option<MessageLevel>) -> std::fmt::Result {
773        write!(self, "{indent} ")
774    }
775    fn term(&mut self, term: &Term, _: Option<MessageLevel>) -> std::fmt::Result {
776        <_ as std::fmt::Debug>::fmt(&term.debug_short(), self)
777    }
778    fn string(&mut self, s: &str, _: Option<MessageLevel>) -> std::fmt::Result {
779        self.write_str(s)
780    }
781    fn variable(&mut self, var: &Variable, _: Option<MessageLevel>) -> std::fmt::Result {
782        self.write_str(var.name())
783    }
784    fn num(&mut self, num: i128, _: Option<MessageLevel>) -> std::fmt::Result {
785        <i128 as std::fmt::Display>::fmt(&num, self)
786    }
787}
788
789#[cfg(feature = "colors")]
790pub struct ColorDisplay<'a, 'b>(&'a mut std::fmt::Formatter<'b>);
791#[cfg(feature = "colors")]
792impl FmtTraceDisplay for ColorDisplay<'_, '_> {
793    fn new(f: &mut std::fmt::Formatter<'_>) -> impl TraceDisplay {
794        ColorDisplay(f)
795    }
796}
797#[cfg(feature = "colors")]
798impl TraceDisplay for ColorDisplay<'_, '_> {
799    fn line(
800        &mut self,
801        _: &CheckLog,
802        indent: Indent,
803    ) -> Result<std::ops::ControlFlow<()>, std::fmt::Error> {
804        self.0.write_char('\n')?;
805        self.indent(indent, None)?;
806        Ok(std::ops::ControlFlow::Continue(()))
807    }
808
809    fn space(&mut self) -> std::fmt::Result {
810        self.0.write_char(' ')
811    }
812
813    /*
814    fn rule(&mut self, rule: &dyn CheckerRule) -> std::fmt::Result {
815        write!(self.0, "{} ", "Using rule: ".italic())?;
816        rule.display(self, None)
817    }
818     */
819
820    fn strategy(&mut self, name: &str, _: &[ComponentVar], _: bool) -> std::fmt::Result {
821        write!(self.0, "Strategy: {}", name.italic())
822    }
823
824    fn task(
825        &mut self,
826        task: CheckingTask<'_>,
827        context: &[ComponentVar],
828        success: bool,
829    ) -> std::fmt::Result {
830        fn do_context(context: &[ComponentVar], f: &mut ColorDisplay<'_, '_>) -> std::fmt::Result {
831            if context.is_empty() {
832                return Ok(());
833            }
834            f.0.write_str("{... ")?;
835            let mut first = true;
836            for ComponentVar { var, tp, df } in context {
837                if first {
838                    first = false;
839                } else {
840                    f.0.write_str(", ")?;
841                }
842                f.variable(var, None)?;
843                if let Some(tp) = tp {
844                    f.0.write_str(" : ")?;
845                    f.term(tp, None)?;
846                }
847                if let Some(df) = df {
848                    f.0.write_str(" : ")?;
849                    f.term(df, None)?;
850                }
851            }
852            f.0.write_str(" } ")
853        }
854        if success {
855            write!(self.0, "{} ", "[SUCCESS]".green())?;
856        } else {
857            write!(self.0, "{} ", "[FAILED]".red())?;
858        }
859        match task {
860            CheckingTask::Simplify(t) => {
861                write!(self.0, "{} ", "Simplifying".bright_white().bold())?;
862                do_context(context, self)?;
863                self.term(t, None)
864            }
865            CheckingTask::Proving(t) => {
866                write!(self.0, "{} ", "Proving".bright_white().bold())?;
867                do_context(context, self)?;
868                self.term(t, None)
869            }
870            CheckingTask::Inference(t) => {
871                write!(self.0, "{} ", "Inferring type of".bright_white().bold())?;
872                do_context(context, self)?;
873                self.term(t, None)
874            }
875            CheckingTask::VariableInference(t) => {
876                write!(
877                    self.0,
878                    "{} ",
879                    "Inferring type of variable".bright_white().bold()
880                )?;
881                do_context(context, self)?;
882                self.0.write_str(t)
883            }
884            CheckingTask::Inhabitable(tm) => {
885                write!(
886                    self.0,
887                    "{} ",
888                    "Checking inhabitability".bright_white().bold()
889                )?;
890                do_context(context, self)?;
891                write!(self.0, "{} ", "⊢ INH".bright_white().bold())?;
892                self.term(tm, None)
893            }
894            CheckingTask::Universe(tm) => {
895                write!(self.0, "{} ", "Checking universe".bright_white().bold())?;
896                do_context(context, self)?;
897                write!(self.0, "{} ", "⊢ UNIV".bright_white().bold())?;
898                self.term(tm, None)
899            }
900            CheckingTask::Subtype(sub, sup) => {
901                write!(self.0, "{} ", "Checking subtyping".bright_white().bold())?;
902                do_context(context, self)?;
903                write!(self.0, "{} ", "⊢".bright_white().bold())?;
904                self.term(sub, None)?;
905                write!(self.0, " {} ", "<:".bright_white().bold())?;
906                self.term(sup, None)
907            }
908            CheckingTask::HasType(tm, tp) => {
909                write!(self.0, "{} ", "Checking typing".bright_white().bold())?;
910                do_context(context, self)?;
911                write!(self.0, "{} ", "⊢".bright_white().bold())?;
912                self.term(tm, None)?;
913                write!(self.0, " {} ", ":".bright_white().bold())?;
914                self.term(tp, None)
915            }
916            CheckingTask::Equality(lhs, rhs) => {
917                write!(self.0, "{} ", "Checking equality".bright_white().bold())?;
918                do_context(context, self)?;
919                write!(self.0, "{} ", "⊢".bright_white().bold())?;
920                self.term(lhs, None)?;
921                write!(self.0, " {} ", "==".bright_white().bold())?;
922                self.term(rhs, None)
923            }
924            CheckingTask::Rule(rl) => {
925                for e in rl.display() {
926                    self.displayable(&e, None)?;
927                }
928                Ok(())
929            }
930            CheckingTask::Strategy(s) => self.strategy(s, context, success),
931        }
932    }
933    fn uri(&mut self, uri: ftml_uris::UriRef, _: Option<MessageLevel>) -> std::fmt::Result {
934        match uri {
935            ftml_uris::UriRef::Symbol(s) => {
936                std::fmt::Display::fmt(&s.module.name, self.0)?;
937                self.0.write_char('?')?;
938                std::fmt::Display::fmt(&s.name, self.0)
939            }
940            _ => std::fmt::Display::fmt(&uri, self.0),
941        }
942    }
943    fn indent(&mut self, indent: Indent, _: Option<MessageLevel>) -> std::fmt::Result {
944        write!(self.0, "{} ", indent.blue())
945    }
946    fn term(&mut self, term: &Term, _: Option<MessageLevel>) -> std::fmt::Result {
947        write!(self.0, "{:?}", term.debug_short().yellow())
948    }
949    fn string(&mut self, s: &str, _: Option<MessageLevel>) -> std::fmt::Result {
950        write!(self.0, "{}", s.bright_black())
951    }
952    fn variable(&mut self, var: &Variable, _: Option<MessageLevel>) -> std::fmt::Result {
953        self.0.write_str(var.name())
954    }
955    fn num(&mut self, num: i128, _: Option<MessageLevel>) -> std::fmt::Result {
956        <i128 as std::fmt::Display>::fmt(&num, self.0)
957    }
958}
959
960#[cfg(feature = "full")]
961struct TraceDisplayer<'d, D: FmtTraceDisplay> {
962    trace: &'d CheckLog,
963    d: PhantomData<D>,
964}
965#[cfg(feature = "full")]
966impl<D: FmtTraceDisplay> std::fmt::Display for TraceDisplayer<'_, D> {
967    #[inline]
968    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
969        self.trace.display_i(&mut D::new(f))
970    }
971}
972
973#[cfg(feature = "full")]
974impl From<i128> for DisplayableRef<'_> {
975    fn from(value: i128) -> Self {
976        Self::Num(value)
977    }
978}
979#[cfg(feature = "full")]
980impl From<usize> for DisplayableRef<'_> {
981    fn from(value: usize) -> Self {
982        Self::Num(value as _)
983    }
984}
985#[cfg(feature = "full")]
986impl From<&'static str> for DisplayableRef<'_> {
987    fn from(value: &'static str) -> Self {
988        Self::String(Cow::Borrowed(value))
989    }
990}
991#[cfg(feature = "full")]
992impl From<String> for DisplayableRef<'_> {
993    fn from(value: String) -> Self {
994        Self::String(Cow::Owned(value))
995    }
996}
997#[cfg(feature = "full")]
998impl<'r> From<&'r Term> for DisplayableRef<'r> {
999    fn from(value: &'r Term) -> Self {
1000        Self::Term(Cow::Borrowed(value))
1001    }
1002}
1003#[cfg(feature = "full")]
1004impl From<Term> for DisplayableRef<'_> {
1005    fn from(value: Term) -> Self {
1006        Self::Term(Cow::Owned(value))
1007    }
1008}
1009#[cfg(feature = "full")]
1010impl<'r> From<UriRef<'r>> for DisplayableRef<'r> {
1011    fn from(value: UriRef<'r>) -> Self {
1012        Self::Uri(either::Left(value))
1013    }
1014}
1015#[cfg(feature = "full")]
1016impl From<Uri> for DisplayableRef<'_> {
1017    fn from(value: Uri) -> Self {
1018        Self::Uri(either::Right(value))
1019    }
1020}
1021#[cfg(feature = "full")]
1022impl<'r> From<&'r Variable> for DisplayableRef<'r> {
1023    fn from(value: &'r Variable) -> Self {
1024        Self::Var(Cow::Borrowed(value))
1025    }
1026}
1027#[cfg(feature = "full")]
1028impl From<Variable> for DisplayableRef<'_> {
1029    fn from(value: Variable) -> Self {
1030        Self::Var(Cow::Owned(value))
1031    }
1032}
1033
1034impl<T: FtmlUri> From<&T> for Displayable {
1035    fn from(value: &T) -> Self {
1036        Self::Uri(value.as_uri().owned())
1037    }
1038}
1039impl From<&str> for Displayable {
1040    fn from(value: &str) -> Self {
1041        Self::String(value.to_string())
1042    }
1043}
1044impl From<String> for Displayable {
1045    fn from(value: String) -> Self {
1046        Self::String(value)
1047    }
1048}
1049impl From<Term> for Displayable {
1050    fn from(value: Term) -> Self {
1051        Self::Term(value)
1052    }
1053}
1054
1055impl From<i128> for Displayable {
1056    fn from(value: i128) -> Self {
1057        Self::Num(value)
1058    }
1059}
1060impl From<usize> for Displayable {
1061    fn from(value: usize) -> Self {
1062        Self::Num(value as _)
1063    }
1064}
1065
1066#[cfg(feature = "full")]
1067#[macro_export]
1068macro_rules! trace {
1069    ($($e:expr),* $(,)? ) => {
1070        {vec![$(
1071            $e.into()
1072        ),*]
1073        }
1074    }
1075}
1076
1077#[cfg(feature = "full")]
1078#[macro_export]
1079macro_rules! traceref {
1080    (FAIL $($e:expr),* $(,)? ) => {
1081        $crate::RefCheckLog::Msg(
1082            vec![$( $e.into() ),*],
1083            $crate::MessageLevel::Failure
1084        )
1085    };
1086    ($($e:expr),* $(,)? ) => {
1087        $crate::RefCheckLog::Msg(
1088            vec![$( $e.into() ),*],
1089            $crate::MessageLevel::Comment
1090        )
1091    }
1092}
ftml_solver_trace/lib.rs

ftml_solver_trace/
lib.rs
