Adds not prover

Putting provers in separate files
Better looking indentation
2026-02-10 00:07:06 +01:00 · 2026-02-09 23:26:29 +01:00 · 2026-02-09 22:49:26 +01:00 · 2026-02-09 22:38:23 +01:00 · 2026-02-09 22:32:01 +01:00
12 changed files with 670 additions and 353 deletions
--- a/1.pl
+++ b/1.pl
@ -1,9 +1,22 @@
+:- use_module(library(clpfd)).
+
 entier(zero).
 entier(s(X)) :- entier(X).

 add(X, zero, X).
 add(X, s(Y), Z) :- add(s(X), Y, Z).

+inf(zero, X) :- entier(X).
+inf(s(X), s(Y)) :- inf(X, Y).
+
 mult(zero, X, zero).
 mult(s(Y), X, Z) :- mult(Y, X, W), add(W, X, Z).

+div(A, B) :- inf(A, B), inf(X, B), mult(X, A, B).
+div_w(X, Y) :- inf(s(X), Y), inf(s(s(zero)), X), div(X, Y).
+prime(X) :- entier(X), \+ div_w(_, X).
+
+peano(X, zero) :- X #= 0.
+peano(X, s(P)) :- X #> 0, X #= Y + 1, peano(Y, P).
+
+
--- a/src/ast.rs
+++ b/src/ast.rs
@ -1,8 +1,5 @@
-use std::fmt::Display;
-
-use owo_colors::{OwoColorize, colors::css::Gray};
-
 use crate::prover::tracing::colored_var;
+use std::fmt::Display;

 pub type Variable = String;

--- a/src/main.rs
+++ b/src/main.rs
@ -21,7 +21,9 @@ 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 = "mult(X, s(zero), s(zero))".into();
+    //let prop: Body = "mult(X, Y, Z)".into();
+    //let prop: Body = "mult(s(s(zero)), s(s(zero)), X)".into();
    for c in module.prove(&prop)
    {
        println!("true:");
--- a/src/prover.rs
+++ b/src/prover.rs
@ -1,26 +1,23 @@
+pub mod and;
+pub mod body;
 pub mod constraints;
+pub mod not;
+pub mod or;
+pub mod predicate;
 pub mod tracing;
 pub mod unification;

 use std::cell::Cell;
-use std::fmt::Write;
 use std::rc::Rc;

 use litemap::LiteMap;
-use owo_colors::OwoColorize;
-use owo_colors::Style;
-use owo_colors::colors::Green;
-use owo_colors::colors::Red;
-use owo_colors::colors::Yellow;

 use crate::ast::Body;
 use crate::ast::Clause;
 use crate::ast::Module;
 use crate::ast::Predicate;
 use crate::prover::constraints::Constraints;
-use crate::prover::tracing::ProofType;
-use crate::prover::tracing::SimpleTracer;
-use crate::prover::tracing::Tracer;
+use crate::prover::tracing::IndentedTracer;

 #[derive(Clone, Copy, Debug, Default)]
 pub struct Counter(usize);
@ -53,344 +50,17 @@ impl GlobalCounter
    }
 }

