Merge remote-tracking branch 'origin/main' into operators

.gitmodules

@@ -0,0 +1,4 @@
+[submodule "winnow"]
+	path = winnow
+	url = git@github.com:supersurviveur/winnow.git
+	branch = operator-in-expression

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).
+
+

Cargo.lock

@@ -11,6 +11,12 @@ dependencies = [
  "memchr",
 ]
 
+[[package]]
+name = "allocator-api2"
+version = "0.2.21"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "683d7910e743518b0e34f1186f92494becacb047c7b6bf616c96772180fef923"
+
 [[package]]
 name = "anstream"
 version = "0.6.21"
@@ -47,7 +53,7 @@ version = "1.1.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "40c48f72fd53cd289104fc64099abca73db4166ad86ea0b4341abe65af83dadc"
 dependencies = [
- "windows-sys 0.61.2",
+ "windows-sys",
 ]
 
 [[package]]
@@ -58,20 +64,14 @@ checksum = "291e6a250ff86cd4a820112fb8898808a366d8f9f58ce16d1f538353ad55747d"
 dependencies = [
  "anstyle",
  "once_cell_polyfill",
- "windows-sys 0.61.2",
+ "windows-sys",
 ]
 
 [[package]]
-name = "autocfg"
-version = "1.5.0"
+name = "bimap"
+version = "0.6.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c08606f8c3cbf4ce6ec8e28fb0014a2c086708fe954eaa885384a6165172e7e8"
-
-[[package]]
-name = "cfg-if"
-version = "1.0.4"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9330f8b2ff13f34540b44e946ef35111825727b38d33286ef986142615121801"
+checksum = "230c5f1ca6a325a32553f8640d31ac9b49f2411e901e427570154868b46da4f7"
 
 [[package]]
 name = "colorchoice"
@@ -79,19 +79,6 @@ version = "1.0.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "b05b61dc5112cbb17e4b6cd61790d9845d13888356391624cbe7e41efeac1e75"
 
-[[package]]
-name = "corosensei"
-version = "0.3.2"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "2b2b4c7e3e97730e6b0b8c5ff5ca82c663d1a645e4f630f4fa4c24e80626787e"
-dependencies = [
- "autocfg",
- "cfg-if",
- "libc",
- "scopeguard",
- "windows-sys 0.59.0",
-]
-
 [[package]]
 name = "env_filter"
 version = "0.1.4"
@@ -115,6 +102,29 @@ dependencies = [
  "log",
 ]
 
+[[package]]
+name = "equivalent"
+version = "1.0.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "877a4ace8713b0bcf2a4e7eec82529c029f1d0619886d18145fea96c3ffe5c0f"
+
+[[package]]
+name = "foldhash"
+version = "0.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "77ce24cb58228fbb8aa041425bb1050850ac19177686ea6e0f41a70416f56fdb"
+
+[[package]]
+name = "hashbrown"
+version = "0.16.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "841d1cc9bed7f9236f321df977030373f4a4163ae1a7dbfe1a51a2c1a51d9100"
+dependencies = [
+ "allocator-api2",
+ "equivalent",
+ "foldhash",
+]
+
 [[package]]
 name = "is_terminal_polyfill"
 version = "1.70.2"
@@ -145,24 +155,21 @@ dependencies = [
  "syn",
 ]
 
-[[package]]
-name = "libc"
-version = "0.2.180"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "bcc35a38544a891a5f7c865aca548a982ccb3b8650a5b06d0fd33a10283c56fc"
-
-[[package]]
-name = "litemap"
-version = "0.8.1"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6373607a59f0be73a39b6fe456b8192fcc3585f602af20751600e974dd455e77"
-
 [[package]]
 name = "log"
 version = "0.4.29"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "5e5032e24019045c762d3c0f28f5b6b8bbf38563a65908389bf7978758920897"
 
+[[package]]
+name = "lru"
+version = "0.16.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a1dc47f592c06f33f8e3aea9591776ec7c9f9e4124778ff8a3c3b87159f7e593"
+dependencies = [
+ "hashbrown",
+]
+
 [[package]]
 name = "memchr"
 version = "2.8.0"
@@ -175,14 +182,21 @@ 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"
 dependencies = [
- "corosensei",
+ "bimap",
  "env_logger",
- "litemap",
  "log",
+ "lru",
+ "owo-colors",
  "winnow",
 ]
 
@@ -248,12 +262,6 @@ version = "0.8.9"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "a96887878f22d7bad8a3b6dc5b7440e0ada9a245242924394987b21cf2210a4c"
 
-[[package]]
-name = "scopeguard"
-version = "1.2.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49"
-
 [[package]]
 name = "serde_core"
 version = "1.0.228"
