Compare commits
18 Commits
134ebc6dc6
...
domains-te
| Author | SHA1 | Date | |
|---|---|---|---|
| 5458b3a822 | |||
| 27af8c9263 | |||
| c82384764c | |||
| 54724c2f4c | |||
| d8180a982e | |||
| 1c17aa20c2 | |||
| 21414f75db | |||
| 298d179943 | |||
| 70afc2a201 | |||
| 3fd8414ba2 | |||
| c920ef8d99 | |||
| 5b9df71704 | |||
| 1ab7d7bf95 | |||
| a151b772aa | |||
| 0f721e34c4 | |||
| bce33de71e | |||
| b80077f3a7 | |||
| 694a84fb00 |
4
.gitmodules
vendored
Normal file
4
.gitmodules
vendored
Normal file
@ -0,0 +1,4 @@
|
||||
[submodule "winnow"]
|
||||
path = winnow
|
||||
url = git@github.com:supersurviveur/winnow.git
|
||||
branch = operator-in-expression
|
||||
13
1.pl
13
1.pl
@ -1,9 +1,22 @@
|
||||
:- use_module(library(clpfd)).
|
||||
|
||||
entier(zero).
|
||||
entier(s(X)) :- entier(X).
|
||||
|
||||
add(X, zero, X).
|
||||
add(X, s(Y), Z) :- add(s(X), Y, Z).
|
||||
|
||||
inf(zero, X) :- entier(X).
|
||||
inf(s(X), s(Y)) :- inf(X, Y).
|
||||
|
||||
mult(zero, X, zero).
|
||||
mult(s(Y), X, Z) :- mult(Y, X, W), add(W, X, Z).
|
||||
|
||||
div(A, B) :- inf(A, B), inf(X, B), mult(X, A, B).
|
||||
div_w(X, Y) :- inf(s(X), Y), inf(s(s(zero)), X), div(X, Y).
|
||||
prime(X) :- entier(X), \+ div_w(_, X).
|
||||
|
||||
peano(X, zero) :- X #= 0.
|
||||
peano(X, s(P)) :- X #> 0, X #= Y + 1, peano(Y, P).
|
||||
|
||||
|
||||
|
||||
171
Cargo.lock
generated
171
Cargo.lock
generated
@ -11,6 +11,12 @@ dependencies = [
|
||||
"memchr",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "allocator-api2"
|
||||
version = "0.2.21"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "683d7910e743518b0e34f1186f92494becacb047c7b6bf616c96772180fef923"
|
||||
|
||||
[[package]]
|
||||
name = "anstream"
|
||||
version = "0.6.21"
|
||||
@ -47,7 +53,7 @@ version = "1.1.5"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "40c48f72fd53cd289104fc64099abca73db4166ad86ea0b4341abe65af83dadc"
|
||||
dependencies = [
|
||||
"windows-sys 0.61.2",
|
||||
"windows-sys",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
@ -58,20 +64,14 @@ checksum = "291e6a250ff86cd4a820112fb8898808a366d8f9f58ce16d1f538353ad55747d"
|
||||
dependencies = [
|
||||
"anstyle",
|
||||
"once_cell_polyfill",
|
||||
"windows-sys 0.61.2",
|
||||
"windows-sys",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "autocfg"
|
||||
version = "1.5.0"
|
||||
name = "bimap"
|
||||
version = "0.6.3"
|
||||
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"
|
||||
checksum = "230c5f1ca6a325a32553f8640d31ac9b49f2411e901e427570154868b46da4f7"
|
||||
|
||||
[[package]]
|
||||
name = "colorchoice"
|
||||
@ -79,19 +79,6 @@ 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"
|
||||
@ -115,6 +102,29 @@ dependencies = [
|
||||
"log",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "equivalent"
|
||||
version = "1.0.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "877a4ace8713b0bcf2a4e7eec82529c029f1d0619886d18145fea96c3ffe5c0f"
|
||||
|
||||
[[package]]
|
||||
name = "foldhash"
|
||||
version = "0.2.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "77ce24cb58228fbb8aa041425bb1050850ac19177686ea6e0f41a70416f56fdb"
|
||||
|
||||
[[package]]
|
||||
name = "hashbrown"
|
||||
version = "0.16.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "841d1cc9bed7f9236f321df977030373f4a4163ae1a7dbfe1a51a2c1a51d9100"
|
||||
dependencies = [
|
||||
"allocator-api2",
|
||||
"equivalent",
|
||||
"foldhash",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "is_terminal_polyfill"
|
||||
version = "1.70.2"
|
||||
@ -145,24 +155,21 @@ dependencies = [
|
||||
"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 = "lru"
|
||||
version = "0.16.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "a1dc47f592c06f33f8e3aea9591776ec7c9f9e4124778ff8a3c3b87159f7e593"
|
||||
dependencies = [
|
||||
"hashbrown",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "memchr"
|
||||
version = "2.8.0"
|
||||
@ -175,14 +182,21 @@ version = "1.70.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "384b8ab6d37215f3c5301a95a4accb5d64aa607f1fcb26a11b5303878451b4fe"
|
||||
|
||||
[[package]]
|
||||
name = "owo-colors"
|
||||
version = "4.2.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "9c6901729fa79e91a0913333229e9ca5dc725089d1c363b2f4b4760709dc4a52"
|
||||
|
||||
[[package]]
|
||||
name = "picolog"
|
||||
version = "0.1.0"
|
||||
dependencies = [
|
||||
"corosensei",
|
||||
"bimap",
|
||||
"env_logger",
|
||||
"litemap",
|
||||
"log",
|
||||
"lru",
|
||||
"owo-colors",
|
||||
"winnow",
|
||||
]
|
||||
|
||||
@ -248,12 +262,6 @@ 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"
|
||||
@ -303,15 +311,6 @@ 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"
|
||||
@ -321,75 +320,9 @@ 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"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "5a5364e9d77fcdeeaa6062ced926ee3381faa2ee02d3eb83a5c27a8825540829"
|
||||
dependencies = [
|
||||
"memchr",
|
||||
]
|
||||
|
||||
@ -4,8 +4,9 @@ version = "0.1.0"
|
||||
edition = "2024"
|
||||
|
||||
[dependencies]
|
||||
corosensei = "0.3.2"
|
||||
bimap = "0.6.3"
|
||||
env_logger = "0.11.8"
|
||||
litemap = "0.8.1"
|
||||
log = "0.4.29"
|
||||
winnow = "0.7.14"
|
||||
winnow = { version = "0.7.14", path = "./winnow" }
|
||||
lru = "0.16.3"
|
||||
owo-colors = "4.2.3"
|
||||
|
||||
5
rustfmt.toml
Normal file
5
rustfmt.toml
Normal file
@ -0,0 +1,5 @@
|
||||
brace_style="AlwaysNextLine"
|
||||
control_brace_style="AlwaysNextLine"
|
||||
combine_control_expr=false
|
||||
|
||||
|
||||
84
src/ast.rs
84
src/ast.rs
@ -1,6 +1,11 @@
|
||||
use owo_colors::{OwoColorize, colors::css::Gray};
|
||||
|
||||
use std::fmt::Display;
|
||||
|
||||
pub type Variable = String;
|
||||
use crate::domain::Domain;
|
||||
|
||||
#[derive(Clone, PartialEq, Eq, Debug, Hash)]
|
||||
pub struct Variable(pub String, pub Option<usize>);
|
||||
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct Module
|
||||
@ -15,7 +20,7 @@ pub struct Clause
|
||||
pub body: Option<Body>,
|
||||
}
|
||||
|
||||
#[derive(Clone, Debug)]
|
||||
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
|
||||
pub enum Body
|
||||
{
|
||||
Term(Predicate),
|
||||
@ -23,11 +28,48 @@ pub enum Body
|
||||
Or(Vec<Body>),
|
||||
}
|
||||
|
||||
#[derive(Clone, Debug)]
|
||||
#[derive(Clone, Debug, Eq, PartialEq, Hash)]
|
||||
pub enum Predicate
|
||||
{
|
||||
Variable(Variable), // Upercase variable like X
|
||||
Fixed(String, Vec<Predicate>),
|
||||
Fixed(Functor, Vec<Predicate>),
|
||||
Domain(Domain),
|
||||
}
|
||||
|
||||
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
|
||||
pub enum Functor
|
||||
{
|
||||
Operator(Operator),
|
||||
Functor(String),
|
||||
}
|
||||
|
||||
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
|
||||
pub struct Operator
|
||||
{
|
||||
pub op: String,
|
||||
pub precedence: usize,
|
||||
pub op_type: OperatorType,
|
||||
}
|
||||
|
||||
impl Operator
|
||||
{
|
||||
pub fn new(op: String, precedence: usize, op_type: OperatorType) -> Self
|
||||
{
|
||||
Self {
|
||||
op,
|
||||
precedence,
|
||||
op_type,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
|
||||
pub enum OperatorType
|
||||
{
|
||||
Prefix,
|
||||
Postfix,
|
||||
LeftInfix,
|
||||
RightInfix,
|
||||
}
|
||||
|
||||
impl Display for Body
|
||||
@ -54,6 +96,19 @@ impl Display for Body
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for Variable
|
||||
{
|
||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result
|
||||
{
|
||||
write!(f, "{}", self.0)?;
|
||||
if let Some(num) = self.1
|
||||
{
|
||||
write!(f, "{}", format!("[{}]", num).fg::<Gray>())?;
|
||||
}
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for Predicate
|
||||
{
|
||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result
|
||||
@ -83,6 +138,7 @@ impl Display for Predicate
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
Predicate::Domain(domain) => write!(f, "{domain}"),
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -110,3 +166,23 @@ 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
|
||||
{
|
||||
write!(f, "{}", self.op)
|
||||
}
|
||||
}
|
||||
|
||||
512
src/domain.rs
Normal file
512
src/domain.rs
Normal file
@ -0,0 +1,512 @@
|
||||
use std::{cmp, fmt::Display};
|
||||
|
||||
use crate::domain;
|
||||
|
||||
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
|
||||
pub struct Domain
|
||||
{
|
||||
pub union: Vec<DomainRange>,
|
||||
}
|
||||
|
||||
#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
|
||||
pub struct DomainRange
|
||||
{
|
||||
pub start: DomainBound,
|
||||
pub end: DomainBound,
|
||||
}
|
||||
|
||||
#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
|
||||
pub enum DomainBound
|
||||
{
|
||||
Unbounded,
|
||||
Bounded(i64),
|
||||
}
|
||||
|
||||
impl Domain
|
||||
{
|
||||
pub fn all() -> Domain
|
||||
{
|
||||
Domain {
|
||||
union: vec![DomainRange {
|
||||
start: DomainBound::Unbounded,
|
||||
end: DomainBound::Unbounded,
|
||||
}],
|
||||
}
|
||||
}
|
||||
|
||||
pub fn included_in(&self, domain: &Domain) -> bool
|
||||
{
|
||||
self.union(domain) == *domain
|
||||
}
|
||||
|
||||
pub fn empty(&self) -> bool
|
||||
{
|
||||
self.union.len() == 0
|
||||
}
|
||||
|
||||
pub fn disjoint(&self, domain: &Domain) -> bool
|
||||
{
|
||||
self.intersection(domain).union.len() == 0
|
||||
}
|
||||
|
||||
pub fn intersection(&self, domain: &Domain) -> Domain
|
||||
{
|
||||
let mut i = 0;
|
||||
let mut j = 0;
|
||||
let mut stack = vec![];
|
||||
|
||||
while i < self.union.len() || j < domain.union.len()
|
||||
{
|
||||
if i < self.union.len() && j < domain.union.len()
|
||||
{
|
||||
let a = self.union[i];
|
||||
let b = domain.union[j];
|
||||
|
||||
if a.disjoint(&b)
|
||||
{
|
||||
if a < b
|
||||
{
|
||||
i += 1;
|
||||
}
|
||||
else
|
||||
{
|
||||
j += 1;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
let inter = a.intersection(&b);
|
||||
if let Some(range) = inter
|
||||
{
|
||||
stack.push(range);
|
||||
};
|
||||
if a.ends_furthest(&b)
|
||||
{
|
||||
i += 1;
|
||||
}
|
||||
else
|
||||
{
|
||||
j += 1;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
Domain { union: stack }
|
||||
}
|
||||
|
||||
pub fn union(&self, domain: &Domain) -> Domain
|
||||
{
|
||||
let mut i = 0;
|
||||
let mut j = 0;
|
||||
let mut stack = vec![];
|
||||
|
||||
while i < self.union.len() || j < domain.union.len()
|
||||
{
|
||||
if i < self.union.len() && j < domain.union.len()
|
||||
{
|
||||
let a = self.union[i];
|
||||
let b = domain.union[j];
|
||||
|
||||
let (min, max) = (a.min(b), a.max(b));
|
||||
|
||||
if let DomainBound::Bounded(end) = min.end
|
||||
&& let DomainBound::Bounded(start) = max.start
|
||||
&& end == start
|
||||
{
|
||||
let union = a.union(&b);
|
||||
stack.extend_from_slice(union.union.as_slice());
|
||||
i += 1;
|
||||
j += 1;
|
||||
}
|
||||
else if a.disjoint(&b)
|
||||
{
|
||||
if a < b
|
||||
{
|
||||
stack.push(a);
|
||||
i += 1;
|
||||
}
|
||||
else
|
||||
{
|
||||
stack.push(b);
|
||||
j += 1;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
let union = a.union(&b);
|
||||
stack.extend_from_slice(union.union.as_slice());
|
||||
i += 1;
|
||||
j += 1;
|
||||
}
|
||||
}
|
||||
else if i < self.union.len()
|
||||
{
|
||||
stack.extend_from_slice(&self.union[i..]);
|
||||
i = self.union.len();
|
||||
}
|
||||
else
|
||||
{
|
||||
stack.extend_from_slice(&domain.union[j..]);
|
||||
j = self.union.len();
|
||||
}
|
||||
}
|
||||
|
||||
Domain { union: stack }
|
||||
}
|
||||
}
|
||||
|
||||
impl From<DomainRange> for Domain
|
||||
{
|
||||
fn from(value: DomainRange) -> Self
|
||||
{
|
||||
Domain { union: vec![value] }
|
||||
}
|
||||
}
|
||||
|
||||
impl DomainBound
|
||||
{
|
||||
pub fn min_start(&self, bound: DomainBound) -> DomainBound
|
||||
{
|
||||
match (self, bound)
|
||||
{
|
||||
(DomainBound::Unbounded, DomainBound::Unbounded) => DomainBound::Unbounded,
|
||||
(DomainBound::Bounded(_), DomainBound::Unbounded)
|
||||
| (DomainBound::Unbounded, DomainBound::Bounded(_)) => DomainBound::Unbounded,
|
||||
(DomainBound::Bounded(a), DomainBound::Bounded(b)) => DomainBound::Bounded(*a.min(&b)),
|
||||
}
|
||||
}
|
||||
|
||||
pub fn max_end(&self, bound: DomainBound) -> DomainBound
|
||||
{
|
||||
match (self, bound)
|
||||
{
|
||||
(DomainBound::Unbounded, DomainBound::Unbounded) => DomainBound::Unbounded,
|
||||
(DomainBound::Bounded(_), DomainBound::Unbounded)
|
||||
| (DomainBound::Unbounded, DomainBound::Bounded(_)) => DomainBound::Unbounded,
|
||||
(DomainBound::Bounded(a), DomainBound::Bounded(b)) => DomainBound::Bounded(*a.max(&b)),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl PartialOrd for DomainRange
|
||||
{
|
||||
fn partial_cmp(&self, other: &Self) -> Option<cmp::Ordering>
|
||||
{
|
||||
Some(self.cmp(other))
|
||||
}
|
||||
}
|
||||
|
||||
impl Ord for DomainRange
|
||||
{
|
||||
fn cmp(&self, other: &Self) -> std::cmp::Ordering
|
||||
{
|
||||
match (self.start, other.start)
|
||||
{
|
||||
(DomainBound::Unbounded, DomainBound::Unbounded) => cmp::Ordering::Equal,
|
||||
(DomainBound::Unbounded, DomainBound::Bounded(_)) => cmp::Ordering::Less,
|
||||
(DomainBound::Bounded(_), DomainBound::Unbounded) => cmp::Ordering::Greater,
|
||||
(DomainBound::Bounded(a), DomainBound::Bounded(b)) => a.cmp(&b),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl DomainRange
|
||||
{
|
||||
pub fn intersection(&self, range: &DomainRange) -> Option<DomainRange>
|
||||
{
|
||||
let (min, max) = (self.min(range), self.max(range));
|
||||
match (min.end, max.start)
|
||||
{
|
||||
(DomainBound::Unbounded, DomainBound::Unbounded) => Some(DomainRange {
|
||||
start: DomainBound::Unbounded,
|
||||
end: DomainBound::Unbounded,
|
||||
}),
|
||||
(DomainBound::Unbounded, DomainBound::Bounded(a)) => Some(DomainRange {
|
||||
start: DomainBound::Bounded(a),
|
||||
end: max.end,
|
||||
}),
|
||||
(DomainBound::Bounded(a), DomainBound::Unbounded) => Some(DomainRange {
|
||||
start: max.start,
|
||||
end: DomainBound::Bounded(a),
|
||||
}),
|
||||
(DomainBound::Bounded(a), DomainBound::Bounded(b)) if b < a => Some(DomainRange {
|
||||
start: DomainBound::Bounded(b),
|
||||
end: DomainBound::Bounded(a),
|
||||
}),
|
||||
_ => None,
|
||||
}
|
||||
}
|
||||
|
||||
pub fn union(&self, range: &DomainRange) -> Domain
|
||||
{
|
||||
if self.disjoint(range)
|
||||
{
|
||||
let (a, b) = (self.min(range), self.max(range));
|
||||
if let DomainBound::Bounded(end) = a.end
|
||||
&& let DomainBound::Bounded(start) = b.start
|
||||
&& end == start
|
||||
{
|
||||
Domain {
|
||||
union: vec![DomainRange {
|
||||
start: a.start,
|
||||
end: b.end,
|
||||
}],
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
Domain {
|
||||
union: vec![*self.min(range), *self.max(range)],
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
let (a, b) = (self.min(range), self.max(range));
|
||||
let range = DomainRange {
|
||||
start: match (a.start, b.start)
|
||||
{
|
||||
(DomainBound::Bounded(a), DomainBound::Bounded(b)) =>
|
||||
{
|
||||
DomainBound::Bounded(a.min(b))
|
||||
}
|
||||
(DomainBound::Unbounded, DomainBound::Bounded(_))
|
||||
| (DomainBound::Bounded(_), DomainBound::Unbounded)
|
||||
| (DomainBound::Unbounded, DomainBound::Unbounded) => DomainBound::Unbounded,
|
||||
},
|
||||
end: match (a.end, b.end)
|
||||
{
|
||||
(DomainBound::Bounded(a), DomainBound::Bounded(b)) =>
|
||||
{
|
||||
DomainBound::Bounded(a.max(b))
|
||||
}
|
||||
(DomainBound::Unbounded, DomainBound::Bounded(_))
|
||||
| (DomainBound::Bounded(_), DomainBound::Unbounded)
|
||||
| (DomainBound::Unbounded, DomainBound::Unbounded) => DomainBound::Unbounded,
|
||||
},
|
||||
};
|
||||
|
||||
Domain { union: vec![range] }
|
||||
}
|
||||
}
|
||||
|
||||
pub fn ends_furthest(&self, end: &DomainRange) -> bool
|
||||
{
|
||||
match (self.end, end.end)
|
||||
{
|
||||
(DomainBound::Unbounded, DomainBound::Unbounded) => true,
|
||||
(DomainBound::Unbounded, DomainBound::Bounded(_)) => true,
|
||||
(DomainBound::Bounded(_), DomainBound::Unbounded) => false,
|
||||
(DomainBound::Bounded(a), DomainBound::Bounded(b)) => a >= b,
|
||||
}
|
||||
}
|
||||
|
||||
pub fn disjoint(&self, range: &DomainRange) -> bool
|
||||
{
|
||||
let (a, b) = (self.min(range), self.max(range));
|
||||
matches!((a.end, b.start), (DomainBound::Bounded(a), DomainBound::Bounded(b)) if a <= b)
|
||||
}
|
||||
|
||||
pub fn singleton(value: i64) -> DomainRange
|
||||
{
|
||||
DomainRange {
|
||||
start: DomainBound::Bounded(value),
|
||||
end: DomainBound::Bounded(value + 1),
|
||||
}
|
||||
}
|
||||
|
||||
pub fn from(value: i64) -> DomainRange
|
||||
{
|
||||
DomainRange {
|
||||
start: DomainBound::Bounded(value),
|
||||
end: DomainBound::Unbounded,
|
||||
}
|
||||
}
|
||||
|
||||
pub fn to(value: i64) -> DomainRange
|
||||
{
|
||||
DomainRange {
|
||||
start: DomainBound::Unbounded,
|
||||
end: DomainBound::Bounded(value),
|
||||
}
|
||||
}
|
||||
|
||||
pub fn closed(start: i64, end: i64) -> DomainRange
|
||||
{
|
||||
DomainRange {
|
||||
start: DomainBound::Bounded(start),
|
||||
end: DomainBound::Bounded(end),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for Domain
|
||||
{
|
||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result
|
||||
{
|
||||
let len = self.union.len();
|
||||
for (i, range) in self.union.iter().enumerate()
|
||||
{
|
||||
write!(f, "{}", range)?;
|
||||
if i != len - 1
|
||||
{
|
||||
write!(f, " ∪ ")?;
|
||||
}
|
||||
}
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for DomainRange
|
||||
{
|
||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result
|
||||
{
|
||||
match (self.start, self.end)
|
||||
{
|
||||
(DomainBound::Bounded(a), DomainBound::Bounded(b)) if b == a + 1 => write!(f, "{}", a),
|
||||
(a, b) => write!(f, "{}..{}", a, b),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for DomainBound
|
||||
{
|
||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result
|
||||
{
|
||||
match self
|
||||
{
|
||||
DomainBound::Unbounded => Ok(()),
|
||||
DomainBound::Bounded(n) => write!(f, "{}", n),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
mod test
|
||||
{
|
||||
#[allow(unused_imports)]
|
||||
use crate::domain::{Domain, DomainBound, DomainRange};
|
||||
|
||||
#[test]
|
||||
pub fn domain_range_parse()
|
||||
{
|
||||
let a: DomainRange = "..".into();
|
||||
assert_eq!(
|
||||
a,
|
||||
DomainRange {
|
||||
start: DomainBound::Unbounded,
|
||||
end: DomainBound::Unbounded
|
||||
}
|
||||
);
|
||||
|
||||
let a: DomainRange = "42..".into();
|
||||
assert_eq!(
|
||||
a,
|
||||
DomainRange {
|
||||
start: DomainBound::Bounded(42),
|
||||
end: DomainBound::Unbounded
|
||||
}
|
||||
);
|
||||
|
||||
let a: DomainRange = "..42".into();
|
||||
assert_eq!(
|
||||
a,
|
||||
DomainRange {
|
||||
start: DomainBound::Unbounded,
|
||||
end: DomainBound::Bounded(42),
|
||||
}
|
||||
);
|
||||
|
||||
let a: DomainRange = "0..42".into();
|
||||
assert_eq!(
|
||||
a,
|
||||
DomainRange {
|
||||
start: DomainBound::Bounded(0),
|
||||
end: DomainBound::Bounded(42),
|
||||
}
|
||||
);
|
||||
}
|
||||
|
||||
#[test]
|
||||
pub fn domain_range_union()
|
||||
{
|
||||
let inf: DomainRange = "..".into();
|
||||
let inf_b: DomainRange = "..42".into();
|
||||
let a_inf: DomainRange = "0..".into();
|
||||
let a_b: DomainRange = "10..20".into();
|
||||
let a_b2: DomainRange = "30..50".into();
|
||||
let a_b3: DomainRange = "20..30".into();
|
||||
|
||||
assert_eq!(inf.union(&inf), "..".into());
|
||||
assert_eq!(inf.union(&inf_b), "..".into());
|
||||
assert_eq!(inf.union(&a_inf), "..".into());
|
||||
assert_eq!(inf.union(&a_b), "..".into());
|
||||
|
||||
assert_eq!(inf.union(&inf), "..".into());
|
||||
assert_eq!(inf_b.union(&inf), "..".into());
|
||||
assert_eq!(a_inf.union(&inf), "..".into());
|
||||
assert_eq!(a_b.union(&inf), "..".into());
|
||||
|
||||
assert_eq!(inf.union(&inf), "..".into());
|
||||
assert_eq!(inf_b.union(&inf_b), "..42".into());
|
||||
assert_eq!(a_inf.union(&a_inf), "0..".into());
|
||||
assert_eq!(a_b.union(&a_b), "10..20".into());
|
||||
|
||||
assert_eq!(
|
||||
a_b.union(&a_b2),
|
||||
Domain {
|
||||
union: vec!["10..20".into(), "30..50".into()]
|
||||
}
|
||||
);
|
||||
|
||||
assert_eq!(a_b.union(&a_b3), "10..30".into());
|
||||
}
|
||||
|
||||
#[test]
|
||||
pub fn domain_union()
|
||||
{
|
||||
let k: Domain = "2..5".into();
|
||||
let k2: Domain = "5..10".into();
|
||||
assert_eq!(
|
||||
k.union(&k2),
|
||||
Domain {
|
||||
union: vec![DomainRange {
|
||||
start: DomainBound::Bounded(2),
|
||||
end: DomainBound::Bounded(10)
|
||||
}]
|
||||
}
|
||||
);
|
||||
}
|
||||
|
||||
#[test]
|
||||
pub fn domain_intersection()
|
||||
{
|
||||
let k: Domain = "0..5".into();
|
||||
let k2: Domain = "10..15".into();
|
||||
|
||||
let k3: Domain = "3..7".into();
|
||||
let k4: Domain = "13..17".into();
|
||||
|
||||
let a = k.union(&k2);
|
||||
let b = k3.union(&k4);
|
||||
assert_eq!(
|
||||
a.intersection(&b),
|
||||
Domain {
|
||||
union: vec![
|
||||
DomainRange {
|
||||
start: DomainBound::Bounded(3),
|
||||
end: DomainBound::Bounded(5)
|
||||
},
|
||||
DomainRange {
|
||||
start: DomainBound::Bounded(13),
|
||||
end: DomainBound::Bounded(15)
|
||||
}
|
||||
]
|
||||
}
|
||||
);
|
||||
}
|
||||
}
|
||||
@ -1,3 +1,4 @@
|
||||
pub mod ast;
|
||||
pub mod domain;
|
||||
pub mod parsing;
|
||||
pub mod prover;
|
||||
|
||||
61
src/main.rs
61
src/main.rs
@ -1,6 +1,7 @@
|
||||
use picolog::ast::Body;
|
||||
use picolog::ast::Module;
|
||||
use picolog::ast::Predicate;
|
||||
use picolog::domain::Domain;
|
||||
|
||||
fn main()
|
||||
{
|
||||
@ -9,26 +10,64 @@ fn main()
|
||||
.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).
|
||||
//
|
||||
// op(10, yfx, +).
|
||||
// op(8, yfx, ^).
|
||||
// op(6, xfy, ::).
|
||||
// op(2, fx, [).
|
||||
// op(2, xf, ]).
|
||||
// op(3, yfx, |).
|
||||
//
|
||||
// A + B :- test.
|
||||
//
|
||||
// A ^ B + C :- test.
|
||||
// A::B::C :- A.
|
||||
// [Hd|Tl] :- Hd::Tl.
|
||||
//
|
||||
// l(X) :- in(X, 3..7).
|
||||
// "
|
||||
// .into();
|
||||
|
||||
let d1: Domain = "5..10".into();
|
||||
let d2: Domain = "7..18".into();
|
||||
|
||||
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).
|
||||
hello(5..10).
|
||||
world(7..18).
|
||||
"
|
||||
.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)
|
||||
//let pred: Predicate = "hello(0..10).".into();
|
||||
let show: Body = "hello(X), world(X)".into();
|
||||
|
||||
for c in module.prove(&show)
|
||||
{
|
||||
println!("true:");
|
||||
println!("{}", c.simplified());
|
||||
let _ = std::io::stdin().read_line(&mut String::new());
|
||||
}
|
||||
//println!("{}", module.prove(&pred).unwrap());
|
||||
// let prop: Body = "mult(X, s(s(s(zero))), s(s(s(s(s(s(s(s(s(zero))))))))))".into();
|
||||
//let prop: Body = "integer(s(X))".into();
|
||||
//let prop: Body = "mult(X, s(s(zero)), s(s(s(s(zero)))))".into();
|
||||
//let prop: Body = "mult(X, Y, Z)".into();
|
||||
//let prop: Body = "mult(s(s(zero)), s(s(zero)), X)".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();
|
||||
|
||||
335
src/parsing.rs
335
src/parsing.rs
@ -1,29 +1,234 @@
|
||||
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::{
|
||||
Parser, Result, Stateful,
|
||||
ascii::{self, alphanumeric1, dec_int, multispace0},
|
||||
combinator::{
|
||||
Infix, Postfix, Prefix, alt, delimited, expression, opt, preceded, repeat, separated, seq,
|
||||
terminated,
|
||||
},
|
||||
error::ContextError,
|
||||
token::literal,
|
||||
};
|
||||
|
||||
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::Variable;
|
||||
use crate::ast::{Body, OperatorType};
|
||||
use crate::domain::{Domain, DomainBound, DomainRange};
|
||||
|
||||
pub fn predicate_parse(input: &mut &str) -> Result<Predicate>
|
||||
impl Operator
|
||||
{
|
||||
let ident = alphanumeric0.parse_next(input)?;
|
||||
pub fn get_precedence(&self) -> usize
|
||||
{
|
||||
self.precedence
|
||||
}
|
||||
pub fn make_infix_operator<'a>(self) -> Infix<Stream<'a>, Predicate, Operator, ContextError>
|
||||
{
|
||||
fn make_predicate(
|
||||
_: &mut Stream,
|
||||
a: Predicate,
|
||||
op: Operator,
|
||||
b: Predicate,
|
||||
) -> Result<Predicate>
|
||||
{
|
||||
Ok(Predicate::Fixed(Functor::Operator(op), vec![a, b]))
|
||||
}
|
||||
let precedence = self.get_precedence() as i64;
|
||||
match self.op_type
|
||||
{
|
||||
OperatorType::LeftInfix => Infix::Left(precedence, self, make_predicate),
|
||||
OperatorType::RightInfix => Infix::Right(precedence, self, make_predicate),
|
||||
_ => unreachable!(),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Operator
|
||||
{
|
||||
fn infix(value: String, state: &State) -> Result<Self>
|
||||
{
|
||||
state
|
||||
.custom_operators
|
||||
.get(&(value.clone(), OperatorType::RightInfix))
|
||||
.or_else(|| {
|
||||
state
|
||||
.custom_operators
|
||||
.get(&(value, OperatorType::LeftInfix))
|
||||
})
|
||||
.ok_or(ContextError::new())
|
||||
.cloned()
|
||||
}
|
||||
fn prefix(value: String, state: &State) -> Result<Self>
|
||||
{
|
||||
state
|
||||
.custom_operators
|
||||
.get(&(value, OperatorType::Prefix))
|
||||
.ok_or(ContextError::new())
|
||||
.cloned()
|
||||
}
|
||||
fn postfix(value: String, state: &State) -> Result<Self>
|
||||
{
|
||||
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 domain_range_parse(input: &mut Stream) -> Result<DomainRange>
|
||||
{
|
||||
let start = opt(dec_int.map(DomainBound::Bounded))
|
||||
.map(|v| v.unwrap_or(DomainBound::Unbounded))
|
||||
.parse_next(input)?;
|
||||
literal("..").parse_next(input)?;
|
||||
let end = opt(dec_int.map(DomainBound::Bounded))
|
||||
.map(|v| v.unwrap_or(DomainBound::Unbounded))
|
||||
.parse_next(input)?;
|
||||
Ok(DomainRange { start, end })
|
||||
}
|
||||
|
||||
pub fn domain_parse(input: &mut Stream) -> Result<Domain>
|
||||
{
|
||||
// Domain is either a..b, ..
|
||||
alt((domain_range_parse, dec_int.map(DomainRange::singleton)))
|
||||
.map(|domain| Domain {
|
||||
union: vec![domain],
|
||||
})
|
||||
.parse_next(input)
|
||||
}
|
||||
|
||||
pub fn operator_parse(input: &mut Stream) -> Result<String>
|
||||
{
|
||||
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>
|
||||
{
|
||||
operator_parse(input).map(|op| Operator::infix(op, &input.state))?
|
||||
}
|
||||
pub fn operator_parse_postfix(input: &mut Stream) -> Result<Operator>
|
||||
{
|
||||
operator_parse(input).map(|op| Operator::postfix(op, &input.state))?
|
||||
}
|
||||
pub fn operator_parse_prefix(input: &mut Stream) -> Result<Operator>
|
||||
{
|
||||
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" => unimplemented!(),
|
||||
"yfx" => OperatorType::LeftInfix,
|
||||
"xfy" => OperatorType::RightInfix,
|
||||
_ => unreachable!(),
|
||||
};
|
||||
input.state.custom_operators.insert(
|
||||
(op.clone(), op_type.clone()),
|
||||
Operator::new(op, precedence, op_type),
|
||||
);
|
||||
Ok(())
|
||||
}
|
||||
|
||||
pub fn predicate_parse_infix_expression<'a>(
|
||||
input: &mut Stream<'a>,
|
||||
) -> Result<Infix<Stream<'a>, Predicate, Operator, ContextError>>
|
||||
{
|
||||
let op = operator_parse_infix.parse_next(input)?;
|
||||
Ok(op.make_infix_operator())
|
||||
}
|
||||
|
||||
pub fn predicate_parse_prefix_expression<'a>(
|
||||
input: &mut Stream<'a>,
|
||||
) -> Result<Prefix<Stream<'a>, 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<Postfix<Stream<'a>, 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<Predicate>
|
||||
{
|
||||
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<Predicate>
|
||||
{
|
||||
let ident = alphanumeric1.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)))
|
||||
Ok(Predicate::Variable(Variable(String::from(ident), None)))
|
||||
}
|
||||
else
|
||||
{
|
||||
@ -34,11 +239,29 @@ pub fn predicate_parse(input: &mut &str) -> Result<Predicate>
|
||||
)
|
||||
.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<Body>
|
||||
pub fn predicate_parse_recursive(input: &mut Stream) -> Result<Predicate>
|
||||
{
|
||||
alt((
|
||||
delimited("(", predicate_parse, ")"),
|
||||
domain_parse.map(Predicate::Domain),
|
||||
predicate_parse_variable_or_functor,
|
||||
))
|
||||
.parse_next(input)
|
||||
}
|
||||
|
||||
pub fn predicate_parse(input: &mut Stream) -> Result<Predicate>
|
||||
{
|
||||
alt((predicate_parse_expression, predicate_parse_recursive)).parse_next(input)
|
||||
}
|
||||
|
||||
fn body_parse_or(input: &mut Stream) -> Result<Body>
|
||||
{
|
||||
separated(
|
||||
1..,
|
||||
@ -52,7 +275,7 @@ fn body_parse_or(input: &mut &str) -> Result<Body>
|
||||
.parse_next(input)
|
||||
}
|
||||
|
||||
pub fn body_parse(input: &mut &str) -> Result<Body>
|
||||
pub fn body_parse(input: &mut Stream) -> Result<Body>
|
||||
{
|
||||
// Parse and
|
||||
separated(1.., body_parse_or, (multispace0, ",", multispace0))
|
||||
@ -60,7 +283,7 @@ pub fn body_parse(input: &mut &str) -> Result<Body>
|
||||
.parse_next(input)
|
||||
}
|
||||
|
||||
pub fn clause_parse(input: &mut &str) -> Result<Clause>
|
||||
pub fn clause_parse(input: &mut Stream) -> Result<Clause>
|
||||
{
|
||||
seq! {
|
||||
Clause
|
||||
@ -74,12 +297,19 @@ pub fn clause_parse(input: &mut &str) -> Result<Clause>
|
||||
.parse_next(input)
|
||||
}
|
||||
|
||||
pub fn module_parse(input: &mut &str) -> Result<Module>
|
||||
pub fn module_parse(input: &mut Stream) -> Result<Module>
|
||||
{
|
||||
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<T> From<T> for Module
|
||||
@ -88,8 +318,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 +342,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 +358,44 @@ 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()
|
||||
}
|
||||
}
|
||||
|
||||
impl<T> From<T> for Domain
|
||||
where
|
||||
T: AsRef<str>,
|
||||
{
|
||||
fn from(value: T) -> Self
|
||||
{
|
||||
let str: &str = value.as_ref();
|
||||
domain_parse
|
||||
.parse_next(&mut Stream {
|
||||
input: str,
|
||||
state: State::new(),
|
||||
})
|
||||
.unwrap()
|
||||
}
|
||||
}
|
||||
|
||||
impl<T> From<T> for DomainRange
|
||||
where
|
||||
T: AsRef<str>,
|
||||
{
|
||||
fn from(value: T) -> Self
|
||||
{
|
||||
let str: &str = value.as_ref();
|
||||
domain_range_parse
|
||||
.parse_next(&mut Stream {
|
||||
input: str,
|
||||
state: State::new(),
|
||||
})
|
||||
.unwrap()
|
||||
}
|
||||
}
|
||||
|
||||
314
src/prover.rs
314
src/prover.rs
@ -1,19 +1,24 @@
|
||||
pub mod and;
|
||||
pub mod body;
|
||||
pub mod constraints;
|
||||
pub mod trace;
|
||||
pub mod not;
|
||||
pub mod or;
|
||||
pub mod predicate;
|
||||
pub mod tracing;
|
||||
pub mod unification;
|
||||
|
||||
use std::cell::Cell;
|
||||
use std::collections::VecDeque;
|
||||
use std::collections::HashMap;
|
||||
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::ast::Variable;
|
||||
use crate::prover::body::BodyProver;
|
||||
use crate::prover::constraints::Constraints;
|
||||
use crate::prover::tracing::IndentedTracer;
|
||||
|
||||
#[derive(Clone, Copy, Debug, Default)]
|
||||
pub struct Counter(usize);
|
||||
@ -25,7 +30,12 @@ impl GlobalCounter
|
||||
{
|
||||
pub fn new() -> GlobalCounter
|
||||
{
|
||||
GlobalCounter(Rc::new(Cell::new(0)))
|
||||
Self::with(0)
|
||||
}
|
||||
|
||||
pub fn with(n: usize) -> GlobalCounter
|
||||
{
|
||||
GlobalCounter(Rc::new(Cell::new(n)))
|
||||
}
|
||||
|
||||
pub fn get(&self) -> usize
|
||||
@ -46,258 +56,6 @@ impl GlobalCounter
|
||||
}
|
||||
}
|
||||
|
||||
pub struct BodyProver<'a>
|
||||
{
|
||||
module: &'a Module,
|
||||
constraints: Constraints,
|
||||
|
||||
prover: Box<dyn Iterator<Item = Constraints> + 'a>,
|
||||
}
|
||||
|
||||
pub struct PredicateProver<'a>
|
||||
{
|
||||
module: &'a Module,
|
||||
predicate: Predicate,
|
||||
constraints: Constraints,
|
||||
counter_snapshot: Counter,
|
||||
|
||||
global_counter: GlobalCounter,
|
||||
current_clause: usize,
|
||||
sub_proof: Option<BodyProver<'a>>,
|
||||
}
|
||||
|
||||
pub struct AndProver<'a>
|
||||
{
|
||||
module: &'a Module,
|
||||
bodies: Vec<Body>,
|
||||
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<dyn Iterator<Item = Constraints>> = 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<Body>,
|
||||
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<Self::Item>
|
||||
{
|
||||
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<Constraints>
|
||||
{
|
||||
self.prover.next()
|
||||
}
|
||||
}
|
||||
|
||||
impl Iterator for AndProver<'_>
|
||||
{
|
||||
type Item = Constraints;
|
||||
|
||||
fn next(&mut self) -> Option<Self::Item>
|
||||
{
|
||||
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>
|
||||
@ -307,6 +65,9 @@ impl Module
|
||||
GlobalCounter::new(),
|
||||
body.clone(),
|
||||
Constraints::none(),
|
||||
//&mut EmptyTracer,
|
||||
&mut IndentedTracer::new(),
|
||||
//&SimpleTracer::new(ProofType::Body),
|
||||
)
|
||||
}
|
||||
}
|
||||
@ -315,7 +76,7 @@ impl Clause
|
||||
{
|
||||
pub fn make_unique(&self, counter: GlobalCounter) -> Clause
|
||||
{
|
||||
let mut unique_map = LiteMap::new();
|
||||
let mut unique_map = HashMap::new();
|
||||
Clause {
|
||||
head: self.head.make_unique(counter.clone(), &mut unique_map),
|
||||
body: self
|
||||
@ -331,7 +92,7 @@ impl Body
|
||||
pub fn make_unique(
|
||||
&self,
|
||||
counter: GlobalCounter,
|
||||
unique_map: &mut LiteMap<String, usize>,
|
||||
unique_map: &mut HashMap<Variable, usize>,
|
||||
) -> Body
|
||||
{
|
||||
match self
|
||||
@ -358,18 +119,15 @@ impl Predicate
|
||||
pub fn make_unique(
|
||||
&self,
|
||||
counter: GlobalCounter,
|
||||
unique_map: &mut LiteMap<String, usize>,
|
||||
unique_map: &mut HashMap<Variable, usize>,
|
||||
) -> Self
|
||||
{
|
||||
match self
|
||||
{
|
||||
Predicate::Variable(name) => Predicate::Variable(format!(
|
||||
"_{}[{}]",
|
||||
name,
|
||||
unique_map
|
||||
.entry(name.clone())
|
||||
.or_insert_with(|| counter.get())
|
||||
)),
|
||||
Predicate::Variable(var) =>
|
||||
{
|
||||
Predicate::Variable(var.make_unique(counter.clone(), unique_map))
|
||||
}
|
||||
Predicate::Fixed(name, predicates) => Predicate::Fixed(
|
||||
name.clone(),
|
||||
predicates
|
||||
@ -377,6 +135,26 @@ impl Predicate
|
||||
.map(|x| x.make_unique(counter.clone(), unique_map))
|
||||
.collect(),
|
||||
),
|
||||
Predicate::Domain(domain) => Predicate::Domain(domain.clone()),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Variable
|
||||
{
|
||||
pub fn make_unique(
|
||||
&self,
|
||||
counter: GlobalCounter,
|
||||
unique_map: &mut HashMap<Variable, usize>,
|
||||
) -> Self
|
||||
{
|
||||
Variable(
|
||||
self.0.clone(),
|
||||
Some(
|
||||
*unique_map
|
||||
.entry(self.clone())
|
||||
.or_insert_with(|| counter.get()),
|
||||
),
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
172
src/prover/and.rs
Normal file
172
src/prover/and.rs
Normal file
@ -0,0 +1,172 @@
|
||||
use std::fmt::Write;
|
||||
|
||||
use owo_colors::OwoColorize;
|
||||
|
||||
use crate::ast::Body;
|
||||
use crate::ast::Module;
|
||||
use crate::prover::Counter;
|
||||
use crate::prover::GlobalCounter;
|
||||
use crate::prover::body::BodyProver;
|
||||
use crate::prover::constraints::Constraints;
|
||||
use crate::prover::tracing::ProofType;
|
||||
use crate::prover::tracing::Tracer;
|
||||
|
||||
pub struct AndProver<'a, T: Tracer>
|
||||
{
|
||||
module: &'a Module,
|
||||
bodies: Vec<Body>,
|
||||
tracer: T,
|
||||
|
||||
global_counter: GlobalCounter,
|
||||
sub_proofs: Vec<(Counter, BodyProver<'a>)>,
|
||||
}
|
||||
impl<T: Tracer> AndProver<'_, T>
|
||||
{
|
||||
pub fn new<'a>(
|
||||
module: &'a Module,
|
||||
global_counter: GlobalCounter,
|
||||
bodies: Vec<Body>,
|
||||
constraints: Constraints,
|
||||
tracer: &mut T,
|
||||
) -> AndProver<'a, T>
|
||||
where
|
||||
T: 'a,
|
||||
{
|
||||
assert!(!bodies.is_empty());
|
||||
|
||||
// Pretty logging
|
||||
let mut tracer = tracer.begin_proof(ProofType::And);
|
||||
let mut next = String::new();
|
||||
for x in bodies.iter().skip(1)
|
||||
{
|
||||
let _ = next.write_str(&format!("{}, ", x));
|
||||
}
|
||||
|
||||
let mut conjuction = String::new();
|
||||
let len = bodies.len();
|
||||
for (i, x) in bodies.iter().enumerate()
|
||||
{
|
||||
let _ = conjuction.write_str(&format!("{}", x));
|
||||
if i != len - 1
|
||||
{
|
||||
let _ = conjuction.write_str(" ∧ ");
|
||||
}
|
||||
}
|
||||
|
||||
tracer.print_step(format!("Proving conjuction {}", conjuction));
|
||||
tracer.print_step(format!("{} :", "Proved".fg::<owo_colors::colors::Green>(),));
|
||||
tracer.print_step(format!(
|
||||
"{} : {}",
|
||||
"Proving".fg::<owo_colors::colors::Yellow>(),
|
||||
bodies[0]
|
||||
));
|
||||
tracer.print_step(format!(
|
||||
"{} : {}",
|
||||
"Next".fg::<owo_colors::colors::Red>(),
|
||||
next
|
||||
));
|
||||
tracer.print_step(format!("With constraints : {}", constraints.simplified()));
|
||||
// End pretty logging
|
||||
|
||||
AndProver {
|
||||
module,
|
||||
sub_proofs: vec![(
|
||||
global_counter.snapshot(),
|
||||
BodyProver::new(
|
||||
module,
|
||||
global_counter.clone(),
|
||||
bodies[0].clone(),
|
||||
constraints.clone(),
|
||||
&mut tracer,
|
||||
),
|
||||
)],
|
||||
tracer,
|
||||
bodies,
|
||||
global_counter,
|
||||
}
|
||||
}
|
||||
}
|
||||
impl<'a, T: Tracer + 'a> Iterator for AndProver<'a, T>
|
||||
{
|
||||
type Item = Constraints;
|
||||
|
||||
fn next(&mut self) -> Option<Self::Item>
|
||||
{
|
||||
if self.sub_proofs.is_empty()
|
||||
{
|
||||
return None;
|
||||
}
|
||||
|
||||
let (current_proof_snap, mut current_proof) = self.sub_proofs.pop().unwrap();
|
||||
|
||||
match current_proof.next()
|
||||
{
|
||||
Some(constraints) =>
|
||||
{
|
||||
if self.sub_proofs.len() == self.bodies.len() - 1
|
||||
{
|
||||
self.sub_proofs.push((current_proof_snap, current_proof));
|
||||
Some(constraints)
|
||||
}
|
||||
else
|
||||
{
|
||||
// Pretty logging
|
||||
let mut proved = String::new();
|
||||
let mut proving = String::new();
|
||||
let mut next = String::new();
|
||||
for (i, x) in self.bodies.iter().enumerate()
|
||||
{
|
||||
let dest;
|
||||
if i == self.sub_proofs.len() + 1
|
||||
{
|
||||
dest = &mut proving;
|
||||
}
|
||||
else if i < self.sub_proofs.len() + 1
|
||||
{
|
||||
dest = &mut proved;
|
||||
}
|
||||
else
|
||||
{
|
||||
dest = &mut next;
|
||||
}
|
||||
let _ = dest.write_str(&format!("{}, ", x));
|
||||
}
|
||||
self.tracer.print_step(format!(
|
||||
"{} : {}",
|
||||
"Proved".fg::<owo_colors::colors::Green>(),
|
||||
proved
|
||||
));
|
||||
self.tracer.print_step(format!(
|
||||
"{} : {}",
|
||||
"Proving".fg::<owo_colors::colors::Yellow>(),
|
||||
proving
|
||||
));
|
||||
self.tracer.print_step(format!(
|
||||
"{} : {}",
|
||||
"Next".fg::<owo_colors::colors::Red>(),
|
||||
next
|
||||
));
|
||||
// End pretty logging
|
||||
|
||||
self.sub_proofs.push((current_proof_snap, current_proof));
|
||||
self.sub_proofs.push((
|
||||
self.global_counter.snapshot(),
|
||||
BodyProver::new(
|
||||
self.module,
|
||||
self.global_counter.clone(),
|
||||
self.bodies[self.sub_proofs.len()].clone(),
|
||||
constraints,
|
||||
&mut self.tracer,
|
||||
),
|
||||
));
|
||||
self.next()
|
||||
}
|
||||
}
|
||||
None =>
|
||||
{
|
||||
self.global_counter.restore(current_proof_snap);
|
||||
self.next()
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
70
src/prover/body.rs
Normal file
70
src/prover/body.rs
Normal file
@ -0,0 +1,70 @@
|
||||
use crate::ast::Body;
|
||||
use crate::ast::Module;
|
||||
use crate::prover::GlobalCounter;
|
||||
use crate::prover::and::AndProver;
|
||||
use crate::prover::constraints::Constraints;
|
||||
use crate::prover::predicate::PredicateProver;
|
||||
use crate::prover::tracing::Tracer;
|
||||
|
||||
pub struct BodyProver<'a>
|
||||
{
|
||||
prover: Box<dyn Iterator<Item = Constraints> + 'a>,
|
||||
}
|
||||
|
||||
impl<'a> BodyProver<'a>
|
||||
{
|
||||
pub fn new<T: Tracer + 'a>(
|
||||
module: &'a Module,
|
||||
global_counter: GlobalCounter,
|
||||
body: Body,
|
||||
constraints: Constraints,
|
||||
tracer: &mut T,
|
||||
) -> BodyProver<'a>
|
||||
{
|
||||
let prover: Box<dyn Iterator<Item = Constraints>> = match &body
|
||||
{
|
||||
Body::Term(predicate) => Box::new(PredicateProver::new(
|
||||
module,
|
||||
global_counter,
|
||||
predicate.clone(),
|
||||
constraints.clone(),
|
||||
tracer,
|
||||
)),
|
||||
|
||||
// Shortcut And & Or prover if it contains only one element to simplify proofs
|
||||
Body::And(items) | Body::Or(items) if items.len() == 1 => Box::new(BodyProver::new(
|
||||
module,
|
||||
global_counter,
|
||||
items[0].clone(),
|
||||
constraints.clone(),
|
||||
tracer,
|
||||
)),
|
||||
|
||||
Body::And(items) => Box::new(AndProver::new(
|
||||
module,
|
||||
global_counter,
|
||||
items.clone(),
|
||||
constraints.clone(),
|
||||
tracer,
|
||||
)),
|
||||
Body::Or(items) => Box::new(BodyProver::new(
|
||||
module,
|
||||
global_counter,
|
||||
items[0].clone(),
|
||||
constraints.clone(),
|
||||
tracer,
|
||||
)),
|
||||
};
|
||||
|
||||
BodyProver { prover }
|
||||
}
|
||||
}
|
||||
|
||||
impl<'a> Iterator for BodyProver<'a>
|
||||
{
|
||||
type Item = Constraints;
|
||||
fn next(&mut self) -> Option<Constraints>
|
||||
{
|
||||
self.prover.next()
|
||||
}
|
||||
}
|
||||
@ -1,16 +1,18 @@
|
||||
use std::collections::HashMap;
|
||||
use std::fmt::Display;
|
||||
|
||||
use litemap::LiteMap;
|
||||
use winnow::Str;
|
||||
|
||||
use crate::ast::Body;
|
||||
use crate::ast::Predicate;
|
||||
use crate::ast::Variable;
|
||||
use crate::prover::constraints;
|
||||
use crate::domain;
|
||||
use crate::domain::Domain;
|
||||
use crate::prover::predicate;
|
||||
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct Constraints
|
||||
{
|
||||
set: LiteMap<Variable, Predicate>,
|
||||
pub(crate) predicates: HashMap<Variable, Predicate>,
|
||||
pub(crate) domains: HashMap<Variable, Domain>,
|
||||
}
|
||||
|
||||
impl Constraints
|
||||
@ -18,21 +20,38 @@ impl Constraints
|
||||
pub fn none() -> Self
|
||||
{
|
||||
Constraints {
|
||||
set: LiteMap::new(),
|
||||
predicates: HashMap::new(),
|
||||
domains: HashMap::new(),
|
||||
}
|
||||
}
|
||||
|
||||
pub fn with(variable: Variable, predicate: Predicate) -> Self
|
||||
pub fn with(variable: Variable, predicate: Option<Predicate>, domain: Option<Domain>) -> Self
|
||||
{
|
||||
let mut c = Constraints::none();
|
||||
c.set.insert(variable, predicate);
|
||||
if let Some(predicate) = predicate
|
||||
{
|
||||
c.predicates.insert(variable.clone(), predicate);
|
||||
}
|
||||
if let Some(domain) = domain
|
||||
{
|
||||
c.domains.insert(variable, domain);
|
||||
}
|
||||
c
|
||||
}
|
||||
|
||||
pub fn try_append(&mut self, variable: &Variable, predicate: &Predicate) -> bool
|
||||
pub fn try_append(
|
||||
&mut self,
|
||||
variable: &Variable,
|
||||
predicate: &Predicate,
|
||||
domain: &Domain,
|
||||
) -> bool
|
||||
{
|
||||
if let Some(other_predicate) = self.set.get(variable)
|
||||
let predicates = if let Some(other_predicate) = self.predicates.get(variable)
|
||||
{
|
||||
if predicate == other_predicate
|
||||
{
|
||||
return true;
|
||||
}
|
||||
// If variable is already contrained, we need to check if both contraints are
|
||||
// contradictory
|
||||
|
||||
@ -44,7 +63,7 @@ impl Constraints
|
||||
// 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());
|
||||
self.predicates.insert(variable.clone(), predicate.clone());
|
||||
true
|
||||
}
|
||||
else
|
||||
@ -61,18 +80,40 @@ impl Constraints
|
||||
else
|
||||
{
|
||||
// No constraint
|
||||
self.set.insert(variable.clone(), predicate.clone());
|
||||
self.predicates
|
||||
.insert(variable.clone(), (predicate.clone(), domain.clone()));
|
||||
true
|
||||
};
|
||||
|
||||
// Check if domains are compatible
|
||||
let domains = if let Some((_, other_domain)) = self.predicates.get_mut(variable)
|
||||
{
|
||||
let intersection = domain.intersection(other_domain);
|
||||
if intersection.empty()
|
||||
{
|
||||
false
|
||||
}
|
||||
else
|
||||
{
|
||||
*other_domain = intersection;
|
||||
true
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
true
|
||||
};
|
||||
|
||||
domains && predicates
|
||||
}
|
||||
|
||||
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()
|
||||
for (var, (pred, domain)) in constraints.predicates.iter()
|
||||
{
|
||||
if !ok.try_append(var, pred)
|
||||
if !ok.try_append(var, pred, domain)
|
||||
{
|
||||
return false;
|
||||
}
|
||||
@ -91,24 +132,26 @@ impl Constraints
|
||||
pub fn simplified(&self) -> Constraints
|
||||
{
|
||||
let mut max_sub = Constraints::none();
|
||||
for (var, pred) in self.set.iter()
|
||||
for (var, (pred, domain)) in self.predicates.iter()
|
||||
{
|
||||
max_sub.set.insert(var.clone(), pred.substitute(self));
|
||||
max_sub
|
||||
.predicates
|
||||
.insert(var.clone(), (pred.substitute(self), domain.clone()));
|
||||
}
|
||||
|
||||
let mut stripped = max_sub.clone();
|
||||
'outer: for (var, _) in max_sub.set.iter()
|
||||
'outer: for (var, _) in max_sub.predicates.iter()
|
||||
{
|
||||
if var.chars().next().is_some_and(|x| x == '_')
|
||||
if var.0.chars().next().is_some_and(|x| x == '_') || var.1.is_some()
|
||||
{
|
||||
for (_, other_pred) in max_sub.set.iter()
|
||||
for (_, (other_pred, _)) in max_sub.predicates.iter()
|
||||
{
|
||||
if other_pred.contains_variable(var)
|
||||
{
|
||||
continue 'outer;
|
||||
}
|
||||
}
|
||||
stripped.set.remove(var);
|
||||
stripped.predicates.remove(var);
|
||||
}
|
||||
}
|
||||
|
||||
@ -124,10 +167,9 @@ impl Predicate
|
||||
{
|
||||
Predicate::Variable(name) =>
|
||||
{
|
||||
if let Some(pred) = constraints.set.get(name)
|
||||
if let Some((pred, _)) = constraints.predicates.get(name)
|
||||
{
|
||||
let max_sub = pred.substitute(constraints);
|
||||
max_sub
|
||||
pred.substitute(constraints)
|
||||
}
|
||||
else
|
||||
{
|
||||
@ -141,18 +183,33 @@ impl Predicate
|
||||
.map(|x| x.substitute(constraints))
|
||||
.collect(),
|
||||
),
|
||||
Predicate::Domain(domain) => Predicate::Domain(domain.clone()),
|
||||
}
|
||||
}
|
||||
|
||||
pub fn contains_variable(&self, name: &String) -> bool
|
||||
pub fn contains_variable(&self, name: &Variable) -> bool
|
||||
{
|
||||
match self
|
||||
{
|
||||
Predicate::Variable(var_name) => name == var_name,
|
||||
Predicate::Fixed(_, predicates) => predicates
|
||||
.iter()
|
||||
.find(|x| x.contains_variable(name))
|
||||
.is_some(),
|
||||
Predicate::Fixed(_, predicates) => predicates.iter().any(|x| x.contains_variable(name)),
|
||||
Predicate::Domain(_) => false,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Body
|
||||
{
|
||||
pub fn substitute(&self, constraints: &Constraints) -> Body
|
||||
{
|
||||
match self
|
||||
{
|
||||
Body::Term(predicate) => Body::Term(predicate.substitute(constraints)),
|
||||
Body::And(items) =>
|
||||
{
|
||||
Body::And(items.iter().map(|x| x.substitute(constraints)).collect())
|
||||
}
|
||||
Body::Or(items) => Body::Or(items.iter().map(|x| x.substitute(constraints)).collect()),
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -169,8 +226,8 @@ 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()
|
||||
let len = self.predicates.len();
|
||||
for (i, (var, (pred, _))) in self.predicates.iter().enumerate()
|
||||
{
|
||||
write!(f, "{} = {}", var, pred)?;
|
||||
if i != len - 1
|
||||
@ -178,6 +235,15 @@ impl Display for Constraints
|
||||
write!(f, ", ")?;
|
||||
}
|
||||
}
|
||||
write!(f, " ;; ")?;
|
||||
for (i, (var, (_, domain))) in self.predicates.iter().enumerate()
|
||||
{
|
||||
write!(f, "{} in {}", var, domain)?;
|
||||
if i != len - 1
|
||||
{
|
||||
write!(f, ", ")?;
|
||||
}
|
||||
}
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
|
||||
50
src/prover/internal_operators.rs
Normal file
50
src/prover/internal_operators.rs
Normal file
@ -0,0 +1,50 @@
|
||||
use crate::{ast::Predicate, prover::constraints::Constraints};
|
||||
|
||||
impl Constraints
|
||||
{
|
||||
pub fn collapsed_operators(&self) -> Constraints
|
||||
{
|
||||
let mut new_constraints = Constraints::none();
|
||||
for (var, pred) in self.set.iter()
|
||||
{
|
||||
new_constraints
|
||||
.set
|
||||
.insert(var.clone(), pred.substitute(self).collapsed_operators());
|
||||
}
|
||||
new_constraints
|
||||
}
|
||||
}
|
||||
|
||||
impl Predicate
|
||||
{
|
||||
pub fn collapsed_operators(&self) -> Predicate
|
||||
{
|
||||
match self
|
||||
{
|
||||
Predicate::Variable(variable) => Predicate::Variable(variable.clone()),
|
||||
Predicate::Fixed(crate::ast::Functor::Operator(op), predicates)
|
||||
if op.op == "+" && predicates.len() == 2 =>
|
||||
{
|
||||
match (predicates[0].clone(), predicates[1].clone())
|
||||
{
|
||||
(Predicate::Number(a), Predicate::Number(b)) => Predicate::Number(a + b),
|
||||
_ => self.clone(),
|
||||
}
|
||||
}
|
||||
Predicate::Fixed(crate::ast::Functor::Operator(op), predicates)
|
||||
if op.op == "-" && predicates.len() == 2 =>
|
||||
{
|
||||
match (predicates[0].clone(), predicates[1].clone())
|
||||
{
|
||||
(Predicate::Number(a), Predicate::Number(b)) => Predicate::Number(a - b),
|
||||
_ => self.clone(),
|
||||
}
|
||||
}
|
||||
Predicate::Fixed(functor, predicates) => Predicate::Fixed(
|
||||
functor.clone(),
|
||||
predicates.iter().map(|x| x.collapsed_operators()).collect(),
|
||||
),
|
||||
Predicate::Number(n) => Predicate::Number(*n),
|
||||
}
|
||||
}
|
||||
}
|
||||
71
src/prover/not.rs
Normal file
71
src/prover/not.rs
Normal file
@ -0,0 +1,71 @@
|
||||
use crate::ast::Body;
|
||||
use crate::ast::Module;
|
||||
use crate::prover::GlobalCounter;
|
||||
use crate::prover::body::BodyProver;
|
||||
use crate::prover::constraints::Constraints;
|
||||
use crate::prover::tracing::ProofType;
|
||||
use crate::prover::tracing::Tracer;
|
||||
|
||||
pub struct NotProver<'a, T: Tracer + 'a>
|
||||
{
|
||||
prover: Option<BodyProver<'a>>,
|
||||
constraints: Constraints,
|
||||
tracer: T,
|
||||
}
|
||||
|
||||
impl<'a, T: Tracer + 'a> NotProver<'a, T>
|
||||
{
|
||||
pub fn new(
|
||||
module: &'a Module,
|
||||
global_counter: GlobalCounter,
|
||||
body: Body,
|
||||
constraints: Constraints,
|
||||
tracer: &mut T,
|
||||
) -> NotProver<'a, T>
|
||||
{
|
||||
let mut not_tracer = tracer.begin_proof(ProofType::Body);
|
||||
NotProver {
|
||||
prover: Some(BodyProver::new(
|
||||
module,
|
||||
global_counter,
|
||||
body,
|
||||
constraints.clone(),
|
||||
&mut not_tracer,
|
||||
)),
|
||||
tracer: not_tracer,
|
||||
constraints: constraints.clone(),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl<'a, T: Tracer + 'a> Iterator for NotProver<'a, T>
|
||||
{
|
||||
type Item = Constraints;
|
||||
fn next(&mut self) -> Option<Constraints>
|
||||
{
|
||||
if let Some(x) = self.prover.as_mut()
|
||||
{
|
||||
match &mut x.next()
|
||||
{
|
||||
Some(_) =>
|
||||
{
|
||||
// The prover showed that the proof is true.
|
||||
// Thus the negation is never true
|
||||
self.prover = None;
|
||||
None
|
||||
}
|
||||
None =>
|
||||
{
|
||||
// The prover did not find any proof
|
||||
// Thus the negation is true
|
||||
self.prover = None;
|
||||
Some(self.constraints.clone())
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
None
|
||||
}
|
||||
}
|
||||
}
|
||||
124
src/prover/or.rs
Normal file
124
src/prover/or.rs
Normal file
@ -0,0 +1,124 @@
|
||||
use std::fmt::Write;
|
||||
|
||||
use crate::ast::Body;
|
||||
use crate::ast::Module;
|
||||
use crate::prover::Counter;
|
||||
use crate::prover::GlobalCounter;
|
||||
use crate::prover::body::BodyProver;
|
||||
use crate::prover::constraints::Constraints;
|
||||
use crate::prover::tracing::ProofType;
|
||||
use crate::prover::tracing::Tracer;
|
||||
|
||||
pub struct OrProver<'a, T: Tracer>
|
||||
{
|
||||
module: &'a Module,
|
||||
bodies: Vec<Body>,
|
||||
constraints: Constraints,
|
||||
tracer: T,
|
||||
|
||||
current_proving: usize,
|
||||
global_counter: GlobalCounter,
|
||||
counter_snapshot: Counter,
|
||||
sub_proof: Option<BodyProver<'a>>,
|
||||
}
|
||||
|
||||
impl<T: Tracer> OrProver<'_, T>
|
||||
{
|
||||
pub fn new<'a>(
|
||||
module: &'a Module,
|
||||
global_counter: GlobalCounter,
|
||||
bodies: Vec<Body>,
|
||||
constraints: Constraints,
|
||||
tracer: &mut T,
|
||||
) -> OrProver<'a, T>
|
||||
where
|
||||
T: 'a,
|
||||
{
|
||||
assert!(!bodies.is_empty());
|
||||
|
||||
// Pretty logging
|
||||
let mut tracer = tracer.begin_proof(ProofType::And);
|
||||
|
||||
let mut next = String::new();
|
||||
for x in bodies.iter().skip(1)
|
||||
{
|
||||
let _ = next.write_str(&format!("{}, ", x));
|
||||
}
|
||||
|
||||
let mut disjunction = String::new();
|
||||
let len = bodies.len();
|
||||
for (i, x) in bodies.iter().enumerate()
|
||||
{
|
||||
let _ = disjunction.write_str(&format!("{}", x));
|
||||
if i != len - 1
|
||||
{
|
||||
let _ = disjunction.write_str(" ∨ ");
|
||||
}
|
||||
}
|
||||
|
||||
// End pretty logging
|
||||
|
||||
OrProver {
|
||||
module,
|
||||
sub_proof: Some(BodyProver::new(
|
||||
module,
|
||||
global_counter.clone(),
|
||||
bodies[0].clone(),
|
||||
constraints.clone(),
|
||||
&mut tracer,
|
||||
)),
|
||||
tracer,
|
||||
current_proving: 0,
|
||||
counter_snapshot: global_counter.snapshot(),
|
||||
bodies,
|
||||
constraints,
|
||||
global_counter,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl<'a, T: Tracer + 'a> Iterator for OrProver<'a, T>
|
||||
{
|
||||
type Item = Constraints;
|
||||
|
||||
fn next(&mut self) -> Option<Self::Item>
|
||||
{
|
||||
let proof = match &mut self.sub_proof
|
||||
{
|
||||
Some(sub_proof) => sub_proof.next(),
|
||||
None =>
|
||||
{
|
||||
return None;
|
||||
}
|
||||
};
|
||||
|
||||
match proof
|
||||
{
|
||||
Some(x) => Some(x),
|
||||
None =>
|
||||
{
|
||||
// Advance to next possibility
|
||||
if self.current_proving == self.bodies.len() - 1
|
||||
{
|
||||
self.sub_proof = None;
|
||||
None
|
||||
}
|
||||
else
|
||||
{
|
||||
self.current_proving += 1;
|
||||
self.global_counter.restore(self.counter_snapshot);
|
||||
self.tracer
|
||||
.print_step(format!("Tring with {}", self.bodies[self.current_proving]));
|
||||
self.sub_proof = Some(BodyProver::new(
|
||||
self.module,
|
||||
self.global_counter.clone(),
|
||||
self.bodies[self.current_proving].clone(),
|
||||
self.constraints.clone(),
|
||||
&mut self.tracer,
|
||||
));
|
||||
self.next()
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
132
src/prover/predicate.rs
Normal file
132
src/prover/predicate.rs
Normal file
@ -0,0 +1,132 @@
|
||||
use owo_colors::OwoColorize;
|
||||
use owo_colors::colors::Green;
|
||||
|
||||
use crate::ast::{Module, Predicate};
|
||||
use crate::prover::body::BodyProver;
|
||||
use crate::prover::constraints::Constraints;
|
||||
use crate::prover::tracing::{ProofType, Tracer};
|
||||
use crate::prover::{Counter, GlobalCounter};
|
||||
|
||||
pub struct PredicateProver<'a, T: Tracer>
|
||||
{
|
||||
module: &'a Module,
|
||||
predicate: Predicate,
|
||||
constraints: Constraints,
|
||||
counter_snapshot: Counter,
|
||||
tracer: T,
|
||||
|
||||
global_counter: GlobalCounter,
|
||||
current_clause: usize,
|
||||
sub_proof: Option<BodyProver<'a>>,
|
||||
}
|
||||
|
||||
impl<'a, T: Tracer + 'a> PredicateProver<'a, T>
|
||||
{
|
||||
pub fn new(
|
||||
module: &'a Module,
|
||||
global_counter: GlobalCounter,
|
||||
predicate: Predicate,
|
||||
constraints: Constraints,
|
||||
tracer: &mut T,
|
||||
) -> PredicateProver<'a, T>
|
||||
{
|
||||
//info!(target: "PredicateProver", "Proving {}", predicate);
|
||||
let mut predicate_prover = tracer.begin_proof(ProofType::Predicate);
|
||||
predicate_prover.print_step(format!(
|
||||
"{} '{}'",
|
||||
"Proving predicate".fg::<Green>(),
|
||||
predicate
|
||||
));
|
||||
PredicateProver {
|
||||
module,
|
||||
tracer: predicate_prover,
|
||||
predicate,
|
||||
constraints,
|
||||
current_clause: 0,
|
||||
sub_proof: None,
|
||||
counter_snapshot: global_counter.snapshot(),
|
||||
global_counter,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl<'a, T: Tracer + 'a> Iterator for PredicateProver<'a, T>
|
||||
{
|
||||
type Item = Constraints;
|
||||
|
||||
fn next(&mut self) -> Option<Self::Item>
|
||||
{
|
||||
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());
|
||||
let uni = self.predicate.matches(&clause.head);
|
||||
let full_constraints = uni.and_then(|x| x.and(&self.constraints));
|
||||
|
||||
if let Some(c) = &full_constraints
|
||||
{
|
||||
self.tracer.print_step(format!(
|
||||
"Unifying '{}' aginst '{}'",
|
||||
self.predicate, clause
|
||||
));
|
||||
self.tracer.print_step(format!(
|
||||
"↳ {}: {}",
|
||||
"Matches".fg::<Green>(),
|
||||
c.simplified()
|
||||
));
|
||||
}
|
||||
|
||||
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,
|
||||
&mut self.tracer,
|
||||
));
|
||||
self.next()
|
||||
}
|
||||
None =>
|
||||
{
|
||||
self.global_counter.restore(self.counter_snapshot);
|
||||
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()
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
146
src/prover/tracing.rs
Normal file
146
src/prover/tracing.rs
Normal file
@ -0,0 +1,146 @@
|
||||
use log::info;
|
||||
use owo_colors::colors::css::DarkGray;
|
||||
use owo_colors::colors::css::Gray;
|
||||
use owo_colors::OwoColorize;
|
||||
use owo_colors::Style;
|
||||
use std::fmt::Display;
|
||||
|
||||
#[derive(Clone, Copy)]
|
||||
pub enum ProofType
|
||||
{
|
||||
Body,
|
||||
And,
|
||||
Predicate,
|
||||
}
|
||||
|
||||
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"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
pub trait Tracer
|
||||
{
|
||||
fn begin_proof(&mut self, proof_type: ProofType) -> Self;
|
||||
fn print_step<T: Display>(&mut self, show: T);
|
||||
fn end_proof(self);
|
||||
}
|
||||
|
||||
pub struct SimpleTracer
|
||||
{
|
||||
proof_type: ProofType,
|
||||
}
|
||||
|
||||
impl SimpleTracer
|
||||
{
|
||||
pub fn new(proof_type: ProofType) -> Self
|
||||
{
|
||||
Self { proof_type }
|
||||
}
|
||||
}
|
||||
|
||||
impl Tracer for SimpleTracer
|
||||
{
|
||||
fn begin_proof(&mut self, proof_type: ProofType) -> Self
|
||||
{
|
||||
SimpleTracer { proof_type }
|
||||
}
|
||||
|
||||
fn print_step<T: Display>(&mut self, show: T)
|
||||
{
|
||||
let str = format!("{}", self.proof_type);
|
||||
info!(target: &str, "{}", show);
|
||||
}
|
||||
|
||||
fn end_proof(self)
|
||||
{
|
||||
todo!()
|
||||
}
|
||||
}
|
||||
|
||||
pub struct IndentedTracer
|
||||
{
|
||||
first: bool,
|
||||
depth: usize,
|
||||
}
|
||||
|
||||
impl IndentedTracer
|
||||
{
|
||||
pub fn new() -> IndentedTracer
|
||||
{
|
||||
IndentedTracer {
|
||||
first: true,
|
||||
depth: 0,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Tracer for IndentedTracer
|
||||
{
|
||||
fn begin_proof(&mut self, _proof_type: ProofType) -> Self
|
||||
{
|
||||
IndentedTracer {
|
||||
first: true,
|
||||
depth: self.depth + 1,
|
||||
}
|
||||
}
|
||||
|
||||
fn print_step<T: Display>(&mut self, show: T)
|
||||
{
|
||||
for i in 0..self.depth
|
||||
{
|
||||
let style = if i % 2 == 0
|
||||
{
|
||||
Style::new().fg::<Gray>()
|
||||
}
|
||||
else
|
||||
{
|
||||
Style::new().fg::<DarkGray>()
|
||||
};
|
||||
print!("{}", "│".style(style));
|
||||
}
|
||||
self.first = false;
|
||||
println!("{}", show);
|
||||
// let _ = std::io::stdin().read_line(&mut String::new());
|
||||
// println!("\x1b[2A");
|
||||
}
|
||||
|
||||
fn end_proof(self)
|
||||
{
|
||||
drop(self);
|
||||
}
|
||||
}
|
||||
|
||||
impl Drop for IndentedTracer
|
||||
{
|
||||
fn drop(&mut self) {}
|
||||
}
|
||||
|
||||
impl Default for IndentedTracer
|
||||
{
|
||||
fn default() -> Self
|
||||
{
|
||||
Self::new()
|
||||
}
|
||||
}
|
||||
|
||||
pub struct EmptyTracer;
|
||||
|
||||
impl Tracer for EmptyTracer
|
||||
{
|
||||
fn begin_proof(&mut self, _proof_type: ProofType) -> Self
|
||||
{
|
||||
EmptyTracer
|
||||
}
|
||||
|
||||
fn print_step<T: Display>(&mut self, _show: T) {}
|
||||
|
||||
fn end_proof(self) {}
|
||||
}
|
||||
@ -1,8 +1,7 @@
|
||||
use std::process::Output;
|
||||
|
||||
use log::debug;
|
||||
use std::clone;
|
||||
|
||||
use crate::ast::Predicate;
|
||||
use crate::domain::{self, Domain};
|
||||
use crate::prover::constraints::Constraints;
|
||||
|
||||
impl Predicate
|
||||
@ -13,16 +12,27 @@ impl Predicate
|
||||
/// returns `None` if the predicate cannot be unified against the other
|
||||
pub fn matches(&self, other: &Predicate) -> Option<Constraints>
|
||||
{
|
||||
debug!("Unifying {} against {}", self, other);
|
||||
match self
|
||||
{
|
||||
Predicate::Variable(variable) =>
|
||||
{
|
||||
//debug!("Unifying var {} against {}", self, other);
|
||||
// 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()))
|
||||
match other
|
||||
{
|
||||
Predicate::Domain(domain) => Some(Constraints::with(
|
||||
variable.clone(),
|
||||
other.clone(),
|
||||
domain.clone(),
|
||||
)),
|
||||
_ => Some(Constraints::with(
|
||||
variable.clone(),
|
||||
other.clone(),
|
||||
Domain::all(),
|
||||
)),
|
||||
}
|
||||
}
|
||||
|
||||
Predicate::Fixed(name, arguments) =>
|
||||
{
|
||||
match other
|
||||
@ -32,13 +42,15 @@ impl Predicate
|
||||
// We are trying to see if something like "predicate(..., ...)" matches X
|
||||
// (any)
|
||||
// This is always true
|
||||
Some(Constraints::with(var.clone(), self.clone()))
|
||||
//debug!("Unifying pred {} against var {}", self, other);
|
||||
Some(Constraints::with(var.clone(), self.clone(), Domain::all()))
|
||||
}
|
||||
// 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
|
||||
//debug!("Unifying fixed {} against fixed {}", self, other);
|
||||
if arguments.is_empty()
|
||||
{
|
||||
return Some(Constraints::none());
|
||||
@ -60,6 +72,20 @@ impl Predicate
|
||||
_ => None,
|
||||
}
|
||||
}
|
||||
Predicate::Domain(domain) => match other
|
||||
{
|
||||
Predicate::Variable(variable) => Some(Constraints::with(
|
||||
variable.clone(),
|
||||
other.clone(),
|
||||
domain.clone(),
|
||||
)),
|
||||
Predicate::Fixed(_, _) => None,
|
||||
Predicate::Domain(other_domain) if !domain.intersection(other_domain).empty() =>
|
||||
{
|
||||
Some(Constraints::none())
|
||||
}
|
||||
Predicate::Domain(_) => None,
|
||||
},
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
1
winnow
Submodule
1
winnow
Submodule
Submodule winnow added at cc0438a28f
Reference in New Issue
Block a user