-pub struct BodyProver<'a, T: Tracer + 'a>
-{
-    module: &'a Module,
-    constraints: Constraints,
-    tracer: Option<T>,
-    prover: Box<dyn Iterator<Item = Constraints> + 'a>,
-}
-
-pub struct PredicateProver<'a, T: Tracer>
-{
-    module: &'a Module,
-    predicate: Predicate,
-    constraints: Constraints,
-    counter_snapshot: Counter,
-    tracer: T,
-
-    global_counter: GlobalCounter,
-    current_clause: usize,
-    sub_proof: Option<BodyProver<'a, T>>,
-}
-
-pub struct AndProver<'a, T: Tracer>
-{
-    module: &'a Module,
-    bodies: Vec<Body>,
-    constraints: Constraints,
-    tracer: T,
-    current_tracer: Option<T>,
-
-    global_counter: GlobalCounter,
-    sub_proofs: Vec<(Counter, BodyProver<'a, T>)>,
-}
-
-impl<'a, T: Tracer + 'a> BodyProver<'a, T>
-{
-    pub fn new(
-        module: &'a Module,
-        global_counter: GlobalCounter,
-        body: Body,
-        constraints: Constraints,
-        tracer: &T,
-    ) -> BodyProver<'a, T>
-    {
-        let body_tracer = if let Body::And(_) = body
-        {
-            Some(tracer.begin_proof(ProofType::Body))
-        }
-        else
-        {
-            None
-        };
-        let prover: Box<dyn Iterator<Item = Constraints>> = match &body
-        {
-            Body::Term(predicate) => Box::new(PredicateProver::new(
-                module,
-                global_counter,
-                predicate.clone(),
-                constraints.clone(),
-                tracer,
-            )),
-
-            // Shortcut And & Or prover if it contains only one element to simplify proofs
-            Body::And(items) | Body::Or(items) if items.len() == 1 => Box::new(BodyProver::new(
-                module,
-                global_counter,
-                items[0].clone(),
-                constraints.clone(),
-                tracer,
-            )),
-
-            Body::And(items) => Box::new(AndProver::new(
-                module,
-                global_counter,
-                items.clone(),
-                constraints.clone(),
-                tracer,
-            )),
-            Body::Or(items) => Box::new(BodyProver::new(
-                module,
-                global_counter,
-                items[0].clone(),
-                constraints.clone(),
-                tracer,
-            )),
-        };
-        //info!(target: "BodyProver", "Proving {}", body);
-        BodyProver {
-            tracer: body_tracer,
-            module,
-            constraints,
-            prover,
-        }
-    }
-}
-
-impl<'a, T: Tracer + 'a> PredicateProver<'a, T>
-{
-    pub fn new(
-        module: &'a Module,
-        global_counter: GlobalCounter,
-        predicate: Predicate,
-        constraints: Constraints,
-        tracer: &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: predicate_prover,
-            predicate,
-            constraints,
-            current_clause: 0,
-            sub_proof: None,
-            counter_snapshot: global_counter.snapshot(),
-            global_counter,
-        }
-    }
-}
-
-impl<T: Tracer> AndProver<'_, T>
-{
-    pub fn new<'a>(
-        module: &'a Module,
-        global_counter: GlobalCounter,
-        bodies: Vec<Body>,
-        constraints: Constraints,
-        tracer: &T,
-    ) -> AndProver<'a, T>
-    where
-        T: 'a,
-    {
-        assert!(!bodies.is_empty());
-
-        AndProver {
-            tracer: tracer.begin_proof(ProofType::And),
-            current_tracer: None,
-            module,
-            sub_proofs: vec![(
-                global_counter.snapshot(),
-                BodyProver::new(
-                    module,
-                    global_counter.clone(),
-                    bodies[0].clone(),
-                    constraints.clone(),
-                    tracer,
-                ),
-            )],
-            bodies,
-            constraints,
-            global_counter,
-        }
-    }
-}
-
-impl<'a, T: Tracer + 'a> Iterator for PredicateProver<'a, T>
-{
-    type Item = Constraints;
-
-    fn next(&mut self) -> Option<Self::Item>
-    {
-        match self.sub_proof.as_mut()
-        {
-            None =>
-            {
-                if self.current_clause == self.module.clauses.len()
-                {
-                    None
-                }
-                else
-                {
-                    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
-                    {
-                        self.tracer
-                            .print_step(format!("🭧 ↳ {}", "Contradictory".fg::<Red>()));
-                    }
-                    match full_constraints
-                    {
-                        Some(constraints) if clause.body.is_none() =>
-                        {
-                            self.current_clause += 1;
-                            Some(constraints)
-                        }
-                        Some(constraints) =>
-                        {
-                            self.current_clause += 1;
-                            self.counter_snapshot = self.global_counter.snapshot();
-                            self.sub_proof = Some(BodyProver::new(
-                                self.module,
-                                self.global_counter.clone(),
-                                clause.body.clone().unwrap(),
-                                constraints,
-                                &self.tracer,
-                            ));
-                            self.next()
-                        }
-                        None =>
-                        {
-                            self.current_clause += 1;
-                            self.next()
-                        }
-                    }
-                }
-            }
-            Some(prover) =>
-            {
-                let next = prover.next();
-                match next
-                {
-                    Some(constraints) => Some(constraints),
-                    None =>
-                    {
-                        self.global_counter.restore(self.counter_snapshot);
-                        self.sub_proof = None;
-                        self.next()
-                    }
-                }
-            }
-        }
-    }
-}
-
-impl<'a, T: Tracer + 'a> Iterator for BodyProver<'a, T>
-{
-    type Item = Constraints;
-    fn next(&mut self) -> Option<Constraints>
-    {
-        self.prover.next()
-    }
-}
-
-impl<'a, T: Tracer + 'a> Iterator for AndProver<'a, T>
-{
-    type Item = Constraints;
-
-    fn next(&mut self) -> Option<Self::Item>
-    {
-        if self.sub_proofs.is_empty()
-        {
-            return None;
-        }
-
-        let (current_proof_snap, mut current_proof) = self.sub_proofs.pop().unwrap();
-
-        match current_proof.next()
-        {
-            Some(constraints) =>
-            {
-                if self.sub_proofs.len() == self.bodies.len() - 1
-                {
-                    self.sub_proofs.push((current_proof_snap, current_proof));
-                    Some(constraints)
-                }
-                else
-                {
-                    // Pretty logging
-                    self.current_tracer = Some(self.tracer.begin_proof(ProofType::And));
-                    self.current_tracer.as_ref().unwrap().print_step(format!(
-                        "And. {} {} {} :",
-                        "Proved".fg::<Green>(),
-                        "Proving".fg::<Yellow>(),
-                        "Left".fg::<Red>()
-                    ));
-                    let mut output = String::new();
-                    for (i, x) in self.bodies.iter().enumerate()
-                    {
-                        let mut color = Style::new();
-                        if i == self.sub_proofs.len() - 1
-                        {
-                            color = color.fg::<Yellow>();
-                        }
-                        else if i < self.sub_proofs.len() - 1
-                        {
-                            color = color.fg::<Green>();
-                        }
-                        else
-                        {
-                            color = color.fg::<Red>();
-                        }
-                        let _ = output.write_str(&format!("{}, ", x.style(color)));
-                    }
-                    self.current_tracer.as_ref().unwrap().print_step(output);
-
-                    // End pretty logging
-                    self.sub_proofs.push((current_proof_snap, current_proof));
-                    self.sub_proofs.push((
-                        self.global_counter.snapshot(),
-                        BodyProver::new(
-                            self.module,
-                            self.global_counter.clone(),
-                            self.bodies[self.sub_proofs.len()].clone(),
-                            constraints,
-                            &self.tracer,
-                        ),
-                    ));
-                    self.next()
-                }
-            }
-            None =>
-            {
-                self.global_counter.restore(current_proof_snap);
-                self.next()
-            }
-        }
-    }
-}
-
 impl Module
 {
-    pub fn prove<'a>(&'a self, body: &'a Body) -> BodyProver<'a, SimpleTracer>
+    pub fn prove<'a>(&'a self, body: &'a Body) -> BodyProver<'a>
    {
        BodyProver::new(
            self,
            GlobalCounter::new(),
            body.clone(),
            Constraints::none(),
-            &SimpleTracer::new(ProofType::Body),
+            &mut IndentedTracer::new(),
+            //&SimpleTracer::new(ProofType::Body),
        )
    }
 }
