Doz progression

.gitmodules

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

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"
@@ -61,6 +67,12 @@ dependencies = [
  "windows-sys",
 ]
 
+[[package]]
+name = "bimap"
+version = "0.6.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "230c5f1ca6a325a32553f8640d31ac9b49f2411e901e427570154868b46da4f7"
+
 [[package]]
 name = "colorchoice"
 version = "1.0.4"
@@ -90,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"
@@ -120,18 +155,21 @@ dependencies = [
  "syn",
 ]
 
-[[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"
@@ -154,9 +192,10 @@ checksum = "9c6901729fa79e91a0913333229e9ca5dc725089d1c363b2f4b4760709dc4a52"
 name = "picolog"
 version = "0.1.0"
 dependencies = [
+ "bimap",
  "env_logger",
- "litemap",
  "log",
+ "lru",
  "owo-colors",
  "winnow",
 ]
@@ -284,8 +323,6 @@ dependencies = [
 [[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]
+bimap = "0.6.3"
 env_logger = "0.11.8"
-litemap = "0.8.1"
 log = "0.4.29"
+winnow = { version = "0.7.14", path = "./winnow" }
+lru = "0.16.3"
 owo-colors = "4.2.3"
-winnow = "0.7.14"

doz/.gitignore

@@ -0,0 +1 @@
+/target

doz/Cargo.lock

@@ -0,0 +1,7 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "doz"
+version = "0.1.0"

doz/Cargo.toml

@@ -0,0 +1,6 @@
+[package]
+name = "doz"
+version = "0.1.0"
+edition = "2024"
+
+[dependencies]

doz/src/constraint.rs

@@ -0,0 +1,103 @@
+pub mod resolution;
+
+use std::collections::{HashMap, VecDeque};
+
+use crate::domain::{Domain, DomainRange};
+
+pub struct Indexical
+{
+    pub variable: usize,
+    pub dependencies: Vec<usize>,
+
+    #[allow(clippy::type_complexity)]
+    pub propagator: Box<dyn Fn(&[DomainRange]) -> DomainRange>,
+}
+
+impl Indexical
+{
+    pub fn new<T>(variable: usize, dependencies: &[usize], propagator: T) -> Indexical
+    where
+        T: Fn(&[DomainRange]) -> DomainRange + 'static,
+    {
+        Indexical {
+            variable,
+            dependencies: dependencies.to_vec(),
+            propagator: Box::new(propagator),
+        }
+    }
+}
+
+pub struct ClpContext
+{
+    pub variables: usize,
+    pub domains: HashMap<usize, Domain>,
+    pub used_by: HashMap<usize, Vec<usize>>,
+    pub constraints: HashMap<usize, Vec<Indexical>>,
+}
+
+impl ClpContext
+{
+    pub fn new() -> Self
+    {
+        ClpContext {
+            variables: 0,
+            domains: HashMap::new(),
+            used_by: HashMap::new(),
+            constraints: HashMap::new(),
+        }
+    }
+
+    pub fn get_var(&mut self) -> usize
+    {
+        let k = self.variables;
+        self.variables += 1;
+        self.domains.insert(k, Domain::from(..));
+        self.used_by.insert(k, vec![]);
+        k
+    }
+
+    pub fn insert_constraint(&mut self, indexical: Indexical)
+    {
+        let vec = self.constraints.entry(indexical.variable).or_insert(vec![]);
+        for x in indexical.dependencies.iter()
+        {
+            self.used_by.get_mut(x).unwrap().push(indexical.variable);
+        }
+        vec.push(indexical);
+    }
+
+    pub fn prune(&mut self) -> bool
+    {
+        let mut queue = VecDeque::from_iter(0..self.variables);
+
+        while !queue.is_empty()
+        {
+            // Apply unary constraints
+            let var = queue.pop_front().unwrap();
+            let constraints = self.constraints.get(&var);
+            if constraints.is_none()
+            {
+                continue;
+            }
+            let constraints = constraints.unwrap();
+
+            for c in constraints.iter()
+            {
+                if c.dependencies.is_empty()
+                {
+                    // Is unary constraint
+                    let domain = self.domains.get(&var).unwrap();
+                }
+            }
+        }
+        todo!();
+    }
+}
+
+impl Default for ClpContext
+{
+    fn default() -> Self
+    {
+        Self::new()
+    }
+}

doz/src/domain.rs

@@ -0,0 +1,241 @@
+pub mod domain_ops;
+pub mod range_ops;
+
+use std::fmt::Display;
+use std::ops::Range;
+use std::ops::RangeFrom;
+use std::ops::RangeFull;
+use std::ops::RangeTo;
+
+pub struct Domain
+{
+    pub ranges: Vec<DomainRange>,
+}
+
+/// Represents the set
+/// $$\{x \in [\text{start}; \text{end}[ | x \equiv \text{congruent} \text{mod} \text{modulo}}$$
+#[derive(Clone, Copy, PartialEq, Eq, Debug)]
+pub struct DomainRange
+{
+    pub start: LowerBound,
+    pub end: HigherBound,
+}
+
+#[derive(Clone, Copy, PartialEq, Eq, Debug)]
+pub enum LowerBound
+{
+    Infinity,
+    Bounded(i64),
+}
+
+#[derive(Clone, Copy, PartialEq, Eq, Debug)]
+pub enum HigherBound
+{
+    Infinity,
+    Bounded(i64),
+}
+
+pub enum UnionResult<T>
+{
+    Single(T),
+    Union(T, T),
+}
+
+impl Domain
+{
+    pub fn empty(&self) -> Domain
+    {
+        Domain { ranges: vec![] }
+    }
+
+    pub fn is_empty(&self) -> bool
+    {
+        self.ranges.is_empty()
+    }
+}
+
+impl DomainRange
+{
+    pub fn range(from: LowerBound, to: HigherBound) -> DomainRange
+    {
+        DomainRange {
+            start: from,
+            end: to,
+        }
+    }
+}
+
+impl From<Range<i64>> for Domain
+{
+    fn from(value: Range<i64>) -> Self
+    {
+        Domain {
+            ranges: vec![value.into()],
+        }
+    }
+}
+
+impl From<RangeFull> for Domain
+{
+    fn from(value: RangeFull) -> Self
+    {
+        Domain {
+            ranges: vec![value.into()],
+        }
+    }
+}
+
+impl From<RangeTo<i64>> for Domain
+{
+    fn from(value: RangeTo<i64>) -> Self
+    {
+        Domain {
+            ranges: vec![value.into()],
+        }
+    }
+}
+
+impl From<RangeFrom<i64>> for Domain
+{
+    fn from(value: RangeFrom<i64>) -> Self
+    {
+        Domain {
+            ranges: vec![value.into()],
+        }
+    }
+}
+
+impl From<Range<i64>> for DomainRange
+{
+    fn from(value: Range<i64>) -> Self
+    {
+        DomainRange::range(
+            LowerBound::Bounded(value.start),
+            HigherBound::Bounded(value.end),
+        )
+    }
+}
+
+impl From<RangeTo<i64>> for DomainRange
+{
+    fn from(value: RangeTo<i64>) -> Self
+    {
+        DomainRange::range(LowerBound::Infinity, HigherBound::Bounded(value.end))
+    }
+}
+
+impl From<RangeFrom<i64>> for DomainRange
+{
+    fn from(value: RangeFrom<i64>) -> Self
+    {
+        DomainRange::range(LowerBound::Bounded(value.start), HigherBound::Infinity)
+    }
+}
+
+impl From<RangeFull> for DomainRange
+{
+    fn from(_: RangeFull) -> Self
+    {
+        DomainRange::range(LowerBound::Infinity, HigherBound::Infinity)
+    }
+}
+
+impl Display for LowerBound
+{
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result
+    {
+        match self
+        {
+            LowerBound::Infinity => write!(f, "-∞"),
+            LowerBound::Bounded(x) => write!(f, "{}", x),
+        }
+    }
+}
+
+impl Display for HigherBound
+{
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result
+    {
+        match self
+        {
+            HigherBound::Infinity => write!(f, "+∞"),
+            HigherBound::Bounded(x) => write!(f, "{}", x),
+        }
+    }
+}
+
+impl Display for DomainRange
+{
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result
+    {
+        write!(f, "{}..{}", self.start, self.end)
+    }
+}
+
+impl Display for Domain
+{
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result
+    {
+        if self.is_empty()
+        {
+            write!(f, "Ø")
+        }
+        else
+        {
+            let len = self.ranges.len();
+            for (i, r) in self.ranges.iter().enumerate()
+            {
+                write!(f, "{}", r)?;
+                if i != len - 1
+                {
+                    write!(f, " ∪ ")?;
+                }
+            }
+            Ok(())
+        }
+    }
+}
+
+impl PartialOrd for LowerBound
+{
+    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering>
+    {
+        Some(self.cmp(other))
+    }
+}
+
+impl Ord for LowerBound
+{
+    fn cmp(&self, other: &Self) -> std::cmp::Ordering
+    {
+        match (self, other)
+        {
+            (LowerBound::Infinity, LowerBound::Infinity) => std::cmp::Ordering::Equal,
+            (LowerBound::Infinity, LowerBound::Bounded(_)) => std::cmp::Ordering::Less,
+            (LowerBound::Bounded(_), LowerBound::Infinity) => std::cmp::Ordering::Greater,
+            (LowerBound::Bounded(a), LowerBound::Bounded(b)) => a.cmp(b),
+        }
+    }
+}
+
+impl PartialOrd for HigherBound
+{
+    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering>
+    {
+        Some(self.cmp(other))
+    }
+}
+
+impl Ord for HigherBound
+{
+    fn cmp(&self, other: &Self) -> std::cmp::Ordering
+    {
+        match (self, other)
+        {
+            (HigherBound::Infinity, HigherBound::Infinity) => std::cmp::Ordering::Equal,
+            (HigherBound::Infinity, HigherBound::Bounded(_)) => std::cmp::Ordering::Greater,
+            (HigherBound::Bounded(_), HigherBound::Infinity) => std::cmp::Ordering::Less,
+            (HigherBound::Bounded(a), HigherBound::Bounded(b)) => a.cmp(b),
+        }
+    }
+}

doz/src/domain/domain_ops.rs

@@ -0,0 +1,90 @@
+use crate::domain::{Domain, DomainRange};
+
+impl Domain
+{
+    pub fn intersection(&self, domain: &Domain) -> Domain
+    {
+        let mut i = 0;
+        let mut j = 0;
+        let mut stack = vec![];
+
+        while i < self.ranges.len() || j < domain.ranges.len()
+        {
+            if i < self.ranges.len() && j < domain.ranges.len()
+            {
+                let a = self.ranges[i];
+                let b = domain.ranges[j];
+
+                if a.disjoint(&b)
+                {
+                    if a.start < b.start
+                    {
+                        i += 1;
+                    }
+                    else
+                    {
+                        j += 1;
+                    }
+                }
+                else
+                {
+                    let inter = a.intersection(&b);
+                    if let Some(range) = inter
+                    {
+                        stack.push(range);
+                    };
+                    if a.end > b.end
+                    {
+                        i += 1;
+                    }
+                    else
+                    {
+                        j += 1;
+                    }
+                }
+            }
+            else
+            {
+                break;
+            }
+        }
+
+        Domain { ranges: stack }
+    }
+
+    pub fn union(&self, domain: &Domain) -> Domain
+    {
+        let mut stack = self
+            .ranges
+            .iter()
+            .copied()
+            .chain(domain.ranges.iter().copied())
+            .collect::<Vec<DomainRange>>();
+
+        stack.sort_by(|a, b| b.start.cmp(&a.start));
+        let mut ranges = vec![];
+
+        while !stack.is_empty()
+        {
+            if stack.len() >= 2
+            {
+                let (a, b) = (stack.pop().unwrap(), stack.pop().unwrap());
+                match a.union(&b)
+                {
+                    crate::domain::UnionResult::Single(x) => stack.push(x),
+                    crate::domain::UnionResult::Union(x, y) =>
+                    {
+                        ranges.push(x);
+                        stack.push(y);
+                    }
+                }
+            }
+            else if stack.len() == 1
+            {
+                ranges.push(stack.pop().unwrap());
+            }
+        }
+
+        Domain { ranges }
+    }
+}

doz/src/domain/range_ops.rs

@@ -0,0 +1,124 @@
+// Module for computing intersection of domains
+
+use crate::domain::DomainRange;
+use crate::domain::HigherBound;
+use crate::domain::LowerBound;
+use crate::domain::UnionResult;
+
+impl DomainRange
+{
+    pub fn union(&self, range: &DomainRange) -> UnionResult<DomainRange>
+    {
+        let (a, b) = (self.min_by_start(range), self.max_by_start(range));
+        match (a.end, b.start)
+        {
+            (HigherBound::Infinity, LowerBound::Infinity) =>
+            {
+                UnionResult::Single(DomainRange::from(..))
+            }
+            (HigherBound::Infinity, LowerBound::Bounded(_)) => UnionResult::Single(DomainRange {
+                start: a.start,
+                end: HigherBound::Infinity,
+            }),
+            (HigherBound::Bounded(_), LowerBound::Infinity) => UnionResult::Single(DomainRange {
+                start: LowerBound::Infinity,
+                end: b.end,
+            }),
+            (HigherBound::Bounded(c), LowerBound::Bounded(d)) if c < d => UnionResult::Union(a, b),
+            (HigherBound::Bounded(_), LowerBound::Bounded(_)) => UnionResult::Single(DomainRange {
+                start: a.start,
+                end: b.end,
+            }),
+        }
+    }
+
+    pub fn intersection(&self, range: &DomainRange) -> Option<DomainRange>
+    {
+        let (a, b) = (self.min_by_start(range), self.max_by_start(range));
+        match (a.end, b.start)
+        {
+            (HigherBound::Infinity, LowerBound::Infinity) => Some(DomainRange::from(..)),
+            (HigherBound::Infinity, LowerBound::Bounded(a)) => Some(DomainRange::from(a..)),
+            (HigherBound::Bounded(a), LowerBound::Infinity) => Some(DomainRange::from(..a)),
+            (HigherBound::Bounded(a), LowerBound::Bounded(b)) if a <= b => None,
+            (HigherBound::Bounded(a), LowerBound::Bounded(b)) => Some(DomainRange::from(a..b)),
+        }
+    }
+
+    pub fn without(&self, range: &DomainRange) -> DomainRange
+    {
+        match self.intersection(range)
+        {
+            Some(intersecting_part) => match self.union(&intersecting_part)
+            {
+                UnionResult::Single(res) => res,
+                UnionResult::Union(_, _) => unreachable!(),
+            },
+            None => *self,
+        }
+    }
+
+    pub fn symetrical_difference(&self, range: &DomainRange) -> Option<UnionResult<DomainRange>>
+    {
+        match self.intersection(range)
+        {
+            Some(intersecting_part) =>
+            {
+                Some((self.without(&intersecting_part)).union(&range.without(&intersecting_part)))
+            }
+            None => Some(self.union(range)),
+        }
+    }
+
+    pub fn disjoint(&self, range: &DomainRange) -> bool
+    {
+        self.intersection(range).is_none()
+    }
+
+    pub fn included_in(&self, range: &DomainRange) -> bool
+    {
+        if let UnionResult::Single(x) = self.union(range)
+            && x == *range
+        {
+            true
+        }
+        else
+        {
+            false
+        }
+    }
+
+    pub fn min_by_start(&self, range: &DomainRange) -> DomainRange
+    {
+        if self.start < range.start
+        {
+            *self
+        }
+        else
+        {
+            *range
+        }
+    }
+
+    pub fn max_by_start(&self, range: &DomainRange) -> DomainRange
+    {
+        if self.start < range.start
+        {
+            *range
+        }
+        else
+        {
+            *self
+        }
+    }
+
+    pub fn min_by_end(&self, range: &DomainRange) -> DomainRange
+    {
+        if self.end < range.end { *self } else { *range }
+    }
+
+    pub fn max_by_end(&self, range: &DomainRange) -> DomainRange
+    {
+        if self.end < range.end { *range } else { *self }
+    }
+}

doz/src/lib.rs

@@ -0,0 +1,2 @@
+pub mod constraint;
+pub mod domain;

doz/src/main.rs

@@ -0,0 +1,21 @@
+use doz::constraint::Indexical;
+use doz::domain::Domain;
+use doz::domain::DomainRange;
+use doz::indexical;
+
+fn main()
+{
+    let even = Domain {
+        ranges: vec![DomainRange {
+            start: doz::domain::LowerBound::Infinity,
+            end: doz::domain::HigherBound::Infinity,
+        }],
+    };
+
+    //let k = Indexical::new([Box::new(|a, b, c| a), Box::new(|a, b, c| b)]);
+    //
+
+    let k = indexical![|[a, _b]| { a }, |[_a, b]| { b }];
+
+    println!("{}", even);
+}

src/ast.rs

@@ -1,7 +1,9 @@
-use crate::prover::tracing::colored_var;
+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
@@ -16,7 +18,7 @@ pub struct Clause
     pub body: Option<Body>,
 }
 
-#[derive(Clone, Debug)]
+#[derive(Clone, Debug, PartialEq, Eq, Hash)]
 pub enum Body
 {
     Term(Predicate),
@@ -24,11 +26,47 @@ pub enum Body
     Or(Vec<Body>),
 }
 
-#[derive(Clone, Debug, PartialEq)]
+#[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
@@ -55,13 +93,26 @@ 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
     {
         match self
         {
-            Predicate::Variable(variable) => write!(f, "{}", colored_var(variable)),
+            Predicate::Variable(variable) => write!(f, "{}", variable),
             Predicate::Fixed(name, predicates) =>
             {
                 write!(f, "{}", name)?;
@@ -111,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

@@ -17,11 +17,26 @@ 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();
 
+    // 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(zero), s(zero))".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)

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

@@ -8,14 +8,15 @@ pub mod tracing;
 pub mod unification;
 
 use std::cell::Cell;
+use std::collections::HashMap;
 use std::rc::Rc;
 
-use litemap::LiteMap;
-
 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;
 
@@ -29,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
@@ -59,6 +65,7 @@ impl Module
             GlobalCounter::new(),
             body.clone(),
             Constraints::none(),
+            //&mut EmptyTracer,
             &mut IndentedTracer::new(),
             //&SimpleTracer::new(ProofType::Body),
         )
@@ -69,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
@@ -85,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
@@ -112,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
@@ -134,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/constraints.rs

@@ -1,16 +1,14 @@
+use std::collections::HashMap;
 use std::fmt::Display;
 
-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
 {
-    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(),
         }
     }
 
@@ -103,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()
                 {
@@ -147,7 +145,7 @@ impl Predicate
         }
     }
 
-    pub fn contains_variable(&self, name: &String) -> bool
+    pub fn contains_variable(&self, name: &Variable) -> bool
     {
         match self
         {
@@ -188,7 +186,7 @@ impl Display for Constraints
         let len = self.set.len();
         for (i, (var, pred)) in self.set.iter().enumerate()
         {
-            write!(f, "{} = {}", colored_var(var), pred)?;
+            write!(f, "{} = {}", var, pred)?;
             if i != len - 1
             {
                 write!(f, ", ")?;

src/prover/tracing.rs

@@ -1,12 +1,10 @@
 use log::info;
-use owo_colors::{
-    OwoColorize, Style,
-    colors::css::{DarkGray, Gray},
-};
+use owo_colors::colors::css::DarkGray;
+use owo_colors::colors::css::Gray;
+use owo_colors::OwoColorize;
+use owo_colors::Style;
 use std::fmt::Display;
 
-use crate::ast::Variable;
-
 #[derive(Clone, Copy)]
 pub enum ProofType
 {
@@ -110,8 +108,8 @@ impl Tracer for IndentedTracer
         }
         self.first = false;
         println!("{}", show);
-        let _ = std::io::stdin().read_line(&mut String::new());
-        println!("\x1b[2A");
+        // let _ = std::io::stdin().read_line(&mut String::new());
+        // println!("\x1b[2A");
     }
 
     fn end_proof(self)
@@ -133,17 +131,16 @@ impl Default for IndentedTracer
     }
 }
 
-pub fn colored_var(var: &Variable) -> String
+pub struct EmptyTracer;
+
+impl Tracer for EmptyTracer
 {
-    let mut idx = None;
-    for (i, char) in var.chars().enumerate()
+    fn begin_proof(&mut self, _proof_type: ProofType) -> Self
     {
-        if char == '['
-        {
-            idx = Some(i);
-        }
+        EmptyTracer
     }
-    let (var, unique) = var.split_at(idx.unwrap_or(var.len()));
-    let unique = unique.fg::<Gray>();
-    format!("{}{}", var, unique)
+
+    fn print_step<T: Display>(&mut self, _show: T) {}
+
+    fn end_proof(self) {}
 }