mod tests;

#[derive(Debug, Clone, Copy, PartialEq)]
pub enum Token {
    Negation,
    Conjunction,
    Disjunction,
    ExclusiveDisjunction,
    MaterialCondition,
    LogicalEquivalence,
}

#[derive(Debug, Clone, PartialEq)]
pub enum Node<T>
where
    T: Clone + std::fmt::Debug,
{
    Leaf(T),
    Unary {
        operator: Token,
        operand: Box<Node<T>>,
    },
    Binary {
        operator: Token,
        lhs: Box<Node<T>>,
        rhs: Box<Node<T>>,
    },
}

impl<T> Node<T>
where
    T: Clone + std::fmt::Debug,
{
    fn negation_conjunction_to_nnf(lhs: &Box<Node<T>>, rhs: &Box<Node<T>>) -> Node<T> {
        Node::Binary {
            operator: Token::Disjunction,
            lhs: Box::new(Node::Unary {
                operator: Token::Negation,
                operand: Box::new(*lhs.clone()),
            }),
            rhs: Box::new(Node::Unary {
                operator: Token::Negation,
                operand: Box::new(*rhs.clone()),
            }),
        }
    }

    fn negation_disjunction_to_nnf(lhs: &Box<Node<T>>, rhs: &Box<Node<T>>) -> Node<T> {
        Node::Binary {
            operator: Token::Conjunction,
            lhs: Box::new(Node::Unary {
                operator: Token::Negation,
                operand: Box::new(*lhs.clone()),
            }),
            rhs: Box::new(Node::Unary {
                operator: Token::Negation,
                operand: Box::new(*rhs.clone()),
            }),
        }
    }

    fn negation_material_condition_to_nnf(lhs: &Box<Node<T>>, rhs: &Box<Node<T>>) -> Node<T> {
        Node::Binary {
            operator: Token::Conjunction,
            lhs: Box::new(*lhs.clone()),
            rhs: Box::new(Node::Unary {
                operator: Token::Negation,
                operand: Box::new(*rhs.clone()),
            }),
        }
    }

    fn material_condition_to_nnf(lhs: &Box<Node<T>>, rhs: &Box<Node<T>>) -> Node<T> {
        Node::Binary {
            operator: Token::Disjunction,
            lhs: Box::new(Node::Unary {
                operator: Token::Negation,
                operand: Box::new(*lhs.clone()),
            }),
            rhs: Box::new(*rhs.clone()),
        }
    }

    fn negation_exclusive_disjunction_to_nnf(lhs: &Box<Node<T>>, rhs: &Box<Node<T>>) -> Node<T> {
        Node::Binary {
            operator: Token::Disjunction,
            lhs: Box::new(Node::Binary {
                operator: Token::Conjunction,
                lhs: Box::new(Node::Unary {
                    operator: Token::Negation,
                    operand: Box::new(*lhs.clone()),
                }),
                rhs: Box::new(Node::Unary {
                    operator: Token::Negation,
                    operand: Box::new(*rhs.clone()),
                }),
            }),
            rhs: Box::new(Node::Binary {
                operator: Token::Conjunction,
                lhs: Box::new(*lhs.clone()),
                rhs: Box::new(*rhs.clone()),
            }),
        }
    }

    fn exclusive_disjunction_to_nnf(lhs: &Box<Node<T>>, rhs: &Box<Node<T>>) -> Node<T> {
        Node::Binary {
            operator: Token::Conjunction,
            lhs: Box::new(Node::Binary {
                operator: Token::Disjunction,
                lhs: Box::new(*lhs.clone()),
                rhs: Box::new(*rhs.clone()),
            }),
            rhs: Box::new(Node::Binary {
                operator: Token::Disjunction,
                lhs: Box::new(Node::Unary {
                    operator: Token::Negation,
                    operand: Box::new(*lhs.clone()),
                }),
                rhs: Box::new(Node::Unary {
                    operator: Token::Negation,
                    operand: Box::new(*rhs.clone()),
                }),
            }),
        }
    }

    fn logical_equivalence_to_nnf(lhs: &Box<Node<T>>, rhs: &Box<Node<T>>) -> Node<T> {
        Node::Binary {
            operator: Token::Conjunction,
            lhs: Box::new(Node::Binary {
                operator: Token::Disjunction,
                lhs: Box::new(Node::Unary {
                    operator: Token::Negation,
                    operand: Box::new(*lhs.clone()),
                }),
                rhs: Box::new(*rhs.clone()),
            }),
            rhs: Box::new(Node::Binary {
                operator: Token::Disjunction,
                lhs: Box::new(Node::Unary {
                    operator: Token::Negation,
                    operand: Box::new(*rhs.clone()),
                }),
                rhs: Box::new(*lhs.clone()),
            }),
        }
    }

    fn negation_logical_equivalence_to_nnf(lhs: &Box<Node<T>>, rhs: &Box<Node<T>>) -> Node<T> {
        Node::Binary {
            operator: Token::Disjunction,
            lhs: Box::new(Node::Binary {
                operator: Token::Conjunction,
                lhs: Box::new(*lhs.clone()),
                rhs: Box::new(Node::Unary {
                    operator: Token::Negation,
                    operand: Box::new(*rhs.clone()),
                }),
            }),
            rhs: Box::new(Node::Binary {
                operator: Token::Conjunction,
                lhs: Box::new(*rhs.clone()),
                rhs: Box::new(Node::Unary {
                    operator: Token::Negation,
                    operand: Box::new(*lhs.clone()),
                }),
            }),
        }
    }

    pub fn simplify(&mut self) {
        match self {
            Node::Unary { operator, operand } if *operator == Token::Negation => match &**operand {
                Node::Unary {
                    operator: inner_op,
                    operand: inner_operand,
                } if *inner_op == Token::Negation => {
                    *self = *inner_operand.clone();
                    self.simplify();
                }
                Node::Binary {
                    operator: inner_op,
                    lhs: inner_lhs,
                    rhs: inner_rhs,
                } => {
                    *self = match *inner_op {
                        Token::Conjunction => {
                            Self::negation_conjunction_to_nnf(inner_lhs, inner_rhs)
                        }
                        Token::Disjunction => {
                            Self::negation_disjunction_to_nnf(inner_lhs, inner_rhs)
                        }
                        Token::ExclusiveDisjunction => {
                            Self::negation_exclusive_disjunction_to_nnf(inner_lhs, inner_rhs)
                        }
                        Token::LogicalEquivalence => {
                            Self::negation_logical_equivalence_to_nnf(inner_lhs, inner_rhs)
                        }
                        Token::MaterialCondition => {
                            Self::negation_material_condition_to_nnf(inner_lhs, inner_rhs)
                        }
                        _ => unreachable!(),
                    };
                    self.simplify();
                }
                _ => (),
            },
            Node::Binary {
                operator, lhs, rhs, ..
            } => {
                if let Some(node) = match *operator {
                    Token::ExclusiveDisjunction => {
                        Some(Self::exclusive_disjunction_to_nnf(lhs, rhs))
                    }
                    Token::LogicalEquivalence => Some(Self::logical_equivalence_to_nnf(lhs, rhs)),
                    Token::MaterialCondition => Some(Self::material_condition_to_nnf(lhs, rhs)),
                    _ => None,
                } {
                    *self = node.clone();
                    self.simplify();
                } else {
                    lhs.simplify();
                    rhs.simplify();
                }
            }
            _ => (),
        }
    }
}

