1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97

use super::formula::Formula;
use super::parser::Match;
pub use super::symbol::Atom;
use super::symbol::{Symbol, Symbolic};
use enum_iterator::Sequence;
#[cfg(feature = "python")]
use pyo3::pyclass;
use std::fmt::Display;

/// The negation operator, nothing super remarkable here.
#[derive(PartialEq, Eq, PartialOrd, Ord, Debug, Clone, Copy, Hash, Default, Sequence)]
#[cfg_attr(feature = "python", pyclass)]
pub enum PropUnary {
    #[default]
    Not,
}

impl Display for PropUnary {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            PropUnary::Not => write!(f, "¬"),
        }
    }
}

impl Symbolic for PropUnary {}

impl Match for PropUnary {
    fn match_str(s: &str) -> Option<Self> {
        match s {
            "¬" | "!" | "~" | "not" => Some(Self::Not),
            _ => None,
        }
    }

    fn get_matches(&self) -> Vec<String> {
        match self {
            PropUnary::Not => vec![
                "¬".to_string(),
                "!".to_string(),
                "~".to_string(),
                "not".to_string(),
            ],
        }
    }
}

/// Deriving `PartialOrd` and `Ord` on this enum means that, by ordering the
/// fields in increasing order of precedence, no other work has to be done
/// to make sure the relative precedence of operators is understood.
#[derive(Sequence, PartialEq, Eq, PartialOrd, Ord, Debug, Clone, Copy, Hash, Default)]
#[cfg_attr(feature = "python", pyclass)]
pub enum PropBinary {
    Iff,
    #[default]
    Implies,
    Or,
    And,
}

impl Display for PropBinary {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            PropBinary::Iff => write!(f, " ↔ "),
            PropBinary::Implies => write!(f, " → "),
            PropBinary::And => write!(f, " ∧ "),
            PropBinary::Or => write!(f, " ∨ "),
        }
    }
}

impl Symbolic for PropBinary {}

impl Match for PropBinary {
    fn match_str(s: &str) -> Option<Self> {
        match s {
            "<->" | "↔" | "iff" => Some(Self::Iff),
            "->" | "→" | "implies" => Some(Self::Implies),
            "\\/" | "∨" | "or" => Some(Self::Or),
            "/\\" | "∧" | "and" => Some(Self::And),
            _ => None,
        }
    }

    fn get_matches(&self) -> Vec<String> {
        match self {
            PropBinary::Iff => vec!["<->".to_string(), "↔".to_string(), "iff".to_string()],
            PropBinary::Implies => vec!["->".to_string(), "→".to_string(), "implies".to_string()],
            PropBinary::Or => vec!["\\/".to_string(), "∨".to_string(), "or".to_string()],
            PropBinary::And => vec!["/\\".to_string(), "∧".to_string(), "and".to_string()],
        }
    }
}

/// Alias for the propositional instantiation of `Formula`.
pub type PropFormula = Formula<PropBinary, PropUnary, Atom>;
pub type PropSymbol = Symbol<PropBinary, PropUnary, Atom>;