--- a/src/prover/and.rs
+++ b/src/prover/and.rs
@ -0,0 +1,172 @@
+use std::fmt::Write;
+
+use owo_colors::OwoColorize;
+
+use crate::ast::Body;
+use crate::ast::Module;
+use crate::prover::Counter;
+use crate::prover::GlobalCounter;
+use crate::prover::body::BodyProver;
+use crate::prover::constraints::Constraints;
+use crate::prover::tracing::ProofType;
+use crate::prover::tracing::Tracer;
+
+pub struct AndProver<'a, T: Tracer>
+{
+    module: &'a Module,
+    bodies: Vec<Body>,
+    tracer: T,
+
+    global_counter: GlobalCounter,
+    sub_proofs: Vec<(Counter, BodyProver<'a>)>,
+}
+impl<T: Tracer> AndProver<'_, T>
+{
+    pub fn new<'a>(
+        module: &'a Module,
+        global_counter: GlobalCounter,
+        bodies: Vec<Body>,
+        constraints: Constraints,
+        tracer: &mut T,
+    ) -> AndProver<'a, T>
+    where
+        T: 'a,
+    {
+        assert!(!bodies.is_empty());
+
+        // Pretty logging
+        let mut tracer = tracer.begin_proof(ProofType::And);
+        let mut next = String::new();
+        for x in bodies.iter().skip(1)
+        {
+            let _ = next.write_str(&format!("{}, ", x));
+        }
+
+        let mut conjuction = String::new();
+        let len = bodies.len();
+        for (i, x) in bodies.iter().enumerate()
+        {
+            let _ = conjuction.write_str(&format!("{}", x));
+            if i != len - 1
+            {
+                let _ = conjuction.write_str(" ∧ ");
+            }
+        }
+
+        tracer.print_step(format!("Proving conjuction {}", conjuction));
+        tracer.print_step(format!("{}  :", "Proved".fg::<owo_colors::colors::Green>(),));
+        tracer.print_step(format!(
+            "{} : {}",
+            "Proving".fg::<owo_colors::colors::Yellow>(),
+            bodies[0]
+        ));
+        tracer.print_step(format!(
+            "{}    : {}",
+            "Next".fg::<owo_colors::colors::Red>(),
+            next
+        ));
+        tracer.print_step(format!("With constraints : {}", constraints.simplified()));
+        // End pretty logging
+
+        AndProver {
+            module,
+            sub_proofs: vec![(
+                global_counter.snapshot(),
+                BodyProver::new(
+                    module,
+                    global_counter.clone(),
+                    bodies[0].clone(),
+                    constraints.clone(),
+                    &mut tracer,
+                ),
+            )],
+            tracer,
+            bodies,
+            global_counter,
+        }
+    }
+}
+impl<'a, T: Tracer + 'a> Iterator for AndProver<'a, T>
+{
+    type Item = Constraints;
+
+    fn next(&mut self) -> Option<Self::Item>
+    {
+        if self.sub_proofs.is_empty()
+        {
+            return None;
+        }
+
+        let (current_proof_snap, mut current_proof) = self.sub_proofs.pop().unwrap();
+
+        match current_proof.next()
+        {
+            Some(constraints) =>
+            {
+                if self.sub_proofs.len() == self.bodies.len() - 1
+                {
+                    self.sub_proofs.push((current_proof_snap, current_proof));
+                    Some(constraints)
+                }
+                else
+                {
+                    // Pretty logging
+                    let mut proved = String::new();
+                    let mut proving = String::new();
+                    let mut next = String::new();
+                    for (i, x) in self.bodies.iter().enumerate()
+                    {
+                        let dest;
+                        if i == self.sub_proofs.len() + 1
+                        {
+                            dest = &mut proving;
+                        }
+                        else if i < self.sub_proofs.len() + 1
+                        {
+                            dest = &mut proved;
+                        }
+                        else
+                        {
+                            dest = &mut next;
+                        }
+                        let _ = dest.write_str(&format!("{}, ", x));
+                    }
+                    self.tracer.print_step(format!(
+                        "{}  : {}",
+                        "Proved".fg::<owo_colors::colors::Green>(),
+                        proved
+                    ));
+                    self.tracer.print_step(format!(
+                        "{} : {}",
+                        "Proving".fg::<owo_colors::colors::Yellow>(),
+                        proving
+                    ));
+                    self.tracer.print_step(format!(
+                        "{}    : {}",
+                        "Next".fg::<owo_colors::colors::Red>(),
+                        next
+                    ));
+                    // End pretty logging
+
+                    self.sub_proofs.push((current_proof_snap, current_proof));
+                    self.sub_proofs.push((
+                        self.global_counter.snapshot(),
+                        BodyProver::new(
+                            self.module,
+                            self.global_counter.clone(),
+                            self.bodies[self.sub_proofs.len()].clone(),
+                            constraints,
+                            &mut self.tracer,
+                        ),
+                    ));
+                    self.next()
+                }
+            }
+            None =>
+            {
+                self.global_counter.restore(current_proof_snap);
+                self.next()
+            }
+        }
+    }
+}
--- a/src/prover/body.rs
+++ b/src/prover/body.rs
@ -0,0 +1,70 @@
+use crate::ast::Body;
+use crate::ast::Module;
+use crate::prover::GlobalCounter;
+use crate::prover::and::AndProver;
+use crate::prover::constraints::Constraints;
+use crate::prover::predicate::PredicateProver;
+use crate::prover::tracing::Tracer;
+
+pub struct BodyProver<'a>
+{
+    prover: Box<dyn Iterator<Item = Constraints> + 'a>,
+}
+
+impl<'a> BodyProver<'a>
+{
+    pub fn new<T: Tracer + 'a>(
+        module: &'a Module,
+        global_counter: GlobalCounter,
+        body: Body,
+        constraints: Constraints,
+        tracer: &mut T,
+    ) -> BodyProver<'a>
+    {
+        let prover: Box<dyn Iterator<Item = Constraints>> = match &body
+        {
+            Body::Term(predicate) => Box::new(PredicateProver::new(
+                module,
+                global_counter,
+                predicate.clone(),
+                constraints.clone(),
+                tracer,
+            )),
+
+            // Shortcut And & Or prover if it contains only one element to simplify proofs
+            Body::And(items) | Body::Or(items) if items.len() == 1 => Box::new(BodyProver::new(
+                module,
+                global_counter,
+                items[0].clone(),
+                constraints.clone(),
+                tracer,
+            )),
+
+            Body::And(items) => Box::new(AndProver::new(
+                module,
+                global_counter,
+                items.clone(),
+                constraints.clone(),
+                tracer,
+            )),
+            Body::Or(items) => Box::new(BodyProver::new(
+                module,
+                global_counter,
+                items[0].clone(),
+                constraints.clone(),
+                tracer,
+            )),
+        };
+
+        BodyProver { prover }
+    }
+}
+
+impl<'a> Iterator for BodyProver<'a>
+{
+    type Item = Constraints;
+    fn next(&mut self) -> Option<Constraints>
+    {
+        self.prover.next()
+    }
+}
--- a/src/prover/not.rs
+++ b/src/prover/not.rs
@ -0,0 +1,71 @@
+use crate::ast::Body;
+use crate::ast::Module;
+use crate::prover::GlobalCounter;
+use crate::prover::body::BodyProver;
+use crate::prover::constraints::Constraints;
+use crate::prover::tracing::ProofType;
+use crate::prover::tracing::Tracer;
+
+pub struct NotProver<'a, T: Tracer + 'a>
+{
+    prover: Option<BodyProver<'a>>,
+    constraints: Constraints,
+    tracer: T,
+}
+
+impl<'a, T: Tracer + 'a> NotProver<'a, T>
+{
+    pub fn new(
+        module: &'a Module,
+        global_counter: GlobalCounter,
+        body: Body,
+        constraints: Constraints,
+        tracer: &mut T,
+    ) -> NotProver<'a, T>
+    {
+        let mut not_tracer = tracer.begin_proof(ProofType::Body);
+        NotProver {
+            prover: Some(BodyProver::new(
+                module,
+                global_counter,
+                body,
+                constraints.clone(),
+                &mut not_tracer,
+            )),
+            tracer: not_tracer,
+            constraints: constraints.clone(),
+        }
+    }
+}
+
+impl<'a, T: Tracer + 'a> Iterator for NotProver<'a, T>
+{
+    type Item = Constraints;
+    fn next(&mut self) -> Option<Constraints>
+    {
+        if let Some(x) = self.prover.as_mut()
+        {
+            match &mut x.next()
+            {
+                Some(_) =>
+                {
+                    // The prover showed that the proof is true.
+                    // Thus the negation is never true
+                    self.prover = None;
+                    None
+                }
+                None =>
+                {
+                    // The prover did not find any proof
+                    // Thus the negation is true
+                    self.prover = None;
+                    Some(self.constraints.clone())
+                }
+            }
+        }
+        else
+        {
+            None
+        }
+    }
+}
--- a/src/prover/or.rs
+++ b/src/prover/or.rs
@ -0,0 +1,124 @@
+use std::fmt::Write;
+
+use crate::ast::Body;
+use crate::ast::Module;
+use crate::prover::Counter;
+use crate::prover::GlobalCounter;
+use crate::prover::body::BodyProver;
+use crate::prover::constraints::Constraints;
+use crate::prover::tracing::ProofType;
+use crate::prover::tracing::Tracer;
+
+pub struct OrProver<'a, T: Tracer>
+{
+    module: &'a Module,
+    bodies: Vec<Body>,
+    constraints: Constraints,
+    tracer: T,
+
+    current_proving: usize,
+    global_counter: GlobalCounter,
+    counter_snapshot: Counter,
+    sub_proof: Option<BodyProver<'a>>,
+}
+
+impl<T: Tracer> OrProver<'_, T>
+{
+    pub fn new<'a>(
+        module: &'a Module,
+        global_counter: GlobalCounter,
+        bodies: Vec<Body>,
+        constraints: Constraints,
+        tracer: &mut T,
+    ) -> OrProver<'a, T>
+    where
+        T: 'a,
+    {
+        assert!(!bodies.is_empty());
+
+        // Pretty logging
+        let mut tracer = tracer.begin_proof(ProofType::And);
+
+        let mut next = String::new();
+        for x in bodies.iter().skip(1)
+        {
+            let _ = next.write_str(&format!("{}, ", x));
+        }
+
+        let mut disjunction = String::new();
+        let len = bodies.len();
+        for (i, x) in bodies.iter().enumerate()
+        {
+            let _ = disjunction.write_str(&format!("{}", x));
+            if i != len - 1
+            {
+                let _ = disjunction.write_str(" ∨ ");
+            }
+        }
+
+        // End pretty logging
+
+        OrProver {
+            module,
+            sub_proof: Some(BodyProver::new(
+                module,
+                global_counter.clone(),
+                bodies[0].clone(),
+                constraints.clone(),
+                &mut tracer,
+            )),
+            tracer,
+            current_proving: 0,
+            counter_snapshot: global_counter.snapshot(),
+            bodies,
+            constraints,
+            global_counter,
+        }
+    }
+}
+
+impl<'a, T: Tracer + 'a> Iterator for OrProver<'a, T>
+{
+    type Item = Constraints;
+
+    fn next(&mut self) -> Option<Self::Item>
+    {
+        let proof = match &mut self.sub_proof
+        {
+            Some(sub_proof) => sub_proof.next(),
+            None =>
+            {
+                return None;
+            }
+        };
+
+        match proof
+        {
+            Some(x) => Some(x),
+            None =>
+            {
+                // Advance to next possibility
+                if self.current_proving == self.bodies.len() - 1
+                {
+                    self.sub_proof = None;
+                    None
+                }
+                else
+                {
+                    self.current_proving += 1;
+                    self.global_counter.restore(self.counter_snapshot);
+                    self.tracer
+                        .print_step(format!("Tring with {}", self.bodies[self.current_proving]));
+                    self.sub_proof = Some(BodyProver::new(
+                        self.module,
+                        self.global_counter.clone(),
+                        self.bodies[self.current_proving].clone(),
+                        self.constraints.clone(),
+                        &mut self.tracer,
+                    ));
+                    self.next()
+                }
+            }
+        }
+    }
+}
--- a/src/prover/predicate.rs
+++ b/src/prover/predicate.rs
@ -0,0 +1,132 @@
+use owo_colors::OwoColorize;
+use owo_colors::colors::Green;
+
+use crate::ast::{Module, Predicate};
+use crate::prover::body::BodyProver;
+use crate::prover::constraints::Constraints;
+use crate::prover::tracing::{ProofType, Tracer};
+use crate::prover::{Counter, GlobalCounter};
+
+pub struct PredicateProver<'a, T: Tracer>
+{
+    module: &'a Module,
+    predicate: Predicate,
+    constraints: Constraints,
+    counter_snapshot: Counter,
+    tracer: T,
+
+    global_counter: GlobalCounter,
+    current_clause: usize,
+    sub_proof: Option<BodyProver<'a>>,
+}
+
+impl<'a, T: Tracer + 'a> PredicateProver<'a, T>
+{
+    pub fn new(
+        module: &'a Module,
+        global_counter: GlobalCounter,
+        predicate: Predicate,
+        constraints: Constraints,
+        tracer: &mut T,
+    ) -> PredicateProver<'a, T>
+    {
+        //info!(target: "PredicateProver", "Proving {}", predicate);
+        let mut predicate_prover = tracer.begin_proof(ProofType::Predicate);
+        predicate_prover.print_step(format!(
+            "{} '{}'",
+            "Proving predicate".fg::<Green>(),
+            predicate
+        ));
+        PredicateProver {
+            module,
+            tracer: predicate_prover,
+            predicate,
+            constraints,
+            current_clause: 0,
+            sub_proof: None,
+            counter_snapshot: global_counter.snapshot(),
+            global_counter,
+        }
+    }
+}
+
+impl<'a, T: Tracer + 'a> Iterator for PredicateProver<'a, T>
+{
+    type Item = Constraints;
+
+    fn next(&mut self) -> Option<Self::Item>
+    {
+        match self.sub_proof.as_mut()
+        {
+            None =>
+            {
+                if self.current_clause == self.module.clauses.len()
+                {
+                    None
+                }
+                else
+                {
+                    let clause = &self.module.clauses[self.current_clause]
+                        .make_unique(self.global_counter.clone());
+                    let uni = self.predicate.matches(&clause.head);
+                    let full_constraints = uni.and_then(|x| x.and(&self.constraints));
+
+                    if let Some(c) = &full_constraints
+                    {
+                        self.tracer.print_step(format!(
+                            "Unifying '{}' aginst '{}'",
+                            self.predicate, clause
+                        ));
+                        self.tracer.print_step(format!(
+                            "↳ {}: {}",
+                            "Matches".fg::<Green>(),
+                            c.simplified()
+                        ));
+                    }
+
+                    match full_constraints
+                    {
+                        Some(constraints) if clause.body.is_none() =>
+                        {
+                            self.current_clause += 1;
+                            Some(constraints)
+                        }
+                        Some(constraints) =>
+                        {
+                            self.current_clause += 1;
+                            self.counter_snapshot = self.global_counter.snapshot();
+                            self.sub_proof = Some(BodyProver::new(
+                                self.module,
+                                self.global_counter.clone(),
+                                clause.body.clone().unwrap(),
+                                constraints,
+                                &mut self.tracer,
+                            ));
+                            self.next()
+                        }
+                        None =>
+                        {
+                            self.global_counter.restore(self.counter_snapshot);
+                            self.current_clause += 1;
+                            self.next()
+                        }
+                    }
+                }
+            }
+            Some(prover) =>
+            {
+                let next = prover.next();
+                match next
+                {
+                    Some(constraints) => Some(constraints),
+                    None =>
+                    {
+                        self.global_counter.restore(self.counter_snapshot);
+                        self.sub_proof = None;
+                        self.next()
+                    }
+                }
+            }
+        }
+    }
+}
--- a/src/prover/tracing.rs
+++ b/src/prover/tracing.rs
@ -1,7 +1,9 @@
-use std::{default, fmt::Display};
-
 use log::info;
