From 4039394e42788d4718dd067a816896450cb14e87 Mon Sep 17 00:00:00 2001 From: Albin Chaboissier Date: Sat, 7 Feb 2026 14:49:06 +0100 Subject: [PATCH] First commit: parsing/unifying --- .gitignore | 1 + 1.pl | 3 ++ Cargo.lock | 136 ++++++++++++++++++++++++++++++++++++++++++++++++ Cargo.toml | 8 +++ src/ast.rs | 105 +++++++++++++++++++++++++++++++++++++ src/lib.rs | 3 ++ src/main.rs | 19 +++++++ src/parsing.rs | 118 ++++++++++++++++++++++++++++++++++++++++++ src/prover.rs | 137 +++++++++++++++++++++++++++++++++++++++++++++++++ 9 files changed, 530 insertions(+) create mode 100644 .gitignore create mode 100644 1.pl create mode 100644 Cargo.lock create mode 100644 Cargo.toml create mode 100644 src/ast.rs create mode 100644 src/lib.rs create mode 100644 src/main.rs create mode 100644 src/parsing.rs create mode 100644 src/prover.rs diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..ea8c4bf --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +/target diff --git a/1.pl b/1.pl new file mode 100644 index 0000000..f861a3c --- /dev/null +++ b/1.pl @@ -0,0 +1,3 @@ +world(zero). +entier(s(X)) :- entier(X). +mimi(hello(X)) :- X. diff --git a/Cargo.lock b/Cargo.lock new file mode 100644 index 0000000..db5cff1 --- /dev/null +++ b/Cargo.lock @@ -0,0 +1,136 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 4 + +[[package]] +name = "autocfg" +version = "1.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c08606f8c3cbf4ce6ec8e28fb0014a2c086708fe954eaa885384a6165172e7e8" + +[[package]] +name = "cfg-if" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9330f8b2ff13f34540b44e946ef35111825727b38d33286ef986142615121801" + +[[package]] +name = "corosensei" +version = "0.3.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2b2b4c7e3e97730e6b0b8c5ff5ca82c663d1a645e4f630f4fa4c24e80626787e" +dependencies = [ + "autocfg", + "cfg-if", + "libc", + "scopeguard", + "windows-sys", +] + +[[package]] +name = "libc" +version = "0.2.180" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bcc35a38544a891a5f7c865aca548a982ccb3b8650a5b06d0fd33a10283c56fc" + +[[package]] +name = "memchr" +version = "2.8.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f8ca58f447f06ed17d5fc4043ce1b10dd205e060fb3ce5b979b8ed8e59ff3f79" + +[[package]] +name = "nanolog" +version = "0.1.0" +dependencies = [ + "corosensei", + "winnow", +] + +[[package]] +name = "scopeguard" +version = "1.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49" + +[[package]] +name = "windows-sys" +version = "0.59.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1e38bc4d79ed67fd075bcc251a1c39b32a1776bbe92e5bef1f0bf1f8c531853b" +dependencies = [ + "windows-targets", +] + +[[package]] +name = "windows-targets" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9b724f72796e036ab90c1021d4780d4d3d648aca59e491e6b98e725b84e99973" +dependencies = [ + "windows_aarch64_gnullvm", + "windows_aarch64_msvc", + "windows_i686_gnu", + "windows_i686_gnullvm", + "windows_i686_msvc", + "windows_x86_64_gnu", + "windows_x86_64_gnullvm", + "windows_x86_64_msvc", +] + +[[package]] +name = "windows_aarch64_gnullvm" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "32a4622180e7a0ec044bb555404c800bc9fd9ec262ec147edd5989ccd0c02cd3" + +[[package]] +name = "windows_aarch64_msvc" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "09ec2a7bb152e2252b53fa7803150007879548bc709c039df7627cabbd05d469" + +[[package]] +name = "windows_i686_gnu" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8e9b5ad5ab802e97eb8e295ac6720e509ee4c243f69d781394014ebfe8bbfa0b" + +[[package]] +name = "windows_i686_gnullvm" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0eee52d38c090b3caa76c563b86c3a4bd71ef1a819287c19d586d7334ae8ed66" + +[[package]] +name = "windows_i686_msvc" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "240948bc05c5e7c6dabba28bf89d89ffce3e303022809e73deaefe4f6ec56c66" + +[[package]] +name = "windows_x86_64_gnu" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "147a5c80aabfbf0c7d901cb5895d1de30ef2907eb21fbbab29ca94c5b08b1a78" + +[[package]] +name = "windows_x86_64_gnullvm" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "24d5b23dc417412679681396f2b49f3de8c1473deb516bd34410872eff51ed0d" + +[[package]] +name = "windows_x86_64_msvc" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec" + +[[package]] +name = "winnow" +version = "0.7.14" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5a5364e9d77fcdeeaa6062ced926ee3381faa2ee02d3eb83a5c27a8825540829" +dependencies = [ + "memchr", +] diff --git a/Cargo.toml b/Cargo.toml new file mode 100644 index 0000000..78905ff --- /dev/null +++ b/Cargo.toml @@ -0,0 +1,8 @@ +[package] +name = "nanolog" +version = "0.1.0" +edition = "2024" + +[dependencies] +corosensei = "0.3.2" +winnow = "0.7.14" diff --git a/src/ast.rs b/src/ast.rs new file mode 100644 index 0000000..fe2258a --- /dev/null +++ b/src/ast.rs @@ -0,0 +1,105 @@ +use std::fmt::{Display, write}; + +#[derive(Clone, Debug)] +pub struct Module +{ + pub clauses: Vec, +} + +#[derive(Clone, Debug)] +pub struct Clause +{ + pub head: Predicate, + pub body: Option, +} + +#[derive(Clone, Debug)] +pub enum Body +{ + Term(Predicate), + And(Vec), + Or(Vec), +} + +#[derive(Clone, Debug)] +pub enum Predicate +{ + Variable(String), // Upercase variable like X + Fixed(String, Vec), +} + +impl Display for Body +{ + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result + { + match self + { + Body::Term(predicate) => write!(f, "{}", predicate), + Body::And(items) | Body::Or(items) => + { + let len = items.len(); + for (i, item) in items.iter().enumerate() + { + write!(f, "{}", item)?; + if i != len - 1 + { + write!(f, ",")?; + } + } + Ok(()) + } + } + } +} + +impl Display for Predicate +{ + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result + { + match self + { + Predicate::Variable(variable) => write!(f, "{}", variable), + Predicate::Fixed(name, predicates) => + { + write!(f, "{}", name)?; + if !predicates.is_empty() + { + write!(f, "(")?; + for predicate in predicates.iter() + { + write!(f, "{}", predicate)?; + } + write!(f, ")") + } + else + { + Ok(()) + } + } + } + } +} + +impl Display for Clause +{ + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result + { + write!(f, "{}", self.head)?; + self.body + .as_ref() + .map_or_else(|| Ok(()), |body| write!(f, ":- {}", body))?; + write!(f, ".") + } +} + +impl Display for Module +{ + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result + { + for clause in self.clauses.iter() + { + writeln!(f, "{}", clause)?; + } + Ok(()) + } +} diff --git a/src/lib.rs b/src/lib.rs new file mode 100644 index 0000000..8b27f29 --- /dev/null +++ b/src/lib.rs @@ -0,0 +1,3 @@ +pub mod ast; +pub mod parsing; +pub mod prover; diff --git a/src/main.rs b/src/main.rs new file mode 100644 index 0000000..931646c --- /dev/null +++ b/src/main.rs @@ -0,0 +1,19 @@ +use nanolog::ast::{Body, Module, Predicate}; + +fn main() +{ + //println!("{:#?}", Module::parse_from_file("1.pl")); + let module: Module = " + integer(zero). + integer(s(X)) :- integer(X). + " + .into(); + + let a: Predicate = "zero".into(); + let b: Predicate = "X".into(); + + println!("{:?}", a.unify(&b)); + + // let body: Body = "integer(s(s(s(s(zer))))).".into(); + // body.prove(&module); +} diff --git a/src/parsing.rs b/src/parsing.rs new file mode 100644 index 0000000..b3b2a01 --- /dev/null +++ b/src/parsing.rs @@ -0,0 +1,118 @@ +use std::path::Path; + +use winnow::{ + Parser, Result, + ascii::{alphanumeric0, multispace0}, + combinator::{alt, delimited, opt, separated, seq}, + error::ContextError, + token::literal, +}; + +use crate::ast::{Body, Clause, Module, Predicate}; + +pub fn predicate_parse(input: &mut &str) -> Result +{ + let ident = alphanumeric0.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))) + } + else + { + let arguments = delimited( + ("(", multispace0), + separated(1.., predicate_parse, ","), + (multispace0, ")"), + ) + .parse_next(input) + .unwrap_or(Vec::new()); + Ok(Predicate::Fixed(String::from(ident), arguments)) + } +} + +fn body_parse_or(input: &mut &str) -> Result +{ + separated( + 1.., + alt(( + delimited("(", body_parse, ")"), + predicate_parse.map(Body::Term), + )), + (multispace0, ";", multispace0), + ) + .map(Body::Or) + .parse_next(input) +} + +pub fn body_parse(input: &mut &str) -> Result +{ + // Parse and + separated(1.., body_parse_or, (multispace0, ",", multispace0)) + .map(Body::And) + .parse_next(input) +} + +pub fn clause_parse(input: &mut &str) -> Result +{ + seq! { + Clause + { + head: predicate_parse, + body: opt((multispace0, ":-", multispace0, body_parse).map(|(_, _, _, b)| b)), + _: multispace0, + _: "." + } + } + .parse_next(input) +} + +pub fn module_parse(input: &mut &str) -> Result +{ + let _: Result<&str, ContextError> = multispace0.parse_next(input); + separated(0.., clause_parse, multispace0) + .map(|clauses| Module { clauses }) + .parse_next(input) +} + +impl From for Module +where + T: AsRef, +{ + fn from(value: T) -> Self + { + let mut str: &str = value.as_ref(); + module_parse.parse_next(&mut str).unwrap() + } +} + +impl Module +{ + pub fn parse_from_file>(path: P) -> Self + { + std::fs::read_to_string(path).unwrap().into() + } +} + +impl From for Predicate +where + T: AsRef, +{ + fn from(value: T) -> Self + { + let mut str: &str = value.as_ref(); + predicate_parse.parse_next(&mut str).unwrap() + } +} + +impl From for Body +where + T: AsRef, +{ + fn from(value: T) -> Self + { + let mut str: &str = value.as_ref(); + body_parse.parse_next(&mut str).unwrap() + } +} diff --git a/src/prover.rs b/src/prover.rs new file mode 100644 index 0000000..8901bcb --- /dev/null +++ b/src/prover.rs @@ -0,0 +1,137 @@ +use std::fmt::{Display, write}; + +use crate::ast::{Body, Module, Predicate}; + +#[derive(Clone, Debug)] +pub struct Constraint +{ + variable: String, + predicate: Predicate, +} + +impl Body +{ + pub fn prove(&self, context: &Module) + { + match self + { + Body::Term(predicate) => + { + for candidate in context.clauses.iter() + { + println!("[Trying] {} unify with {}", predicate, candidate.head); + if let Some(new_constraints) = predicate.unify(&candidate.head) + { + for x in new_constraints.iter() + { + println!("[Constraints] {}", x); + } + match &candidate.body + { + Some(next) => + { + let mut next = next.clone(); + new_constraints.iter().for_each(|x| next.substitute(x)); + next.prove(context) + } + None => + { + println!("TRUE."); + return; + } + } + } + } + } + Body::And(x) => x.iter().for_each(|x| x.prove(context)), + Body::Or(x) => x.iter().for_each(|x| x.prove(context)), + } + } + + pub fn substitute(&mut self, constraint: &Constraint) + { + match self + { + Body::Term(predicate) => predicate.substitute(constraint), + Body::And(items) => items.iter_mut().for_each(|x| x.substitute(constraint)), + Body::Or(items) => items.iter_mut().for_each(|x| x.substitute(constraint)), + } + } +} + +impl Predicate +{ + pub fn unify(&self, other: &Predicate) -> Option> + { + match self + { + Predicate::Variable(variable) => Some(vec![Constraint { + variable: variable.clone(), + predicate: other.clone(), + }]), + Predicate::Fixed(name, predicates) => match other + { + Predicate::Variable(variable) => Some(vec![Constraint { + variable: variable.clone(), + predicate: self.clone(), + }]), + Predicate::Fixed(other_name, other_predicates) + if other_name == name && predicates.len() == other_predicates.len() => + { + if predicates.len() == 0 + { + Some(vec![]) + } + else + { + predicates + .iter() + .zip(other_predicates) + .map(|(a, b)| { + println!("[Unify] {} unify with {}", a, b); + let k = a.unify(b); + println!("{:?}", k); + k + }) + .reduce(|prev, now| match (prev, now) + { + (Some(c1), Some(c2)) => + { + let mut c = c1.clone(); + c.extend_from_slice(c2.as_slice()); + Some(c) + } + _ => None, + }) + .flatten() + } + } + Predicate::Fixed(_, _) => None, + }, + } + } + + pub fn substitute(&mut self, constraint: &Constraint) + { + match self + { + Predicate::Variable(name) if *name == constraint.variable => + { + *self = constraint.predicate.clone() + } + Predicate::Variable(_) => (), + Predicate::Fixed(_, predicates) => + { + predicates.iter_mut().for_each(|x| x.substitute(constraint)) + } + } + } +} + +impl Display for Constraint +{ + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result + { + write!(f, "{} = {}", self.variable, self.predicate) + } +}