@@ -303,15 +311,6 @@ version = "0.2.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "f0805222e57f7521d6a62e36fa9163bc891acd422f971defe97d64e70d0a4fe5"
 
-[[package]]
-name = "windows-sys"
-version = "0.59.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1e38bc4d79ed67fd075bcc251a1c39b32a1776bbe92e5bef1f0bf1f8c531853b"
-dependencies = [
- "windows-targets",
-]
-
 [[package]]
 name = "windows-sys"
 version = "0.61.2"
@@ -321,75 +320,9 @@ dependencies = [
  "windows-link",
 ]
 
-[[package]]
-name = "windows-targets"
-version = "0.52.6"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9b724f72796e036ab90c1021d4780d4d3d648aca59e491e6b98e725b84e99973"
-dependencies = [
- "windows_aarch64_gnullvm",
- "windows_aarch64_msvc",
- "windows_i686_gnu",
- "windows_i686_gnullvm",
- "windows_i686_msvc",
- "windows_x86_64_gnu",
- "windows_x86_64_gnullvm",
- "windows_x86_64_msvc",
-]
-
-[[package]]
-name = "windows_aarch64_gnullvm"
-version = "0.52.6"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "32a4622180e7a0ec044bb555404c800bc9fd9ec262ec147edd5989ccd0c02cd3"
-
-[[package]]
-name = "windows_aarch64_msvc"
-version = "0.52.6"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "09ec2a7bb152e2252b53fa7803150007879548bc709c039df7627cabbd05d469"
-
-[[package]]
-name = "windows_i686_gnu"
-version = "0.52.6"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "8e9b5ad5ab802e97eb8e295ac6720e509ee4c243f69d781394014ebfe8bbfa0b"
-
-[[package]]
-name = "windows_i686_gnullvm"
-version = "0.52.6"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "0eee52d38c090b3caa76c563b86c3a4bd71ef1a819287c19d586d7334ae8ed66"
-
-[[package]]
-name = "windows_i686_msvc"
-version = "0.52.6"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "240948bc05c5e7c6dabba28bf89d89ffce3e303022809e73deaefe4f6ec56c66"
-
-[[package]]
-name = "windows_x86_64_gnu"
-version = "0.52.6"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "147a5c80aabfbf0c7d901cb5895d1de30ef2907eb21fbbab29ca94c5b08b1a78"
-
-[[package]]
-name = "windows_x86_64_gnullvm"
-version = "0.52.6"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "24d5b23dc417412679681396f2b49f3de8c1473deb516bd34410872eff51ed0d"
-
-[[package]]
-name = "windows_x86_64_msvc"
-version = "0.52.6"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec"
-
 [[package]]
 name = "winnow"
 version = "0.7.14"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5a5364e9d77fcdeeaa6062ced926ee3381faa2ee02d3eb83a5c27a8825540829"
 dependencies = [
  "memchr",
 ]

Cargo.toml

@@ -4,8 +4,9 @@ version = "0.1.0"
 edition = "2024"
 
 [dependencies]
-corosensei = "0.3.2"
+bimap = "0.6.3"
 env_logger = "0.11.8"
-litemap = "0.8.1"
 log = "0.4.29"
-winnow = "0.7.14"
+winnow = { version = "0.7.14", path = "./winnow" }
+lru = "0.16.3"
+owo-colors = "4.2.3"

rustfmt.toml

@@ -0,0 +1,5 @@
+brace_style="AlwaysNextLine"
+control_brace_style="AlwaysNextLine"
+combine_control_expr=false
+
+

src/ast.rs

@@ -1,6 +1,9 @@
+use owo_colors::{OwoColorize, colors::css::Gray};
+
 use std::fmt::Display;
 
-pub type Variable = String;
+#[derive(Clone, PartialEq, Eq, Debug, Hash)]
+pub struct Variable(pub String, pub Option<usize>);
 
 #[derive(Clone, Debug)]
 pub struct Module
@@ -15,7 +18,7 @@ pub struct Clause
     pub body: Option<Body>,
 }
 
-#[derive(Clone, Debug)]
+#[derive(Clone, Debug, PartialEq, Eq, Hash)]
 pub enum Body
 {
     Term(Predicate),
@@ -23,11 +26,47 @@ pub enum Body
     Or(Vec<Body>),
 }
 
