notmuch-tagrewriter 0.1.0

use std::{
    collections::BTreeSet,
    fmt::{Debug, Display},
    hash::Hash,
};

use derive_more::derive::{AsRef, Deref, DerefMut, Display, From, IntoIterator};
use itertools::Itertools;

pub const SYMBOL_NOT: char = '!';
pub const SYMBOL_AND: char = '&';
pub const SYMBOL_OR: char = '|';
pub const SYMBOL_TRUE: char = 'T';
pub const SYMBOL_TRUE_ALT: char = '*';
pub const SYMBOL_FALSE: char = 'F';
pub const SYMBOL_ALLTAGS: char = 'A';
pub const SYMBOL_ALLNOTAGS: char = 'N';

pub const SYMBOL_NOT_FANCY: char = '¬';
pub const SYMBOL_AND_FANCY: char = '∧';
pub const SYMBOL_OR_FANCY: char = '∨';
pub const SYMBOL_TRUE_FANCY: char = '⊤';
pub const SYMBOL_FALSE_FANCY: char = '⊥';
pub const SYMBOL_FALSE_FANCY_ALT: char = '∅';
pub const SYMBOL_ALLTAGS_FANCY: char = '∀';
pub const SYMBOL_ALLNOTTAGS_FANCY: char = '∄';

pub trait LitteralTrait: Clone + Debug + Ord + Hash {}

/// A trait to facilitate conversion between types that really are
/// just booleans in disguise.
pub trait BooleanLike: Copy + Eq + PartialEq + PartialOrd + Ord + Hash {
    /// The False value
    const FALSY: Self;
    /// The True value
    const TRUTHY: Self;
    /// Represent self as a boolean.
    fn as_bool(&self) -> bool {
        *self == Self::TRUTHY
    }
    /// Convert from boolean
    fn from_bool(boolean: bool) -> Self {
        if boolean { Self::TRUTHY } else { Self::FALSY }
    }

    /// Convert to other BooleanLike
    fn as_other<B: BooleanLike>(&self) -> B {
        B::from_bool(self.as_bool())
    }
}

impl BooleanLike for bool {
    const FALSY: Self = false;
    const TRUTHY: Self = true;
}

impl<T: LitteralTrait, B: BooleanLike> Formula<T> for B {
    type OrTarget = Self;
    type AndTarget = Self;
    type NotTarget = Self;
    fn not(&self) -> Self::NotTarget {
        (!(self.as_bool())).as_other()
    }
    fn or<U: Into<Self> + Clone>(&self, rhs: &U) -> Self::OrTarget {
        (self.as_bool() || rhs.clone().into().as_bool()).as_other()
    }
    fn and<U: Into<Self> + Clone>(&self, rhs: &U) -> Self::AndTarget {
        (self.as_bool() && rhs.clone().into().as_bool()).as_other()
    }
    fn terms(&self) -> BTreeSet<T> {
        BTreeSet::new()
    }
}

#[derive(Copy, Clone, Hash, PartialEq, Eq, PartialOrd, Ord, Display, Debug)]
/// A Sign type
pub enum Sign {
    #[display("-")]
    Negative,
    #[display("+")]
    Positive,
}

impl BooleanLike for Sign {
    const TRUTHY: Self = Sign::Positive;
    const FALSY: Self = Sign::Negative;
}

#[derive(Clone, From, PartialEq, PartialOrd, Eq, Ord, Debug, Hash, Display)]
#[display(bound(T: Display))]
pub enum Litteral<T: LitteralTrait> {
    #[from]
    #[display("{}", if _0.as_bool() { SYMBOL_TRUE_FANCY } else { SYMBOL_FALSE_FANCY })]
    Constant(Sign),
    #[display("{_0}")]
    #[from]
    Val(T),
}
#[derive(Clone, From, Ord, PartialEq, PartialOrd, Eq, Debug, Hash, Display)]
#[display(bound(T: Display))]
pub enum SignedLitteral<T: LitteralTrait> {
    #[from]
    #[display("{}", _0.as_bool())]
    Constant(Sign),

