Domains test

.gitmodules

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

Cargo.lock

@@ -323,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

@@ -7,6 +7,6 @@ edition = "2024"
 bimap = "0.6.3"
 env_logger = "0.11.8"
 log = "0.4.29"
+winnow = { version = "0.7.14", path = "./winnow" }
 lru = "0.16.3"
 owo-colors = "4.2.3"
-winnow = "0.7.14"

src/ast.rs

@@ -2,6 +2,8 @@ use owo_colors::{OwoColorize, colors::css::Gray};
 
 use std::fmt::Display;
 
+use crate::domain::Domain;
+
 #[derive(Clone, PartialEq, Eq, Debug, Hash)]
 pub struct Variable(pub String, pub Option<usize>);
 
@@ -30,7 +32,44 @@ pub enum Body
 pub enum Predicate
 {
     Variable(Variable), // Upercase variable like X
-    Fixed(String, Vec<Predicate>),
+    Fixed(Functor, Vec<Predicate>),
+    Domain(Domain),
+}
+
+#[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
@@ -99,6 +138,7 @@ impl Display for Predicate
                     Ok(())
                 }
             }
+            Predicate::Domain(domain) => write!(f, "{domain}"),
         }
     }
 }
@@ -126,3 +166,23 @@ 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/domain.rs

