use hashconsing::HConsign;
use simple_term_rewriter::position::PositionInLanguageTerm;
use simple_term_rewriter::rule::RewriteRule;
use simple_term_rewriter::rules::primitives::flush::{
AssociativityChecker, FlushLeftRule, FlushRightRule,
};
use simple_term_rewriter::term;
use simple_term_rewriter::term::syntax::{
LanguageOperatorArity, RewritableLanguageOperatorSymbol, TermFactory,
};
#[derive(Clone, PartialEq, Eq, Hash, Debug)]
enum CatOp {
Cat,
A,
B,
C,
D,
}
impl RewritableLanguageOperatorSymbol for CatOp {
fn arity(&self) -> LanguageOperatorArity {
match self {
CatOp::Cat => LanguageOperatorArity::Fixed(2),
_ => LanguageOperatorArity::Fixed(0),
}
}
}
struct CatChecker;
impl AssociativityChecker<CatOp> for CatChecker {
fn is_binary_associative(&self, op: &CatOp) -> bool {
*op == CatOp::Cat
}
}
fn root_pos() -> PositionInLanguageTerm {
PositionInLanguageTerm::get_root_position()
}
fn flush_right() -> FlushRightRule<CatOp> {
FlushRightRule::new("flush right", CatChecker)
}
fn flush_left() -> FlushLeftRule<CatOp> {
FlushLeftRule::new("flush left", CatChecker)
}
#[test]
fn flush_right_fires_on_left_nested() {
let mut f: TermFactory<CatOp> = HConsign::empty();
let t = term!(&mut f, CatOp::Cat; term!(&mut f, CatOp::Cat; term!(&mut f, CatOp::A), term!(&mut f, CatOp::B)), term!(&mut f, CatOp::C));
assert_eq!(
flush_right().try_apply(&t, &t, &root_pos(), &mut f),
Some(
term!(&mut f, CatOp::Cat; term!(&mut f, CatOp::A), term!(&mut f, CatOp::Cat; term!(&mut f, CatOp::B), term!(&mut f, CatOp::C)))
)
);
}
#[test]
fn flush_right_no_fire_when_left_is_leaf() {
let mut f: TermFactory<CatOp> = HConsign::empty();
let t = term!(&mut f, CatOp::Cat; term!(&mut f, CatOp::A), term!(&mut f, CatOp::Cat; term!(&mut f, CatOp::B), term!(&mut f, CatOp::C)));
assert!(flush_right()
.try_apply(&t, &t, &root_pos(), &mut f)
.is_none());
}
#[test]
fn flush_right_no_fire_on_flat_pair() {
let mut f: TermFactory<CatOp> = HConsign::empty();
let t = term!(&mut f, CatOp::Cat; term!(&mut f, CatOp::A), term!(&mut f, CatOp::B));
assert!(flush_right()
.try_apply(&t, &t, &root_pos(), &mut f)
.is_none());
}
#[test]
fn flush_right_no_fire_on_leaf() {
let mut f: TermFactory<CatOp> = HConsign::empty();
let t = term!(&mut f, CatOp::A);
assert!(flush_right()
.try_apply(&t, &t, &root_pos(), &mut f)
.is_none());
}
#[test]
fn flush_right_three_elements_two_steps() {
let pos = root_pos();
let mut f: TermFactory<CatOp> = HConsign::empty();
let t0 = term!(&mut f, CatOp::Cat;
term!(&mut f, CatOp::Cat;
term!(&mut f, CatOp::Cat; term!(&mut f, CatOp::A), term!(&mut f, CatOp::B)),
term!(&mut f, CatOp::C)),
term!(&mut f, CatOp::D));
let t1 = flush_right()
.try_apply(&t0, &t0, &pos, &mut f)
.expect("step 1 should fire");
assert_eq!(
t1,
term!(&mut f, CatOp::Cat;
term!(&mut f, CatOp::Cat; term!(&mut f, CatOp::A), term!(&mut f, CatOp::B)),
term!(&mut f, CatOp::Cat; term!(&mut f, CatOp::C), term!(&mut f, CatOp::D)))
);
let t2 = flush_right()
.try_apply(&t1, &t1, &pos, &mut f)
.expect("step 2 should fire");
assert_eq!(
t2,
term!(&mut f, CatOp::Cat;
term!(&mut f, CatOp::A),
term!(&mut f, CatOp::Cat;
term!(&mut f, CatOp::B),
term!(&mut f, CatOp::Cat; term!(&mut f, CatOp::C), term!(&mut f, CatOp::D))))
);
assert!(
flush_right().try_apply(&t2, &t2, &pos, &mut f).is_none(),
"should be irreducible"
);
}
#[test]
fn flush_left_fires_on_right_nested() {
let mut f: TermFactory<CatOp> = HConsign::empty();
let t = term!(&mut f, CatOp::Cat; term!(&mut f, CatOp::A), term!(&mut f, CatOp::Cat; term!(&mut f, CatOp::B), term!(&mut f, CatOp::C)));
assert_eq!(
flush_left().try_apply(&t, &t, &root_pos(), &mut f),
Some(
term!(&mut f, CatOp::Cat; term!(&mut f, CatOp::Cat; term!(&mut f, CatOp::A), term!(&mut f, CatOp::B)), term!(&mut f, CatOp::C))
)
);
}
#[test]
fn flush_left_no_fire_when_right_is_leaf() {
let mut f: TermFactory<CatOp> = HConsign::empty();
let t = term!(&mut f, CatOp::Cat; term!(&mut f, CatOp::Cat; term!(&mut f, CatOp::A), term!(&mut f, CatOp::B)), term!(&mut f, CatOp::C));
assert!(flush_left()
.try_apply(&t, &t, &root_pos(), &mut f)
.is_none());
}
#[test]
fn flush_left_no_fire_on_flat_pair() {
let mut f: TermFactory<CatOp> = HConsign::empty();
let t = term!(&mut f, CatOp::Cat; term!(&mut f, CatOp::A), term!(&mut f, CatOp::B));
assert!(flush_left()
.try_apply(&t, &t, &root_pos(), &mut f)
.is_none());
}
#[test]
fn flush_left_three_elements_two_steps() {
let pos = root_pos();
let mut f: TermFactory<CatOp> = HConsign::empty();
let t0 = term!(&mut f, CatOp::Cat;
term!(&mut f, CatOp::A),
term!(&mut f, CatOp::Cat;
term!(&mut f, CatOp::B),
term!(&mut f, CatOp::Cat; term!(&mut f, CatOp::C), term!(&mut f, CatOp::D))));
let t1 = flush_left()
.try_apply(&t0, &t0, &pos, &mut f)
.expect("step 1 should fire");
assert_eq!(
t1,
term!(&mut f, CatOp::Cat;
term!(&mut f, CatOp::Cat; term!(&mut f, CatOp::A), term!(&mut f, CatOp::B)),
term!(&mut f, CatOp::Cat; term!(&mut f, CatOp::C), term!(&mut f, CatOp::D)))
);
let t2 = flush_left()
.try_apply(&t1, &t1, &pos, &mut f)
.expect("step 2 should fire");
assert_eq!(
t2,
term!(&mut f, CatOp::Cat;
term!(&mut f, CatOp::Cat;
term!(&mut f, CatOp::Cat; term!(&mut f, CatOp::A), term!(&mut f, CatOp::B)),
term!(&mut f, CatOp::C)),
term!(&mut f, CatOp::D))
);
assert!(
flush_left().try_apply(&t2, &t2, &pos, &mut f).is_none(),
"should be irreducible"
);
}
#[test]
fn flush_right_then_left_roundtrip() {
let pos = root_pos();
let mut f: TermFactory<CatOp> = HConsign::empty();
let original = term!(&mut f, CatOp::Cat;
term!(&mut f, CatOp::Cat; term!(&mut f, CatOp::A), term!(&mut f, CatOp::B)),
term!(&mut f, CatOp::C));
let after_right = flush_right()
.try_apply(&original, &original, &pos, &mut f)
.expect("flush right should fire");
let after_left = flush_left()
.try_apply(&after_right, &after_right, &pos, &mut f)
.expect("flush left should fire");
assert_eq!(after_left, original);
}
#[test]
fn flush_right_rule_get_desc() {
assert_eq!(flush_right().get_desc(), "flush right");
}
#[test]
fn flush_left_rule_get_desc() {
assert_eq!(flush_left().get_desc(), "flush left");
}