-#[derive(Clone, Debug)]
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
 pub enum Predicate
 {
     Variable(Variable), // Upercase variable like X
-    Fixed(String, Vec<Predicate>),
+    Fixed(Functor, Vec<Predicate>),
+}
+
+#[derive(Clone, Debug, PartialEq, Eq, Hash)]
+pub enum Functor
+{
+    Operator(Operator),
+    Functor(String),
+}
+
+#[derive(Clone, Debug, PartialEq, Eq, Hash)]
+pub struct Operator
+{
+    pub op: String,
+    pub precedence: usize,
+    pub op_type: OperatorType,
+}
+
+impl Operator
+{
+    pub fn new(op: String, precedence: usize, op_type: OperatorType) -> Self
+    {
+        Self {
+            op,
+            precedence,
+            op_type,
+        }
+    }
+}
+
+#[derive(Clone, Debug, PartialEq, Eq, Hash)]
+pub enum OperatorType
+{
+    Prefix,
+    Postfix,
+    LeftInfix,
+    RightInfix,
 }
 
 impl Display for Body
@@ -54,6 +93,19 @@ impl Display for Body
     }
 }
 
+impl Display for Variable
+{
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result
+    {
+        write!(f, "{}", self.0)?;
+        if let Some(num) = self.1
+        {
+            write!(f, "{}", format!("[{}]", num).fg::<Gray>())?;
+        }
+        Ok(())
+    }
+}
+
 impl Display for Predicate
 {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result
@@ -110,3 +162,22 @@ impl Display for Module
         Ok(())
     }
 }
+
+impl Display for Functor
+{
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result
+    {
+        match self
+        {
+            Functor::Operator(op) => write!(f, "{}", op),
+            Functor::Functor(name) => write!(f, "{}", name),
+        }
+    }
+}
+impl Display for Operator
+{
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result
+    {
+        write!(f, "{}", self.op)
+    }
+}

src/main.rs

@@ -1,6 +1,5 @@
 use picolog::ast::Body;
 use picolog::ast::Module;
-use picolog::ast::Predicate;
 
 fn main()
 {
@@ -18,20 +17,39 @@ fn main()
 
         mult(zero, X, zero).
         mult(s(Y), X, Z) :- mult(Y, X, W), add(W, X, Z).
+
+        op(10, yfx, +).
+        op(8, yfx, ^).
+        op(6, xfy, ::).
+        op(2, fx, [).
+        op(2, xf, ]).
+        op(3, yfx, |).
+
+        A + B :- test.
+
+        A ^ B + C :- test.
+        A::B::C :- A.
+        [Hd|Tl] :- Hd::Tl.
     "
     .into();
 
-    //let prop: Body = "integer(s(zero))".into();
-    let prop: Body = "mult(X, s(s(s(zero))), s(s(s(s(s(s(s(s(s(zero))))))))))".into();
+    // println!("{}", module);
+    // 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(zero)), s(s(s(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:");
         println!("{}", c.simplified());
         let _ = std::io::stdin().read_line(&mut String::new());
     }
+
     // let p: Predicate = "add(s(zero), zero, Y)".into();
     // let p1: Predicate = "add(X, zero, X)".into();
     // // let p: Predicate = "integer(s(zero))".into();
     // // let p1: Predicate = "integer(s(X))".into();
     // println!("{}", p.matches(&p1).unwrap());
+    //
 }

src/parsing.rs

@@ -1,29 +1,210 @@
-use std::path::Path;
+use std::{collections::HashMap, path::Path};
 
-use winnow::Parser;
-use winnow::Result;
-use winnow::ascii::alphanumeric0;
-use winnow::ascii::multispace0;
-use winnow::combinator::alt;
-use winnow::combinator::delimited;
-use winnow::combinator::opt;
-use winnow::combinator::separated;
-use winnow::combinator::seq;
-use winnow::error::ContextError;
+use winnow::{
+    ascii::{self, alphanumeric1, multispace0},
+    combinator::{
+        alt, delimited, expression, opt, preceded, repeat, separated, seq, terminated, Infix,
+        Postfix, Prefix,
+    },
+    error::ContextError,
+    Parser, Result, Stateful,
+};
 
-use crate::ast::Body;
 use crate::ast::Clause;
+use crate::ast::Functor;
 use crate::ast::Module;
+use crate::ast::Operator;
 use crate::ast::Predicate;
+use crate::ast::{Body, OperatorType};
+use crate::ast::Variable;
 