@@ -0,0 +1,512 @@
+use std::{cmp, fmt::Display};
+
+use crate::domain;
+
+#[derive(Clone, Debug, PartialEq, Eq, Hash)]
+pub struct Domain
+{
+    pub union: Vec<DomainRange>,
+}
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
+pub struct DomainRange
+{
+    pub start: DomainBound,
+    pub end: DomainBound,
+}
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
+pub enum DomainBound
+{
+    Unbounded,
+    Bounded(i64),
+}
+
+impl Domain
+{
+    pub fn all() -> Domain
+    {
+        Domain {
+            union: vec![DomainRange {
+                start: DomainBound::Unbounded,
+                end: DomainBound::Unbounded,
+            }],
+        }
+    }
+
+    pub fn included_in(&self, domain: &Domain) -> bool
+    {
+        self.union(domain) == *domain
+    }
+
+    pub fn empty(&self) -> bool
+    {
+        self.union.len() == 0
+    }
+
+    pub fn disjoint(&self, domain: &Domain) -> bool
+    {
+        self.intersection(domain).union.len() == 0
+    }
+
+    pub fn intersection(&self, domain: &Domain) -> Domain
+    {
+        let mut i = 0;
+        let mut j = 0;
+        let mut stack = vec![];
+
+        while i < self.union.len() || j < domain.union.len()
+        {
+            if i < self.union.len() && j < domain.union.len()
+            {
+                let a = self.union[i];
+                let b = domain.union[j];
+
+                if a.disjoint(&b)
+                {
+                    if a < b
+                    {
+                        i += 1;
+                    }
+                    else
+                    {
+                        j += 1;
+                    }
+                }
+                else
+                {
+                    let inter = a.intersection(&b);
+                    if let Some(range) = inter
+                    {
+                        stack.push(range);
+                    };
+                    if a.ends_furthest(&b)
+                    {
+                        i += 1;
+                    }
+                    else
+                    {
+                        j += 1;
+                    }
+                }
+            }
+            else
+            {
+                break;
+            }
+        }
+
+        Domain { union: stack }
+    }
+
+    pub fn union(&self, domain: &Domain) -> Domain
+    {
+        let mut i = 0;
+        let mut j = 0;
+        let mut stack = vec![];
+
+        while i < self.union.len() || j < domain.union.len()
+        {
+            if i < self.union.len() && j < domain.union.len()
+            {
+                let a = self.union[i];
+                let b = domain.union[j];
+
+                let (min, max) = (a.min(b), a.max(b));
+
+                if let DomainBound::Bounded(end) = min.end
+                    && let DomainBound::Bounded(start) = max.start
+                    && end == start
+                {
+                    let union = a.union(&b);
+                    stack.extend_from_slice(union.union.as_slice());
+                    i += 1;
+                    j += 1;
+                }
+                else if a.disjoint(&b)
+                {
+                    if a < b
+                    {
+                        stack.push(a);
+                        i += 1;
+                    }
+                    else
+                    {
+                        stack.push(b);
+                        j += 1;
+                    }
+                }
+                else
+                {
+                    let union = a.union(&b);
+                    stack.extend_from_slice(union.union.as_slice());
+                    i += 1;
+                    j += 1;
+                }
+            }
+            else if i < self.union.len()
+            {
+                stack.extend_from_slice(&self.union[i..]);
+                i = self.union.len();
+            }
+            else
+            {
+                stack.extend_from_slice(&domain.union[j..]);
+                j = self.union.len();
+            }
+        }
+
+        Domain { union: stack }
+    }
+}
+
+impl From<DomainRange> for Domain
+{
+    fn from(value: DomainRange) -> Self
+    {
+        Domain { union: vec![value] }
+    }
+}
+
+impl DomainBound
+{
+    pub fn min_start(&self, bound: DomainBound) -> DomainBound
+    {
+        match (self, bound)
+        {
+            (DomainBound::Unbounded, DomainBound::Unbounded) => DomainBound::Unbounded,
+            (DomainBound::Bounded(_), DomainBound::Unbounded)
+            | (DomainBound::Unbounded, DomainBound::Bounded(_)) => DomainBound::Unbounded,
+            (DomainBound::Bounded(a), DomainBound::Bounded(b)) => DomainBound::Bounded(*a.min(&b)),
+        }
+    }
+
+    pub fn max_end(&self, bound: DomainBound) -> DomainBound
+    {
+        match (self, bound)
+        {
+            (DomainBound::Unbounded, DomainBound::Unbounded) => DomainBound::Unbounded,
+            (DomainBound::Bounded(_), DomainBound::Unbounded)
+            | (DomainBound::Unbounded, DomainBound::Bounded(_)) => DomainBound::Unbounded,
+            (DomainBound::Bounded(a), DomainBound::Bounded(b)) => DomainBound::Bounded(*a.max(&b)),
+        }
+    }
+}
+
+impl PartialOrd for DomainRange
+{
+    fn partial_cmp(&self, other: &Self) -> Option<cmp::Ordering>
+    {
+        Some(self.cmp(other))
+    }
+}
+
+impl Ord for DomainRange
+{
+    fn cmp(&self, other: &Self) -> std::cmp::Ordering
+    {
+        match (self.start, other.start)
+        {
+            (DomainBound::Unbounded, DomainBound::Unbounded) => cmp::Ordering::Equal,
+            (DomainBound::Unbounded, DomainBound::Bounded(_)) => cmp::Ordering::Less,
+            (DomainBound::Bounded(_), DomainBound::Unbounded) => cmp::Ordering::Greater,
+            (DomainBound::Bounded(a), DomainBound::Bounded(b)) => a.cmp(&b),
+        }
+    }
+}
+
+impl DomainRange
+{
+    pub fn intersection(&self, range: &DomainRange) -> Option<DomainRange>
+    {
+        let (min, max) = (self.min(range), self.max(range));
+        match (min.end, max.start)
+        {
+            (DomainBound::Unbounded, DomainBound::Unbounded) => Some(DomainRange {
+                start: DomainBound::Unbounded,
+                end: DomainBound::Unbounded,
+            }),
+            (DomainBound::Unbounded, DomainBound::Bounded(a)) => Some(DomainRange {
+                start: DomainBound::Bounded(a),
+                end: max.end,
+            }),
+            (DomainBound::Bounded(a), DomainBound::Unbounded) => Some(DomainRange {
+                start: max.start,
+                end: DomainBound::Bounded(a),
+            }),
+            (DomainBound::Bounded(a), DomainBound::Bounded(b)) if b < a => Some(DomainRange {
+                start: DomainBound::Bounded(b),
+                end: DomainBound::Bounded(a),
+            }),
+            _ => None,
+        }
+    }
+
+    pub fn union(&self, range: &DomainRange) -> Domain
+    {
+        if self.disjoint(range)
+        {
+            let (a, b) = (self.min(range), self.max(range));
+            if let DomainBound::Bounded(end) = a.end
+                && let DomainBound::Bounded(start) = b.start
+                && end == start
+            {
+                Domain {
+                    union: vec![DomainRange {
+                        start: a.start,
+                        end: b.end,
+                    }],
+                }
+            }
+            else
+            {
+                Domain {
+                    union: vec![*self.min(range), *self.max(range)],
+                }
+            }
+        }
+        else
+        {
+            let (a, b) = (self.min(range), self.max(range));
+            let range = DomainRange {
+                start: match (a.start, b.start)
+                {
+                    (DomainBound::Bounded(a), DomainBound::Bounded(b)) =>
+                    {
+                        DomainBound::Bounded(a.min(b))
+                    }
+                    (DomainBound::Unbounded, DomainBound::Bounded(_))
+                    | (DomainBound::Bounded(_), DomainBound::Unbounded)
+                    | (DomainBound::Unbounded, DomainBound::Unbounded) => DomainBound::Unbounded,
+                },
+                end: match (a.end, b.end)
+                {
+                    (DomainBound::Bounded(a), DomainBound::Bounded(b)) =>
+                    {
+                        DomainBound::Bounded(a.max(b))
+                    }
+                    (DomainBound::Unbounded, DomainBound::Bounded(_))
+                    | (DomainBound::Bounded(_), DomainBound::Unbounded)
+                    | (DomainBound::Unbounded, DomainBound::Unbounded) => DomainBound::Unbounded,
+                },
+            };
+
+            Domain { union: vec![range] }
+        }
+    }
+
+    pub fn ends_furthest(&self, end: &DomainRange) -> bool
+    {
+        match (self.end, end.end)
+        {
+            (DomainBound::Unbounded, DomainBound::Unbounded) => true,
+            (DomainBound::Unbounded, DomainBound::Bounded(_)) => true,
+            (DomainBound::Bounded(_), DomainBound::Unbounded) => false,
+            (DomainBound::Bounded(a), DomainBound::Bounded(b)) => a >= b,
+        }
+    }
+
+    pub fn disjoint(&self, range: &DomainRange) -> bool
+    {
+        let (a, b) = (self.min(range), self.max(range));
+        matches!((a.end, b.start), (DomainBound::Bounded(a), DomainBound::Bounded(b)) if a <= b)
+    }
+
+    pub fn singleton(value: i64) -> DomainRange
+    {
+        DomainRange {
+            start: DomainBound::Bounded(value),
+            end: DomainBound::Bounded(value + 1),
+        }
+    }
+
+    pub fn from(value: i64) -> DomainRange
+    {
+        DomainRange {
+            start: DomainBound::Bounded(value),
+            end: DomainBound::Unbounded,
+        }
+    }
+
+    pub fn to(value: i64) -> DomainRange
+    {
+        DomainRange {
+            start: DomainBound::Unbounded,
+            end: DomainBound::Bounded(value),
+        }
+    }
+
+    pub fn closed(start: i64, end: i64) -> DomainRange
+    {
+        DomainRange {
+            start: DomainBound::Bounded(start),
+            end: DomainBound::Bounded(end),
+        }
+    }
+}
+
+impl Display for Domain
+{
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result
+    {
+        let len = self.union.len();
+        for (i, range) in self.union.iter().enumerate()
+        {
+            write!(f, "{}", range)?;
+            if i != len - 1
+            {
+                write!(f, " ∪ ")?;
+            }
+        }
+        Ok(())
+    }
+}
+
+impl Display for DomainRange
+{
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result
+    {
+        match (self.start, self.end)
+        {
+            (DomainBound::Bounded(a), DomainBound::Bounded(b)) if b == a + 1 => write!(f, "{}", a),
+            (a, b) => write!(f, "{}..{}", a, b),
+        }
+    }
+}
+
+impl Display for DomainBound
+{
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result
+    {
+        match self
+        {
+            DomainBound::Unbounded => Ok(()),
+            DomainBound::Bounded(n) => write!(f, "{}", n),
+        }
+    }
+}
+
+mod test
+{
+    #[allow(unused_imports)]
+    use crate::domain::{Domain, DomainBound, DomainRange};
+
+    #[test]
+    pub fn domain_range_parse()
+    {
+        let a: DomainRange = "..".into();
+        assert_eq!(
+            a,
+            DomainRange {
+                start: DomainBound::Unbounded,
+                end: DomainBound::Unbounded
+            }
+        );
+
+        let a: DomainRange = "42..".into();
+        assert_eq!(
+            a,
+            DomainRange {
+                start: DomainBound::Bounded(42),
+                end: DomainBound::Unbounded
+            }
+        );
+
+        let a: DomainRange = "..42".into();
+        assert_eq!(
+            a,
+            DomainRange {
+                start: DomainBound::Unbounded,
+                end: DomainBound::Bounded(42),
+            }
+        );
+
+        let a: DomainRange = "0..42".into();
+        assert_eq!(
+            a,
+            DomainRange {
+                start: DomainBound::Bounded(0),
+                end: DomainBound::Bounded(42),
+            }
+        );
+    }
+
+    #[test]
+    pub fn domain_range_union()
+    {
+        let inf: DomainRange = "..".into();
+        let inf_b: DomainRange = "..42".into();
+        let a_inf: DomainRange = "0..".into();
+        let a_b: DomainRange = "10..20".into();
+        let a_b2: DomainRange = "30..50".into();
+        let a_b3: DomainRange = "20..30".into();
+
+        assert_eq!(inf.union(&inf), "..".into());
+        assert_eq!(inf.union(&inf_b), "..".into());
+        assert_eq!(inf.union(&a_inf), "..".into());
+        assert_eq!(inf.union(&a_b), "..".into());
+
+        assert_eq!(inf.union(&inf), "..".into());
+        assert_eq!(inf_b.union(&inf), "..".into());
+        assert_eq!(a_inf.union(&inf), "..".into());
+        assert_eq!(a_b.union(&inf), "..".into());
+
+        assert_eq!(inf.union(&inf), "..".into());
+        assert_eq!(inf_b.union(&inf_b), "..42".into());
+        assert_eq!(a_inf.union(&a_inf), "0..".into());
+        assert_eq!(a_b.union(&a_b), "10..20".into());
+
+        assert_eq!(
+            a_b.union(&a_b2),
+            Domain {
+                union: vec!["10..20".into(), "30..50".into()]
+            }
+        );
+
+        assert_eq!(a_b.union(&a_b3), "10..30".into());
+    }
+
+    #[test]
+    pub fn domain_union()
+    {
+        let k: Domain = "2..5".into();
+        let k2: Domain = "5..10".into();
+        assert_eq!(
+            k.union(&k2),
+            Domain {
+                union: vec![DomainRange {
+                    start: DomainBound::Bounded(2),
+                    end: DomainBound::Bounded(10)
+                }]
+            }
+        );
+    }
+
+    #[test]
+    pub fn domain_intersection()
+    {
+        let k: Domain = "0..5".into();
+        let k2: Domain = "10..15".into();
+
+        let k3: Domain = "3..7".into();
+        let k4: Domain = "13..17".into();
+
+        let a = k.union(&k2);
+        let b = k3.union(&k4);
+        assert_eq!(
+            a.intersection(&b),
+            Domain {
+                union: vec![
+                    DomainRange {
+                        start: DomainBound::Bounded(3),
+                        end: DomainBound::Bounded(5)
+                    },
+                    DomainRange {
+                        start: DomainBound::Bounded(13),
+                        end: DomainBound::Bounded(15)
+                    }
+                ]
+            }
+        );
+    }
+}