    #[display("{}{litteral}", if !sign.as_bool() {SYMBOL_NOT_FANCY.to_string()} else {"".to_string()})]
    Val { litteral: T, sign: Sign },
}

impl<T: LitteralTrait> From<Litteral<T>> for SignedLitteral<T> {
    fn from(value: Litteral<T>) -> Self {
        match value {
            Litteral::Constant(t) => SignedLitteral::Constant(t),
            Litteral::Val(t) => SignedLitteral::Val {
                sign: Sign::Positive,
                litteral: t,
            },
        }
    }
}

#[derive(
    Debug, Clone, From, Hash, Eq, PartialEq, Deref, DerefMut, IntoIterator, AsRef, PartialOrd, Ord,
)]
pub struct Conjunction<T: LitteralTrait>(BTreeSet<SignedLitteral<T>>);

impl<T: Display + LitteralTrait> Display for Conjunction<T> {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(
            f,
            "{}",
            self.iter()
                .format_with(&format!(" {SYMBOL_AND_FANCY} "), |e, g| { g(e) })
        )
    }
}

impl<T: LitteralTrait> From<SignedLitteral<T>> for Conjunction<T> {
    fn from(value: SignedLitteral<T>) -> Self {
        BTreeSet::from([value]).into()
    }
}

impl<T: LitteralTrait> From<Litteral<T>> for Conjunction<T> {
    fn from(value: Litteral<T>) -> Self {
        SignedLitteral::from(value).into()
    }
}

impl<T: LitteralTrait> From<Sign> for Conjunction<T> {
    fn from(value: Sign) -> Self {
        SignedLitteral::from(value).into()
    }
}

impl<T: LitteralTrait> Conjunction<T> {
    pub fn is_true(&self) -> bool {
        self.0.len() == 0
            || self
                .iter()
                .any(|x| x == &SignedLitteral::Constant(Sign::Positive))
    }
    pub fn is_false(&self) -> bool {
        self.iter().any(|x| match x {
            SignedLitteral::Constant(Sign::Negative) => true,
            SignedLitteral::Constant(Sign::Positive) => false,
            SignedLitteral::Val {
                litteral: l1,
                sign: s1,
            } => self.iter().any(|y| match y {
                SignedLitteral::Constant(Sign::Negative) => true,
                SignedLitteral::Constant(Sign::Positive) => false,
                SignedLitteral::Val {
                    litteral: l2,
                    sign: s2,
                } => l1 == l2 && s1 != s2,
            }),
        })
    }
}

#[derive(
    Debug, Clone, From, Hash, Eq, PartialEq, Deref, DerefMut, IntoIterator, AsRef, PartialOrd, Ord,
)]
pub struct Disjunction<T: LitteralTrait>(BTreeSet<SignedLitteral<T>>);

impl<T: Display + LitteralTrait> Display for Disjunction<T> {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(
            f,
            "{}",
            self.iter()
                .format_with(&format!(" {SYMBOL_OR_FANCY} "), |e, g| { g(e) })
        )
    }
}

impl<T: LitteralTrait> From<SignedLitteral<T>> for Disjunction<T> {
    fn from(value: SignedLitteral<T>) -> Self {
        BTreeSet::from([value]).into()
    }
}

impl<T: LitteralTrait> From<Litteral<T>> for Disjunction<T> {
    fn from(value: Litteral<T>) -> Self {
        SignedLitteral::from(value).into()
    }
}

impl<T: LitteralTrait> From<Sign> for Disjunction<T> {
    fn from(value: Sign) -> Self {
        SignedLitteral::from(value).into()
    }
}

#[derive(
    Debug, Clone, From, Eq, PartialEq, Deref, DerefMut, IntoIterator, AsRef, PartialOrd, Ord,
)]
pub struct DisjunctiveNormalForm<T: LitteralTrait>(BTreeSet<Conjunction<T>>);