-pub fn predicate_parse(input: &mut &str) -> Result<Predicate>
+impl Operator
 {
-    let ident = alphanumeric0.parse_next(input)?;
+    pub fn get_precedence(&self) -> usize
+    {
+        self.precedence
+    }
+    pub fn make_infix_operator<'a>(self) -> Infix<Stream<'a>, Predicate, Operator, ContextError>
+    {
+        fn make_predicate(
+            _: &mut Stream,
+            a: Predicate,
+            op: Operator,
+            b: Predicate,
+        ) -> Result<Predicate>
+        {
+            Ok(Predicate::Fixed(Functor::Operator(op), vec![a, b]))
+        }
+        let precedence = self.get_precedence() as i64;
+        match self.op_type
+        {
+            OperatorType::LeftInfix => Infix::Left(precedence, self, make_predicate),
+            OperatorType::RightInfix => Infix::Right(precedence, self, make_predicate),
+            _ => unreachable!(),
+        }
+    }
+}
+
+impl Operator
+{
+    fn infix(value: String, state: &State) -> Result<Self>
+    {
+        state
+            .custom_operators
+            .get(&(value.clone(), OperatorType::RightInfix))
+            .or_else(|| {
+                state
+                    .custom_operators
+                    .get(&(value, OperatorType::LeftInfix))
+            })
+            .ok_or(ContextError::new())
+            .cloned()
+    }
+    fn prefix(value: String, state: &State) -> Result<Self>
+    {
+        state
+            .custom_operators
+            .get(&(value, OperatorType::Prefix))
+            .ok_or(ContextError::new())
+            .cloned()
+    }
+    fn postfix(value: String, state: &State) -> Result<Self>
+    {
+        state
+            .custom_operators
+            .get(&(value, OperatorType::Postfix))
+            .ok_or(ContextError::new())
+            .cloned()
+    }
+}
+
+const OPERATORS: [&str; 9] = [":", "-", "+", "|", "/", "*", "[", "]", "^"];
+
+#[derive(Debug)]
+pub struct State
+{
+    custom_operators: HashMap<(String, OperatorType), Operator>,
+}
+
+impl Default for State
+{
+    fn default() -> Self
+    {
+        Self::new()
+    }
+}
+
+impl State
+{
+    pub fn new() -> Self
+    {
+        Self {
+            custom_operators: HashMap::new(),
+        }
+    }
+}
+
+type Stream<'is> = Stateful<&'is str, State>;
+
+pub fn operator_parse(input: &mut Stream) -> Result<String>
+{
+    delimited(multispace0, repeat(1.., alt(OPERATORS)), multispace0)
+        .map(|op: String| Ok(op))
+        .parse_next(input)?
+}
+
+pub fn operator_parse_infix(input: &mut Stream) -> Result<Operator>
+{
+    operator_parse(input).map(|op| Operator::infix(op, &input.state))?
+}
+pub fn operator_parse_postfix(input: &mut Stream) -> Result<Operator>
+{
+    operator_parse(input).map(|op| Operator::postfix(op, &input.state))?
+}
+pub fn operator_parse_prefix(input: &mut Stream) -> Result<Operator>
+{
+    operator_parse(input).map(|op| Operator::prefix(op, &input.state))?
+}
+
+pub fn operator_definition_parse(input: &mut Stream) -> Result<()>
+{
+    let (precedence, op_type, op) = preceded(
+        "op",
+        delimited(
+            ("(", multispace0),
+            seq! {
+                ascii::dec_uint,
+                _: (multispace0, ",", multispace0),
+                alt(("xfx", "xfy", "yfx", "xf", "yf", "fy", "fx")),
+                _: (multispace0, ",", multispace0),
+                operator_parse,
+            },
+            (multispace0, ")", multispace0, "."),
+        ),
+    )
+    .parse_next(input)?;
+    let op_type = match op_type
+    {
+        "xf" | "yf" => OperatorType::Postfix,
+        "fx" | "fy" => OperatorType::Prefix,
+        "xfx" => unimplemented!(),
+        "yfx" => OperatorType::LeftInfix,
+        "xfy" => OperatorType::RightInfix,
+        _ => unreachable!(),
+    };
+    input.state.custom_operators.insert(
+        (op.clone(), op_type.clone()),
+        Operator::new(op, precedence, op_type),
+    );
+    Ok(())
+}
+
+pub fn predicate_parse_infix_expression<'a>(
+    input: &mut Stream<'a>,
+) -> Result<Infix<Stream<'a>, Predicate, Operator, ContextError>>
+{
+    let op = operator_parse_infix.parse_next(input)?;
+    Ok(op.make_infix_operator())
+}
+
+pub fn predicate_parse_prefix_expression<'a>(
+    input: &mut Stream<'a>,
+) -> Result<Prefix<Stream<'a>, Predicate, Operator, ContextError>>
+{
+    let op = operator_parse_prefix.parse_next(input)?;
+    let precedence = op.get_precedence() as i64;
+    Ok(Prefix(precedence, op, |_, op, a| {
+        Ok(Predicate::Fixed(Functor::Operator(op), vec![a]))
+    }))
+}
+pub fn predicate_parse_postfix_expression<'a>(
+    input: &mut Stream<'a>,
+) -> Result<Postfix<Stream<'a>, Predicate, Operator, ContextError>>
+{
+    let op = operator_parse_postfix.parse_next(input)?;
+    let precedence = op.get_precedence() as i64;
+    Ok(Postfix(precedence, op, |_, a, op| {
+        Ok(Predicate::Fixed(Functor::Operator(op), vec![a]))
+    }))
+}
+
+pub fn predicate_parse_expression(input: &mut Stream) -> Result<Predicate>
+{
+    expression(predicate_parse_recursive)
+        .infix(predicate_parse_infix_expression)
+        .postfix(predicate_parse_postfix_expression)
+        .prefix(predicate_parse_prefix_expression)
+        .parse_next(input)
+}
+
+pub fn predicate_parse_variable_or_functor(input: &mut Stream) -> Result<Predicate>
+{
+    let ident = alphanumeric1.parse_next(input)?;
 
     // Check if output is a variable
     if ident.chars().next().is_some_and(|char| char.is_uppercase())
     {
-        Ok(Predicate::Variable(String::from(ident)))
+        Ok(Predicate::Variable(Variable(String::from(ident), None)))
     }
     else
     {
@@ -34,11 +215,28 @@ pub fn predicate_parse(input: &mut &str) -> Result<Predicate>
         )
         .parse_next(input)
         .unwrap_or(Vec::new());
-        Ok(Predicate::Fixed(String::from(ident), arguments))
+        Ok(Predicate::Fixed(
+            Functor::Functor(String::from(ident)),
+            arguments,
+        ))
     }
 }
 