src/lib.rs

@@ -1,3 +1,4 @@
 pub mod ast;
+pub mod domain;
 pub mod parsing;
 pub mod prover;

src/main.rs

@@ -1,5 +1,7 @@
 use picolog::ast::Body;
 use picolog::ast::Module;
+use picolog::ast::Predicate;
+use picolog::domain::Domain;
 
 fn main()
 {
@@ -8,33 +10,67 @@ fn main()
         .format_timestamp(None)
         .init();
     //println!("{:#?}", Module::parse_from_file("1.pl"));
+    // let module: Module = "
+    //     integer(zero).
+    //     integer(s(X)) :- integer(X).
+    //
+    //     add(X, zero, X).
+    //     add(X, s(Y), Z) :- add(s(X), Y, Z).
+    //
+    //     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.
+    //
+    //     l(X) :- in(X, 3..7).
+    // "
+    // .into();
+
+    let d1: Domain = "5..10".into();
+    let d2: Domain = "7..18".into();
+
     let module: Module = "
-        integer(zero).
-        integer(s(X)) :- integer(X).
-
-        add(X, zero, X).
-        add(X, s(Y), Z) :- add(s(X), Y, Z).
-
-        mult(zero, X, zero).
-        mult(s(Y), X, Z) :- mult(Y, X, W), add(W, X, Z).
+        hello(5..10).
+        world(7..18).
     "
     .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)
