Adds operators

.gitmodules

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

Cargo.lock

@@ -277,8 +277,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,4 +7,4 @@ edition = "2024"
 env_logger = "0.11.8"
 litemap = "0.8.1"
 log = "0.4.29"
-winnow = "0.7.14"
+winnow = { version = "0.7.14", path = "./winnow" }

src/ast.rs

@@ -27,7 +27,31 @@ pub enum Body
 pub enum Predicate
 {
     Variable(Variable), // Upercase variable like X
-    Fixed(String, Vec<Predicate>),
+    Fixed(Functor, Vec<Predicate>),
+}
+
+#[derive(Clone, Debug, PartialEq)]
+pub enum Functor
+{
+    Operator(Operator),
+    Functor(String),
+}
+
+#[derive(Clone, Debug, PartialEq)]
+pub enum Operator
+{
+    Plus,
+    Minus,
+    Cons,
+    Custom(String, usize, OperatorType),
+}
+
+#[derive(Clone, Debug, PartialEq, Eq, Hash)]
+pub enum OperatorType
+{
+    Prefix,
+    Postfix,
+    Infix,
 }
 
 impl Display for Body
@@ -110,3 +134,28 @@ 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
+    {
+        match self
+        {
+            Operator::Plus => write!(f, "+"),
+            Operator::Minus => write!(f, "-"),
+            Operator::Cons => write!(f, "::"),
+            Operator::Custom(string, _, _) => write!(f, "{}", string),
+        }
+    }
+}

src/main.rs

@@ -17,11 +17,20 @@ fn main()
 
         mult(zero, X, zero).
         mult(s(Y), X, Z) :- mult(Y, X, W), add(W, X, Z).
+
+        A + B :- test.
+
+        op(8, xfx, ^).
+
+        A ^ B + C :- test.
+        (A::B)::C :- A.
+        [Hd|Tl] :- Hd::Tl.
     "
     .into();
 
-    //let prop: Body = "integer(s(X))".into();
-    let prop: Body = "mult(X, s(s(s(zero))), s(s(s(s(s(s(s(s(s(zero))))))))))".into();
+    println!("{}", module);
+    let prop: Body = "integer(s(X))".into();
+    // let prop: Body = "mult(X, s(s(s(zero))), s(s(s(s(s(s(s(s(s(zero))))))))))".into();
     for c in module.prove(&prop)
     {
         println!("true:");

src/parsing.rs

@@ -1,24 +1,206 @@
-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};
 
-pub fn predicate_parse(input: &mut &str) -> Result<Predicate>
+impl Operator
 {
-    let ident = alphanumeric0.parse_next(input)?;
+    pub fn get_precedence(&self) -> usize
+    {
+        match self
+        {
+            Operator::Plus | Operator::Minus => 10,
+            Operator::Cons => 12,
+            Operator::Custom(_, precedence, _) => *precedence,
+        }
+    }
+}
+
+impl Operator
+{
+    fn infix(value: String, state: &State) -> Result<Self>
+    {
+        match value.as_str()
+        {
+            "+" => Ok(Operator::Plus),
+            "::" => Ok(Operator::Cons),
+            _ => state
+                .custom_operators
+                .get(&(value, OperatorType::Infix))
+                .ok_or(ContextError::new())
+                .cloned(),
+        }
+    }
+    fn prefix(value: String, state: &State) -> Result<Self>
+    {
+        match value.as_str()
+        {
+            _ => state
+                .custom_operators
+                .get(&(value, OperatorType::Prefix))
+                .ok_or(ContextError::new())
+                .cloned(),
+        }
+    }
+    fn postfix(value: String, state: &State) -> Result<Self>
+    {
+        match value.as_str()
+        {
+            _ => 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" | "xfy" | "yfx" => OperatorType::Infix,
+        _ => unreachable!(),
+    };
+    input.state.custom_operators.insert(
+        (op.clone(), op_type.clone()),
+        Operator::Custom(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)?;
+    let precedence = op.get_precedence() as i64;
+    Ok(Infix::Left(precedence, op, |_, a, op, b| {
+        Ok(Predicate::Fixed(
+            Functor::Operator(op),
+            vec![a, b],
+        ))
+    }))
+}
+
+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())
@@ -34,11 +216,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 +251,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 +259,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 +273,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 +294,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 +318,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 +334,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

@@ -6,7 +6,6 @@ use std::cell::Cell;
 use std::rc::Rc;
 
 use litemap::LiteMap;
-use log::info;
 
 use crate::ast::Body;
 use crate::ast::Clause;

src/prover/tracing.rs

@@ -1,21 +1,17 @@
-use std::{default, fmt::Display};
+use std::fmt::Display;
 
 use log::info;
 
 #[derive(Clone, Copy)]
-pub enum ProofType
-{
+pub enum ProofType {
     Body,
     And,
     Predicate,
 }
 
-impl Display for ProofType
-{
-    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result
-    {
-        match self
-        {
+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"),
@@ -23,41 +19,33 @@ impl Display for ProofType
     }
 }
 
-pub trait Tracer
-{
+pub trait Tracer {
     fn begin_proof(&self, proof_type: ProofType) -> Self;
     fn print_step<T: Display>(&self, show: T);
     fn end_proof(self);
 }
 
-pub struct SimpleTracer
-{
+pub struct SimpleTracer {
     proof_type: ProofType,
 }
 
-impl SimpleTracer
-{
-    pub fn new(proof_type: ProofType) -> Self
-    {
+impl SimpleTracer {
+    pub fn new(proof_type: ProofType) -> Self {
         Self { proof_type }
     }
 }
 
-impl Tracer for SimpleTracer
-{
-    fn begin_proof(&self, proof_type: ProofType) -> Self
-    {
+impl Tracer for SimpleTracer {
+    fn begin_proof(&self, proof_type: ProofType) -> Self {
         SimpleTracer { proof_type }
     }
 
-    fn print_step<T: Display>(&self, show: T)
-    {
+    fn print_step<T: Display>(&self, show: T) {
         let str = format!("{}", self.proof_type);
         info!(target: &str, "{}", show);
     }
 
-    fn end_proof(self)
-    {
+    fn end_proof(self) {
         todo!()
     }
 }

src/prover/unification.rs

@@ -1,4 +1,3 @@
-use log::debug;
 
 use crate::ast::Predicate;
 use crate::prover::constraints::Constraints;