impl<T: Display + LitteralTrait> Display for DisjunctiveNormalForm<T> {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(
            f,
            "{}",
            self.iter()
                .format_with(&format!(" {SYMBOL_OR_FANCY} "), |e, g| {
                    g(&format_args!("({e})"))
                })
        )
    }
}

impl<T: LitteralTrait> From<Conjunction<T>> for DisjunctiveNormalForm<T> {
    fn from(value: Conjunction<T>) -> Self {
        BTreeSet::from([value]).into()
    }
}

impl<T: LitteralTrait> From<Disjunction<T>> for DisjunctiveNormalForm<T> {
    fn from(value: Disjunction<T>) -> Self {
        value
            .into_iter()
            .map_into()
            .collect::<BTreeSet<Conjunction<T>>>()
            .into()
    }
}

impl<T: LitteralTrait> From<SignedLitteral<T>> for DisjunctiveNormalForm<T> {
    fn from(value: SignedLitteral<T>) -> Self {
        Conjunction::from(value).into()
    }
}

impl<T: LitteralTrait> From<Litteral<T>> for DisjunctiveNormalForm<T> {
    fn from(value: Litteral<T>) -> Self {
        Conjunction::from(value).into()
    }
}

impl<T: LitteralTrait> From<Sign> for DisjunctiveNormalForm<T> {
    fn from(value: Sign) -> Self {
        Conjunction::from(value).into()
    }
}

#[derive(
    Debug, Clone, From, Eq, PartialEq, Deref, DerefMut, IntoIterator, AsRef, PartialOrd, Ord,
)]
pub(super) struct ConjunctiveNormalForm<T: LitteralTrait>(BTreeSet<Disjunction<T>>);
impl<T: Display + LitteralTrait> Display for ConjunctiveNormalForm<T> {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(
            f,
            "{}",
            self.iter()
                .format_with(&format!(" {SYMBOL_AND_FANCY} "), |e, g| {
                    g(&format_args!("({e})"))
                })
        )
    }
}

impl<T: LitteralTrait> From<Disjunction<T>> for ConjunctiveNormalForm<T> {
    fn from(value: Disjunction<T>) -> Self {
        BTreeSet::from([value]).into()
    }
}

impl<T: LitteralTrait> From<Conjunction<T>> for ConjunctiveNormalForm<T> {
    fn from(value: Conjunction<T>) -> Self {
        value
            .into_iter()
            .map_into()
            .collect::<BTreeSet<Disjunction<T>>>()
            .into()
    }
}

impl<T: LitteralTrait> From<SignedLitteral<T>> for ConjunctiveNormalForm<T> {
    fn from(value: SignedLitteral<T>) -> Self {
        Disjunction::from(value).into()
    }
}

impl<T: LitteralTrait> From<Litteral<T>> for ConjunctiveNormalForm<T> {
    fn from(value: Litteral<T>) -> Self {
        Disjunction::from(value).into()
    }
}

impl<T: LitteralTrait> From<Sign> for ConjunctiveNormalForm<T> {
    fn from(value: Sign) -> Self {
        Disjunction::from(value).into()
    }
}

pub(super) trait Formula<T: LitteralTrait>: Clone {
    type AndTarget: Formula<T>;
    type NotTarget: Formula<T>;
    type OrTarget: Formula<T>;

    fn and<U: Into<Self> + Clone>(&self, rhs: &U) -> Self::AndTarget;
    fn or<U: Into<Self> + Clone>(&self, rhs: &U) -> Self::OrTarget;
    fn not(&self) -> Self::NotTarget;

    fn terms(&self) -> BTreeSet<T>;
}

impl<T: LitteralTrait> Formula<T> for Litteral<T> {
    type AndTarget = Conjunction<T>;
    type OrTarget = Disjunction<T>;
    type NotTarget = SignedLitteral<T>;

