Starts a good tracing interface

src/ast.rs

@@ -1,5 +1,9 @@
 use std::fmt::Display;
 
+use owo_colors::{OwoColorize, colors::css::Gray};
+
+use crate::prover::tracing::colored_var;
+
 pub type Variable = String;
 
 #[derive(Clone, Debug)]
@@ -60,7 +64,7 @@ impl Display for Predicate
     {
         match self
         {
-            Predicate::Variable(variable) => write!(f, "{}", variable),
+            Predicate::Variable(variable) => write!(f, "{}", colored_var(variable)),
             Predicate::Fixed(name, predicates) =>
             {
                 write!(f, "{}", name)?;

src/main.rs

@@ -20,8 +20,8 @@ fn main()
     "
     .into();
 
-    //let prop: Body = "integer(s(X))".into();
-    let prop: Body = "mult(X, s(s(s(zero))), s(s(s(s(s(s(s(s(s(zero))))))))))".into();
+    let prop: Body = "integer(s(X))".into();
+    //let prop: Body = "mult(X, s(s(s(zero))), s(s(s(s(s(s(s(s(s(zero))))))))))".into();
     for c in module.prove(&prop)
     {
         println!("true:");

src/prover.rs

@@ -7,6 +7,10 @@ use std::rc::Rc;
 
 use litemap::LiteMap;
 use log::info;
+use owo_colors::OwoColorize;
+use owo_colors::colors::Green;
+use owo_colors::colors::Red;
+use owo_colors::colors::css::Gray;
 
 use crate::ast::Body;
 use crate::ast::Clause;
@@ -143,9 +147,15 @@ impl<'a, T: Tracer + 'a> PredicateProver<'a, T>
     ) -> PredicateProver<'a, T>
     {
         //info!(target: "PredicateProver", "Proving {}", predicate);
+        let predicate_prover = tracer.begin_proof(ProofType::Predicate);
+        predicate_prover.print_step(format!(
+            "{} '{}'",
+            "Proving predicate".fg::<Green>(),
+            predicate
+        ));
         PredicateProver {
             module,
-            tracer: tracer.begin_proof(ProofType::Predicate),
+            tracer: predicate_prover,
             predicate,
             constraints,
             current_clause: 0,
@@ -209,16 +219,23 @@ impl<'a, T: Tracer + 'a> Iterator for PredicateProver<'a, T>
                     let clause = &self.module.clauses[self.current_clause]
                         .make_unique(self.global_counter.clone());
                     //info!(target: "PredicateProver", "Unifying '{}' against '{}'", self.predicate, clause);
+                    self.tracer.print_step(format!(
+                        "🭆 Unifying '{}' aginst '{}'",
+                        self.predicate, clause
+                    ));
                     let uni = self.predicate.matches(&clause.head);
                     let full_constraints = uni.and_then(|x| x.and(&self.constraints));
 
                     if let Some(c) = &full_constraints
                     {
                         //info!(target: "PredicateProver", " => {}", c);
+                        self.tracer
+                            .print_step(format!("🭧 ↳ {}: {}", "Matches".fg::<Green>(), c));
                     }
                     else
                     {
-                        //info!(target: "PredicateProver", " => (Can't unify)");
+                        self.tracer
+                            .print_step(format!("🭧 ↳ {}", "Contradictory".fg::<Red>()));
                     }
                     match full_constraints
                     {

src/prover/constraints.rs

@@ -5,6 +5,7 @@ use litemap::LiteMap;
 use crate::ast::Body;
 use crate::ast::Predicate;
 use crate::ast::Variable;
+use crate::prover::tracing::colored_var;
 
 #[derive(Clone, Debug)]
 pub struct Constraints
@@ -187,7 +188,7 @@ impl Display for Constraints
         let len = self.set.len();
         for (i, (var, pred)) in self.set.iter().enumerate()
         {
-            write!(f, "{} = {}", var, pred)?;
+            write!(f, "{} = {}", colored_var(var), pred)?;
             if i != len - 1
             {
                 write!(f, ", ")?;

src/prover/tracing.rs

@@ -1,6 +1,9 @@
 use std::{default, fmt::Display};
 
 use log::info;
+use owo_colors::{OwoColorize, colors::css::Gray};
+
+use crate::ast::Variable;
 
 #[derive(Clone, Copy)]
 pub enum ProofType
@@ -61,3 +64,18 @@ impl Tracer for SimpleTracer
         todo!()
     }
 }
+
+pub fn colored_var(var: &Variable) -> String
+{
+    let mut idx = None;
+    for (i, char) in var.chars().enumerate()
+    {
+        if char == '['
+        {
+            idx = Some(i);
+        }
+    }
+    let (var, unique) = var.split_at(idx.unwrap_or(var.len()));
+    let unique = unique.fg::<Gray>();
+    format!("{}{}", var, unique)
+}