-fn body_parse_or(input: &mut &str) -> Result<Body>
+pub fn predicate_parse_recursive(input: &mut Stream) -> Result<Predicate>
+{
+    alt((
+        delimited("(", predicate_parse, ")"),
+        predicate_parse_variable_or_functor,
+    ))
+    .parse_next(input)
+}
+
+pub fn predicate_parse(input: &mut Stream) -> Result<Predicate>
+{
+    alt((predicate_parse_expression, predicate_parse_recursive)).parse_next(input)
+}
+
+fn body_parse_or(input: &mut Stream) -> Result<Body>
 {
     separated(
         1..,
@@ -52,7 +250,7 @@ fn body_parse_or(input: &mut &str) -> Result<Body>
     .parse_next(input)
 }
 
-pub fn body_parse(input: &mut &str) -> Result<Body>
+pub fn body_parse(input: &mut Stream) -> Result<Body>
 {
     // Parse and
     separated(1.., body_parse_or, (multispace0, ",", multispace0))
@@ -60,7 +258,7 @@ pub fn body_parse(input: &mut &str) -> Result<Body>
         .parse_next(input)
 }
 
-pub fn clause_parse(input: &mut &str) -> Result<Clause>
+pub fn clause_parse(input: &mut Stream) -> Result<Clause>
 {
     seq! {
         Clause
@@ -74,12 +272,19 @@ pub fn clause_parse(input: &mut &str) -> Result<Clause>
     .parse_next(input)
 }
 
-pub fn module_parse(input: &mut &str) -> Result<Module>
+pub fn module_parse(input: &mut Stream) -> Result<Module>
 {
     let _: Result<&str, ContextError> = multispace0.parse_next(input);
-    separated(0.., clause_parse, multispace0)
-        .map(|clauses| Module { clauses })
-        .parse_next(input)
+    separated(
+        0..,
+        preceded::<_, (), _, _, _, _>(
+            repeat(0.., terminated(operator_definition_parse, multispace0)),
+            clause_parse,
+        ),
+        multispace0,
+    )
+    .map(|clauses| Module { clauses })
+    .parse_next(input)
 }
 
 impl<T> From<T> for Module
@@ -88,8 +293,13 @@ where
 {
     fn from(value: T) -> Self
     {
-        let mut str: &str = value.as_ref();
-        module_parse.parse_next(&mut str).unwrap()
+        let str: &str = value.as_ref();
+        module_parse
+            .parse_next(&mut Stream {
+                input: str,
+                state: State::new(),
+            })
+            .unwrap()
     }
 }
 
@@ -107,8 +317,13 @@ where
 {
     fn from(value: T) -> Self
     {
-        let mut str: &str = value.as_ref();
-        predicate_parse.parse_next(&mut str).unwrap()
+        let str: &str = value.as_ref();
+        predicate_parse
+            .parse_next(&mut Stream {
+                input: str,
+                state: State::new(),
+            })
+            .unwrap()
     }
 }
 
@@ -118,7 +333,12 @@ where
 {
     fn from(value: T) -> Self
     {
-        let mut str: &str = value.as_ref();
-        body_parse.parse_next(&mut str).unwrap()
+        let str: &str = value.as_ref();
+        body_parse
+            .parse_next(&mut Stream {
+                input: str,
+                state: State::new(),
+            })
+            .unwrap()
     }
 }

src/prover.rs

@@ -1,19 +1,24 @@
+pub mod and;
+pub mod body;
 pub mod constraints;
-pub mod trace;
+pub mod not;
+pub mod or;
+pub mod predicate;
+pub mod tracing;
 pub mod unification;
 
 use std::cell::Cell;
-use std::collections::VecDeque;
+use std::collections::HashMap;
 use std::rc::Rc;
 
-use litemap::LiteMap;
-use log::info;
-
 use crate::ast::Body;
 use crate::ast::Clause;
 use crate::ast::Module;
 use crate::ast::Predicate;
+use crate::ast::Variable;
+use crate::prover::body::BodyProver;
 use crate::prover::constraints::Constraints;
+use crate::prover::tracing::IndentedTracer;
 
 #[derive(Clone, Copy, Debug, Default)]
 pub struct Counter(usize);
@@ -25,7 +30,12 @@ impl GlobalCounter
 {
     pub fn new() -> GlobalCounter
     {
-        GlobalCounter(Rc::new(Cell::new(0)))
+        Self::with(0)
+    }
+
+    pub fn with(n: usize) -> GlobalCounter
+    {
+        GlobalCounter(Rc::new(Cell::new(n)))
     }
 
     pub fn get(&self) -> usize
@@ -46,258 +56,6 @@ impl GlobalCounter
     }
 }
 
-pub struct BodyProver<'a>
-{
-    module: &'a Module,
-    constraints: Constraints,
-
-    prover: Box<dyn Iterator<Item = Constraints> + 'a>,
-}
-
-pub struct PredicateProver<'a>
-{
-    module: &'a Module,
-    predicate: Predicate,
-    constraints: Constraints,
-    counter_snapshot: Counter,
-
-    global_counter: GlobalCounter,
-    current_clause: usize,
-    sub_proof: Option<BodyProver<'a>>,
-}
-
-pub struct AndProver<'a>
-{
-    module: &'a Module,
-    bodies: Vec<Body>,
-    constraints: Constraints,
-
-    global_counter: GlobalCounter,
-    sub_proofs: VecDeque<(Counter, BodyProver<'a>)>,
-}
-
-impl BodyProver<'_>
-{
-    pub fn new<'a>(
-        module: &'a Module,
-        global_counter: GlobalCounter,
-        body: Body,
-        constraints: Constraints,
-    ) -> 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(),
-            )),
-            Body::And(items) => Box::new(AndProver::new(
-                module,
-                global_counter,
-                items.clone(),
-                constraints.clone(),
-            )),
-            Body::Or(items) => Box::new(BodyProver::new(
-                module,
-                global_counter,
-                items[0].clone(),
-                constraints.clone(),
-            )),
-        };
-        info!(target: "BodyProver", "Proving {}", body);
-        BodyProver {
-            module,
-            constraints,
-            prover,
-        }
-    }
-}
-
-impl PredicateProver<'_>
-{
-    pub fn new<'a>(
-        module: &'a Module,
-        global_counter: GlobalCounter,
-        predicate: Predicate,
-        constraints: Constraints,
-    ) -> PredicateProver<'a>
-    {
-        info!(target: "PredicateProver", "Proving {}", predicate);
-        PredicateProver {
-            module,
-            predicate,
-            constraints,
-            current_clause: 0,
-            sub_proof: None,
-            counter_snapshot: global_counter.snapshot(),
-            global_counter,
-        }
-    }
-}
-
-impl AndProver<'_>
-{
-    pub fn new<'a>(
-        module: &'a Module,
-        global_counter: GlobalCounter,
-        bodies: Vec<Body>,
-        constraints: Constraints,
-    ) -> AndProver<'a>
-    {
-        assert!(!bodies.is_empty());
-
-        AndProver {
-            module,
-            sub_proofs: VecDeque::from(vec![(
-                global_counter.snapshot(),
-                BodyProver::new(
-                    module,
-                    global_counter.clone(),
-                    bodies[0].clone(),
-                    constraints.clone(),
-                ),
-            )]),
-            bodies,
-            constraints,
-            global_counter,
-        }
-    }
-}
-
-impl Iterator for PredicateProver<'_>
-{
-    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);
-                    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);
-                    }
-                    else
-                    {
-                        info!(target: "PredicateProver", " => (Can't unify)");
-                    }
-                    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.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 Iterator for BodyProver<'_>
-{
-    type Item = Constraints;
-    fn next(&mut self) -> Option<Constraints>
-    {
-        self.prover.next()
-    }
-}
-
-impl Iterator for AndProver<'_>
-{
-    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_back().unwrap();
-
-        match current_proof.next()
-        {
-            Some(constraints) =>
-            {
-                if self.sub_proofs.len() == self.bodies.len() - 1
-                {
-                    self.sub_proofs
-                        .push_back((current_proof_snap, current_proof));
-                    Some(constraints)
-                }
-                else
-                {
-                    self.sub_proofs
-                        .push_back((current_proof_snap, current_proof));
-                    self.sub_proofs.push_back((
-                        self.global_counter.snapshot(),
-                        BodyProver::new(
-                            self.module,
-                            self.global_counter.clone(),
-                            self.bodies[self.sub_proofs.len()].clone(),
-                            constraints,
-                        ),
-                    ));
-                    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>
@@ -307,6 +65,9 @@ impl Module
             GlobalCounter::new(),
             body.clone(),
             Constraints::none(),
+            //&mut EmptyTracer,
+            &mut IndentedTracer::new(),
+            //&SimpleTracer::new(ProofType::Body),
         )
     }
 }
@@ -315,7 +76,7 @@ impl Clause
 {
     pub fn make_unique(&self, counter: GlobalCounter) -> Clause
     {
-        let mut unique_map = LiteMap::new();
+        let mut unique_map = HashMap::new();
         Clause {
             head: self.head.make_unique(counter.clone(), &mut unique_map),
             body: self
@@ -331,7 +92,7 @@ impl Body
     pub fn make_unique(
         &self,
         counter: GlobalCounter,
-        unique_map: &mut LiteMap<String, usize>,
+        unique_map: &mut HashMap<Variable, usize>,
     ) -> Body
     {
         match self
@@ -358,18 +119,15 @@ impl Predicate
     pub fn make_unique(
         &self,
         counter: GlobalCounter,
-        unique_map: &mut LiteMap<String, usize>,
+        unique_map: &mut HashMap<Variable, usize>,
     ) -> Self
     {
         match self
         {
-            Predicate::Variable(name) => Predicate::Variable(format!(
-                "_{}[{}]",
-                name,
-                unique_map
-                    .entry(name.clone())
-                    .or_insert_with(|| counter.get())
-            )),
+            Predicate::Variable(var) =>
+            {
+                Predicate::Variable(var.make_unique(counter.clone(), unique_map))
+            }
             Predicate::Fixed(name, predicates) => Predicate::Fixed(
                 name.clone(),
                 predicates
@@ -380,3 +138,22 @@ impl Predicate
         }
     }
 }
+
+impl Variable
+{
+    pub fn make_unique(
+        &self,
+        counter: GlobalCounter,
+        unique_map: &mut HashMap<Variable, usize>,
+    ) -> Self
+    {
+        Variable(
+            self.0.clone(),
+            Some(
+                *unique_map
+                    .entry(self.clone())
+                    .or_insert_with(|| counter.get()),
+            ),
+        )
+    }
+}

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()
+            }
+        }
+    }
+}

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()
+    }
+}