    fn or<U: Into<Self> + Clone>(&self, rhs: &U) -> Self::OrTarget {
        Self::OrTarget::from(BTreeSet::from([
            SignedLitteral::from(self.clone()),
            SignedLitteral::from(rhs.clone().into()),
        ]))
    }
    fn and<U: Into<Self> + Clone>(&self, rhs: &U) -> Self::AndTarget {
        Self::AndTarget::from(BTreeSet::from([
            SignedLitteral::from(self.clone()),
            SignedLitteral::from(rhs.clone().into()),
        ]))
    }
    fn not(&self) -> Self::NotTarget {
        Self::NotTarget::from(self.clone()).not()
    }
    fn terms(&self) -> BTreeSet<T> {
        match self {
            Litteral::Val(t) => BTreeSet::from([t.clone()]),
            Litteral::Constant(_) => BTreeSet::new(),
        }
    }
}

impl<T: LitteralTrait> Formula<T> for SignedLitteral<T> {
    type AndTarget = Conjunction<T>;
    type OrTarget = Disjunction<T>;
    type NotTarget = Self;

    fn not(&self) -> Self::NotTarget {
        match self {
            Self::Constant(sign) => <Sign as Formula<T>>::not(sign).into(),
            Self::Val { sign, litteral } => Self::Val {
                sign: <Sign as Formula<T>>::not(sign).into(),
                litteral: litteral.clone(),
            },
        }
    }
    fn or<U: Into<Self> + Clone>(&self, rhs: &U) -> Self::OrTarget {
        Self::OrTarget::from(BTreeSet::from([self.clone(), rhs.clone().into()]))
    }
    fn and<U: Into<Self> + Clone>(&self, rhs: &U) -> Self::AndTarget {
        Self::AndTarget::from(BTreeSet::from([self.clone(), rhs.clone().into()]))
    }

    fn terms(&self) -> BTreeSet<T> {
        match self {
            SignedLitteral::Constant(_) => BTreeSet::new(),
            SignedLitteral::Val { litteral, sign: _ } => BTreeSet::from([litteral.clone()]),
        }
    }
}

impl<T: LitteralTrait> Formula<T> for Conjunction<T> {
    type AndTarget = Self;
    type OrTarget = DisjunctiveNormalForm<T>;
    type NotTarget = Disjunction<T>;

    fn and<U: Into<Self> + Clone>(&self, rhs: &U) -> Self::AndTarget {
        self.union(rhs.clone().into().as_ref())
            .cloned()
            .collect::<BTreeSet<_>>()
            .into()
    }
    fn or<U: Into<Self> + Clone>(&self, rhs: &U) -> Self::OrTarget {
        BTreeSet::from([self.clone(), rhs.clone().into()]).into()
    }
    fn not(&self) -> Self::NotTarget {
        self.iter()
            .map(Formula::not)
            .collect::<BTreeSet<_>>()
            .into()
    }

    fn terms(&self) -> BTreeSet<T> {
        self.iter().flat_map(Formula::terms).collect()
    }
}

impl<T: LitteralTrait> Formula<T> for Disjunction<T> {
    type AndTarget = ConjunctiveNormalForm<T>;
    type OrTarget = Self;
    type NotTarget = Conjunction<T>;

    fn or<U: Into<Self> + Clone>(&self, rhs: &U) -> Self::OrTarget {
        self.union(rhs.clone().into().as_ref())
            .cloned()
            .collect::<BTreeSet<_>>()
            .into()
    }
    fn and<U: Into<Self> + Clone>(&self, rhs: &U) -> Self::AndTarget {
        BTreeSet::from([self.clone(), rhs.clone().into()]).into()
    }
    fn not(&self) -> Self::NotTarget {
        self.iter()
            .map(Formula::not)
            .collect::<BTreeSet<_>>()
            .into()
    }

    fn terms(&self) -> BTreeSet<T> {
        self.iter().flat_map(Formula::terms).collect()
    }
}

impl<T: LitteralTrait> Conjunction<T> {
    fn complete(&self, terms: &BTreeSet<T>) -> DisjunctiveNormalForm<T> {
        let conj_terms = self.terms();
        let to_add = terms.difference(&conj_terms).cloned().map(Litteral::from);

        to_add.fold(self.clone().into(), |prev, term| {
            DisjunctiveNormalForm::from(
                prev.into_iter()
                    .flat_map(|c| [c.and(&term), c.and(&term.not())])
                    .collect::<BTreeSet<_>>(),
            )
        })
    }
}