-use owo_colors::{OwoColorize, colors::css::Gray};
+use owo_colors::{
+    OwoColorize, Style,
+    colors::css::{DarkGray, Gray},
+};
+use std::fmt::Display;

 use crate::ast::Variable;

@ -28,8 +30,8 @@ impl Display for ProofType

 pub trait Tracer
 {
-    fn begin_proof(&self, proof_type: ProofType) -> Self;
-    fn print_step<T: Display>(&self, show: T);
+    fn begin_proof(&mut self, proof_type: ProofType) -> Self;
+    fn print_step<T: Display>(&mut self, show: T);
    fn end_proof(self);
 }

@ -48,12 +50,12 @@ impl SimpleTracer

 impl Tracer for SimpleTracer
 {
-    fn begin_proof(&self, proof_type: ProofType) -> Self
+    fn begin_proof(&mut self, proof_type: ProofType) -> Self
    {
        SimpleTracer { proof_type }
    }

-    fn print_step<T: Display>(&self, show: T)
+    fn print_step<T: Display>(&mut self, show: T)
    {
        let str = format!("{}", self.proof_type);
        info!(target: &str, "{}", show);
@ -65,6 +67,72 @@ impl Tracer for SimpleTracer
    }
 }

+pub struct IndentedTracer
+{
+    first: bool,
+    depth: usize,
+}
+
+impl IndentedTracer
+{
+    pub fn new() -> IndentedTracer
+    {
+        IndentedTracer {
+            first: true,
+            depth: 0,
+        }
+    }
+}
+
+impl Tracer for IndentedTracer
+{
+    fn begin_proof(&mut self, _proof_type: ProofType) -> Self
+    {
+        IndentedTracer {
+            first: true,
+            depth: self.depth + 1,
+        }
+    }
+
+    fn print_step<T: Display>(&mut self, show: T)
+    {
+        for i in 0..self.depth
+        {
+            let style = if i % 2 == 0
+            {
+                Style::new().fg::<Gray>()
+            }
+            else
+            {
+                Style::new().fg::<DarkGray>()
+            };
+            print!("{}", "│".style(style));
+        }
+        self.first = false;
+        println!("{}", show);
+        let _ = std::io::stdin().read_line(&mut String::new());
+        println!("\x1b[2A");
+    }
+
+    fn end_proof(self)
+    {
+        drop(self);
+    }
+}
+
+impl Drop for IndentedTracer
+{
+    fn drop(&mut self) {}
+}
+
+impl Default for IndentedTracer
+{
+    fn default() -> Self
+    {
+        Self::new()
+    }
+}
+
 pub fn colored_var(var: &Variable) -> String
 {
    let mut idx = None;
--- a/src/prover/unification.rs
+++ b/src/prover/unification.rs
@ -1,5 +1,3 @@
-use log::debug;
-
 use crate::ast::Predicate;
 use crate::prover::constraints::Constraints;

--- a/src/tracing.rs
+++ b/src/tracing.rs
Author	SHA1	Message	Date
Albin Chaboissier	298d179943	Adds not prover	2026-02-10 00:07:06 +01:00
Albin Chaboissier	70afc2a201	Putting provers in separate files	2026-02-09 23:26:29 +01:00
Albin Chaboissier	3fd8414ba2	Better looking indentation	2026-02-09 22:49:26 +01:00
Albin Chaboissier	c920ef8d99	Removes all warnings	2026-02-09 22:38:23 +01:00
Albin Chaboissier	5b9df71704	Somewhat indented trace + Or prover	2026-02-09 22:32:01 +01:00