First commit: parsing/unifying

.gitignore

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

1.pl

@@ -0,0 +1,3 @@
+world(zero).
+entier(s(X)) :- entier(X).
+mimi(hello(X)) :- X.

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",
+]

Cargo.toml

@@ -0,0 +1,8 @@
+[package]
+name = "nanolog"
+version = "0.1.0"
+edition = "2024"
+
+[dependencies]
+corosensei = "0.3.2"
+winnow = "0.7.14"

src/ast.rs

@@ -0,0 +1,105 @@
+use std::fmt::{Display, write};
+
+#[derive(Clone, Debug)]
+pub struct Module
+{
+    pub clauses: Vec<Clause>,
+}
+
+#[derive(Clone, Debug)]
+pub struct Clause
+{
+    pub head: Predicate,
+    pub body: Option<Body>,
+}
+
+#[derive(Clone, Debug)]
+pub enum Body
+{
+    Term(Predicate),
+    And(Vec<Body>),
+    Or(Vec<Body>),
+}
+
+#[derive(Clone, Debug)]
+pub enum Predicate
+{
+    Variable(String), // Upercase variable like X
+    Fixed(String, Vec<Predicate>),
+}
+
+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(())
+    }
+}

src/lib.rs

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

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);
+}

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<Predicate>
+{
+    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<Body>
+{
+    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<Body>
+{
+    // Parse and
+    separated(1.., body_parse_or, (multispace0, ",", multispace0))
+        .map(Body::And)
+        .parse_next(input)
+}
+
+pub fn clause_parse(input: &mut &str) -> Result<Clause>
+{
+    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<Module>
+{
+    let _: Result<&str, ContextError> = multispace0.parse_next(input);
+    separated(0.., clause_parse, multispace0)
+        .map(|clauses| Module { clauses })
+        .parse_next(input)
+}
+
+impl<T> From<T> for Module
+where
+    T: AsRef<str>,
+{
+    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<P: AsRef<Path>>(path: P) -> Self
+    {
+        std::fs::read_to_string(path).unwrap().into()
+    }
+}
+
+impl<T> From<T> for Predicate
+where
+    T: AsRef<str>,
+{
+    fn from(value: T) -> Self
+    {
+        let mut str: &str = value.as_ref();
+        predicate_parse.parse_next(&mut str).unwrap()
+    }
+}
+
+impl<T> From<T> for Body
+where
+    T: AsRef<str>,
+{
+    fn from(value: T) -> Self
+    {
+        let mut str: &str = value.as_ref();
+        body_parse.parse_next(&mut str).unwrap()
+    }
+}

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<Vec<Constraint>>
+    {
+        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)
+    }
+}