From 134ebc6dc6a70c456554fc5a8680ea005814cd3e Mon Sep 17 00:00:00 2001 From: Albin Chaboissier Date: Sun, 8 Feb 2026 22:48:51 +0100 Subject: [PATCH] Working --- 1.pl | 9 + Cargo.lock | 363 ++++++++++++++++++++++++++++++++++++ Cargo.toml | 3 + src/ast.rs | 112 +++++++++++ src/lib.rs | 3 + src/main.rs | 35 +++- src/parsing.rs | 124 +++++++++++++ src/prover.rs | 382 ++++++++++++++++++++++++++++++++++++++ src/prover/constraints.rs | 183 ++++++++++++++++++ src/prover/trace.rs | 0 src/prover/unification.rs | 65 +++++++ 11 files changed, 1278 insertions(+), 1 deletion(-) create mode 100644 1.pl create mode 100644 src/ast.rs create mode 100644 src/lib.rs create mode 100644 src/parsing.rs create mode 100644 src/prover.rs create mode 100644 src/prover/constraints.rs create mode 100644 src/prover/trace.rs create mode 100644 src/prover/unification.rs diff --git a/1.pl b/1.pl new file mode 100644 index 0000000..4363d7e --- /dev/null +++ b/1.pl @@ -0,0 +1,9 @@ +entier(zero). +entier(s(X)) :- entier(X). + +add(X, zero, X). +add(X, s(Y), Z) :- add(s(X), Y, Z). + +mult(zero, X, zero). +mult(s(Y), X, Z) :- mult(Y, X, W), add(W, X, Z). + diff --git a/Cargo.lock b/Cargo.lock index e35d48c..3f473bf 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2,26 +2,389 @@ # 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" +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 = "colorchoice" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b05b61dc5112cbb17e4b6cd61790d9845d13888356391624cbe7e41efeac1e75" + +[[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 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]] +name = "libc" +version = "0.2.180" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bcc35a38544a891a5f7c865aca548a982ccb3b8650a5b06d0fd33a10283c56fc" + [[package]] name = "litemap" version = "0.8.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "6373607a59f0be73a39b6fe456b8192fcc3585f602af20751600e974dd455e77" +[[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" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "f8ca58f447f06ed17d5fc4043ce1b10dd205e060fb3ce5b979b8ed8e59ff3f79" +[[package]] +name = "once_cell_polyfill" +version = "1.70.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "384b8ab6d37215f3c5301a95a4accb5d64aa607f1fcb26a11b5303878451b4fe" + [[package]] name = "picolog" version = "0.1.0" dependencies = [ + "corosensei", + "env_logger", "litemap", + "log", "winnow", ] +[[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" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1e38bc4d79ed67fd075bcc251a1c39b32a1776bbe92e5bef1f0bf1f8c531853b" +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" +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" diff --git a/Cargo.toml b/Cargo.toml index ac15b5f..2570f5d 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -4,5 +4,8 @@ version = "0.1.0" edition = "2024" [dependencies] +corosensei = "0.3.2" +env_logger = "0.11.8" litemap = "0.8.1" +log = "0.4.29" winnow = "0.7.14" diff --git a/src/ast.rs b/src/ast.rs new file mode 100644 index 0000000..1d9173c --- /dev/null +++ b/src/ast.rs @@ -0,0 +1,112 @@ +use std::fmt::Display; + +pub type Variable = String; + +#[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(Variable), // 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, "(")?; + let len = predicates.len(); + for (i, predicate) in predicates.iter().enumerate() + { + write!(f, "{}", predicate)?; + if i != len - 1 + { + write!(f, ", ")?; + } + } + 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 index a4f2e4f..1837da3 100644 --- a/src/main.rs +++ b/src/main.rs @@ -1,4 +1,37 @@ +use picolog::ast::Body; +use picolog::ast::Module; +use picolog::ast::Predicate; + fn main() { - println!("Hello, world!"); + env_logger::builder() + .filter_level(log::LevelFilter::Debug) + .format_timestamp(None) + .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). + + mult(zero, X, zero). + mult(s(Y), X, Z) :- mult(Y, X, W), add(W, X, Z). + " + .into(); + + //let prop: Body = "integer(s(zero))".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:"); + println!("{}", c.simplified()); + let _ = std::io::stdin().read_line(&mut String::new()); + } + // let p: Predicate = "add(s(zero), zero, Y)".into(); + // let p1: Predicate = "add(X, zero, X)".into(); + // // let p: Predicate = "integer(s(zero))".into(); + // // let p1: Predicate = "integer(s(X))".into(); + // println!("{}", p.matches(&p1).unwrap()); } diff --git a/src/parsing.rs b/src/parsing.rs new file mode 100644 index 0000000..44d5dfc --- /dev/null +++ b/src/parsing.rs @@ -0,0 +1,124 @@ +use std::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 crate::ast::Body; +use crate::ast::Clause; +use crate::ast::Module; +use crate::ast::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, ",", multispace0)), + (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..4e14557 --- /dev/null +++ b/src/prover.rs @@ -0,0 +1,382 @@ +pub mod constraints; +pub mod trace; +pub mod unification; + +use std::cell::Cell; +use std::collections::VecDeque; +use std::rc::Rc; + +use litemap::LiteMap; +use log::info; + +use crate::ast::Body; +use crate::ast::Clause; +use crate::ast::Module; +use crate::ast::Predicate; +use crate::prover::constraints::Constraints; + +#[derive(Clone, Copy, Debug, Default)] +pub struct Counter(usize); + +#[derive(Clone, Debug, Default)] +pub struct GlobalCounter(Rc>); + +impl GlobalCounter +{ + pub fn new() -> GlobalCounter + { + GlobalCounter(Rc::new(Cell::new(0))) + } + + pub fn get(&self) -> usize + { + let val = self.0.get(); + self.0.set(val + 1); + val + } + + pub fn snapshot(&self) -> Counter + { + Counter(self.0.get()) + } + + pub fn restore(&mut self, snapshot: Counter) + { + self.0.set(snapshot.0); + } +} + +pub struct BodyProver<'a> +{ + module: &'a Module, + constraints: Constraints, + + prover: Box + 'a>, +} + +pub struct PredicateProver<'a> +{ + module: &'a Module, + predicate: Predicate, + constraints: Constraints, + counter_snapshot: Counter, + + global_counter: GlobalCounter, + current_clause: usize, + sub_proof: Option>, +} + +pub struct AndProver<'a> +{ + module: &'a Module, + bodies: Vec, + constraints: Constraints, + + global_counter: GlobalCounter, + sub_proofs: VecDeque<(Counter, BodyProver<'a>)>, +} + +impl BodyProver<'_> +{ + pub fn new<'a>( + module: &'a Module, + global_counter: GlobalCounter, + body: Body, + constraints: Constraints, + ) -> BodyProver<'a> + { + let prover: Box> = match &body + { + Body::Term(predicate) => Box::new(PredicateProver::new( + module, + global_counter, + predicate.clone(), + constraints.clone(), + )), + Body::And(items) => Box::new(AndProver::new( + module, + global_counter, + items.clone(), + constraints.clone(), + )), + Body::Or(items) => Box::new(BodyProver::new( + module, + global_counter, + items[0].clone(), + constraints.clone(), + )), + }; + info!(target: "BodyProver", "Proving {}", body); + BodyProver { + module, + constraints, + prover, + } + } +} + +impl PredicateProver<'_> +{ + pub fn new<'a>( + module: &'a Module, + global_counter: GlobalCounter, + predicate: Predicate, + constraints: Constraints, + ) -> PredicateProver<'a> + { + info!(target: "PredicateProver", "Proving {}", predicate); + PredicateProver { + module, + predicate, + constraints, + current_clause: 0, + sub_proof: None, + counter_snapshot: global_counter.snapshot(), + global_counter, + } + } +} + +impl AndProver<'_> +{ + pub fn new<'a>( + module: &'a Module, + global_counter: GlobalCounter, + bodies: Vec, + constraints: Constraints, + ) -> AndProver<'a> + { + assert!(!bodies.is_empty()); + + AndProver { + module, + sub_proofs: VecDeque::from(vec![( + global_counter.snapshot(), + BodyProver::new( + module, + global_counter.clone(), + bodies[0].clone(), + constraints.clone(), + ), + )]), + bodies, + constraints, + global_counter, + } + } +} + +impl Iterator for PredicateProver<'_> +{ + type Item = Constraints; + + fn next(&mut self) -> Option + { + match self.sub_proof.as_mut() + { + None => + { + if self.current_clause == self.module.clauses.len() + { + None + } + else + { + let clause = &self.module.clauses[self.current_clause] + .make_unique(self.global_counter.clone()); + info!(target: "PredicateProver", "Unifying '{}' against '{}'", self.predicate, clause); + let uni = self.predicate.matches(&clause.head); + let full_constraints = uni.and_then(|x| x.and(&self.constraints)); + + if let Some(c) = &full_constraints + { + info!(target: "PredicateProver", " => {}", c); + } + else + { + info!(target: "PredicateProver", " => (Can't unify)"); + } + match full_constraints + { + Some(constraints) if clause.body.is_none() => + { + self.current_clause += 1; + Some(constraints) + } + Some(constraints) => + { + self.current_clause += 1; + self.counter_snapshot = self.global_counter.snapshot(); + self.sub_proof = Some(BodyProver::new( + self.module, + self.global_counter.clone(), + clause.body.clone().unwrap(), + constraints, + )); + self.next() + } + None => + { + self.current_clause += 1; + self.next() + } + } + } + } + Some(prover) => + { + let next = prover.next(); + match next + { + Some(constraints) => Some(constraints), + None => + { + self.global_counter.restore(self.counter_snapshot); + self.sub_proof = None; + self.next() + } + } + } + } + } +} + +impl Iterator for BodyProver<'_> +{ + type Item = Constraints; + fn next(&mut self) -> Option + { + self.prover.next() + } +} + +impl Iterator for AndProver<'_> +{ + type Item = Constraints; + + fn next(&mut self) -> Option + { + if self.sub_proofs.is_empty() + { + return None; + } + + let (current_proof_snap, mut current_proof) = self.sub_proofs.pop_back().unwrap(); + + match current_proof.next() + { + Some(constraints) => + { + if self.sub_proofs.len() == self.bodies.len() - 1 + { + self.sub_proofs + .push_back((current_proof_snap, current_proof)); + Some(constraints) + } + else + { + self.sub_proofs + .push_back((current_proof_snap, current_proof)); + self.sub_proofs.push_back(( + self.global_counter.snapshot(), + BodyProver::new( + self.module, + self.global_counter.clone(), + self.bodies[self.sub_proofs.len()].clone(), + constraints, + ), + )); + self.next() + } + } + None => + { + self.global_counter.restore(current_proof_snap); + self.next() + } + } + } +} + +impl Module +{ + pub fn prove<'a>(&'a self, body: &'a Body) -> BodyProver<'a> + { + BodyProver::new( + self, + GlobalCounter::new(), + body.clone(), + Constraints::none(), + ) + } +} + +impl Clause +{ + pub fn make_unique(&self, counter: GlobalCounter) -> Clause + { + let mut unique_map = LiteMap::new(); + Clause { + head: self.head.make_unique(counter.clone(), &mut unique_map), + body: self + .body + .as_ref() + .map(|body| body.make_unique(counter.clone(), &mut unique_map)), + } + } +} + +impl Body +{ + pub fn make_unique( + &self, + counter: GlobalCounter, + unique_map: &mut LiteMap, + ) -> Body + { + match self + { + Body::Term(predicate) => Body::Term(predicate.make_unique(counter.clone(), unique_map)), + Body::And(items) => Body::And( + items + .iter() + .map(|x| x.make_unique(counter.clone(), unique_map)) + .collect(), + ), + Body::Or(items) => Body::Or( + items + .iter() + .map(|x| x.make_unique(counter.clone(), unique_map)) + .collect(), + ), + } + } +} + +impl Predicate +{ + pub fn make_unique( + &self, + counter: GlobalCounter, + unique_map: &mut LiteMap, + ) -> Self + { + match self + { + Predicate::Variable(name) => Predicate::Variable(format!( + "_{}[{}]", + name, + unique_map + .entry(name.clone()) + .or_insert_with(|| counter.get()) + )), + Predicate::Fixed(name, predicates) => Predicate::Fixed( + name.clone(), + predicates + .iter() + .map(|x| x.make_unique(counter.clone(), unique_map)) + .collect(), + ), + } + } +} diff --git a/src/prover/constraints.rs b/src/prover/constraints.rs new file mode 100644 index 0000000..ae8f85a --- /dev/null +++ b/src/prover/constraints.rs @@ -0,0 +1,183 @@ +use std::fmt::Display; + +use litemap::LiteMap; +use winnow::Str; + +use crate::ast::Predicate; +use crate::ast::Variable; +use crate::prover::constraints; + +#[derive(Clone, Debug)] +pub struct Constraints +{ + set: LiteMap, +} + +impl Constraints +{ + pub fn none() -> Self + { + Constraints { + set: LiteMap::new(), + } + } + + pub fn with(variable: Variable, predicate: Predicate) -> Self + { + let mut c = Constraints::none(); + c.set.insert(variable, predicate); + c + } + + pub fn try_append(&mut self, variable: &Variable, predicate: &Predicate) -> bool + { + if let Some(other_predicate) = self.set.get(variable) + { + // If variable is already contrained, we need to check if both contraints are + // contradictory + + // Try to unify both predicates + let unification = predicate.matches(other_predicate); + if let Some(unification_contraints) = unification + { + // Instead of adding the variable = predicates contraint, + // We can try adding the unification contraints which is implicitely the same + if self.try_merge(&unification_contraints) + { + self.set.insert(variable.clone(), predicate.clone()); + true + } + else + { + false + } + } + else + { + // Unification is impossible, variable = predicates is contradictory under self + false + } + } + else + { + // No constraint + self.set.insert(variable.clone(), predicate.clone()); + true + } + } + + pub fn try_merge(&mut self, constraints: &Constraints) -> bool + { + // Trying to merge, is just trying to add all of the constraints into self + let mut ok = self.clone(); + for (var, pred) in constraints.set.iter() + { + if !ok.try_append(var, pred) + { + return false; + } + } + *self = ok; + true + } + + pub fn and(&self, constraints: &Constraints) -> Option + { + let mut new_contraints = self.clone(); + let valid = new_contraints.try_merge(constraints); + if valid { Some(new_contraints) } else { None } + } + + pub fn simplified(&self) -> Constraints + { + let mut max_sub = Constraints::none(); + for (var, pred) in self.set.iter() + { + max_sub.set.insert(var.clone(), pred.substitute(self)); + } + + let mut stripped = max_sub.clone(); + 'outer: for (var, _) in max_sub.set.iter() + { + if var.chars().next().is_some_and(|x| x == '_') + { + for (_, other_pred) in max_sub.set.iter() + { + if other_pred.contains_variable(var) + { + continue 'outer; + } + } + stripped.set.remove(var); + } + } + + stripped + } +} + +impl Predicate +{ + pub fn substitute(&self, constraints: &Constraints) -> Predicate + { + match self + { + Predicate::Variable(name) => + { + if let Some(pred) = constraints.set.get(name) + { + let max_sub = pred.substitute(constraints); + max_sub + } + else + { + Predicate::Variable(name.clone()) + } + } + Predicate::Fixed(name, predicates) => Predicate::Fixed( + name.clone(), + predicates + .iter() + .map(|x| x.substitute(constraints)) + .collect(), + ), + } + } + + pub fn contains_variable(&self, name: &String) -> bool + { + match self + { + Predicate::Variable(var_name) => name == var_name, + Predicate::Fixed(_, predicates) => predicates + .iter() + .find(|x| x.contains_variable(name)) + .is_some(), + } + } +} + +impl Default for Constraints +{ + fn default() -> Self + { + Self::none() + } +} + +impl Display for Constraints +{ + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result + { + let len = self.set.len(); + for (i, (var, pred)) in self.set.iter().enumerate() + { + write!(f, "{} = {}", var, pred)?; + if i != len - 1 + { + write!(f, ", ")?; + } + } + Ok(()) + } +} diff --git a/src/prover/trace.rs b/src/prover/trace.rs new file mode 100644 index 0000000..e69de29 diff --git a/src/prover/unification.rs b/src/prover/unification.rs new file mode 100644 index 0000000..84d1769 --- /dev/null +++ b/src/prover/unification.rs @@ -0,0 +1,65 @@ +use std::process::Output; + +use log::debug; + +use crate::ast::Predicate; +use crate::prover::constraints::Constraints; + +impl Predicate +{ + /// Checks if `self` can be unified with `other` + /// + /// returns `Some(constraints)` if the unification is valid under `constraints` + /// returns `None` if the predicate cannot be unified against the other + pub fn matches(&self, other: &Predicate) -> Option + { + debug!("Unifying {} against {}", self, other); + match self + { + Predicate::Variable(variable) => + { + // We are trying to see if X (any) matches the other Predicate. + // This is always true if X = other_predicate + Some(Constraints::with(variable.clone(), other.clone())) + } + + Predicate::Fixed(name, arguments) => + { + match other + { + Predicate::Variable(var) => + { + // We are trying to see if something like "predicate(..., ...)" matches X + // (any) + // This is always true + Some(Constraints::with(var.clone(), self.clone())) + } + // Match pred(X, Y, Z, ...) with pred(_X, _Y, _Z, ...) + Predicate::Fixed(other_name, other_arguments) + if other_name == name && other_arguments.len() == arguments.len() => + { + // If there is no arguments, no constraints + if arguments.is_empty() + { + return Some(Constraints::none()); + } + + // We unify with other only if our arguments unify with theirs + arguments + .iter() + .zip(other_arguments.iter()) + .map(|(ours, theirs)| ours.matches(theirs)) + .reduce(|a, b| match (a, b) + { + (Some(c1), Some(c2)) => c1.and(&c2), + _ => None, + }) + .unwrap_or(None) + } + + _ => None, + } + } + } + } +}