impl<T: LitteralTrait> Disjunction<T> {
    fn complete(&self, terms: &BTreeSet<T>) -> ConjunctiveNormalForm<T> {
        let disj_terms = self.terms();
        let to_add = terms.difference(&disj_terms).cloned().map(Litteral::from);

        to_add.fold(self.clone().into(), |prev, term| {
            ConjunctiveNormalForm::from(
                prev.into_iter()
                    .flat_map(|c| [c.or(&term), c.or(&term.not())])
                    .collect::<BTreeSet<_>>(),
            )
        })
    }
}

impl<T: LitteralTrait> DisjunctiveNormalForm<T> {
    fn cnf(&self) -> Option<ConjunctiveNormalForm<T>> {
        self.clone()
            .into_iter()
            .map(ConjunctiveNormalForm::from)
            .reduce(|l, r| l.or(&r))
    }

    pub fn full(&self) -> Self {
        let terms = self.terms();
        self.iter()
            .map(|c| c.complete(&terms))
            .reduce(|l, r| l.or(&r))
            .unwrap_or(BTreeSet::new().into())
    }
}
impl<T: LitteralTrait> ConjunctiveNormalForm<T> {
    fn dnf(&self) -> Option<DisjunctiveNormalForm<T>> {
        self.clone()
            .into_iter()
            .map(DisjunctiveNormalForm::from)
            .reduce(|l, r| l.and(&r))
    }
    pub fn full(&self) -> Self {
        let terms = self.terms();
        self.iter()
            .map(|c| c.complete(&terms))
            .reduce(|l, r| l.and(&r))
            .unwrap_or(BTreeSet::new().into())
    }
}

impl<T: LitteralTrait> Formula<T> for DisjunctiveNormalForm<T> {
    type NotTarget = Self;
    type AndTarget = Self;
    type OrTarget = Self;
    fn or<U: Into<Self> + Clone>(&self, rhs: &U) -> Self::OrTarget {
        self.union(rhs.clone().into().as_ref())
            .cloned()
            .collect::<BTreeSet<_>>()
            .into()
    }
    fn and<U: Into<Self> + Clone>(&self, rhs: &U) -> Self::AndTarget {
        let r: Self = rhs.clone().into();
        self.iter()
            .flat_map(|c| r.iter().map(|cr| cr.and(c)))
            .collect::<BTreeSet<_>>()
            .into()
    }
    fn not(&self) -> Self::NotTarget {
        ConjunctiveNormalForm::from(self.iter().map(Formula::not).collect::<BTreeSet<_>>())
            .dnf()
            .unwrap_or(Self::NotTarget::from(BTreeSet::new()))
    }
    fn terms(&self) -> BTreeSet<T> {
        self.iter().flat_map(Formula::terms).collect()
    }
}

impl<T: LitteralTrait> Formula<T> for ConjunctiveNormalForm<T> {
    type NotTarget = Self;
    type AndTarget = Self;
    type OrTarget = Self;
    fn or<U: Into<Self> + Clone>(&self, rhs: &U) -> Self::OrTarget {
        let r: Self = rhs.clone().into();
        self.iter()
            .flat_map(|c| r.iter().map(|cr| cr.or(c)))
            .collect::<BTreeSet<_>>()
            .into()
    }
    fn and<U: Into<Self> + Clone>(&self, rhs: &U) -> Self::AndTarget {
        self.union(rhs.clone().into().as_ref())
            .cloned()
            .collect::<BTreeSet<_>>()
            .into()
    }
    fn not(&self) -> Self::NotTarget {
        DisjunctiveNormalForm::from(self.iter().map(Formula::not).collect::<BTreeSet<_>>())
            .cnf()
            .unwrap_or(Self::NotTarget::from(BTreeSet::new()))
    }
    fn terms(&self) -> BTreeSet<T> {
        self.iter().flat_map(Formula::terms).collect()
    }
}