impl Node<bool> {
    pub fn parse_formula(formula: &str) -> Node<bool> {
        let mut stack = vec![];
        for c in formula.chars() {
            match c {
                '0' => stack.push(Node::Leaf(false)),
                '1' => stack.push(Node::Leaf(true)),
                '!' => add_unary_node(&mut stack, Token::Negation),
                '&' => add_binary_node(&mut stack, Token::Conjunction),
                '|' => add_binary_node(&mut stack, Token::Disjunction),
                '^' => add_binary_node(&mut stack, Token::ExclusiveDisjunction),
                '>' => add_binary_node(&mut stack, Token::MaterialCondition),
                '=' => add_binary_node(&mut stack, Token::LogicalEquivalence),
                _ => panic!("Error: {} is not a valid character", c),
            }
        }
        stack.pop().unwrap()
    }

    pub fn ast_to_formula(ast: &Node<bool>) -> String {
        let mut str = String::from("");
        match ast {
            Node::Unary { operator, operand } => {
                str.push_str(Self::ast_to_formula(operand).as_str());
                str.push(token_to_char(*operator));
            }
            Node::Binary { operator, lhs, rhs } => {
                str.push_str(Self::ast_to_formula(lhs).as_str());
                str.push_str(Self::ast_to_formula(rhs).as_str());
                str.push(token_to_char(*operator));
            }
            Node::Leaf(b) => str.push(bool_to_char(*b)),
        };
        str
    }
}

impl Node<char> {
    pub fn parse_formula(formula: &str) -> Node<char> {
        let mut stack = vec![];
        for c in formula.chars() {
            match c {
                'A'..='Z' => stack.push(Node::Leaf(c)),
                '!' => add_unary_node(&mut stack, Token::Negation),
                '&' => add_binary_node(&mut stack, Token::Conjunction),
                '|' => add_binary_node(&mut stack, Token::Disjunction),
                '^' => add_binary_node(&mut stack, Token::ExclusiveDisjunction),
                '>' => add_binary_node(&mut stack, Token::MaterialCondition),
                '=' => add_binary_node(&mut stack, Token::LogicalEquivalence),
                _ => panic!("Error: {} is not a valid character", c),
            }
        }
        stack.pop().unwrap()
    }

    pub fn ast_to_formula(ast: &Node<char>) -> String {
        let mut str = String::from("");
        match ast {
            Node::Unary { operator, operand } => {
                str.push_str(Self::ast_to_formula(operand).as_str());
                str.push(token_to_char(*operator));
            }
            Node::Binary { operator, lhs, rhs } => {
                str.push_str(Self::ast_to_formula(lhs).as_str());
                str.push_str(Self::ast_to_formula(rhs).as_str());
                str.push(token_to_char(*operator));
            }
            Node::Leaf(c) => str.push(*c),
        };
        str
    }
}

pub fn add_unary_node<T>(stack: &mut Vec<Node<T>>, token: Token)
where
    T: Clone + std::fmt::Debug,
{
    let operand = Box::new(stack.pop().unwrap());
    stack.push(Node::Unary {
        operator: token,
        operand,
    });
}

pub fn add_binary_node<T>(stack: &mut Vec<Node<T>>, token: Token)
where
    T: Clone + std::fmt::Debug,
{
    let rhs = Box::new(stack.pop().unwrap());
    let lhs = Box::new(stack.pop().unwrap());
    stack.push(Node::Binary {
        operator: token,
        lhs,
        rhs,
    });
}

fn bool_to_char(b: bool) -> char {
    match b {
        false => '0',
        true => '1',
    }
}

fn token_to_char(token: Token) -> char {
    match token {
        Token::Negation => '!',
        Token::Conjunction => '&',
        Token::Disjunction => '|',
        Token::ExclusiveDisjunction => '^',
        Token::MaterialCondition => '>',
        Token::LogicalEquivalence => '=',
    }
}