+    //let pred: Predicate = "hello(0..10).".into();
+    let show: Body = "hello(X), world(X)".into();
+
+    for c in module.prove(&show)
     {
         println!("true:");
         println!("{}", c.simplified());
         let _ = std::io::stdin().read_line(&mut String::new());
     }
-
+    //println!("{}", module.prove(&pred).unwrap());
+    // 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,25 +1,229 @@
-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::{
+    Parser, Result, Stateful,
+    ascii::{self, alphanumeric1, dec_int, multispace0},
+    combinator::{
+        Infix, Postfix, Prefix, alt, delimited, expression, opt, preceded, repeat, separated, seq,
+        terminated,
+    },
+    error::ContextError,
+    token::literal,
+};
 
-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::Variable;
+use crate::ast::{Body, OperatorType};
+use crate::domain::{Domain, DomainBound, DomainRange};
 
-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 domain_range_parse(input: &mut Stream) -> Result<DomainRange>
+{
+    let start = opt(dec_int.map(DomainBound::Bounded))
+        .map(|v| v.unwrap_or(DomainBound::Unbounded))
+        .parse_next(input)?;
+    literal("..").parse_next(input)?;
+    let end = opt(dec_int.map(DomainBound::Bounded))
+        .map(|v| v.unwrap_or(DomainBound::Unbounded))
+        .parse_next(input)?;
+    Ok(DomainRange { start, end })
+}
+
+pub fn domain_parse(input: &mut Stream) -> Result<Domain>
+{
+    // Domain is either a..b, ..
+    alt((domain_range_parse, dec_int.map(DomainRange::singleton)))
+        .map(|domain| Domain {
+            union: vec![domain],
+        })
+        .parse_next(input)
+}
+
+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())
@@ -35,11 +239,29 @@ 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, ")"),
+        domain_parse.map(Predicate::Domain),
+        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..,
@@ -53,7 +275,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))
@@ -61,7 +283,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
@@ -75,12 +297,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
@@ -89,8 +318,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()
     }
 }
 
