use crate::position::PositionInLanguageTerm;
use crate::term::syntax::{LanguageTerm, RewritableLanguageOperatorSymbol};
pub trait RewriteApplicationGuard<LOS: RewritableLanguageOperatorSymbol> {
fn allows(
&self,
term: &LanguageTerm<LOS>,
context_term: &LanguageTerm<LOS>,
position: &PositionInLanguageTerm,
) -> bool;
}
pub struct RootOnlyRewriteApplicationGuard;
impl<LOS: RewritableLanguageOperatorSymbol> RewriteApplicationGuard<LOS>
for RootOnlyRewriteApplicationGuard
{
fn allows(
&self,
_term: &LanguageTerm<LOS>,
_context_term: &LanguageTerm<LOS>,
position: &PositionInLanguageTerm,
) -> bool {
position.get_depth() == 0
}
}
pub struct NotUnderSameOpRewriteApplicationGuard;
impl<LOS: RewritableLanguageOperatorSymbol> RewriteApplicationGuard<LOS>
for NotUnderSameOpRewriteApplicationGuard
{
fn allows(
&self,
term: &LanguageTerm<LOS>,
context_term: &LanguageTerm<LOS>,
position: &PositionInLanguageTerm,
) -> bool {
match position.get_parent_position() {
None => true,
Some(parent_pos) => match context_term.get_sub_term_at_position(&parent_pos) {
None => true,
Some(parent) => parent.operator != term.operator,
},
}
}
}
pub struct OnlyUnderOpRewriteApplicationGuard<LOS: RewritableLanguageOperatorSymbol> {
pred: Box<dyn Fn(&LOS) -> bool>,
}
impl<LOS: RewritableLanguageOperatorSymbol> OnlyUnderOpRewriteApplicationGuard<LOS> {
pub fn new<F: Fn(&LOS) -> bool + 'static>(pred: F) -> Self {
Self {
pred: Box::new(pred),
}
}
}
impl<LOS: RewritableLanguageOperatorSymbol> RewriteApplicationGuard<LOS>
for OnlyUnderOpRewriteApplicationGuard<LOS>
{
fn allows(
&self,
_term: &LanguageTerm<LOS>,
context_term: &LanguageTerm<LOS>,
position: &PositionInLanguageTerm,
) -> bool {
match position.get_parent_position() {
None => false,
Some(parent_pos) => match context_term.get_sub_term_at_position(&parent_pos) {
None => false,
Some(parent) => (self.pred)(&parent.operator),
},
}
}
}
#[allow(clippy::type_complexity)]
pub struct TermPredicateRewriteApplicationGuard<LOS: RewritableLanguageOperatorSymbol> {
pred: Box<dyn Fn(&LanguageTerm<LOS>) -> bool>,
}
impl<LOS: RewritableLanguageOperatorSymbol> TermPredicateRewriteApplicationGuard<LOS> {
pub fn new<F: Fn(&LanguageTerm<LOS>) -> bool + 'static>(pred: F) -> Self {
Self {
pred: Box::new(pred),
}
}
}
impl<LOS: RewritableLanguageOperatorSymbol> RewriteApplicationGuard<LOS>
for TermPredicateRewriteApplicationGuard<LOS>
{
fn allows(
&self,
term: &LanguageTerm<LOS>,
_context_term: &LanguageTerm<LOS>,
_position: &PositionInLanguageTerm,
) -> bool {
(self.pred)(term)
}
}
#[allow(clippy::type_complexity)]
pub struct ClosureRewriteApplicationGuard<LOS: RewritableLanguageOperatorSymbol> {
pred: Box<dyn Fn(&LanguageTerm<LOS>, &LanguageTerm<LOS>, &PositionInLanguageTerm) -> bool>,
}
impl<LOS: RewritableLanguageOperatorSymbol> ClosureRewriteApplicationGuard<LOS> {
pub fn new<F>(pred: F) -> Self
where
F: Fn(&LanguageTerm<LOS>, &LanguageTerm<LOS>, &PositionInLanguageTerm) -> bool + 'static,
{
Self {
pred: Box::new(pred),
}
}
}
impl<LOS: RewritableLanguageOperatorSymbol> RewriteApplicationGuard<LOS>
for ClosureRewriteApplicationGuard<LOS>
{
fn allows(
&self,
term: &LanguageTerm<LOS>,
context_term: &LanguageTerm<LOS>,
position: &PositionInLanguageTerm,
) -> bool {
(self.pred)(term, context_term, position)
}
}