From 762647ed5fbc3a22ec4c2143e5644738a787e6c6 Mon Sep 17 00:00:00 2001 From: ecoricemon Date: Mon, 16 Mar 2026 17:40:11 +0900 Subject: [PATCH] refactor: Generalize for various input types Any types that implement `Atom` is now can be represented as `Term`, `Expr`, and `Clause`, so that they can be evaluated. --- Cargo.toml | 2 +- crates/logic-eval-util/src/reference.rs | 2 +- crates/logic-eval/Cargo.toml | 5 +- crates/logic-eval/README.md | 15 +- crates/logic-eval/src/lib.rs | 138 +----- crates/logic-eval/src/parse/common.rs | 123 +++++ crates/logic-eval/src/parse/inner.rs | 26 ++ crates/logic-eval/src/parse/mod.rs | 2 +- crates/logic-eval/src/parse/repr.rs | 117 ++--- crates/logic-eval/src/parse/text.rs | 89 ++-- crates/logic-eval/src/prove/common.rs | 18 + crates/logic-eval/src/prove/db.rs | 598 +++++++++++++----------- crates/logic-eval/src/prove/mod.rs | 1 + crates/logic-eval/src/prove/prover.rs | 322 ++++++------- crates/logic-eval/src/prove/repr.rs | 84 ++-- src/lib.rs | 1 - 16 files changed, 792 insertions(+), 751 deletions(-) create mode 100644 crates/logic-eval/src/parse/common.rs create mode 100644 crates/logic-eval/src/prove/common.rs delete mode 100644 src/lib.rs diff --git a/Cargo.toml b/Cargo.toml index 1a72ddf..dba3bad 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -6,7 +6,7 @@ members = ["crates/*"] any-intern = { version = "0.1.5", path = "crates/any-intern" } logic-eval-util = { version = "0.1.5", path = "crates/logic-eval-util" } indexmap = "2.2.1" -smallvec = "1" +smallvec = "1.15.1" bumpalo = "3.10" fxhash = "0.2.1" hashbrown = "0.16.1" diff --git a/crates/logic-eval-util/src/reference.rs b/crates/logic-eval-util/src/reference.rs index ffc7cad..948c375 100644 --- a/crates/logic-eval-util/src/reference.rs +++ b/crates/logic-eval-util/src/reference.rs @@ -1,4 +1,4 @@ -use std::{marker::PhantomData, ptr::NonNull}; +use core::{marker::PhantomData, ptr::NonNull}; /// A lightweight wrapper around a non-null pointer for a shared reference. /// diff --git a/crates/logic-eval/Cargo.toml b/crates/logic-eval/Cargo.toml index ad7a4a3..da309b3 100644 --- a/crates/logic-eval/Cargo.toml +++ b/crates/logic-eval/Cargo.toml @@ -1,9 +1,9 @@ [package] name = "logic-eval" -version = "0.1.5" +version = "0.2.0" edition = "2021" rust-version = "1.65.0" -description = "A simple logic evaluator" +description = "A prolog-like logic evaluator" readme = "README.md" repository = "https://github.com/ecoricemon/logic-eval" license = "Apache-2.0 OR MIT" @@ -14,3 +14,4 @@ any-intern = { workspace = true } logic-eval-util = { workspace = true } indexmap = { workspace = true } fxhash = { workspace = true } +smallvec = { workspace = true } diff --git a/crates/logic-eval/README.md b/crates/logic-eval/README.md index adddc69..3a036b1 100644 --- a/crates/logic-eval/README.md +++ b/crates/logic-eval/README.md @@ -11,15 +11,16 @@ [codecov-badge]: https://codecov.io/gh/ecoricemon/logic-eval/graph/badge.svg?flag=logic-eval [codecov-url]: https://app.codecov.io/gh/ecoricemon/logic-eval?flags%5B0%5D=logic-eval -A simple logic evaluator. +A prolog-like logic evaluator. ## Example ```rust -use logic_eval::{Database, parse_str}; +use logic_eval::{Database, StrInterner, parse_str}; -// Creates a DB with default interner. +// Creates a DB. let mut db = Database::new(); +let interner = StrInterner::new(); // Initializes the DB with a little bit of logic. let dataset = " @@ -28,12 +29,12 @@ let dataset = " descend($X, $Y) :- child($X, $Y). descend($X, $Z) :- child($X, $Y), descend($Y, $Z). "; -db.insert_dataset(parse_str(dataset, db.interner()).unwrap()); +db.insert_dataset(parse_str(dataset, &interner).unwrap()); db.commit(); // Queries the DB. let query = "descend($X, $Y)."; -let mut cx = db.query(parse_str(query, db.interner()).unwrap()); +let mut cx = db.query(parse_str(query, &interner).unwrap()); let mut answer = Vec::new(); while let Some(eval) = cx.prove_next() { @@ -46,8 +47,4 @@ assert_eq!(answer, [ "$X = b, $Y = c", "$X = a, $Y = c", ]); - -// If the database was created with default interner, it should be deallocated. -drop(cx); -db.dealloc(); ``` diff --git a/crates/logic-eval/src/lib.rs b/crates/logic-eval/src/lib.rs index 644e31b..42bdeb3 100644 --- a/crates/logic-eval/src/lib.rs +++ b/crates/logic-eval/src/lib.rs @@ -6,12 +6,14 @@ mod prove; // === Re-exports === pub use parse::{ + common::{Intern, InternedStr, StrCanonicalizer, StrInterner}, inner::VAR_PREFIX, inner::{parse_str, Parse}, repr::{Clause, ClauseDataset, Expr, Predicate, Term}, text::Name, }; pub use prove::{ + common::Atom, db::{ClauseIter, ClauseRef, Database}, prover::ProveCx, }; @@ -20,19 +22,30 @@ pub mod intern { pub use any_intern::*; } +// === Re-exports for this crate === + +pub(crate) use intern_alias::*; +#[allow(unused)] +mod intern_alias { + use crate::{parse, prove, Intern}; + pub(crate) type NameIn<'int, Int> = parse::text::Name<::Interned<'int>>; + pub(crate) type TermIn<'int, Int> = parse::repr::Term>; + pub(crate) type ExprIn<'int, Int> = parse::repr::Expr>; + pub(crate) type ClauseIn<'int, Int> = parse::repr::Clause>; + pub(crate) type UniqueTermArrayIn<'int, Int> = prove::repr::UniqueTermArray>; + pub(crate) type TermStorageIn<'int, Int> = prove::repr::TermStorage>; + pub(crate) type ClauseDatasetIn<'int, Int> = parse::repr::ClauseDataset>; +} + +// === Hash map and set used within this crate === + use std::{ - borrow::Borrow, - collections::{HashMap, HashSet}, error::Error as StdError, - fmt::{self, Debug, Display}, - hash::{BuildHasherDefault, Hash, Hasher}, + hash::{BuildHasherDefault, Hasher}, result::Result as StdResult, - sync::{Arc, Mutex}, }; -// === Hash map and set used within this crate === - -pub(crate) type Map = HashMap; +pub(crate) type Map = fxhash::FxHashMap; #[derive(Default, Clone, Copy)] struct PassThroughHasher { @@ -59,112 +72,3 @@ pub(crate) type PassThroughState = BuildHasherDefault; pub(crate) type Result = StdResult; pub(crate) type Error = Box; - -// === Interning dependency === - -pub trait Intern { - type InternedStr<'a>: AsRef + Borrow + Clone + Eq + Ord + Hash + Debug + Display - where - Self: 'a; - - fn intern_formatted_str( - &self, - value: &T, - upper_size: usize, - ) -> StdResult, fmt::Error>; - - fn intern_str(&self, text: &str) -> Self::InternedStr<'_> { - self.intern_formatted_str(text, text.len()).unwrap() - } -} - -type DefaultInternerInner = HashSet, fxhash::FxBuildHasher>; -pub struct DefaultInterner(Mutex); - -impl Default for DefaultInterner { - fn default() -> Self { - let set = HashSet::default(); - Self(Mutex::new(set)) - } -} - -impl Intern for DefaultInterner { - type InternedStr<'a> - = Arc - where - Self: 'a; - - fn intern_formatted_str( - &self, - value: &T, - _: usize, - ) -> StdResult, fmt::Error> { - let mut set = self.0.lock().unwrap(); - - let value = value.to_string(); - if let Some(existing_value) = set.get(&*value) { - Ok(existing_value.clone()) - } else { - let value: Arc = value.into(); - set.insert(value.clone()); - Ok(value) - } - } -} - -impl Intern for any_intern::DroplessInterner { - type InternedStr<'a> - = any_intern::Interned<'a, str> - where - Self: 'a; - - fn intern_formatted_str( - &self, - value: &T, - upper_size: usize, - ) -> StdResult, fmt::Error> { - self.intern_formatted_str(value, upper_size) - } - - fn intern_str(&self, text: &str) -> Self::InternedStr<'_> { - self.intern(text) - } -} - -impl Intern for any_intern::Interner { - type InternedStr<'a> - = any_intern::Interned<'a, str> - where - Self: 'a; - - fn intern_formatted_str( - &self, - value: &T, - upper_size: usize, - ) -> StdResult, fmt::Error> { - self.intern_formatted_str(value, upper_size) - } - - fn intern_str(&self, text: &str) -> Self::InternedStr<'_> { - self.intern_dropless(text) - } -} - -// === Type aliases for complex `Intern` related types === - -pub(crate) use intern_alias::*; -#[allow(unused)] -mod intern_alias { - use super::{parse, prove, Intern}; - pub(crate) type NameIn<'int, Int> = parse::text::Name<::InternedStr<'int>>; - pub(crate) type TermIn<'int, Int> = parse::repr::Term>; - pub(crate) type ExprIn<'int, Int> = parse::repr::Expr>; - pub(crate) type ClauseIn<'int, Int> = parse::repr::Clause>; - pub(crate) type UniqueTermArrayIn<'int, Int> = prove::repr::UniqueTermArray>; - pub(crate) type TermStorageIn<'int, Int> = prove::repr::TermStorage>; - pub(crate) type ClauseDatasetIn<'int, Int> = parse::repr::ClauseDataset>; - pub(crate) type Name2Int<'int, Int> = - prove::prover::IdxMap<'int, NameIn<'int, Int>, prove::prover::Integer, Int>; - pub(crate) type Int2Name<'int, Int> = - prove::prover::IdxMap<'int, prove::prover::Integer, NameIn<'int, Int>, Int>; -} diff --git a/crates/logic-eval/src/parse/common.rs b/crates/logic-eval/src/parse/common.rs new file mode 100644 index 0000000..b45b867 --- /dev/null +++ b/crates/logic-eval/src/parse/common.rs @@ -0,0 +1,123 @@ +use crate::{Atom, Clause, Expr, Term}; +use core::fmt::{self, Display}; +use smallvec::SmallVec; + +pub trait Intern { + type Interned<'a>: Atom + where + Self: 'a; + + fn intern_str(&self, s: &str) -> Self::Interned<'_>; + + fn intern_formatted_str( + &self, + value: &T, + upper_size: usize, + ) -> Result, fmt::Error>; +} + +impl Intern for any_intern::DroplessInterner { + type Interned<'a> + = any_intern::Interned<'a, str> + where + Self: 'a; + + fn intern_str(&self, s: &str) -> Self::Interned<'_> { + self.intern(s) + } + + fn intern_formatted_str( + &self, + value: &T, + upper_size: usize, + ) -> Result, fmt::Error> { + ::intern_formatted_str(self, value, upper_size) + } +} + +impl Intern for any_intern::Interner { + type Interned<'a> + = any_intern::Interned<'a, str> + where + Self: 'a; + + fn intern_str(&self, s: &str) -> Self::Interned<'_> { + self.intern_dropless(s) + } + + fn intern_formatted_str( + &self, + value: &T, + upper_size: usize, + ) -> Result, fmt::Error> { + ::intern_formatted_str(self, value, upper_size) + } +} + +pub type StrInterner = any_intern::DroplessInterner; +pub type InternedStr<'int> = any_intern::Interned<'int, str>; + +pub struct StrCanonicalizer<'int> { + interner: &'int StrInterner, +} + +impl<'int> StrCanonicalizer<'int> { + pub fn new(interner: &'int StrInterner) -> Self { + Self { interner } + } + + pub fn canonicalize(&self, clause: Clause>) -> Clause> { + let mut vars = SmallVec::new(); + find_var_in_clause(&clause, &mut vars); + + let mut clause = clause; + clause.replace_term(&mut |term| { + if !term.args.is_empty() { + return None; + } + vars.iter().enumerate().find_map(|(i, var)| { + if &term.functor == var { + Some(Term { + functor: self.interner.intern_formatted_str(&i, i % 10 + 1).unwrap(), + args: Vec::new(), + }) + } else { + None + } + }) + }); + + return clause; + + // === Internal helper functions === + + fn find_var_in_clause(clause: &Clause, vars: &mut SmallVec<[T; 4]>) { + find_var_in_term(&clause.head, vars); + if let Some(body) = &clause.body { + find_var_in_expr(body, vars); + } + } + + fn find_var_in_expr(expr: &Expr, vars: &mut SmallVec<[T; 4]>) { + match expr { + Expr::Term(term) => find_var_in_term(term, vars), + Expr::Not(expr) => find_var_in_expr(expr, vars), + Expr::And(expr) | Expr::Or(expr) => { + for inner_expr in expr.iter() { + find_var_in_expr(inner_expr, vars); + } + } + } + } + + fn find_var_in_term(term: &Term, vars: &mut SmallVec<[T; 4]>) { + if term.functor.is_variable() { + vars.push(term.functor.clone()); + } else { + for arg in &term.args { + find_var_in_term(arg, vars); + } + } + } + } +} diff --git a/crates/logic-eval/src/parse/inner.rs b/crates/logic-eval/src/parse/inner.rs index 68047e7..1941097 100644 --- a/crates/logic-eval/src/parse/inner.rs +++ b/crates/logic-eval/src/parse/inner.rs @@ -192,3 +192,29 @@ pub(crate) struct Location { /// Exclusive right: usize, } + +#[cfg(test)] +mod tests { + use super::*; + use crate::parse::repr::Clause; + + type Interner = any_intern::DroplessInterner; + + #[test] + fn test_parse() { + fn assert(text: &str, interner: &Interner) { + let clause: Clause<_> = parse_str(text, interner).unwrap(); + assert_eq!(text, clause.to_string()); + } + + let interner = Interner::new(); + + assert("f.", &interner); + assert("f(a, b).", &interner); + assert("f(a, b) :- f.", &interner); + assert("f(a, b) :- f(a).", &interner); + assert("f(a, b) :- f(a), f(b).", &interner); + assert("f(a, b) :- f(a); f(b).", &interner); + assert("f(a, b) :- f(a), (f(b); f(c)).", &interner); + } +} diff --git a/crates/logic-eval/src/parse/mod.rs b/crates/logic-eval/src/parse/mod.rs index b191ad7..6fe869d 100644 --- a/crates/logic-eval/src/parse/mod.rs +++ b/crates/logic-eval/src/parse/mod.rs @@ -1,5 +1,5 @@ +pub(crate) mod common; pub(crate) mod inner; pub(crate) mod repr; pub(crate) mod text; - pub(crate) use inner::*; diff --git a/crates/logic-eval/src/parse/repr.rs b/crates/logic-eval/src/parse/repr.rs index e19e195..eb7ac85 100644 --- a/crates/logic-eval/src/parse/repr.rs +++ b/crates/logic-eval/src/parse/repr.rs @@ -1,11 +1,12 @@ use super::text::Name; +use crate::Atom; use std::{ fmt::{self, Debug, Display, Write}, ops, vec::IntoIter, }; -#[derive(Clone)] +#[derive(Clone, Debug, Hash)] pub struct ClauseDataset(pub Vec>); impl IntoIterator for ClauseDataset { @@ -25,21 +26,32 @@ impl ops::Deref for ClauseDataset { } } -#[derive(Clone, PartialEq, Eq)] +#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)] pub struct Clause { pub head: Term, pub body: Option>, } impl Clause { - pub(crate) fn map U>(self, f: &mut F) -> Clause { + pub fn fact(head: Term) -> Self { + Self { head, body: None } + } + + pub fn rule(head: Term, body: Expr) -> Self { + Self { + head, + body: Some(body), + } + } + + pub fn map U>(self, f: &mut F) -> Clause { Clause { head: self.head.map(f), body: self.body.map(|expr| expr.map(f)), } } - pub(crate) fn replace_term(&mut self, f: &mut F) + pub fn replace_term(&mut self, f: &mut F) where F: FnMut(&Term) -> Option>, { @@ -50,7 +62,7 @@ impl Clause { } } -impl> Display for Clause { +impl Display for Clause { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { self.head.fmt(f)?; if let Some(body) = &self.body { @@ -61,14 +73,28 @@ impl> Display for Clause { } } -#[derive(Default, Clone, PartialEq, Eq)] +#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)] pub struct Term { pub functor: T, pub args: Vec>, } impl Term { - pub(crate) fn map U>(self, f: &mut F) -> Term { + pub fn atom(functor: T) -> Self { + Term { + functor, + args: vec![], + } + } + + pub fn compound>>(functor: T, args: I) -> Self { + Term { + functor, + args: args.into_iter().collect(), + } + } + + pub fn map U>(self, f: &mut F) -> Term { Term { functor: f(self.functor), args: self.args.into_iter().map(|arg| arg.map(f)).collect(), @@ -101,7 +127,7 @@ impl Term { } } -impl> Term> { +impl Term> { pub fn is_variable(&self) -> bool { let is_variable = self.functor.is_variable(); @@ -122,10 +148,9 @@ impl> Term> { } } -impl> Display for Term { +impl Display for Term { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - let functor: &str = self.functor.as_ref(); - f.write_str(functor)?; + fmt::Display::fmt(&self.functor, f)?; if !self.args.is_empty() { f.write_char('(')?; for (i, arg) in self.args.iter().enumerate() { @@ -140,22 +165,7 @@ impl> Display for Term { } } -impl> Debug for Term> { - fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - let functor: &str = self.functor.as_ref(); - if self.args.is_empty() { - f.write_str(functor) - } else { - let mut d = f.debug_tuple(functor); - for arg in &self.args { - d.field(&arg); - } - d.finish() - } - } -} - -#[derive(Clone, PartialEq, Eq)] +#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)] pub enum Expr { Term(Term), Not(Box>), @@ -164,7 +174,31 @@ pub enum Expr { } impl Expr { - pub(crate) fn map U>(self, f: &mut F) -> Expr { + pub fn term(term: Term) -> Self { + Self::Term(term) + } + + pub fn term_atom(functor: T) -> Self { + Self::Term(Term::atom(functor)) + } + + pub fn term_compound>>(functor: T, args: I) -> Self { + Self::Term(Term::compound(functor, args)) + } + + pub fn expr_not(expr: Expr) -> Self { + Self::Not(Box::new(expr)) + } + + pub fn expr_and>>(elems: I) -> Self { + Self::And(elems.into_iter().collect()) + } + + pub fn expr_or>>(elems: I) -> Self { + Self::Or(elems.into_iter().collect()) + } + + pub fn map U>(self, f: &mut F) -> Expr { match self { Self::Term(v) => Expr::Term(v.map(f)), Self::Not(v) => Expr::Not(Box::new(v.map(f))), @@ -173,7 +207,7 @@ impl Expr { } } - pub(crate) fn replace_term(&mut self, f: &mut F) + pub fn replace_term(&mut self, f: &mut F) where F: FnMut(&Term) -> Option>, { @@ -191,7 +225,7 @@ impl Expr { } } -impl> Display for Expr { +impl Display for Expr { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Self::Term(term) => term.fmt(f)?, @@ -232,29 +266,6 @@ impl> Display for Expr { } } -impl> Debug for Expr> { - fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - match self { - Self::Term(term) => fmt::Debug::fmt(term, f), - Self::Not(inner) => f.debug_tuple("Not").field(inner).finish(), - Self::And(args) => { - let mut d = f.debug_tuple("And"); - for arg in args { - d.field(arg); - } - d.finish() - } - Self::Or(args) => { - let mut d = f.debug_tuple("Or"); - for arg in args { - d.field(arg); - } - d.finish() - } - } - } -} - #[derive(Debug, PartialEq, Eq, Hash)] pub struct Predicate { pub functor: T, diff --git a/crates/logic-eval/src/parse/text.rs b/crates/logic-eval/src/parse/text.rs index b86ccec..a81c78f 100644 --- a/crates/logic-eval/src/parse/text.rs +++ b/crates/logic-eval/src/parse/text.rs @@ -1,9 +1,9 @@ use super::{ - repr::{Clause, Expr, Term}, + repr::{Clause, ClauseDataset, Expr, Term}, CloseParenToken, CommaToken, DotToken, HornToken, Ident, NegationToken, OpenParenToken, Parse, - ParseBuffer, VAR_PREFIX, + ParseBuffer, }; -use crate::{ClauseDatasetIn, ClauseIn, Error, ExprIn, Intern, NameIn, Result, TermIn}; +use crate::{Atom, ClauseDatasetIn, ClauseIn, Error, ExprIn, Intern, NameIn, Result, TermIn}; use std::{ borrow::Borrow, fmt::{self, Debug, Display}, @@ -12,26 +12,25 @@ use std::{ }; impl<'int, Int: Intern> Parse<'int, Int> for ClauseDatasetIn<'int, Int> { - fn parse(buf: &mut ParseBuffer<'_>, interner: &'int Int) -> Result { - let clauses = buf.parse(interner)?; - Ok(Self(clauses)) - } -} - -impl<'int, Int: Intern> Parse<'int, Int> for Vec> { fn parse(buf: &mut ParseBuffer<'_>, interner: &'int Int) -> Result { let mut v = Vec::new(); - while let Some((clause, moved_buf)) = buf.peek_parse::>>(interner) { + while let Some(moved_buf) = { + let mut peek = *buf; + ClauseIn::<'int, Int>::parse(&mut peek, interner) + .ok() + .map(|c| (c, peek)) + } { + let (clause, moved) = moved_buf; v.push(clause); - *buf = moved_buf; + *buf = moved; } - Ok(v) + Ok(ClauseDataset(v)) } } impl<'int, Int: Intern> Parse<'int, Int> for ClauseIn<'int, Int> { fn parse(buf: &mut ParseBuffer<'_>, interner: &'int Int) -> Result { - let head = buf.parse::>>(interner)?; + let head = TermIn::<'int, Int>::parse(buf, interner)?; let body = if let Some((_, mut body_buf)) = buf.peek_parse::(interner) { let dot = body_buf @@ -39,7 +38,7 @@ impl<'int, Int: Intern> Parse<'int, Int> for ClauseIn<'int, Int> { .find('.') .ok_or(Error::from("clause must end with `.`"))?; body_buf.end = body_buf.start + dot; - let body = body_buf.parse::>>(interner)?; + let body = ExprIn::<'int, Int>::parse(&mut body_buf, interner)?; buf.start = body_buf.end + 1; // Next to the dot Some(body) @@ -48,11 +47,29 @@ impl<'int, Int: Intern> Parse<'int, Int> for ClauseIn<'int, Int> { None }; - Ok(Self { head, body }) + Ok(Clause { head, body }) + } +} + +impl<'int, Int: Intern> Parse<'int, Int> for ExprIn<'int, Int> { + /// Caller is supposed to give the exact buffer for an Expr. + fn parse(buf: &mut ParseBuffer<'_>, interner: &'int Int) -> Result { + Expr::>::parse_or(*buf, interner) + } +} + +impl<'int, Int: Intern> Parse<'int, Int> for TermIn<'int, Int> { + fn parse(buf: &mut ParseBuffer<'_>, interner: &'int Int) -> Result { + let functor = Name::parse(buf, interner)?; + let args = Term::parse_args(buf, interner)?; + Ok(Term { functor, args }) } } -// Precedence: `Paren ()` -> `Not \+` -> `And ,` -> `Or ;` +// Precedence: `Paren ()` -> `Not \+` -> `And ,` -> `Or ;`. +// - So, `parse_or` is the entry point to parse an Expr. +// - Plus, caller is supposed to give the exact buffer for an Expr. This can be done by detecting +// end of clause or something like that. That's why methods here don't take `&mut ParseBuffer`. impl Expr> { fn parse_or<'int, Int: Intern>( buf: ParseBuffer<'_>, @@ -87,7 +104,7 @@ impl Expr> { if let Some((_, mut moved_buf)) = buf.peek_parse::(interner) { let r = moved_buf.cur_text().rfind(')').unwrap(); moved_buf.end = moved_buf.start + r; - moved_buf.parse::>>(interner) + ExprIn::<'int, Int>::parse(&mut moved_buf, interner) } else { Self::parse_term(buf, interner) } @@ -100,7 +117,7 @@ impl Expr> { if buf.cur_text().chars().all(|c: char| c.is_whitespace()) { Err("expected a non-empty term expression".into()) } else { - buf.parse::>>(interner).map(Expr::Term) + TermIn::<'int, Int>::parse(&mut buf, interner).map(Expr::Term) } } @@ -149,13 +166,6 @@ impl Expr> { } } -impl<'int, Int: Intern> Parse<'int, Int> for ExprIn<'int, Int> { - fn parse(buf: &mut ParseBuffer<'_>, interner: &'int Int) -> Result { - // The buffer range is not being moved by this call. - Expr::parse_or(*buf, interner) - } -} - impl Term> { fn parse_args<'int, Int: Intern>( buf: &mut ParseBuffer<'_>, @@ -184,7 +194,7 @@ impl Term> { return Err(format!("expected `,` from {}", buf.cur_text()).into()); } - let arg = buf.parse::>>(interner)?; + let arg = TermIn::<'int, Int>::parse(buf, interner)?; args.push(arg); let comma = buf.parse::(interner); @@ -199,30 +209,28 @@ impl Term> { } } -impl<'int, Int: Intern> Parse<'int, Int> for TermIn<'int, Int> { - fn parse(buf: &mut ParseBuffer<'_>, interner: &'int Int) -> Result { - let functor = Name::parse(buf, interner)?; - let args = Term::parse_args(buf, interner)?; - Ok(Self { functor, args }) +/// Non-empty string. +#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub struct Name(T); + +impl> Name { + pub fn new(s: T) -> Self { + assert!(!s.as_ref().is_empty()); + Self(s) } } -#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] -pub struct Name(pub T); // Non-empty string - impl Name<()> { pub fn with_intern<'int, Int: Intern>(s: &str, interner: &'int Int) -> NameIn<'int, Int> { - debug_assert!(!s.is_empty()); - + assert!(!s.is_empty()); let interned = interner.intern_str(s); Name(interned) } } -impl> Name { +impl Name { pub(crate) fn is_variable(&self) -> bool { - let first = self.0.as_ref().chars().next().unwrap(); - first == VAR_PREFIX // btw, prolog style is `is_uppercase() or '_'` + self.0.is_variable() } } @@ -230,7 +238,6 @@ impl<'int, Int: Intern> Parse<'int, Int> for NameIn<'int, Int> { fn parse(buf: &mut ParseBuffer<'_>, interner: &'int Int) -> Result { let ident = buf.parse::(interner)?; let interned = interner.intern_str(ident.to_text(buf.text)); - debug_assert!(!interned.as_ref().is_empty()); Ok(Self(interned)) } } diff --git a/crates/logic-eval/src/prove/common.rs b/crates/logic-eval/src/prove/common.rs new file mode 100644 index 0000000..5f21d42 --- /dev/null +++ b/crates/logic-eval/src/prove/common.rs @@ -0,0 +1,18 @@ +use crate::{Name, VAR_PREFIX}; +use core::hash::Hash; + +pub trait Atom: Clone + Eq + Hash { + fn is_variable(&self) -> bool; +} + +impl<'int> Atom for any_intern::Interned<'int, str> { + fn is_variable(&self) -> bool { + self.starts_with(VAR_PREFIX) + } +} + +impl<'int> Atom for Name> { + fn is_variable(&self) -> bool { + self.starts_with(VAR_PREFIX) + } +} diff --git a/crates/logic-eval/src/prove/db.rs b/crates/logic-eval/src/prove/db.rs index cf9a9f2..67f22f6 100644 --- a/crates/logic-eval/src/prove/db.rs +++ b/crates/logic-eval/src/prove/db.rs @@ -7,27 +7,24 @@ use super::{ }; use crate::{ parse::{ - repr::{Clause, Expr, Predicate, Term}, - text::Name, + repr::{Clause, ClauseDataset, Expr, Predicate, Term}, VAR_PREFIX, }, prove::repr::{ExprKind, ExprView, TermView, TermViewIter}, - ClauseDatasetIn, ClauseIn, DefaultInterner, ExprIn, Int2Name, Intern, Map, + Atom, Map, }; -use indexmap::{IndexMap, IndexSet}; -use logic_eval_util::reference::Ref; -use std::{ - fmt::{self, Write}, - iter, +use core::{ + fmt::{self, Debug, Display, Write}, + iter::FusedIterator, }; +use indexmap::{IndexMap, IndexSet}; -#[derive(Debug)] -pub struct Database<'int, Int: Intern = DefaultInterner> { +pub struct Database { /// Clause id dataset. clauses: IndexMap, Vec>, /// We do not allow duplicated clauses in the dataset. - clause_texts: IndexSet, + clause_set: IndexSet>, /// Term and expression storage. stor: TermStorage, @@ -35,87 +32,38 @@ pub struct Database<'int, Int: Intern = DefaultInterner> { /// Proof search engine. prover: Prover, - /// Mappings between [`Name`] and [`Int`]. + /// Mappings between T and Integer. /// - /// [`Int`] is internally used for fast comparison, but we need to get it - /// back to [`Name`] for the clients. - nimap: NameIntMap<'int, Int>, + /// Integer is internally used for fast comparison, but we need to get it back to T for the + /// clients. + nimap: NameIntMap, /// States of DB's fields. /// /// This is used when we discard some changes on the DB. revert_point: Option, - - interner: Ref<'int, Int>, } -impl Database<'static> { - /// Creates a database with default string interner. - /// - /// Because creating database through this method makes a leaked memory, you should not forget - /// to call [`dealloc`](Self::dealloc). - #[allow(clippy::new_without_default)] +impl Database { pub fn new() -> Self { - let leaked = Box::leak(Box::new(DefaultInterner::default())); - let interner = Ref::from_mut(leaked); - - Self { - clauses: IndexMap::default(), - clause_texts: IndexSet::default(), - stor: TermStorage::new(), - prover: Prover::new(), - nimap: NameIntMap::new(interner), - revert_point: None, - interner, - } - } - - #[rustfmt::skip] - pub fn dealloc(self) { - // Prevents us from accidently implementing Clone for the type. Deallocation relies on the - // fact that the type cannot be cloned, so that we have only one instance. - #[allow(dead_code)] - { - struct ImplDetector(std::marker::PhantomData); - trait NotClone { const IS_CLONE: bool = false; } - impl NotClone for ImplDetector {} - impl ImplDetector { const IS_CLONE: bool = true; } - const _: () = assert!(!ImplDetector::>::IS_CLONE); - } - - // Safety: - // * There's only one instance and we got the ownership of the instance. - let _ = unsafe { Box::from_raw(self.interner.as_ptr()) }; - } -} - -impl<'int, Int: Intern> Database<'int, Int> { - pub fn with_interner(interner: &'int Int) -> Self { - let interner = Ref::from_ref(interner); - Self { clauses: IndexMap::default(), - clause_texts: IndexSet::default(), + clause_set: IndexSet::default(), stor: TermStorage::new(), prover: Prover::new(), - nimap: NameIntMap::new(interner), + nimap: NameIntMap::new(), revert_point: None, - interner, } } - pub fn interner(&self) -> &'int Int { - self.interner.as_ref() - } - - pub fn terms(&self) -> NamedTermViewIter<'_, 'int, Int> { + pub fn terms(&self) -> NamedTermViewIter<'_, T> { NamedTermViewIter { term_iter: self.stor.terms.terms(), int2name: &self.nimap.int2name, } } - pub fn clauses(&self) -> ClauseIter<'_, 'int, Int> { + pub fn clauses(&self) -> ClauseIter<'_, T> { ClauseIter { clauses: &self.clauses, stor: &self.stor, @@ -125,32 +73,24 @@ impl<'int, Int: Intern> Database<'int, Int> { } } - pub fn insert_dataset(&mut self, dataset: ClauseDatasetIn<'int, Int>) { + pub fn insert_dataset(&mut self, dataset: ClauseDataset) { for clause in dataset { self.insert_clause(clause); } } - pub fn insert_clause(&mut self, clause: ClauseIn<'int, Int>) { - // Saves current state. We will revert DB when the change is not - // committed. + pub fn insert_clause(&mut self, clause: Clause) { + // Saves current state. We will revert DB when the change is not committed. if self.revert_point.is_none() { self.revert_point = Some(self.state()); } - // If this DB contains the given clause, then returns. - let serialized = if let Some(converted) = - Clause::convert_var_into_num(&clause, self.interner.as_ref()) - { - converted.to_string() - } else { - clause.to_string() - }; - if !self.clause_texts.insert(serialized) { + // If the DB already contains the given clause, then returns. + if !self.clause_set.insert(clause.clone()) { return; } - let clause = clause.map(&mut |name| self.nimap.name_to_int(name)); + let clause = clause.map(&mut |t| self.nimap.name_to_int(t)); let key = clause.head.predicate(); let value = ClauseId { @@ -168,8 +108,8 @@ impl<'int, Int: Intern> Database<'int, Int> { .or_insert(vec![value]); } - pub fn query(&mut self, expr: ExprIn<'int, Int>) -> ProveCx<'_, 'int, Int> { - // Discards uncomitted changes. + pub fn query(&mut self, expr: Expr) -> ProveCx<'_, T> { + // Discards uncommitted changes. if let Some(revert_point) = self.revert_point.take() { self.revert(revert_point); } @@ -183,7 +123,13 @@ impl<'int, Int: Intern> Database<'int, Int> { } /// * sanitize - Removes unacceptable characters from prolog. - pub fn to_prolog &str>(&self, sanitize: F) -> String { + /// + /// Requires T to implement [`AsRef`] so that functor names can be serialized into Prolog + /// syntax. + pub fn to_prolog &str>(&self, sanitize: F) -> String + where + T: AsRef, + { let mut prolog_text = String::new(); let mut conv_map = ConversionMap { @@ -213,17 +159,17 @@ impl<'int, Int: Intern> Database<'int, Int> { // === Internal helper functions === - struct ConversionMap<'a, 'int, Int: Intern, F> { + struct ConversionMap<'a, T, F> { int_to_str: Map, // e.g. 0 -> No suffix, 1 -> _1, 2 -> _2, ... sanitized_to_suffix: Map<&'a str, u32>, - int2name: &'a Int2Name<'int, Int>, + int2name: &'a IndexMap, sanitizer: F, } - impl ConversionMap<'_, '_, Int, F> + impl ConversionMap<'_, T, F> where - Int: Intern, + T: AsRef, F: FnMut(&str) -> &str, { fn int_to_str(&mut self, int: Integer) -> &str { @@ -275,12 +221,12 @@ impl<'int, Int: Intern> Database<'int, Int> { } } - fn write_term( + fn write_term( term: TermView<'_, Integer>, - conv_map: &mut ConversionMap<'_, '_, Int, F>, + conv_map: &mut ConversionMap<'_, T, F>, prolog_text: &mut String, ) where - Int: Intern, + T: AsRef, F: FnMut(&str) -> &str, { let functor = term.functor(); @@ -302,12 +248,12 @@ impl<'int, Int: Intern> Database<'int, Int> { } } - fn write_expr( + fn write_expr( expr: ExprView<'_, Integer>, - conv_map: &mut ConversionMap<'_, '_, Int, F>, + conv_map: &mut ConversionMap<'_, T, F>, prolog_text: &mut String, ) where - Int: Intern, + T: AsRef, F: FnMut(&str) -> &str, { match expr.as_kind() { @@ -356,7 +302,7 @@ impl<'int, Int: Intern> Database<'int, Int> { &mut self, DatabaseState { clauses_len, - clause_texts_len, + clause_set_len, stor_len, nimap_state, }: DatabaseState, @@ -365,7 +311,7 @@ impl<'int, Int: Intern> Database<'int, Int> { for (i, len) in clauses_len.into_iter().enumerate() { self.clauses[i].truncate(len); } - self.clause_texts.truncate(clause_texts_len); + self.clause_set.truncate(clause_set_len); self.stor.truncate(stor_len); self.nimap.revert(nimap_state); // `self.prover: Prover` does not store any persistent data. @@ -374,32 +320,109 @@ impl<'int, Int: Intern> Database<'int, Int> { fn state(&self) -> DatabaseState { DatabaseState { clauses_len: self.clauses.values().map(|v| v.len()).collect(), - clause_texts_len: self.clause_texts.len(), + clause_set_len: self.clause_set.len(), stor_len: self.stor.len(), nimap_state: self.nimap.state(), } } } +impl Default for Database { + fn default() -> Self { + Self::new() + } +} + +impl Debug for Database { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + f.debug_struct("Database") + .field("clauses", &self.clauses) + .field("clause_set", &self.clause_set) + .field("stor", &self.stor) + .field("nimap", &self.nimap) + .field("revert_point", &self.revert_point) + .finish_non_exhaustive() + } +} + #[derive(Debug, PartialEq, Eq)] struct DatabaseState { clauses_len: Vec, - clause_texts_len: usize, + clause_set_len: usize, stor_len: TermStorageLen, nimap_state: NameIntMapState, } +/// Turns variables into `_$0`, `_$1`, and so on using the given canonical_var function. +/// +/// Returns `None` if `canonical_var` is `None` (i.e. deduplication disabled). +fn _convert_var_into_num( + this: &Clause, + canonical_var: Option<&dyn Fn(usize) -> T>, +) -> Option> { + let canonical_var = canonical_var?; + let mut cloned: Option> = None; + + let mut i = 0; + + while let Some(from) = find_var_in_clause(cloned.as_ref().unwrap_or(this)) { + let from = from.clone(); + let canonical_t = canonical_var(i); + + let mut convert = |term: &Term| { + (term.functor == from && term.args.is_empty()).then_some(Term { + functor: canonical_t.clone(), + args: vec![], + }) + }; + + if let Some(cloned) = &mut cloned { + cloned.replace_term(&mut convert); + } else { + let mut this = this.clone(); + this.replace_term(&mut convert); + cloned = Some(this); + } + + i += 1; + } + + return cloned; + + // === Internal helper functions === + + fn find_var_in_clause(clause: &Clause) -> Option { + find_var_in_term(&clause.head).or_else(|| clause.body.as_ref().and_then(find_var_in_expr)) + } + + fn find_var_in_expr(expr: &Expr) -> Option { + match expr { + Expr::Term(t) => find_var_in_term(t), + Expr::Not(e) => find_var_in_expr(e), + Expr::And(v) | Expr::Or(v) => v.iter().find_map(find_var_in_expr), + } + } + + fn find_var_in_term(term: &Term) -> Option { + if term.functor.is_variable() { + Some(term.functor.clone()) + } else { + term.args.iter().find_map(find_var_in_term) + } + } +} + #[derive(Clone)] -pub struct ClauseIter<'a, 'int, Int: Intern> { +pub struct ClauseIter<'a, T> { clauses: &'a IndexMap, Vec>, stor: &'a TermStorage, - int2name: &'a Int2Name<'int, Int>, + int2name: &'a IndexMap, i: usize, j: usize, } -impl<'a, 'int, Int: Intern> Iterator for ClauseIter<'a, 'int, Int> { - type Item = ClauseRef<'a, 'int, Int>; +impl<'a, T> Iterator for ClauseIter<'a, T> { + type Item = ClauseRef<'a, T>; fn next(&mut self) -> Option { let id = loop { @@ -422,21 +445,21 @@ impl<'a, 'int, Int: Intern> Iterator for ClauseIter<'a, 'int, Int> { } } -impl iter::FusedIterator for ClauseIter<'_, '_, Int> {} +impl FusedIterator for ClauseIter<'_, T> {} -pub struct ClauseRef<'a, 'int, Int: Intern> { +pub struct ClauseRef<'a, T> { id: ClauseId, stor: &'a TermStorage, - int2name: &'a Int2Name<'int, Int>, + int2name: &'a IndexMap, } -impl<'a, 'int, Int: Intern> ClauseRef<'a, 'int, Int> { - pub fn head(&self) -> NamedTermView<'a, 'int, Int> { +impl<'a, T: Atom> ClauseRef<'a, T> { + pub fn head(&self) -> NamedTermView<'a, T> { let head = self.stor.get_term(self.id.head); NamedTermView::new(head, self.int2name) } - pub fn body(&self) -> Option> { + pub fn body(&self) -> Option> { self.id.body.map(|id| { let body = self.stor.get_expr(id); NamedExprView::new(body, self.int2name) @@ -444,20 +467,20 @@ impl<'a, 'int, Int: Intern> ClauseRef<'a, 'int, Int> { } } -impl fmt::Display for ClauseRef<'_, '_, Int> { +impl Display for ClauseRef<'_, T> { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - fmt::Display::fmt(&self.head(), f)?; + Display::fmt(&self.head(), f)?; if let Some(body) = self.body() { f.write_str(" :- ")?; - fmt::Display::fmt(&body, f)? + Display::fmt(&body, f)? } f.write_char('.') } } -impl fmt::Debug for ClauseRef<'_, '_, Int> { +impl Debug for ClauseRef<'_, T> { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { let mut d = f.debug_struct("Clause"); @@ -473,76 +496,13 @@ impl fmt::Debug for ClauseRef<'_, '_, Int> { } } -impl Clause> { - /// Turns variables into `_$0`, `_$1`, and so on. - pub(crate) fn convert_var_into_num<'int, Int: Intern>( - this: &ClauseIn<'int, Int>, - interner: &'int Int, - ) -> Option> { - let mut cloned: Option> = None; - - let mut i = 0; - - while let Some(var) = find_var_in_clause(cloned.as_ref().unwrap_or(this)) { - let from = var.clone(); - - let mut convert = |term: &Term>| { - (term == &from).then_some(Term { - functor: Name::with_intern(&format!("_{VAR_PREFIX}{i}"), interner), - args: [].into(), - }) - }; - - if let Some(cloned) = &mut cloned { - cloned.replace_term(&mut convert); - } else { - let mut this = this.clone(); - this.replace_term(&mut convert); - cloned = Some(this); - } - - i += 1; - } - - return cloned; - - // === Internal helper functions === - - fn find_var_in_clause>(clause: &Clause>) -> Option<&Term>> { - let var = find_var_in_term(&clause.head); - if var.is_some() { - return var; - } - find_var_in_expr(clause.body.as_ref()?) - } - - fn find_var_in_expr>(expr: &Expr>) -> Option<&Term>> { - match expr { - Expr::Term(term) => find_var_in_term(term), - Expr::Not(inner) => find_var_in_expr(inner), - Expr::And(args) | Expr::Or(args) => args.iter().find_map(find_var_in_expr), - } - } - - fn find_var_in_term>(term: &Term>) -> Option<&Term>> { - const _: () = assert!(VAR_PREFIX == '$'); - - if term.is_variable() && !term.functor.as_ref().starts_with("_$") { - Some(term) - } else { - term.args.iter().find_map(find_var_in_term) - } - } - } -} - -pub struct NamedTermViewIter<'a, 'int, Int: Intern> { +pub struct NamedTermViewIter<'a, T> { term_iter: TermViewIter<'a, Integer>, - int2name: &'a Int2Name<'int, Int>, + int2name: &'a IndexMap, } -impl<'a, 'int, Int: Intern> Iterator for NamedTermViewIter<'a, 'int, Int> { - type Item = NamedTermView<'a, 'int, Int>; +impl<'a, T: Atom> Iterator for NamedTermViewIter<'a, T> { + type Item = NamedTermView<'a, T>; fn next(&mut self) -> Option { self.term_iter @@ -551,110 +511,81 @@ impl<'a, 'int, Int: Intern> Iterator for NamedTermViewIter<'a, 'int, Int> { } } -impl iter::FusedIterator for NamedTermViewIter<'_, '_, Int> {} +impl FusedIterator for NamedTermViewIter<'_, T> {} #[cfg(test)] -mod tests { - use super::*; - use crate::parse::{ - self, - repr::{Clause, ClauseDataset, Expr}, - }; - use any_intern::DroplessInterner; +mod str_atom_tests { + use crate::{parse, NameIn}; + + type Interner = any_intern::DroplessInterner; + type Database<'int> = crate::Database>; + type ProveCx<'a, 'int> = crate::ProveCx<'a, NameIn<'int, Interner>>; + type ClauseDataset<'int> = crate::ClauseDatasetIn<'int, Interner>; + type Expr<'int> = crate::ExprIn<'int, Interner>; + type Clause<'int> = crate::ClauseIn<'int, Interner>; #[test] - fn test_parse() { - fn assert(text: &str, interner: &impl Intern) { - let clause: Clause> = parse::parse_str(text, interner).unwrap(); - assert_eq!(text, clause.to_string()); - } + fn test_serial_queries() { + fn assert_query<'int>(db: &mut Database<'int>, interner: &'int Interner) { + let query = "g($X)."; + let query: Expr<'int> = parse::parse_str(query, interner).unwrap(); - let interner = DroplessInterner::default(); + let cx = db.query(query); + let answer = collect_answer(cx); + let expected = [["$X = a"], ["$X = b"]]; + assert_eq!(answer, expected); + } - assert("f.", &interner); - assert("f(a, b).", &interner); - assert("f(a, b) :- f.", &interner); - assert("f(a, b) :- f(a).", &interner); - assert("f(a, b) :- f(a), f(b).", &interner); - assert("f(a, b) :- f(a); f(b).", &interner); - assert("f(a, b) :- f(a), (f(b); f(c)).", &interner); - } + let mut db = Database::new(); + let interner = Interner::new(); - #[test] - fn test_serial_queries() { - fn insert(db: &mut Database<'_, Int>) { + for _ in 0..2 { insert_dataset( - db, + &mut db, + &interner, r" f(a). f(b). g($X) :- f($X). ", ); + let len = db.stor.len(); + assert_query(&mut db, &interner); + assert_eq!(db.stor.len(), len); } - - fn query(db: &mut Database<'_, Int>) { - let query = "g($X)."; - let query: Expr> = parse::parse_str(query, db.interner()).unwrap(); - let answer = collect_answer(db.query(query)); - - let expected = [["$X = a"], ["$X = b"]]; - - assert_eq!(answer, expected); - } - - let mut db = Database::new(); - - insert(&mut db); - let org_stor_len = db.stor.len(); - query(&mut db); - debug_assert_eq!(org_stor_len, db.stor.len()); - - insert(&mut db); - debug_assert_eq!(org_stor_len, db.stor.len()); - query(&mut db); - debug_assert_eq!(org_stor_len, db.stor.len()); - - db.dealloc(); } #[test] - fn test_various_expressions() { - test_not_expression(); - test_and_expression(); - test_or_expression(); - test_mixed_expression(); - } - fn test_not_expression() { let mut db = Database::new(); + let interner = Interner::new(); insert_dataset( &mut db, + &interner, r" g(a). f($X) :- \+ g($X). ", ); - let query = "f(a)."; - let query: Expr> = parse::parse_str(query, db.interner()).unwrap(); + let query: Expr<'_> = parse::parse_str("f(a).", &interner).unwrap(); let answer = collect_answer(db.query(query)); assert!(answer.is_empty()); - let query = "f(b)."; - let query: Expr> = parse::parse_str(query, db.interner()).unwrap(); + let query: Expr<'_> = parse::parse_str("f(b).", &interner).unwrap(); let answer = collect_answer(db.query(query)); assert_eq!(answer.len(), 1); - - db.dealloc(); } + #[test] fn test_and_expression() { let mut db = Database::new(); + let interner = Interner::new(); insert_dataset( &mut db, + &interner, r" g(a). g(b). @@ -663,21 +594,20 @@ mod tests { ", ); - let query = "f($X)."; - let query: Expr> = parse::parse_str(query, db.interner()).unwrap(); + let query: Expr<'_> = parse::parse_str("f($X).", &interner).unwrap(); let answer = collect_answer(db.query(query)); - let expected = [["$X = b"]]; assert_eq!(answer, expected); - - db.dealloc(); } + #[test] fn test_or_expression() { let mut db = Database::new(); + let interner = Interner::new(); insert_dataset( &mut db, + &interner, r" g(a). h(b). @@ -685,21 +615,20 @@ mod tests { ", ); - let query = "f($X)."; - let query: Expr> = parse::parse_str(query, db.interner()).unwrap(); + let query: Expr<'_> = parse::parse_str("f($X).", &interner).unwrap(); let answer = collect_answer(db.query(query)); - let expected = [["$X = a"], ["$X = b"]]; assert_eq!(answer, expected); - - db.dealloc(); } + #[test] fn test_mixed_expression() { let mut db = Database::new(); + let interner = Interner::new(); insert_dataset( &mut db, + &interner, r" g(b). g(c). @@ -714,27 +643,20 @@ mod tests { ", ); - let query = "f($X)."; - let query: Expr> = parse::parse_str(query, db.interner()).unwrap(); + let query: Expr<'_> = parse::parse_str("f($X).", &interner).unwrap(); let answer = collect_answer(db.query(query)); - let expected = [["$X = b"]]; assert_eq!(answer, expected); - - db.dealloc(); } #[test] - fn test_recursion() { - test_simple_recursion(); - test_right_recursion(); - } - fn test_simple_recursion() { let mut db = Database::new(); + let interner = Interner::new(); insert_dataset( &mut db, + &interner, r" impl(Clone, a). impl(Clone, b). @@ -743,8 +665,7 @@ mod tests { ", ); - let query = "impl(Clone, $T)."; - let query: Expr> = parse::parse_str(query, db.interner()).unwrap(); + let query: Expr<'_> = parse::parse_str("impl(Clone, $T).", &interner).unwrap(); let mut cx = db.query(query); let mut assert_next = |expected: &[&str]| { @@ -762,16 +683,16 @@ mod tests { assert_next(&["$T = Vec(Vec(a))"]); assert_next(&["$T = Vec(Vec(b))"]); assert_next(&["$T = Vec(Vec(c))"]); - - drop(cx); - db.dealloc(); } + #[test] fn test_right_recursion() { let mut db = Database::new(); + let interner = Interner::new(); insert_dataset( &mut db, + &interner, r" child(a, b). child(b, c). @@ -781,8 +702,7 @@ mod tests { ", ); - let query = "descend($X, $Y)."; - let query: Expr> = parse::parse_str(query, db.interner()).unwrap(); + let query: Expr<'_> = parse::parse_str("descend($X, $Y).", &interner).unwrap(); let mut answer = collect_answer(db.query(query)); let mut expected = [ @@ -797,43 +717,39 @@ mod tests { answer.sort_unstable(); expected.sort_unstable(); assert_eq!(answer, expected); - - db.dealloc(); } #[test] fn test_discarding_uncomitted_change() { let mut db = Database::new(); + let interner = Interner::new(); - let text = "f(a)."; - let clause = parse::parse_str(text, db.interner()).unwrap(); + let clause: Clause<'_> = parse::parse_str("f(a).", &interner).unwrap(); db.insert_clause(clause); let fa_state = db.state(); db.commit(); - let text = "f(b)."; - let clause = parse::parse_str(text, db.interner()).unwrap(); + let clause: Clause<'_> = parse::parse_str("f(b).", &interner).unwrap(); db.insert_clause(clause); - let query = "f($X)."; - let query: Expr> = parse::parse_str(query, db.interner()).unwrap(); + let query: Expr<'_> = parse::parse_str("f($X).", &interner).unwrap(); let answer = collect_answer(db.query(query)); // `f(b).` was discarded. let expected = [["$X = a"]]; assert_eq!(answer, expected); assert_eq!(db.state(), fa_state); - - db.dealloc(); } - fn insert_dataset(db: &mut Database<'_, Int>, text: &str) { - let dataset: ClauseDataset> = parse::parse_str(text, db.interner()).unwrap(); + // === Test helper functions === + + fn insert_dataset<'int>(db: &mut Database<'int>, interner: &'int Interner, text: &str) { + let dataset: ClauseDataset<'int> = parse::parse_str(text, interner).unwrap(); db.insert_dataset(dataset); db.commit(); } - fn collect_answer(mut cx: ProveCx<'_, '_, Int>) -> Vec> { + fn collect_answer(mut cx: ProveCx<'_, '_>) -> Vec> { let mut v = Vec::new(); while let Some(eval) = cx.prove_next() { let x = eval.map(|assign| assign.to_string()).collect::>(); @@ -842,3 +758,117 @@ mod tests { v } } + +#[cfg(test)] +mod tests { + use crate::{Atom, Clause, ClauseDataset, Database, Expr, ProveCx, Term}; + + #[test] + fn test_custom_atom() { + #[allow(non_camel_case_types)] + #[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Debug)] + enum A { + child, + descend, + a, + b, + c, + d, + X, + Y, + Z, + } + + impl Atom for A { + fn is_variable(&self) -> bool { + matches!(self, A::X | A::Y | A::Z) + } + } + + let mut db = Database::new(); + + let child_a_b = Clause::fact(Term::compound( + A::child, + [Term::atom(A::a), Term::atom(A::b)], + )); + let child_b_c = Clause::fact(Term::compound( + A::child, + [Term::atom(A::b), Term::atom(A::c)], + )); + let child_c_d = Clause::fact(Term::compound( + A::child, + [Term::atom(A::c), Term::atom(A::d)], + )); + let descend_x_y = Clause::rule( + Term::compound(A::descend, [Term::atom(A::X), Term::atom(A::Y)]), + Expr::term_compound(A::child, [Term::atom(A::X), Term::atom(A::Y)]), + ); + let descend_x_z = Clause::rule( + Term::compound(A::descend, [Term::atom(A::X), Term::atom(A::Z)]), + Expr::expr_and([ + Expr::term_compound(A::child, [Term::atom(A::X), Term::atom(A::Y)]), + Expr::term_compound(A::descend, [Term::atom(A::Y), Term::atom(A::Z)]), + ]), + ); + insert_dataset( + &mut db, + crate::ClauseDataset(vec![ + child_a_b, + child_b_c, + child_c_d, + descend_x_y, + descend_x_z, + ]), + ); + + let query = Expr::term_compound(A::descend, [Term::atom(A::X), Term::atom(A::Y)]); + let mut answer = collect_answer(db.query(query)); + + let mut expected = [ + [ + (Term::atom(A::X), Term::atom(A::a)), + (Term::atom(A::Y), Term::atom(A::b)), + ], + [ + (Term::atom(A::X), Term::atom(A::a)), + (Term::atom(A::Y), Term::atom(A::c)), + ], + [ + (Term::atom(A::X), Term::atom(A::a)), + (Term::atom(A::Y), Term::atom(A::d)), + ], + [ + (Term::atom(A::X), Term::atom(A::b)), + (Term::atom(A::Y), Term::atom(A::c)), + ], + [ + (Term::atom(A::X), Term::atom(A::b)), + (Term::atom(A::Y), Term::atom(A::d)), + ], + [ + (Term::atom(A::X), Term::atom(A::c)), + (Term::atom(A::Y), Term::atom(A::d)), + ], + ]; + + answer.sort_unstable(); + expected.sort_unstable(); + assert_eq!(answer, expected); + } + + // === Test helper functions === + + fn insert_dataset(db: &mut Database, dataset: ClauseDataset) { + db.insert_dataset(dataset); + db.commit(); + } + + fn collect_answer(mut cx: ProveCx<'_, T>) -> Vec, Term)>> { + let mut v = Vec::new(); + while let Some(eval) = cx.prove_next() { + let pairs = eval.map(|assign| (assign.lhs(), assign.rhs())).collect(); + v.push(pairs); + } + v + } +} diff --git a/crates/logic-eval/src/prove/mod.rs b/crates/logic-eval/src/prove/mod.rs index e1f64e3..fae0be2 100644 --- a/crates/logic-eval/src/prove/mod.rs +++ b/crates/logic-eval/src/prove/mod.rs @@ -1,3 +1,4 @@ +pub(crate) mod common; pub(crate) mod db; pub(crate) mod prover; pub(crate) mod repr; diff --git a/crates/logic-eval/src/prove/prover.rs b/crates/logic-eval/src/prove/prover.rs index fbfc39d..af17d06 100644 --- a/crates/logic-eval/src/prove/prover.rs +++ b/crates/logic-eval/src/prove/prover.rs @@ -3,23 +3,17 @@ use super::repr::{ TermStorageLen, TermView, TermViewMut, UniqueTermArray, }; use crate::{ - parse::{ - repr::{Predicate, Term}, - text::Name, - VAR_PREFIX, - }, - ExprIn, Int2Name, Intern, Map, Name2Int, NameIn, TermIn, + parse::repr::{Expr, Predicate, Term}, + Atom, Map, VAR_PREFIX, }; -use indexmap::IndexMap; -use logic_eval_util::reference::Ref; -use std::{ - borrow::Borrow, - collections::VecDeque, - fmt::{self, Debug, Write}, +use core::{ + fmt::{self, Debug, Display, Write}, hash::Hash, iter, ops::{self, Range}, }; +use indexmap::IndexMap; +use std::collections::VecDeque; pub(crate) type ClauseMap = IndexMap, Vec>; @@ -32,9 +26,8 @@ pub(crate) struct Prover { /// Variable assignments. /// - /// For example, `assignment[X] = a` means that `X(term id)` is assigned to - /// `a(term id)`. If a value is identical to its index, it means the term is - /// not assigned to anything. + /// For example, `assignment[X] = a` means that `X(term id)` is assigned to `a(term id)`. If a + /// value is identical to its index, it means the term is not assigned to anything. assignments: Vec, /// A given query. @@ -50,12 +43,11 @@ pub(crate) struct Prover { /// A buffer containing mapping between variables and temporary variables. /// - /// This buffer is used when we convert variables into temporary variables - /// for a clause. After the conversion, this buffer get empty. + /// This buffer is used when we convert variables into temporary variables for a clause. After + /// the conversion, this buffer get empty. temp_var_buf: Map, - /// A monotonically increasing integer that is used for generating - /// temporary variables. + /// A monotonically increasing integer that is used for generating temporary variables. temp_var_int: u32, } @@ -81,13 +73,13 @@ impl Prover { self.queue.clear(); } - pub(crate) fn prove<'a, 'int, Int: Intern>( + pub(crate) fn prove<'a, T: Atom>( &'a mut self, - query: ExprIn<'int, Int>, + query: Expr, clause_map: &'a ClauseMap, stor: &'a mut TermStorage, - nimap: &'a mut NameIntMap<'int, Int>, - ) -> ProveCx<'a, 'int, Int> { + nimap: &'a mut NameIntMap, + ) -> ProveCx<'a, T> { self.clear(); let old_nimap_state = nimap.state(); @@ -111,12 +103,12 @@ impl Prover { ProveCx::new(self, clause_map, stor, nimap, old_stor_len, old_nimap_state) } - /// Evaluates the given node with all possible clauses in the clause - /// dataset, then returns whether a proof search path is complete or not. + /// Evaluates the given node with all possible clauses in the clause dataset, then returns + /// whether a proof search path is complete or not. /// - /// If it reached an end of paths, it returns proof search result within - /// `Some`. The proof search result is either true or false, which means - /// the expression in the given node is true or not. + /// If it reached an end of paths, it returns proof search result within `Some`. The proof + /// search result is either true or false, which means the expression in the given node is true + /// or not. fn evaluate_node( &mut self, node_index: usize, @@ -159,11 +151,10 @@ impl Prover { } } - // We may need to apply true or false to the leftmost term of the node - // expression due to unification failure or exhaustive search. + // We may need to apply true or false to the leftmost term of the node expression due to + // unification failure or exhaustive search. // - Unification failure means the leftmost term should be false. - // - But we need to consider exhaustive search possibility at the same - // time. + // - But we need to consider exhaustive search possibility at the same time. let expr = stor.get_expr(node_expr); let eval = self.nodes.len() > old_len; @@ -198,16 +189,14 @@ impl Prover { // === Internal helper functions === enum AssumeResult { - /// The whole expression could not completely evaluated even though - /// the assumption is realized. + /// The whole expression could not completely evaluated even though the assumption is + /// realized. Incomplete { - /// Whether or not the assumption will make us lose some search - /// possibilities. + /// Whether or not the assumption will make us lose some search possibilities. lost: bool, }, - /// The whole expression will be completely evaluated if the - /// assumption is realized. + /// The whole expression will be completely evaluated if the assumption is realized. Complete { /// Evalauted as true or false. eval: bool, @@ -228,9 +217,9 @@ impl Prover { } }, ExprKind::And(mut args) => { - // Unlike 'Or', even if 'And' contains variables and the - // whole expression will be evaluated false, those variables - // must be ignored. They don't belong to 'lost'. + // Unlike 'Or', even if 'And' contains variables and the whole expression will + // be evaluated false, those variables must be ignored. They don't belong to + // 'lost'. match assume_leftmost_term(args.next().unwrap(), to) { res @ AssumeResult::Incomplete { .. } => res, AssumeResult::Complete { eval, lost } => { @@ -243,9 +232,8 @@ impl Prover { } } ExprKind::Or(mut args) => { - // The whole 'Or' is true if any argument is true. But we - // will lose possible search paths if we ignore right - // variables. + // The whole 'Or' is true if any argument is true. But we will lose possible + // search paths if we ignore right variables. match assume_leftmost_term(args.next().unwrap(), to) { res @ AssumeResult::Incomplete { .. } => res, AssumeResult::Complete { eval, lost } => { @@ -266,15 +254,14 @@ impl Prover { } /// Replaces variables in a clause with other temporary variables. - /// - // Why we replace variables with temporary variables in clauses before - // unifying? - // 1. That's because variables in different clauses are actually different - // from each other even they have the same identity. Variable's identity - // is valid only in the one clause where they belong. - // 2. Also, we apply this method whenever unification happens because one - // clause can be used mupltiple times in a single proof search path. Then - // it is considered as a different clause. + // + // Why we replace variables with temporary variables in clauses before unifying? + // 1. That's because variables in different clauses are actually different from each other even + // they have the same identity. Variable's identity is valid only in the one clause where + // they belong. + // 2. Also, we apply this method whenever unification happens because one clause can be used + // mupltiple times in a single proof search path. Then it is considered as a different + // clause. fn convert_var_into_temp( mut clause_id: ClauseId, stor: &mut TermStorage, @@ -417,8 +404,8 @@ struct UnificationOperator { /// History of unification. /// - /// A pair of term ids means that `pair.0` is assiend to `pair.1`. For - /// example, `(X, a)` means `X` is assigned to `a`. + /// A pair of term ids means that `pair.0` is assiend to `pair.1`. For example, `(X, a)` means + /// `X` is assigned to `a`. record: Vec<(TermId, TermId)>, } @@ -486,8 +473,7 @@ struct Node { #[derive(Debug, Clone, Copy)] enum NodeKind { - /// A non-terminal node containig an expression id that needs to be - /// evaluated. + /// A non-terminal node containig an expression id that needs to be evaluated. Expr(ExprId), /// A terminal node containing whether a proof path ends with true or false. @@ -500,21 +486,21 @@ enum UnifyOp { Right { from: TermId, to: TermId }, } -pub struct ProveCx<'a, 'int, Int: Intern> { +pub struct ProveCx<'a, T: Atom> { prover: &'a mut Prover, clause_map: &'a ClauseMap, stor: &'a mut TermStorage, - nimap: &'a mut NameIntMap<'int, Int>, + nimap: &'a mut NameIntMap, old_stor_len: TermStorageLen, old_nimap_state: NameIntMapState, } -impl<'a, 'int, Int: Intern> ProveCx<'a, 'int, Int> { +impl<'a, T: Atom> ProveCx<'a, T> { fn new( prover: &'a mut Prover, clause_map: &'a ClauseMap, stor: &'a mut TermStorage, - nimap: &'a mut NameIntMap<'int, Int>, + nimap: &'a mut NameIntMap, old_stor_len: TermStorageLen, old_nimap_state: NameIntMapState, ) -> Self { @@ -528,7 +514,7 @@ impl<'a, 'int, Int: Intern> ProveCx<'a, 'int, Int> { } } - pub fn prove_next(&mut self) -> Option> { + pub fn prove_next(&mut self) -> Option> { while let Some(node_index) = self.prover.queue.pop_front() { if let Some(proof_result) = self.prover @@ -555,32 +541,32 @@ impl<'a, 'int, Int: Intern> ProveCx<'a, 'int, Int> { } } -impl Drop for ProveCx<'_, '_, Int> { +impl Drop for ProveCx<'_, T> { fn drop(&mut self) { self.stor.truncate(self.old_stor_len.clone()); self.nimap.revert(self.old_nimap_state.clone()); } } -pub struct EvalView<'a, 'int, Int: Intern> { +pub struct EvalView<'a, T> { query_vars: &'a [TermId], terms: &'a [TermElem], assignments: &'a [usize], - int2name: &'a Int2Name<'int, Int>, + int2name: &'a IndexMap, /// Inclusive start: usize, /// Exclusive end: usize, } -impl EvalView<'_, '_, Int> { +impl EvalView<'_, T> { const fn len(&self) -> usize { self.end - self.start } } -impl<'a, 'int, Int: Intern> Iterator for EvalView<'a, 'int, Int> { - type Item = Assignment<'a, 'int, Int>; +impl<'a, T> Iterator for EvalView<'a, T> { + type Item = Assignment<'a, T>; fn next(&mut self) -> Option { if self.start < self.end { @@ -604,57 +590,52 @@ impl<'a, 'int, Int: Intern> Iterator for EvalView<'a, 'int, Int> { } } -impl ExactSizeIterator for EvalView<'_, '_, Int> { +impl ExactSizeIterator for EvalView<'_, T> { fn len(&self) -> usize { ::len(self) } } -impl iter::FusedIterator for EvalView<'_, '_, Int> {} +impl iter::FusedIterator for EvalView<'_, T> {} -pub struct Assignment<'a, 'int, Int: Intern> { +pub struct Assignment<'a, T> { buf: &'a [TermElem], from: TermId, assignments: &'a [usize], - int2name: &'a Int2Name<'int, Int>, + int2name: &'a IndexMap, } -impl<'a, 'int: 'a, Int: Intern> Assignment<'a, 'int, Int> { +impl<'a, T: Atom + 'a> Assignment<'a, T> { /// Creates left hand side term of the assignment. /// /// To create a term, this method could allocate memory for the term. - pub fn lhs(&self) -> TermIn<'int, Int> { + pub fn lhs(&self) -> Term { Self::term_view_to_term(self.lhs_view(), self.int2name) } /// Creates right hand side term of the assignment. /// /// To create a term, this method could allocate memory for the term. - pub fn rhs(&self) -> TermIn<'int, Int> { + pub fn rhs(&self) -> Term { Self::term_deep_view_to_term(self.rhs_view(), self.int2name) } /// Returns left hand side variable name of the assignment. /// /// Note that assignment's left hand side is always variable. - pub fn get_lhs_variable(&self) -> &NameIn<'int, Int> { + pub fn get_lhs_variable(&self) -> &T { let int = self.lhs_view().get_contained_variable().unwrap(); self.int2name.get(&int).unwrap() } - fn term_view_to_term( - view: TermView<'_, Integer>, - int2name: &Int2Name<'int, Int>, - ) -> TermIn<'int, Int> { + fn term_view_to_term(view: TermView<'_, Integer>, int2name: &IndexMap) -> Term { let functor = view.functor(); let args = view.args(); let functor = if let Some(name) = int2name.get(functor) { name.clone() } else { - let mut debug_string = String::new(); - write!(&mut debug_string, "{:?}", functor).unwrap(); - Name::with_intern(&debug_string, int2name.interner()) + unreachable!("integer {:?} has no name mapping", functor) }; let args = args @@ -667,17 +648,15 @@ impl<'a, 'int: 'a, Int: Intern> Assignment<'a, 'int, Int> { fn term_deep_view_to_term( view: TermDeepView<'_, Integer>, - int2name: &Int2Name<'int, Int>, - ) -> TermIn<'int, Int> { + int2name: &IndexMap, + ) -> Term { let functor = view.functor(); let args = view.args(); let functor = if let Some(name) = int2name.get(functor) { name.clone() } else { - let mut debug_string = String::new(); - write!(&mut debug_string, "{:?}", functor).unwrap(); - Name::with_intern(&debug_string, int2name.interner()) + unreachable!("integer {:?} has no name mapping", functor) }; let args = args @@ -704,19 +683,19 @@ impl<'a, 'int: 'a, Int: Intern> Assignment<'a, 'int, Int> { } } -impl fmt::Display for Assignment<'_, '_, Int> { +impl Display for Assignment<'_, T> { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { let view = format::NamedTermView::new(self.lhs_view(), self.int2name); - fmt::Display::fmt(&view, f)?; + Display::fmt(&view, f)?; f.write_str(" = ")?; let view = format::NamedTermDeepView::new(self.rhs_view(), self.int2name); - fmt::Display::fmt(&view, f) + Display::fmt(&view, f) } } -impl fmt::Debug for Assignment<'_, '_, Int> { +impl Debug for Assignment<'_, T> { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { let lhs = format::NamedTermView::new(self.lhs_view(), self.int2name); let rhs = format::NamedTermDeepView::new(self.rhs_view(), self.int2name); @@ -842,7 +821,7 @@ impl Integer { const VAR_FLAG: u32 = 0x1 << 31; const TEMPORARY_FLAG: u32 = 0x1 << 30; - pub(crate) fn from_text>(s: &Name, mut index: u32) -> Self { + pub(crate) fn from_value(s: &T, mut index: u32) -> Self { if s.is_variable() { index |= Self::VAR_FLAG; } @@ -874,7 +853,7 @@ impl Debug for Integer { if self.is_temporary_variable() { f.write_char('#')?; } - index.fmt(f) + Debug::fmt(&index, f) } } @@ -884,29 +863,38 @@ impl ops::AddAssign for Integer { } } -/// Only mapping of user-input clauses and queries are stored in this map. -/// Auto-generated variables or something like that are not stored here. -#[derive(Debug)] -pub(crate) struct NameIntMap<'int, Int: Intern> { - pub(crate) name2int: Name2Int<'int, Int>, - pub(crate) int2name: Int2Name<'int, Int>, +/// Only mapping of user-input clauses and queries are stored in this map. Auto-generated variables +/// or something like that are not stored here. +pub(crate) struct NameIntMap { + pub(crate) name2int: IndexMap, + pub(crate) int2name: IndexMap, next_int: u32, } -impl<'int, Int: Intern> NameIntMap<'int, Int> { - pub(crate) fn new(interner: Ref<'int, Int>) -> Self { +impl fmt::Debug for NameIntMap { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + f.debug_struct("NameIntMap") + .field("name2int", &self.name2int) + .field("int2name", &self.int2name) + .field("next_int", &self.next_int) + .finish() + } +} + +impl NameIntMap { + pub(crate) fn new() -> Self { Self { - name2int: IdxMap::new(interner), - int2name: IdxMap::new(interner), + name2int: IndexMap::default(), + int2name: IndexMap::default(), next_int: 0, } } - pub(crate) fn name_to_int(&mut self, name: NameIn<'int, Int>) -> Integer { + pub(crate) fn name_to_int(&mut self, name: T) -> Integer { if let Some(int) = self.name2int.get(&name) { *int } else { - let int = Integer::from_text(&name, self.next_int); + let int = Integer::from_value(&name, self.next_int); self.name2int.insert(name.clone(), int); self.int2name.insert(int, name); @@ -938,48 +926,6 @@ impl<'int, Int: Intern> NameIntMap<'int, Int> { } } -#[derive(Debug)] -pub(crate) struct IdxMap<'int, K, V, Int> { - map: IndexMap, - pub(crate) interner: Ref<'int, Int>, -} - -impl<'int, K, V, Int> IdxMap<'int, K, V, Int> { - pub(crate) fn new(interner: Ref<'int, Int>) -> Self { - Self { - map: IndexMap::default(), - interner, - } - } - - pub(crate) fn interner(&self) -> &'int Int { - self.interner.as_ref() - } - - pub(crate) fn len(&self) -> usize { - self.map.len() - } - - pub(crate) fn truncate(&mut self, len: usize) { - self.map.truncate(len); - } - - pub(crate) fn get(&self, key: &Q) -> Option<&V> - where - K: Borrow, - Q: Hash + Eq + ?Sized, - { - self.map.get(key) - } - - pub(crate) fn insert(&mut self, key: K, value: V) -> Option - where - K: Hash + Eq, - { - self.map.insert(key, value) - } -} - #[derive(Debug, Clone, PartialEq, Eq)] pub(crate) struct NameIntMapState { name2int_len: usize, @@ -990,20 +936,20 @@ pub(crate) struct NameIntMapState { pub(crate) mod format { use super::*; - pub struct NamedTermView<'a, 'int, Int: Intern> { + pub struct NamedTermView<'a, T> { view: TermView<'a, Integer>, - int2name: &'a Int2Name<'int, Int>, + int2name: &'a IndexMap, } - impl<'a, 'int, Int: Intern> NamedTermView<'a, 'int, Int> { + impl<'a, T: Atom> NamedTermView<'a, T> { pub(crate) const fn new( view: TermView<'a, Integer>, - int2name: &'a Int2Name<'int, Int>, + int2name: &'a IndexMap, ) -> Self { Self { view, int2name } } - pub fn is(&self, term: &TermIn<'int, Int>) -> bool { + pub fn is(&self, term: &Term) -> bool { let functor = self.view.functor(); let Some(functor) = self.int2name.get(functor) else { return false; @@ -1016,7 +962,7 @@ pub(crate) mod format { self.args().zip(&term.args).all(|(l, r)| l.is(r)) } - pub fn contains(&self, term: &TermIn<'int, Int>) -> bool { + pub fn contains(&self, term: &Term) -> bool { if self.is(term) { return true; } @@ -1024,7 +970,7 @@ pub(crate) mod format { self.args().any(|arg| arg.contains(term)) } - fn args<'s>(&'s self) -> impl Iterator> + 's { + fn args<'s>(&'s self) -> impl Iterator> + 's { self.view.args().map(|arg| Self { view: arg, int2name: self.int2name, @@ -1032,7 +978,7 @@ pub(crate) mod format { } } - impl<'a, 'int, Int: Intern> fmt::Display for NamedTermView<'a, 'int, Int> { + impl<'a, T: Atom + Display> Display for NamedTermView<'a, T> { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { let Self { view, int2name } = self; @@ -1056,7 +1002,7 @@ pub(crate) mod format { } } - impl<'a, 'int, Int: Intern> fmt::Debug for NamedTermView<'a, 'int, Int> { + impl<'a, T: Atom + Debug> Debug for NamedTermView<'a, T> { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { let Self { view, int2name } = self; @@ -1065,15 +1011,18 @@ pub(crate) mod format { let num_args = args.len(); if num_args == 0 { - write_int(functor, int2name, f) + if let Some(name) = int2name.get(functor) { + fmt::Debug::fmt(name, f) + } else { + fmt::Debug::fmt(functor, f) + } } else { - let mut d = if let Some(name) = int2name.get(functor) { - f.debug_tuple(name.as_ref()) + let name_str = if let Some(name) = int2name.get(functor) { + format!("{:?}", name) } else { - let mut debug_string = String::new(); - write!(&mut debug_string, "{:?}", functor)?; - f.debug_tuple(&debug_string) + format!("{:?}", functor) }; + let mut d = f.debug_tuple(&name_str); for arg in args { d.field(&Self::new(arg, int2name)); @@ -1083,21 +1032,21 @@ pub(crate) mod format { } } - pub(crate) struct NamedTermDeepView<'a, 'int, Int: Intern> { + pub(crate) struct NamedTermDeepView<'a, T> { view: TermDeepView<'a, Integer>, - int2name: &'a Int2Name<'int, Int>, + int2name: &'a IndexMap, } - impl<'a, 'int, Int: Intern> NamedTermDeepView<'a, 'int, Int> { + impl<'a, T> NamedTermDeepView<'a, T> { pub(crate) const fn new( view: TermDeepView<'a, Integer>, - int2name: &'a Int2Name<'int, Int>, + int2name: &'a IndexMap, ) -> Self { Self { view, int2name } } } - impl<'a, 'int, Int: Intern> fmt::Display for NamedTermDeepView<'a, 'int, Int> { + impl<'a, T: Display> Display for NamedTermDeepView<'a, T> { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { let Self { view, int2name } = self; @@ -1121,7 +1070,7 @@ pub(crate) mod format { } } - impl<'a, 'int, Int: Intern> fmt::Debug for NamedTermDeepView<'a, 'int, Int> { + impl<'a, T: Debug> Debug for NamedTermDeepView<'a, T> { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { let Self { view, int2name } = self; @@ -1130,15 +1079,18 @@ pub(crate) mod format { let num_args = args.len(); if num_args == 0 { - write_int(functor, int2name, f) + if let Some(name) = int2name.get(functor) { + fmt::Debug::fmt(name, f) + } else { + fmt::Debug::fmt(functor, f) + } } else { - let mut d = if let Some(name) = int2name.get(functor) { - f.debug_tuple(name.as_ref()) + let name_str = if let Some(name) = int2name.get(functor) { + format!("{:?}", name) } else { - let mut debug_string = String::new(); - write!(&mut debug_string, "{:?}", functor)?; - f.debug_tuple(&debug_string) + format!("{:?}", functor) }; + let mut d = f.debug_tuple(&name_str); for arg in args { d.field(&Self::new(arg, int2name)); @@ -1148,20 +1100,20 @@ pub(crate) mod format { } } - pub struct NamedExprView<'a, 'int, Int: Intern> { + pub struct NamedExprView<'a, T> { view: ExprView<'a, Integer>, - int2name: &'a Int2Name<'int, Int>, + int2name: &'a IndexMap, } - impl<'a, 'int, Int: Intern> NamedExprView<'a, 'int, Int> { + impl<'a, T: Atom> NamedExprView<'a, T> { pub(crate) const fn new( view: ExprView<'a, Integer>, - int2name: &'a Int2Name<'int, Int>, + int2name: &'a IndexMap, ) -> Self { Self { view, int2name } } - pub fn contains_term(&self, term: &TermIn<'int, Int>) -> bool { + pub fn contains_term(&self, term: &Term) -> bool { match self.view.as_kind() { ExprKind::Term(view) => NamedTermView { view, @@ -1184,7 +1136,7 @@ pub(crate) mod format { } } - impl<'a, 'int, Int: Intern> fmt::Display for NamedExprView<'a, 'int, Int> { + impl<'a, T: Atom + Display> Display for NamedExprView<'a, T> { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { let Self { view, int2name } = self; @@ -1235,7 +1187,7 @@ pub(crate) mod format { } } - impl<'a, 'int, Int: Intern> fmt::Debug for NamedExprView<'a, 'int, Int> { + impl<'a, T: Atom + Debug> Debug for NamedExprView<'a, T> { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { let Self { view, int2name } = self; @@ -1263,13 +1215,13 @@ pub(crate) mod format { } } - fn write_int<'int, Int: Intern>( + fn write_int( int: &Integer, - map: &Int2Name<'int, Int>, + map: &IndexMap, f: &mut fmt::Formatter<'_>, ) -> fmt::Result { if let Some(name) = map.get(int) { - f.write_str(name.as_ref()) + fmt::Display::fmt(name, f) } else { fmt::Debug::fmt(int, f) } diff --git a/crates/logic-eval/src/prove/repr.rs b/crates/logic-eval/src/prove/repr.rs index a9b2e98..675a0b5 100644 --- a/crates/logic-eval/src/prove/repr.rs +++ b/crates/logic-eval/src/prove/repr.rs @@ -1,7 +1,4 @@ -use crate::{ - parse::repr::{Expr, Predicate, Term}, - PassThroughState, -}; +use crate::{Expr, PassThroughState, Predicate, Term}; use fxhash::FxHasher; use indexmap::IndexMap; use std::{ @@ -15,8 +12,6 @@ pub(crate) struct ClauseId { pub(crate) body: Option, } -// === TermStorage === - #[derive(Debug)] pub(crate) struct TermStorage { pub(crate) exprs: ExprArray, @@ -76,8 +71,6 @@ impl TermStorage { } } -// === ExprArray === - #[derive(Debug)] pub(crate) struct ExprArray { buf: Vec, @@ -231,8 +224,6 @@ impl ops::IndexMut for [ExprElem] { } } -// === ExprView === - #[derive(Clone, Copy)] pub(crate) struct ExprView<'a, T> { expr_buf: &'a [ExprElem], @@ -353,8 +344,6 @@ impl ExactSizeIterator for ExprViewIter<'_, T> { impl iter::FusedIterator for ExprViewIter<'_, T> {} -// === ExprViewMut === - pub(crate) struct ExprViewMut<'a, T> { exprs: &'a mut ExprArray, terms: &'a mut UniqueTermArray, @@ -366,8 +355,8 @@ impl<'a, T> ExprViewMut<'a, T> { self.id } - /// Finds the destination of jump (Elem::Expr) chain then moves this view - /// to the final expression. + /// Finds the destination of jump (Elem::Expr) chain then moves this view to the final + /// expression. fn find_then_move(&mut self) { self.id = self.find(self.id); } @@ -417,21 +406,18 @@ impl<'a, T> ExprViewMut<'a, T> { #[derive(Debug, PartialEq, Eq)] pub(crate) enum ApplyResult { - /// An expression still remains as an expression after application of a - /// boolean value. + /// An expression still remains as an expression after application of a boolean value. Expr, - /// An expression is completely evaluated after application of a boolean - /// value. + /// An expression is completely evaluated after application of a boolean value. Complete(bool), } impl<'a, T: Clone> ExprViewMut<'a, T> { /// Sets the most left term to the given boolean value. /// - /// This operation always clones the original expression then does the - /// setting on that. Plus, this could unwrap AND or OR if they do not - /// contain two or more arguments after evaluation. + /// This operation always clones the original expression then does the setting on that. Plus, + /// this could unwrap AND or OR if they do not contain two or more arguments after evaluation. pub(crate) fn apply_to_leftmost_term(&mut self, to: bool) -> ApplyResult { // Clones this expression deeply. let mut handle_term = |this: &mut Self, term_id: TermId, _: ()| { @@ -511,12 +497,10 @@ impl<'a, T: Clone> ExprViewMut<'a, T> { } } - /// Replaces the most left expression(term) to the given `to` in a - /// clone-on-write way. + /// Replaces the most left expression(term) to the given `to` in a clone-on-write way. /// - /// If the replacement took place, then a new expression is created then - /// this view becomes to point the new expression instead of modifying - /// original expression directly. + /// If the replacement took place, then a new expression is created then this view becomes to + /// point the new expression instead of modifying original expression directly. pub(crate) fn replace_leftmost_term(&mut self, to: ExprId) -> bool { let mut has_met_first_term = false; @@ -633,12 +617,10 @@ impl<'a, T: Clone> ExprViewMut<'a, T> { } impl<'a, T: Clone + Eq + Hash> ExprViewMut<'a, T> { - /// If this expression contains `from`, then replaces them to `to` in a - /// clone-on-write way. + /// If this expression contains `from`, then replaces them to `to` in a clone-on-write way. /// - /// If the replacement took place, then a new expression is created then - /// this view becomes to point the new expression instead of modifying - /// original expression directly. + /// If the replacement took place, then a new expression is created then this view becomes to + /// point the new expression instead of modifying original expression directly. pub(crate) fn replace_term(&mut self, from: TermId, to: TermId) -> bool { let mut handle_term = |this: &mut Self, term_id: TermId, (from, to): (TermId, TermId)| { let mut term_view = TermViewMut { @@ -705,8 +687,6 @@ impl ops::AddAssign for ExprId { } } -// === UniqueTermArray === - #[derive(Debug)] pub(crate) struct UniqueTermArray { /// e.g. ... [Functor], [Len], [Arg0], [Arg1], ... @@ -714,15 +694,13 @@ pub(crate) struct UniqueTermArray { /// Mapping between term's hash values and terms. /// - /// This helps you find similar terms to keep the uniqueness. But for - /// efficiency, the value, [`Vec`], could contain stale data. For - /// example, [`Self::buf`] could be shrunk by truncate method, but values of - /// this map still would point to removed area of the buffer becuase values - /// themselves are not shrunk. + /// This helps you find similar terms to keep the uniqueness. But for efficiency, the value, + /// [`Vec`], could contain stale data. For example, [`Self::buf`] could be shrunk by + /// truncate method, but values of this map still would point to removed area of the buffer + /// becuase values themselves are not shrunk. /// - /// You are encouraged to call two methods below to access this field, - /// [`Self::add_mapping`] and [`Self::get_similar`], which hide the - /// problem. + /// You are encouraged to call two methods below to access this field, [`Self::add_mapping`] and + /// [`Self::get_similar`], which hide the problem. pub(crate) map: IndexMap, PassThroughState>, } @@ -825,8 +803,8 @@ impl UniqueTermArray { // === Internal helper functions === - /// Checks whether arguments of the given term has been set or not - /// by compairing with the predefined dummy value. + /// Checks whether arguments of the given term has been set or not by compairing with the + /// predefined dummy value. fn is_arg_set(buf: &[TermElem], id: TermId) -> bool { let arity = UniqueTermArray::_get(buf, id).arity(); (0..arity).all(|i| buf[id.0 + 2 + i as usize] != TermElem::dummy()) @@ -931,8 +909,6 @@ impl<'a, T> Iterator for TermViewIter<'a, T> { impl iter::FusedIterator for TermViewIter<'_, T> {} -// === TermView === - #[derive(Clone)] pub struct TermView<'a, T> { pub(crate) buf: &'a [TermElem], @@ -1172,12 +1148,11 @@ impl<'a, T> TermViewMut<'a, T> { } impl TermViewMut<'_, T> { - /// If this term is `from` or contains `from`, then replaces them to `to` in - /// a clone-on-write way. + /// If this term is `from` or contains `from`, then replaces them to `to` in a clone-on-write + /// way. /// - /// If the replacement took place, then a new term is created then this view - /// becomes to point the new term instead of modifying original term - /// directly. + /// If the replacement took place, then a new term is created then this view becomes to point + /// the new term instead of modifying original term directly. pub(crate) fn replace(&mut self, from: TermId, to: TermId) -> bool { if from == to { return false; @@ -1341,10 +1316,7 @@ fn buf_term_hash(buf: &[TermElem], id: TermId) -> u64 { #[cfg(test)] mod tests { use super::*; - use crate::{ - parse::{self, text::Name}, - Intern, TermStorageIn, UniqueTermArrayIn, - }; + use crate::{parse, ExprIn, Intern, Name, TermIn, TermStorageIn, UniqueTermArrayIn}; use any_intern::DroplessInterner; #[test] @@ -1537,7 +1509,7 @@ mod tests { interner: &'int Int, text: &str, ) -> ExprId { - let expr: Expr> = parse::parse_str(text, interner).unwrap(); + let expr: ExprIn<'int, Int> = parse::parse_str(text, interner).unwrap(); buf.insert_expr(expr) } @@ -1546,7 +1518,7 @@ mod tests { interner: &'int Int, text: &str, ) -> TermId { - let term: Term> = parse::parse_str(text, interner).unwrap(); + let term: TermIn<'int, Int> = parse::parse_str(text, interner).unwrap(); arr.insert(term) } } diff --git a/src/lib.rs b/src/lib.rs deleted file mode 100644 index 4fa662b..0000000 --- a/src/lib.rs +++ /dev/null @@ -1 +0,0 @@ -// Dummy