From 21414f75dbe9792ebe542c5be4961da8f4ddd024 Mon Sep 17 00:00:00 2001 From: supersurviveur Date: Tue, 10 Feb 2026 15:41:56 +0100 Subject: [PATCH] Adds operators --- .gitmodules | 4 + Cargo.lock | 2 - Cargo.toml | 2 +- src/ast.rs | 51 ++++++- src/main.rs | 13 +- src/parsing.rs | 277 ++++++++++++++++++++++++++++++++++---- src/prover.rs | 1 - src/prover/tracing.rs | 38 ++---- src/prover/unification.rs | 1 - winnow | 1 + 10 files changed, 329 insertions(+), 61 deletions(-) create mode 100644 .gitmodules create mode 160000 winnow diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 0000000..e24addf --- /dev/null +++ b/.gitmodules @@ -0,0 +1,4 @@ +[submodule "winnow"] + path = winnow + url = git@github.com:supersurviveur/winnow.git + branch = operator-in-expression diff --git a/Cargo.lock b/Cargo.lock index 3d771a3..ea83c5f 100644 --- a/Cargo.lock +++ b/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", ] diff --git a/Cargo.toml b/Cargo.toml index 6952248..421cf1a 100644 --- a/Cargo.toml +++ b/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" } diff --git a/src/ast.rs b/src/ast.rs index f56d75d..55da5a5 100644 --- a/src/ast.rs +++ b/src/ast.rs @@ -27,7 +27,31 @@ pub enum Body pub enum Predicate { Variable(Variable), // Upercase variable like X - Fixed(String, Vec), + Fixed(Functor, Vec), +} + +#[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), + } + } +} diff --git a/src/main.rs b/src/main.rs index d120503..06727e0 100644 --- a/src/main.rs +++ b/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:"); diff --git a/src/parsing.rs b/src/parsing.rs index 44d5dfc..9ee938f 100644 --- a/src/parsing.rs +++ b/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 +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 + { + 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 + { + match value.as_str() + { + _ => state + .custom_operators + .get(&(value, OperatorType::Prefix)) + .ok_or(ContextError::new()) + .cloned(), + } + } + fn postfix(value: String, state: &State) -> Result + { + 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 +{ + 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_parse(input).map(|op| Operator::infix(op, &input.state))? +} +pub fn operator_parse_postfix(input: &mut Stream) -> Result +{ + operator_parse(input).map(|op| Operator::postfix(op, &input.state))? +} +pub fn operator_parse_prefix(input: &mut Stream) -> Result +{ + 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, 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, 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, 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 +{ + 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 +{ + 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 ) .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 +pub fn predicate_parse_recursive(input: &mut Stream) -> Result +{ + alt(( + delimited("(", predicate_parse, ")"), + predicate_parse_variable_or_functor, + )) + .parse_next(input) +} + +pub fn predicate_parse(input: &mut Stream) -> Result +{ + alt((predicate_parse_expression, predicate_parse_recursive)).parse_next(input) +} + +fn body_parse_or(input: &mut Stream) -> Result { separated( 1.., @@ -52,7 +251,7 @@ fn body_parse_or(input: &mut &str) -> Result .parse_next(input) } -pub fn body_parse(input: &mut &str) -> Result +pub fn body_parse(input: &mut Stream) -> Result { // Parse and separated(1.., body_parse_or, (multispace0, ",", multispace0)) @@ -60,7 +259,7 @@ pub fn body_parse(input: &mut &str) -> Result .parse_next(input) } -pub fn clause_parse(input: &mut &str) -> Result +pub fn clause_parse(input: &mut Stream) -> Result { seq! { Clause @@ -74,12 +273,19 @@ pub fn clause_parse(input: &mut &str) -> Result .parse_next(input) } -pub fn module_parse(input: &mut &str) -> Result +pub fn module_parse(input: &mut Stream) -> Result { 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 From 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() } } diff --git a/src/prover.rs b/src/prover.rs index d081f10..9ccff63 100644 --- a/src/prover.rs +++ b/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; diff --git a/src/prover/tracing.rs b/src/prover/tracing.rs index 94ef708..ea856ac 100644 --- a/src/prover/tracing.rs +++ b/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(&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(&self, show: T) - { + fn print_step(&self, show: T) { let str = format!("{}", self.proof_type); info!(target: &str, "{}", show); } - fn end_proof(self) - { + fn end_proof(self) { todo!() } } diff --git a/src/prover/unification.rs b/src/prover/unification.rs index 747d458..91ce1b9 100644 --- a/src/prover/unification.rs +++ b/src/prover/unification.rs @@ -1,4 +1,3 @@ -use log::debug; use crate::ast::Predicate; use crate::prover::constraints::Constraints; diff --git a/winnow b/winnow new file mode 160000 index 0000000..cc0438a --- /dev/null +++ b/winnow @@ -0,0 +1 @@ +Subproject commit cc0438a28f73307c1e6a6a13ce89f97b249353ce