src/prover/constraints.rs

@@ -1,16 +1,14 @@
+use std::collections::HashMap;
 use std::fmt::Display;
 
-use litemap::LiteMap;
-use winnow::Str;
-
+use crate::ast::Body;
 use crate::ast::Predicate;
 use crate::ast::Variable;
-use crate::prover::constraints;
 
 #[derive(Clone, Debug)]
 pub struct Constraints
 {
-    set: LiteMap<Variable, Predicate>,
+    pub(crate) set: HashMap<Variable, Predicate>,
 }
 
 impl Constraints
@@ -18,7 +16,7 @@ impl Constraints
     pub fn none() -> Self
     {
         Constraints {
-            set: LiteMap::new(),
+            set: HashMap::new(),
         }
     }
 
@@ -33,6 +31,10 @@ impl Constraints
     {
         if let Some(other_predicate) = self.set.get(variable)
         {
+            if predicate == other_predicate
+            {
+                return true;
+            }
             // If variable is already contrained, we need to check if both contraints are
             // contradictory
 
@@ -99,7 +101,7 @@ impl Constraints
         let mut stripped = max_sub.clone();
         'outer: for (var, _) in max_sub.set.iter()
         {
-            if var.chars().next().is_some_and(|x| x == '_')
+            if var.0.chars().next().is_some_and(|x| x == '_') || var.1.is_some()
             {
                 for (_, other_pred) in max_sub.set.iter()
                 {
@@ -126,8 +128,7 @@ impl Predicate
             {
                 if let Some(pred) = constraints.set.get(name)
                 {
-                    let max_sub = pred.substitute(constraints);
-                    max_sub
+                    pred.substitute(constraints)
                 }
                 else
                 {
@@ -144,15 +145,28 @@ impl Predicate
         }
     }
 
-    pub fn contains_variable(&self, name: &String) -> bool
+    pub fn contains_variable(&self, name: &Variable) -> bool
     {
         match self
         {
             Predicate::Variable(var_name) => name == var_name,
-            Predicate::Fixed(_, predicates) => predicates
-                .iter()
-                .find(|x| x.contains_variable(name))
-                .is_some(),
+            Predicate::Fixed(_, predicates) => predicates.iter().any(|x| x.contains_variable(name)),
+        }
+    }
+}
+
+impl Body
+{
+    pub fn substitute(&self, constraints: &Constraints) -> Body
+    {
+        match self
+        {
+            Body::Term(predicate) => Body::Term(predicate.substitute(constraints)),
+            Body::And(items) =>
+            {
+                Body::And(items.iter().map(|x| x.substitute(constraints)).collect())
+            }
+            Body::Or(items) => Body::Or(items.iter().map(|x| x.substitute(constraints)).collect()),
         }
     }
 }

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
+        }
+    }
+}

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()
+                }
+            }
+        }
+    }
+}

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()
+                    }
+                }
+            }
+        }
+    }
+}

