From 3c51b65be2be7a510e73d392394bb8e2d342c793 Mon Sep 17 00:00:00 2001 From: Albin Chaboissier Date: Sat, 7 Feb 2026 22:15:07 +0100 Subject: [PATCH] Coroutines --- 1.pl | 8 +- Cargo.lock | 254 ++++++++++++++++++++++++++++++++++++++++++++++- Cargo.toml | 2 + src/ast.rs | 10 +- src/main.rs | 29 ++++-- src/parsing.rs | 25 +++-- src/prover.rs | 263 ++++++++++++++++++++++++++++++++++++++++--------- 7 files changed, 524 insertions(+), 67 deletions(-) diff --git a/1.pl b/1.pl index f861a3c..1852205 100644 --- a/1.pl +++ b/1.pl @@ -1,3 +1,5 @@ -world(zero). -entier(s(X)) :- entier(X). -mimi(hello(X)) :- X. +int(zero). +int(s(X)) :- int(X). +add(X, zero, X). +add(X, s(Y), Z) :- add(s(X), Y, Z). + diff --git a/Cargo.lock b/Cargo.lock index db5cff1..9075aa4 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2,6 +2,65 @@ # It is not intended for manual editing. version = 4 +[[package]] +name = "aho-corasick" +version = "1.1.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ddd31a130427c27518df266943a5308ed92d4b226cc639f5a8f1002816174301" +dependencies = [ + "memchr", +] + +[[package]] +name = "anstream" +version = "0.6.21" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "43d5b281e737544384e969a5ccad3f1cdd24b48086a0fc1b2a5262a26b8f4f4a" +dependencies = [ + "anstyle", + "anstyle-parse", + "anstyle-query", + "anstyle-wincon", + "colorchoice", + "is_terminal_polyfill", + "utf8parse", +] + +[[package]] +name = "anstyle" +version = "1.0.13" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5192cca8006f1fd4f7237516f40fa183bb07f8fbdfedaa0036de5ea9b0b45e78" + +[[package]] +name = "anstyle-parse" +version = "0.2.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4e7644824f0aa2c7b9384579234ef10eb7efb6a0deb83f9630a49594dd9c15c2" +dependencies = [ + "utf8parse", +] + +[[package]] +name = "anstyle-query" +version = "1.1.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "40c48f72fd53cd289104fc64099abca73db4166ad86ea0b4341abe65af83dadc" +dependencies = [ + "windows-sys 0.61.2", +] + +[[package]] +name = "anstyle-wincon" +version = "3.0.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "291e6a250ff86cd4a820112fb8898808a366d8f9f58ce16d1f538353ad55747d" +dependencies = [ + "anstyle", + "once_cell_polyfill", + "windows-sys 0.61.2", +] + [[package]] name = "autocfg" version = "1.5.0" @@ -14,6 +73,12 @@ version = "1.0.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9330f8b2ff13f34540b44e946ef35111825727b38d33286ef986142615121801" +[[package]] +name = "colorchoice" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b05b61dc5112cbb17e4b6cd61790d9845d13888356391624cbe7e41efeac1e75" + [[package]] name = "corosensei" version = "0.3.2" @@ -24,7 +89,60 @@ dependencies = [ "cfg-if", "libc", "scopeguard", - "windows-sys", + "windows-sys 0.59.0", +] + +[[package]] +name = "env_filter" +version = "0.1.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1bf3c259d255ca70051b30e2e95b5446cdb8949ac4cd22c0d7fd634d89f568e2" +dependencies = [ + "log", + "regex", +] + +[[package]] +name = "env_logger" +version = "0.11.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "13c863f0904021b108aa8b2f55046443e6b1ebde8fd4a15c399893aae4fa069f" +dependencies = [ + "anstream", + "anstyle", + "env_filter", + "jiff", + "log", +] + +[[package]] +name = "is_terminal_polyfill" +version = "1.70.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a6cb138bb79a146c1bd460005623e142ef0181e3d0219cb493e02f7d08a35695" + +[[package]] +name = "jiff" +version = "0.2.19" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d89a5b5e10d5a9ad6e5d1f4bd58225f655d6fe9767575a5e8ac5a6fe64e04495" +dependencies = [ + "jiff-static", + "log", + "portable-atomic", + "portable-atomic-util", + "serde_core", +] + +[[package]] +name = "jiff-static" +version = "0.2.19" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ff7a39c8862fc1369215ccf0a8f12dd4598c7f6484704359f0351bd617034dbf" +dependencies = [ + "proc-macro2", + "quote", + "syn", ] [[package]] @@ -33,6 +151,12 @@ version = "0.2.180" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "bcc35a38544a891a5f7c865aca548a982ccb3b8650a5b06d0fd33a10283c56fc" +[[package]] +name = "log" +version = "0.4.29" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5e5032e24019045c762d3c0f28f5b6b8bbf38563a65908389bf7978758920897" + [[package]] name = "memchr" version = "2.8.0" @@ -44,15 +168,134 @@ name = "nanolog" version = "0.1.0" dependencies = [ "corosensei", + "env_logger", + "log", "winnow", ] +[[package]] +name = "once_cell_polyfill" +version = "1.70.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "384b8ab6d37215f3c5301a95a4accb5d64aa607f1fcb26a11b5303878451b4fe" + +[[package]] +name = "portable-atomic" +version = "1.13.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c33a9471896f1c69cecef8d20cbe2f7accd12527ce60845ff44c153bb2a21b49" + +[[package]] +name = "portable-atomic-util" +version = "0.2.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7a9db96d7fa8782dd8c15ce32ffe8680bbd1e978a43bf51a34d39483540495f5" +dependencies = [ + "portable-atomic", +] + +[[package]] +name = "proc-macro2" +version = "1.0.106" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8fd00f0bb2e90d81d1044c2b32617f68fcb9fa3bb7640c23e9c748e53fb30934" +dependencies = [ + "unicode-ident", +] + +[[package]] +name = "quote" +version = "1.0.44" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "21b2ebcf727b7760c461f091f9f0f539b77b8e87f2fd88131e7f1b433b3cece4" +dependencies = [ + "proc-macro2", +] + +[[package]] +name = "regex" +version = "1.12.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e10754a14b9137dd7b1e3e5b0493cc9171fdd105e0ab477f51b72e7f3ac0e276" +dependencies = [ + "aho-corasick", + "memchr", + "regex-automata", + "regex-syntax", +] + +[[package]] +name = "regex-automata" +version = "0.4.14" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6e1dd4122fc1595e8162618945476892eefca7b88c52820e74af6262213cae8f" +dependencies = [ + "aho-corasick", + "memchr", + "regex-syntax", +] + +[[package]] +name = "regex-syntax" +version = "0.8.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a96887878f22d7bad8a3b6dc5b7440e0ada9a245242924394987b21cf2210a4c" + [[package]] name = "scopeguard" version = "1.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49" +[[package]] +name = "serde_core" +version = "1.0.228" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "41d385c7d4ca58e59fc732af25c3983b67ac852c1a25000afe1175de458b67ad" +dependencies = [ + "serde_derive", +] + +[[package]] +name = "serde_derive" +version = "1.0.228" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d540f220d3187173da220f885ab66608367b6574e925011a9353e4badda91d79" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "syn" +version = "2.0.114" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d4d107df263a3013ef9b1879b0df87d706ff80f65a86ea879bd9c31f9b307c2a" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + +[[package]] +name = "unicode-ident" +version = "1.0.22" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9312f7c4f6ff9069b165498234ce8be658059c6728633667c526e27dc2cf1df5" + +[[package]] +name = "utf8parse" +version = "0.2.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "06abde3611657adf66d383f00b093d7faecc7fa57071cce2578660c9f1010821" + +[[package]] +name = "windows-link" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f0805222e57f7521d6a62e36fa9163bc891acd422f971defe97d64e70d0a4fe5" + [[package]] name = "windows-sys" version = "0.59.0" @@ -62,6 +305,15 @@ dependencies = [ "windows-targets", ] +[[package]] +name = "windows-sys" +version = "0.61.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ae137229bcbd6cdf0f7b80a31df61766145077ddf49416a728b02cb3921ff3fc" +dependencies = [ + "windows-link", +] + [[package]] name = "windows-targets" version = "0.52.6" diff --git a/Cargo.toml b/Cargo.toml index 78905ff..b277a62 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -5,4 +5,6 @@ edition = "2024" [dependencies] corosensei = "0.3.2" +env_logger = "0.11.8" +log = "0.4.29" winnow = "0.7.14" diff --git a/src/ast.rs b/src/ast.rs index fe2258a..f02aa9e 100644 --- a/src/ast.rs +++ b/src/ast.rs @@ -1,4 +1,5 @@ -use std::fmt::{Display, write}; +use std::fmt::Display; +use std::fmt::write; #[derive(Clone, Debug)] pub struct Module @@ -65,9 +66,14 @@ impl Display for Predicate if !predicates.is_empty() { write!(f, "(")?; - for predicate in predicates.iter() + let len = predicates.len(); + for (i, predicate) in predicates.iter().enumerate() { write!(f, "{}", predicate)?; + if i != len - 1 + { + write!(f, ", ")?; + } } write!(f, ")") } diff --git a/src/main.rs b/src/main.rs index 931646c..d313fe1 100644 --- a/src/main.rs +++ b/src/main.rs @@ -1,19 +1,36 @@ -use nanolog::ast::{Body, Module, Predicate}; +use corosensei::Coroutine; +use nanolog::ast::Body; +use nanolog::ast::Module; +use nanolog::ast::Predicate; fn main() { + env_logger::builder() + .filter_level(log::LevelFilter::Info) + .format_timestamp(None) + .format_module_path(false) + .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). " .into(); - let a: Predicate = "zero".into(); - let b: Predicate = "X".into(); + // let a: Predicate = "integer(s(zero))".into(); + // let b: Predicate = "integer(s(X))".into(); + // + // println!("{:?}", a.unify(&b)); - println!("{:?}", a.unify(&b)); + let body: Body = "add(s(s(zero)), s(zero), s(s(s(zero))))".into(); + let body: Body = "add(s(zero), s(zero), X).".into(); + body.prove_in_module(&module).next().next(); - // let body: Body = "integer(s(s(s(s(zer))))).".into(); - // body.prove(&module); + // let body: Body = "integer(X).".into(); + // body.prove_in_module(&module).next().next(); + + //println!("{}", module); + // } diff --git a/src/parsing.rs b/src/parsing.rs index b3b2a01..fc148fc 100644 --- a/src/parsing.rs +++ b/src/parsing.rs @@ -1,14 +1,21 @@ use std::path::Path; -use winnow::{ - Parser, Result, - ascii::{alphanumeric0, multispace0}, - combinator::{alt, delimited, opt, separated, seq}, - error::ContextError, - token::literal, -}; +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::token::literal; -use crate::ast::{Body, Clause, Module, Predicate}; +use crate::ast::Body; +use crate::ast::Clause; +use crate::ast::Module; +use crate::ast::Predicate; pub fn predicate_parse(input: &mut &str) -> Result { @@ -23,7 +30,7 @@ pub fn predicate_parse(input: &mut &str) -> Result { let arguments = delimited( ("(", multispace0), - separated(1.., predicate_parse, ","), + separated(1.., predicate_parse, (multispace0, ",", multispace0)), (multispace0, ")"), ) .parse_next(input) diff --git a/src/prover.rs b/src/prover.rs index 8901bcb..e971a34 100644 --- a/src/prover.rs +++ b/src/prover.rs @@ -1,6 +1,19 @@ -use std::fmt::{Display, write}; +use std::cell::Cell; +use std::cell::RefCell; +use std::collections::HashMap; +use std::fmt::Display; +use std::fmt::write; +use std::rc::Rc; -use crate::ast::{Body, Module, Predicate}; +use corosensei::Coroutine; +use corosensei::Yielder; +use log::info; +use log::warn; + +use crate::ast::Body; +use crate::ast::Clause; +use crate::ast::Module; +use crate::ast::Predicate; #[derive(Clone, Debug)] pub struct Constraint @@ -9,42 +22,77 @@ pub struct Constraint predicate: Predicate, } +struct Context<'a, 'b> +{ + module: &'a Module, + yielder: &'b Yielder<(), Vec>, + depth: usize, + global_counter: Rc>, +} + +impl Context<'_, '_> +{ + pub fn descend(&self) -> Self + { + Context { + module: self.module, + depth: self.depth + 1, + yielder: self.yielder, + global_counter: self.global_counter.clone(), + } + } +} + +pub struct Prover +{ + coroutine: Coroutine<(), Vec, ()>, +} + +impl Prover +{ + pub fn next(mut self) -> Prover + { + self.coroutine.resume(()); + self + } +} + impl Body { - pub fn prove(&self, context: &Module) + pub fn prove_in_module(&self, module: &Module) -> Prover + { + let cloned_body = self.clone(); + let cloned_module = module.clone(); + let coroutine = Coroutine::new(move |yielder, ()| { + cloned_body.prove(Context { + module: &cloned_module, + depth: 0, + yielder, + global_counter: Rc::new(Cell::new(0)), + }); + }); + Prover { coroutine } + } + + fn prove(&self, context: Context<'_, '_>) { match self { Body::Term(predicate) => { - for candidate in context.clauses.iter() + for candidate in context.module.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; - } - } - } + predicate.prove_with_clause( + &candidate.unique(context.global_counter.clone()), + context.descend(), + ); } } - Body::And(x) => x.iter().for_each(|x| x.prove(context)), - Body::Or(x) => x.iter().for_each(|x| x.prove(context)), + Body::And(x) => x.iter().for_each(|x| x.prove(context.descend())), + Body::Or(x) => x.iter().for_each(|x| { + info!(target: "Proving", "{}", self); + x.prove(context.descend()) + }), } } @@ -57,10 +105,61 @@ impl Body Body::Or(items) => items.iter_mut().for_each(|x| x.substitute(constraint)), } } + + fn unique_with(&self, counter: Rc>, map: &mut HashMap) -> Self + { + match self + { + Body::Term(predicate) => Body::Term(predicate.unique_with(counter.clone(), map)), + Body::And(items) => Body::And( + items + .iter() + .map(|x| x.unique_with(counter.clone(), map)) + .collect(), + ), + Body::Or(items) => Body::Or( + items + .iter() + .map(|x| x.unique_with(counter.clone(), map)) + .collect(), + ), + } + } } impl Predicate { + fn prove_with_clause(&self, clause: &Clause, context: Context<'_, '_>) + { + info!(target: "With", "{}", clause); + if let Some(constraints) = self.unify(&clause.head) + { + for x in constraints.iter() + { + info!(target: "Constraints", "{}", x); + } + + match &clause.body + { + Some(body) => + { + let mut next = body.clone(); + constraints.iter().for_each(|x| next.substitute(x)); + next.prove(context.descend()) + } + None => + { + info!(target: "[Solution]", "true."); + context.yielder.suspend(constraints); + } + } + } + else + { + info!(target: "Cancel", "Can't unify."); + } + } + pub fn unify(&self, other: &Predicate) -> Option> { match self @@ -78,32 +177,32 @@ impl Predicate Predicate::Fixed(other_name, other_predicates) if other_name == name && predicates.len() == other_predicates.len() => { - if predicates.len() == 0 + if predicates.is_empty() { 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) + let mut new_constraints = vec![]; + for (a, b) in predicates.iter().zip(other_predicates) + { + if let Some(constraints) = a.unify(b) { - (Some(c1), Some(c2)) => + for c in constraints.iter() { - let mut c = c1.clone(); - c.extend_from_slice(c2.as_slice()); - Some(c) + if c.merge_into(&mut new_constraints).is_none() + { + warn!(target: "Contradiction", "The property is contradictory."); + return None; + } } - _ => None, - }) - .flatten() + } + else + { + return None; + } + } + Some(new_constraints) } } Predicate::Fixed(_, _) => None, @@ -126,6 +225,55 @@ impl Predicate } } } + + fn unique_with(&self, counter: Rc>, map: &mut HashMap) -> Self + { + match self + { + Predicate::Variable(var) => + { + let num; + if let Some(n) = map.get(var) + { + num = *n; + } + else + { + let counter_val = counter.get(); + counter.set(counter_val + 1); + map.insert(var.clone(), counter_val); + num = counter_val; + } + Predicate::Variable(format!("_{}{}", num, var)) + } + Predicate::Fixed(name, predicates) => Predicate::Fixed( + name.clone(), + predicates + .iter() + .map(|x| x.unique_with(counter.clone(), map)) + .collect::>(), + ), + } + } +} + +impl Clause +{ + pub fn unique(&self, counter: Rc>) -> Self + { + self.unique_with(counter, &mut HashMap::new()) + } + + fn unique_with(&self, counter: Rc>, map: &mut HashMap) -> Self + { + Clause { + head: self.head.unique_with(counter.clone(), map), + body: self + .body + .clone() + .map(|x| x.unique_with(counter.clone(), map)), + } + } } impl Display for Constraint @@ -135,3 +283,26 @@ impl Display for Constraint write!(f, "{} = {}", self.variable, self.predicate) } } + +impl Constraint +{ + fn merge_into(&self, constraints: &mut Vec) -> Option<()> + { + // Check if constraint is contradictory with other constraints + for c in constraints.iter() + { + if self.variable == c.variable + { + let unification = self.predicate.unify(&c.predicate); + if unification.is_none() + { + info!(target: "Constraint", "Contradiction. Abort"); + return None; + } + } + } + + constraints.push(self.clone()); + Some(()) + } +}