implies/
prop.rs

1use super::formula::Formula;
2use super::parser::Match;
3pub use super::symbol::Atom;
4use super::symbol::{Symbol, Symbolic};
5use enum_iterator::Sequence;
6#[cfg(feature = "python")]
7use pyo3::pyclass;
8use std::fmt::Display;
9
10/// The negation operator, nothing super remarkable here.
11#[derive(PartialEq, Eq, PartialOrd, Ord, Debug, Clone, Copy, Hash, Default, Sequence)]
12#[cfg_attr(feature = "python", pyclass)]
13pub enum PropUnary {
14    #[default]
15    Not,
16}
17
18impl Display for PropUnary {
19    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
20        match self {
21            PropUnary::Not => write!(f, "¬"),
22        }
23    }
24}
25
26impl Symbolic for PropUnary {}
27
28impl Match for PropUnary {
29    fn match_str(s: &str) -> Option<Self> {
30        match s {
31            "¬" | "!" | "~" | "not" => Some(Self::Not),
32            _ => None,
33        }
34    }
35
36    fn get_matches(&self) -> Vec<String> {
37        match self {
38            PropUnary::Not => vec![
39                "¬".to_string(),
40                "!".to_string(),
41                "~".to_string(),
42                "not".to_string(),
43            ],
44        }
45    }
46}
47
48/// Deriving `PartialOrd` and `Ord` on this enum means that, by ordering the
49/// fields in increasing order of precedence, no other work has to be done
50/// to make sure the relative precedence of operators is understood.
51#[derive(Sequence, PartialEq, Eq, PartialOrd, Ord, Debug, Clone, Copy, Hash, Default)]
52#[cfg_attr(feature = "python", pyclass)]
53pub enum PropBinary {
54    Iff,
55    #[default]
56    Implies,
57    Or,
58    And,
59}
60
61impl Display for PropBinary {
62    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
63        match self {
64            PropBinary::Iff => write!(f, " ↔ "),
65            PropBinary::Implies => write!(f, " → "),
66            PropBinary::And => write!(f, " ∧ "),
67            PropBinary::Or => write!(f, " ∨ "),
68        }
69    }
70}
71
72impl Symbolic for PropBinary {}
73
74impl Match for PropBinary {
75    fn match_str(s: &str) -> Option<Self> {
76        match s {
77            "<->" | "↔" | "iff" => Some(Self::Iff),
78            "->" | "→" | "implies" => Some(Self::Implies),
79            "\\/" | "∨" | "or" => Some(Self::Or),
80            "/\\" | "∧" | "and" => Some(Self::And),
81            _ => None,
82        }
83    }
84
85    fn get_matches(&self) -> Vec<String> {
86        match self {
87            PropBinary::Iff => vec!["<->".to_string(), "↔".to_string(), "iff".to_string()],
88            PropBinary::Implies => vec!["->".to_string(), "→".to_string(), "implies".to_string()],
89            PropBinary::Or => vec!["\\/".to_string(), "∨".to_string(), "or".to_string()],
90            PropBinary::And => vec!["/\\".to_string(), "∧".to_string(), "and".to_string()],
91        }
92    }
93}
94
95/// Alias for the propositional instantiation of `Formula`.
96pub type PropFormula = Formula<PropBinary, PropUnary, Atom>;
97pub type PropSymbol = Symbol<PropBinary, PropUnary, Atom>;
implies/prop.rs

implies/
prop.rs