@@ -108,8 +342,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()
     }
 }
 
@@ -119,7 +358,44 @@ 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()
+    }
+}
+
+impl<T> From<T> for Domain
+where
+    T: AsRef<str>,
+{
+    fn from(value: T) -> Self
+    {
+        let str: &str = value.as_ref();
+        domain_parse
+            .parse_next(&mut Stream {
+                input: str,
+                state: State::new(),
+            })
+            .unwrap()
+    }
+}
+
+impl<T> From<T> for DomainRange
+where
+    T: AsRef<str>,
+{
+    fn from(value: T) -> Self
+    {
+        let str: &str = value.as_ref();
+        domain_range_parse
+            .parse_next(&mut Stream {
+                input: str,
+                state: State::new(),
+            })
+            .unwrap()
     }
 }

src/prover.rs

@@ -135,6 +135,7 @@ impl Predicate
                     .map(|x| x.make_unique(counter.clone(), unique_map))
                     .collect(),
             ),
+            Predicate::Domain(domain) => Predicate::Domain(domain.clone()),
         }
     }
 }

src/prover/constraints.rs

@@ -4,11 +4,15 @@ use std::fmt::Display;
 use crate::ast::Body;
 use crate::ast::Predicate;
 use crate::ast::Variable;
+use crate::domain;
+use crate::domain::Domain;
+use crate::prover::predicate;
 
 #[derive(Clone, Debug)]
 pub struct Constraints
 {
-    pub(crate) set: HashMap<Variable, Predicate>,
+    pub(crate) predicates: HashMap<Variable, Predicate>,
+    pub(crate) domains: HashMap<Variable, Domain>,
 }
 
 impl Constraints
@@ -16,20 +20,33 @@ impl Constraints
     pub fn none() -> Self
     {
         Constraints {
-            set: HashMap::new(),
+            predicates: HashMap::new(),
+            domains: HashMap::new(),
         }
     }
 