src/prover/tracing.rs

@@ -0,0 +1,146 @@
+use log::info;
+use owo_colors::colors::css::DarkGray;
+use owo_colors::colors::css::Gray;
+use owo_colors::OwoColorize;
+use owo_colors::Style;
+use std::fmt::Display;
+
+#[derive(Clone, Copy)]
+pub enum ProofType
+{
+    Body,
+    And,
+    Predicate,
+}
+
+impl Display for ProofType
+{
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result
+    {
+        match self
+        {
+            ProofType::Body => write!(f, "body_prover"),
+            ProofType::And => write!(f, "and_prover"),
+            ProofType::Predicate => write!(f, "predicate_prover"),
+        }
+    }
+}
+
+pub trait Tracer
+{
+    fn begin_proof(&mut self, proof_type: ProofType) -> Self;
+    fn print_step<T: Display>(&mut self, show: T);
+    fn end_proof(self);
+}
+
+pub struct SimpleTracer
+{
+    proof_type: ProofType,
+}
+
+impl SimpleTracer
+{
+    pub fn new(proof_type: ProofType) -> Self
+    {
+        Self { proof_type }
+    }
+}
+
+impl Tracer for SimpleTracer
+{
+    fn begin_proof(&mut self, proof_type: ProofType) -> Self
+    {
+        SimpleTracer { proof_type }
+    }
+
+    fn print_step<T: Display>(&mut self, show: T)
+    {
+        let str = format!("{}", self.proof_type);
+        info!(target: &str, "{}", show);
+    }
+
+    fn end_proof(self)
+    {
+        todo!()
+    }
+}
+
+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 struct EmptyTracer;
+
+impl Tracer for EmptyTracer
+{
+    fn begin_proof(&mut self, _proof_type: ProofType) -> Self
+    {
+        EmptyTracer
+    }
+
+    fn print_step<T: Display>(&mut self, _show: T) {}
+
+    fn end_proof(self) {}
+}

