From a151b772aa4c070f299c69461bef03ff5ef55768 Mon Sep 17 00:00:00 2001 From: Albin Chaboissier Date: Mon, 9 Feb 2026 16:40:51 +0100 Subject: [PATCH] Starts a good tracing interface --- Cargo.lock | 7 +++++++ Cargo.toml | 1 + src/ast.rs | 6 +++++- src/main.rs | 4 ++-- src/prover.rs | 21 +++++++++++++++++++-- src/prover/constraints.rs | 3 ++- src/prover/tracing.rs | 18 ++++++++++++++++++ 7 files changed, 54 insertions(+), 6 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 3d771a3..c7c015a 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -144,6 +144,12 @@ version = "1.70.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "384b8ab6d37215f3c5301a95a4accb5d64aa607f1fcb26a11b5303878451b4fe" +[[package]] +name = "owo-colors" +version = "4.2.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9c6901729fa79e91a0913333229e9ca5dc725089d1c363b2f4b4760709dc4a52" + [[package]] name = "picolog" version = "0.1.0" @@ -151,6 +157,7 @@ dependencies = [ "env_logger", "litemap", "log", + "owo-colors", "winnow", ] diff --git a/Cargo.toml b/Cargo.toml index 6952248..7d57d83 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -7,4 +7,5 @@ edition = "2024" env_logger = "0.11.8" litemap = "0.8.1" log = "0.4.29" +owo-colors = "4.2.3" winnow = "0.7.14" diff --git a/src/ast.rs b/src/ast.rs index f56d75d..f07abbc 100644 --- a/src/ast.rs +++ b/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)?; diff --git a/src/main.rs b/src/main.rs index d120503..9b537fa 100644 --- a/src/main.rs +++ b/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:"); diff --git a/src/prover.rs b/src/prover.rs index d081f10..9208a3d 100644 --- a/src/prover.rs +++ b/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::(), + 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::(), c)); } else { - //info!(target: "PredicateProver", " => (Can't unify)"); + self.tracer + .print_step(format!("🭧 ↳ {}", "Contradictory".fg::())); } match full_constraints { diff --git a/src/prover/constraints.rs b/src/prover/constraints.rs index a13eab2..4bad744 100644 --- a/src/prover/constraints.rs +++ b/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, ", ")?; diff --git a/src/prover/tracing.rs b/src/prover/tracing.rs index 94ef708..47ccfbf 100644 --- a/src/prover/tracing.rs +++ b/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::(); + format!("{}{}", var, unique) +}