-    pub fn with(variable: Variable, predicate: Predicate) -> Self
+    pub fn with(variable: Variable, predicate: Option<Predicate>, domain: Option<Domain>) -> Self
     {
         let mut c = Constraints::none();
-        c.set.insert(variable, predicate);
+        if let Some(predicate) = predicate
+        {
+            c.predicates.insert(variable.clone(), predicate);
+        }
+        if let Some(domain) = domain
+        {
+            c.domains.insert(variable, domain);
+        }
         c
     }
 
-    pub fn try_append(&mut self, variable: &Variable, predicate: &Predicate) -> bool
+    pub fn try_append(
+        &mut self,
+        variable: &Variable,
+        predicate: &Predicate,
+        domain: &Domain,
+    ) -> bool
     {
-        if let Some(other_predicate) = self.set.get(variable)
+        let predicates = if let Some(other_predicate) = self.predicates.get(variable)
         {
             if predicate == other_predicate
             {
@@ -46,7 +63,7 @@ impl Constraints
                 // We can try adding the unification contraints which is implicitely the same
                 if self.try_merge(&unification_contraints)
                 {
-                    self.set.insert(variable.clone(), predicate.clone());
+                    self.predicates.insert(variable.clone(), predicate.clone());
                     true
                 }
                 else
@@ -63,18 +80,40 @@ impl Constraints
         else
         {
             // No constraint
-            self.set.insert(variable.clone(), predicate.clone());
+            self.predicates
+                .insert(variable.clone(), (predicate.clone(), domain.clone()));
             true
+        };
+
+        // Check if domains are compatible
+        let domains = if let Some((_, other_domain)) = self.predicates.get_mut(variable)
+        {
+            let intersection = domain.intersection(other_domain);
+            if intersection.empty()
+            {
+                false
+            }
+            else
+            {
+                *other_domain = intersection;
+                true
+            }
         }
+        else
+        {
+            true
+        };
+
+        domains && predicates
     }
 
     pub fn try_merge(&mut self, constraints: &Constraints) -> bool
     {
         // Trying to merge, is just trying to add all of the constraints into self
         let mut ok = self.clone();
-        for (var, pred) in constraints.set.iter()
+        for (var, (pred, domain)) in constraints.predicates.iter()
         {
-            if !ok.try_append(var, pred)
+            if !ok.try_append(var, pred, domain)
             {
                 return false;
             }
@@ -93,24 +132,26 @@ impl Constraints
     pub fn simplified(&self) -> Constraints
     {
         let mut max_sub = Constraints::none();
-        for (var, pred) in self.set.iter()
+        for (var, (pred, domain)) in self.predicates.iter()
         {
-            max_sub.set.insert(var.clone(), pred.substitute(self));
+            max_sub
+                .predicates
+                .insert(var.clone(), (pred.substitute(self), domain.clone()));
         }
 
         let mut stripped = max_sub.clone();
-        'outer: for (var, _) in max_sub.set.iter()
+        'outer: for (var, _) in max_sub.predicates.iter()
         {
             if var.0.chars().next().is_some_and(|x| x == '_') || var.1.is_some()
             {
-                for (_, other_pred) in max_sub.set.iter()
+                for (_, (other_pred, _)) in max_sub.predicates.iter()
                 {
                     if other_pred.contains_variable(var)
                     {
                         continue 'outer;
                     }
                 }
-                stripped.set.remove(var);
+                stripped.predicates.remove(var);
             }
         }
 
@@ -126,7 +167,7 @@ impl Predicate
         {
             Predicate::Variable(name) =>
             {
-                if let Some(pred) = constraints.set.get(name)
+                if let Some((pred, _)) = constraints.predicates.get(name)
                 {
                     pred.substitute(constraints)
                 }
@@ -142,6 +183,7 @@ impl Predicate
                     .map(|x| x.substitute(constraints))
                     .collect(),
             ),
+            Predicate::Domain(domain) => Predicate::Domain(domain.clone()),
         }
     }
 
@@ -151,6 +193,7 @@ impl Predicate
         {
             Predicate::Variable(var_name) => name == var_name,
             Predicate::Fixed(_, predicates) => predicates.iter().any(|x| x.contains_variable(name)),
+            Predicate::Domain(_) => false,
         }
     }
 }
@@ -183,8 +226,8 @@ impl Display for Constraints
 {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result
     {
-        let len = self.set.len();
-        for (i, (var, pred)) in self.set.iter().enumerate()
+        let len = self.predicates.len();
+        for (i, (var, (pred, _))) in self.predicates.iter().enumerate()
         {
             write!(f, "{} = {}", var, pred)?;
             if i != len - 1
@@ -192,6 +235,15 @@ impl Display for Constraints
                 write!(f, ", ")?;
             }
         }
+        write!(f, " ;; ")?;
+        for (i, (var, (_, domain))) in self.predicates.iter().enumerate()
+        {
+            write!(f, "{} in {}", var, domain)?;
+            if i != len - 1
+            {
+                write!(f, ", ")?;
+            }
+        }
         Ok(())
     }
 }

src/prover/internal_operators.rs

@@ -0,0 +1,50 @@
+use crate::{ast::Predicate, prover::constraints::Constraints};
+
+impl Constraints
+{
+    pub fn collapsed_operators(&self) -> Constraints
+    {
+        let mut new_constraints = Constraints::none();
+        for (var, pred) in self.set.iter()
+        {
+            new_constraints
+                .set
+                .insert(var.clone(), pred.substitute(self).collapsed_operators());
+        }
+        new_constraints
+    }
+}
+
+impl Predicate
+{
+    pub fn collapsed_operators(&self) -> Predicate
+    {
+        match self
+        {
+            Predicate::Variable(variable) => Predicate::Variable(variable.clone()),
+            Predicate::Fixed(crate::ast::Functor::Operator(op), predicates)
+                if op.op == "+" && predicates.len() == 2 =>
+            {
+                match (predicates[0].clone(), predicates[1].clone())
+                {
+                    (Predicate::Number(a), Predicate::Number(b)) => Predicate::Number(a + b),
+                    _ => self.clone(),
+                }
+            }
+            Predicate::Fixed(crate::ast::Functor::Operator(op), predicates)
+                if op.op == "-" && predicates.len() == 2 =>
+            {
+                match (predicates[0].clone(), predicates[1].clone())
+                {
+                    (Predicate::Number(a), Predicate::Number(b)) => Predicate::Number(a - b),
+                    _ => self.clone(),
+                }
+            }
+            Predicate::Fixed(functor, predicates) => Predicate::Fixed(
+                functor.clone(),
+                predicates.iter().map(|x| x.collapsed_operators()).collect(),
+            ),
+            Predicate::Number(n) => Predicate::Number(*n),
+        }
+    }
+}

src/prover/tracing.rs

@@ -1,8 +1,8 @@
 use log::info;
-use owo_colors::OwoColorize;
-use owo_colors::Style;
 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)]