src/prover/unification.rs

@@ -1,7 +1,3 @@
-use std::process::Output;
-
-use log::debug;
-
 use crate::ast::Predicate;
 use crate::prover::constraints::Constraints;
 
@@ -13,11 +9,11 @@ impl Predicate
     /// returns `None` if the predicate cannot be unified against the other
     pub fn matches(&self, other: &Predicate) -> Option<Constraints>
     {
-        debug!("Unifying {} against {}", self, other);
         match self
         {
             Predicate::Variable(variable) =>
             {
+                //debug!("Unifying var {} against {}", self, other);
                 // We are trying to see if X (any) matches the other Predicate.
                 // This is always true if X = other_predicate
                 Some(Constraints::with(variable.clone(), other.clone()))
@@ -32,6 +28,7 @@ impl Predicate
                         // We are trying to see if something like "predicate(..., ...)" matches X
                         // (any)
                         // This is always true
+                        //debug!("Unifying pred {} against var {}", self, other);
                         Some(Constraints::with(var.clone(), self.clone()))
                     }
                     // Match pred(X, Y, Z, ...) with pred(_X, _Y, _Z, ...)
@@ -39,6 +36,7 @@ impl Predicate
                         if other_name == name && other_arguments.len() == arguments.len() =>
                     {
                         // If there is no arguments, no constraints
+                        //debug!("Unifying fixed {} against fixed {}", self, other);
                         if arguments.is_empty()
                         {
                             return Some(Constraints::none());