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