src/prover/unification.rs

@@ -1,4 +1,7 @@
+use std::clone;
+
 use crate::ast::Predicate;
+use crate::domain::{self, Domain};
 use crate::prover::constraints::Constraints;
 
 impl Predicate
@@ -16,9 +19,20 @@ impl Predicate
                 //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()))
+                match other
+                {
+                    Predicate::Domain(domain) => Some(Constraints::with(
+                        variable.clone(),
+                        other.clone(),
+                        domain.clone(),
+                    )),
+                    _ => Some(Constraints::with(
+                        variable.clone(),
+                        other.clone(),
+                        Domain::all(),
+                    )),
+                }
             }
-
             Predicate::Fixed(name, arguments) =>
             {
                 match other
@@ -29,7 +43,7 @@ impl Predicate
                         // (any)
                         // This is always true
                         //debug!("Unifying pred {} against var {}", self, other);
-                        Some(Constraints::with(var.clone(), self.clone()))
+                        Some(Constraints::with(var.clone(), self.clone(), Domain::all()))
                     }
                     // Match pred(X, Y, Z, ...) with pred(_X, _Y, _Z, ...)
                     Predicate::Fixed(other_name, other_arguments)
@@ -58,6 +72,20 @@ impl Predicate
                     _ => None,
                 }
             }
+            Predicate::Domain(domain) => match other
+            {
+                Predicate::Variable(variable) => Some(Constraints::with(
+                    variable.clone(),
+                    other.clone(),
+                    domain.clone(),
+                )),
+                Predicate::Fixed(_, _) => None,
+                Predicate::Domain(other_domain) if !domain.intersection(other_domain).empty() =>
+                {
+                    Some(Constraints::none())
+                }
+                Predicate::Domain(_) => None,
+            },
         }
     }
 }