raa_tt 0.9.1

use parol_runtime::log::{debug, trace};
use petgraph::{
    algo::all_simple_paths,
    dot::{Config, Dot},
    graph::NodeIndex,
    prelude::DiGraph,
    visit::DfsPostOrder,
};
use std::{
    cell::RefCell,
    fmt::{Display, Error, Formatter},
    vec,
};

use crate::{
    bi_implication::BiImplication,
    conjunction::Conjunction,
    disjunction::Disjunction,
    errors::{RaaError, Result},
    implication::Implication,
    negation::Negation,
    proposition::Proposition,
};

#[derive(Debug, Default, Clone, Copy, PartialEq, Eq)]
pub(crate) enum TransformationState {
    #[default]
    Unprocessed,
    Transformed,
    Closed,
}

impl Display for TransformationState {
    fn fmt(&self, f: &mut Formatter<'_>) -> std::result::Result<(), Error> {
        match self {
            TransformationState::Unprocessed => write!(f, "?"),
            TransformationState::Transformed => write!(f, "✓"),
            TransformationState::Closed => write!(f, "✖"),
        }
    }
}

// The nodes of our proposition tree are propositions paired with a transformation state to indicate
// whether a node has been processed already or whether the branch is closed.
pub(crate) type PropositionTree = DiGraph<(Proposition, TransformationState), ()>;

/// The outcome of the prover algorithm for a specific proposition
#[derive(Debug, Default, Clone, Copy, PartialEq, Eq)]
pub enum ProveResult {
    /// Default value
    /// Meaningless
    #[default]
    Undefined,

    /// Solve process is still ongoing
    Processing,

    /// *Tautology*
    /// The proposition is always TRUE independent from the values of its variables
    Proven,

    /// The propositions truth dependents on the values of its variables
    Contingent,

    /// *Contradiction*
    /// The proposition is always FALSE independent from the values of its variables
    Falsified,
}

impl Display for ProveResult {
    fn fmt(&self, f: &mut Formatter<'_>) -> std::result::Result<(), Error> {
        match self {
            ProveResult::Undefined => write!(f, "Undefined"),
            ProveResult::Processing => write!(f, "Processing"),
            ProveResult::Proven => write!(f, "Logically True"),
            ProveResult::Contingent => write!(f, "Contingent"),
            ProveResult::Falsified => write!(f, "Logically False"),
        }
    }
}

#[derive(Debug)]
pub struct Prover {
    root: RefCell<NodeIndex>,
}

impl Default for Prover {
    fn default() -> Self {
        Self {
            root: RefCell::new(NodeIndex::end()),
        }
    }
}

impl Prover {
    /// Creates a new instance of the Prover.
    ///
    /// This initializes the prover with an empty state, ready to analyze logical propositions
    /// using the analytic tableaux (truth tree) method.
    ///
    /// # Examples
    ///
    /// ```
    /// use raa_tt::prover::Prover;
    ///
    /// let prover = Prover::new();
    /// ```
    pub fn new() -> Self {
        Self::default()
    }

    /// Proves the logical validity of a proposition using the analytic tableaux (truth tree) method.
    ///
    /// This method implements a systematic proof technique that attempts to determine whether a
    /// logical proposition is a tautology (always true), contradiction (always false), or
    /// contingent (truth value depends on variable assignments).
    ///
    /// ## Algorithm Overview
    ///
    /// The truth tree method works by:
    /// 1. **Assumption**: Start by assuming the negation of the proposition to be proved
    /// 2. **Decomposition**: Systematically break down complex logical formulas into simpler components
    /// 3. **Branch Creation**: Create separate branches for disjunctive cases (OR-like operations)
    /// 4. **Contradiction Detection**: Look for contradictions (P and ¬P on the same branch)
    /// 5. **Closure**: Close branches that contain contradictions
    /// 6. **Result**: If all branches close, the original proposition is proven; otherwise it's contingent or false
    ///
    /// The method applies transformation rules for each logical operator:
    /// - **Conjunction (A ∧ B)**: Add both A and B to the current branch
    /// - **Disjunction (A ∨ B)**: Create two branches, one with A and one with B
    /// - **Implication (A → B)**: Create two branches, one with ¬A and one with B
    /// - **Biimplication (A ↔ B)**: Create two branches, one with A∧B and one with ¬A∧¬B
    /// - **Negation**: Apply De Morgan's laws and double negation elimination
    ///
    /// ## Complexity Analysis
    ///
    /// - **Time Complexity**: O(2^n) in the worst case, where n is the number of propositional variables.
    ///   This exponential behavior occurs because the algorithm may need to explore all possible
    ///   truth value assignments in pathological cases. However, many practical formulas can be
    ///   resolved much faster due to early contradiction detection.
    ///
    /// - **Space Complexity**: O(2^n) in the worst case for storing the tree structure. The depth
    ///   of the tree is bounded by the complexity of the formula, but the branching factor can
    ///   lead to exponential space usage in the worst case.
    ///
    /// ## Examples
    ///
    /// ### Proving a Tautology (Modus Ponens)
    /// ```
    /// use raa_tt::{
    ///     prover::{Prover, ProveResult},
    ///     proposition::Proposition,
    ///     conjunction::Conjunction,
    ///     implication::Implication,
    /// };
    ///
    /// // Prove: (P ∧ (P → Q)) → Q
    /// let prover = Prover::new();
    /// let proposition = Proposition::Implication(Implication {
    ///     left: Box::new(Proposition::Conjunction(Conjunction {
    ///         left: Box::new("P".into()),
    ///         right: Box::new(Proposition::Implication(Implication {
    ///             left: Box::new("P".into()),
    ///             right: Box::new("Q".into()),
    ///         })),
    ///     })),
    ///     right: Box::new("Q".into()),
    /// });
    ///
    /// let result = prover.prove(&proposition).unwrap();
    /// assert_eq!(result, ProveResult::Proven);
    /// ```
    ///
    /// ### Testing a Simple Proposition
    /// ```
    /// use raa_tt::{
    ///     prover::{Prover, ProveResult},
    ///     proposition::Proposition,
    ///     disjunction::Disjunction,
    ///     negation::Negation,
    /// };
    ///
    /// // Test: P ∨ ¬P (Law of Excluded Middle)
    /// let prover = Prover::new();
    /// let proposition = Proposition::Disjunction(Disjunction {
    ///     left: Box::new("P".into()),
    ///     right: Box::new(Proposition::Negation(Negation {
    ///         inner: Box::new("P".into()),
    ///     })),
    /// });
    ///
    /// let result = prover.prove(&proposition).unwrap();
    /// assert_eq!(result, ProveResult::Proven);
    /// ```
    ///
    /// ### Detecting a Contradiction
    /// ```
    /// use raa_tt::{
    ///     prover::{Prover, ProveResult},
    ///     proposition::Proposition,
    ///     conjunction::Conjunction,
    ///     negation::Negation,
    /// };
    ///
    /// // Test: P ∧ ¬P (contradiction)
    /// let prover = Prover::new();
    /// let proposition = Proposition::Conjunction(Conjunction {
    ///     left: Box::new("P".into()),
    ///     right: Box::new(Proposition::Negation(Negation {
    ///         inner: Box::new("P".into()),
    ///     })),
    /// });
    ///
    /// let result = prover.prove(&proposition).unwrap();
    /// assert_eq!(result, ProveResult::Falsified);
    /// ```
    ///
    /// ## Return Values
    ///
    /// - [`ProveResult::Proven`]: The proposition is a tautology (logically true)
    /// - [`ProveResult::Falsified`]: The proposition is a contradiction (logically false)
    /// - [`ProveResult::Contingent`]: The proposition's truth value depends on variable assignments
    ///
    /// ## Errors
    ///
    /// Returns [`RaaError`] if the proposition contains invalid or void expressions.
    ///
    /// [`ProveResult::Proven`]: crate::prover::ProveResult::Proven
    /// [`ProveResult::Falsified`]: crate::prover::ProveResult::Falsified
    /// [`ProveResult::Contingent`]: crate::prover::ProveResult::Contingent
    /// [`RaaError`]: crate::errors::RaaError
    pub fn prove(&self, proposition: &Proposition) -> Result<ProveResult> {
        let mut prove_result = self.try_prove(proposition, true)?;
        if prove_result == ProveResult::Contingent {
            prove_result = self.try_prove(proposition, false)?;
        }
        Ok(prove_result)
    }

    fn try_prove(&self, proposition: &Proposition, negated: bool) -> Result<ProveResult> {
        let mut prove_result = ProveResult::Processing;
        let mut graph = PropositionTree::new();
        self.init_proposition_tree(proposition, &mut graph, negated)?;
        while prove_result == ProveResult::Processing {
            trace!(
                "{}{:?}",
                if negated { "neg " } else { "" },
                Dot::with_attr_getters(
                    &graph,
                    &[Config::EdgeNoLabel, Config::NodeNoLabel],
                    &|_, _| { String::default() },
                    &|g, n| { format!("label = \"{} ({}, {})\"", g[n.0].0, n.0.index(), g[n.0].1) }
                )
            );
            prove_result = self.inner_prove(&mut graph, negated)?;
        }
        trace!(
            "{}{:?}",
            if negated { "neg " } else { "" },
            Dot::with_attr_getters(
                &graph,
                &[Config::EdgeNoLabel, Config::NodeNoLabel],
                &|_, _| { String::default() },
                &|g, n| { format!("label = \"{} ({}, {})\"", g[n.0].0, n.0.index(), g[n.0].1) }
            )
        );
        Ok(prove_result)
    }

    // We insert a (possibly negated) variant of our proposition and try to refute it later.
    fn init_proposition_tree(
        &self,
        proposition: &Proposition,
        graph: &mut PropositionTree,
        negate: bool,
    ) -> Result<()> {
        // The node id of the root is stored in `self.root`.
        *self.root.borrow_mut() = match proposition {
            Proposition::Void => Err(RaaError::VoidExpression)?,
            _ => graph.add_node((
                if negate {
                    Proposition::Negation(Negation {
                        inner: Box::new(proposition.clone()),
                    })
                } else {
                    proposition.clone()
                },
                TransformationState::default(),
            )),
        };
        Ok(())
    }

    fn transform(proposition: &Proposition) -> Result<(Vec<Proposition>, Vec<Proposition>)> {
        Ok(match proposition {
            Proposition::Void => Err(RaaError::VoidExpression)?,
            Proposition::Atom(a) => {
                debug!("Transfer Atom {a}");
                (vec![], vec![])
            }
            Proposition::Negation(n) => match &*n.inner {
                // Rule "Double negation"
                // A branch that contains a proposition in the form ¬¬A can be appended with A.
                Proposition::Negation(Negation { inner }) => {
                    debug!("Transfer double negation {n} =>");
                    debug!("    [{}]", inner);
                    debug!("    []");
                    (vec![(**inner).clone()], vec![])
                }
                // Rule "Negated biimplication"
                // A branch that contains a proposition in the form ¬(A <-> B) can be appended with
                // two new branches, one containing A and ¬B and one containing ¬A and B.
                Proposition::BiImplication(BiImplication { left, right }) => {
                    debug!("Transfer negated biimplication {n} =>");
                    debug!("    [{}, !{}]", left, right);
                    debug!("    [!{}, {}]", left, right);
                    (
                        vec![
                            (**left).clone(),
                            Proposition::Negation(Negation {
                                inner: Box::new((**right).clone()),
                            }),
                        ],
                        vec![
                            Proposition::Negation(Negation {
                                inner: Box::new((**left).clone()),
                            }),
                            (**right).clone(),
                        ],
                    )
                }
                // Rule "Negated implication"
                // A branch that contains a proposition in the form ¬(A -> B) can be appended
                // with A and ¬B.
                Proposition::Implication(Implication { left, right }) => {
                    debug!("Transfer negated implication {n} =>");
                    debug!("    [{}, !{}]", left, right);
                    debug!("    []");
                    (
                        vec![
                            (**left).clone(),
                            Proposition::Negation(Negation {
                                inner: Box::new((**right).clone()),
                            }),
                        ],
                        vec![],
                    )
                }
                // Rule "Negated disjunction"
                // A branch that contains a proposition in the form ¬(A ∨ B) can be appended
                // with ¬A and ¬B.
                Proposition::Disjunction(Disjunction { left, right }) => {
                    debug!("Transfer negated disjunction {n} =>");
                    debug!("    [!{}, !{}]", left, right);
                    debug!("    []");
                    (
                        vec![
                            Proposition::Negation(Negation {
                                inner: Box::new((**left).clone()),
                            }),
                            Proposition::Negation(Negation {
                                inner: Box::new((**right).clone()),
                            }),
                        ],
                        vec![],
                    )
                }
                // Rule "Negated conjunction"
                // A branch that contains a proposition in the form ¬(A ∧ B) can be appended
                // with two new branches ¬A and ¬B.
                Proposition::Conjunction(Conjunction { left, right }) => {
                    debug!("Transfer negated conjunction {n} =>");
                    debug!("    [!{}]", left);
                    debug!("    [!{}]", right);
                    (
                        vec![Proposition::Negation(Negation {
                            inner: Box::new((**left).clone()),
                        })],
                        vec![Proposition::Negation(Negation {
                            inner: Box::new((**right).clone()),
                        })],
                    )
                }
                // Otherwise no changes
                _ => (vec![], vec![]),
            },
            // Rule "Implication"
            // A branch that contains a proposition in the form A -> B can be appended with two
            // new branches ¬A and B.
            Proposition::Implication(Implication { left, right }) => {
                debug!("Transfer implication {proposition} =>");
                debug!("    [!{}]", left);
                debug!("    [{}]", right);
                (
                    vec![Proposition::Negation(Negation {
                        inner: Box::new((**left).clone()),
                    })],
                    vec![(**right).clone()],
                )
            }
            // Rule "BiImplication"
            // A branch that contains a proposition in the form A <-> B can be appended with two
            // new branches, one containing A and B and one containing ¬A and ¬B.
            Proposition::BiImplication(BiImplication { left, right }) => {
                debug!("Transfer biimplication {proposition} =>");
                debug!("    [{}, {}]", left, right);
                debug!("    [!{}, !{}]", left, right);
                (
                    vec![(**left).clone(), (**right).clone()],
                    vec![
                        Proposition::Negation(Negation {
                            inner: Box::new((**left).clone()),
                        }),
                        Proposition::Negation(Negation {
                            inner: Box::new((**right).clone()),
                        }),
                    ],
                )
            }
            // Rule "Disjunction"
            // A branch that contains a proposition in the form A ∨ B can be appended with two
            // new branches A and B.
            Proposition::Disjunction(Disjunction { left, right }) => {
                debug!("Transfer disjunction {proposition} =>");
                debug!("    [{}]", left);
                debug!("    [{}]", right);
                (vec![(**left).clone()], vec![(**right).clone()])
            }
            // Rule "Conjunction"
            // A branch that contains a proposition in the form A ∧ B can be appended with A and
            // B.
            Proposition::Conjunction(Conjunction { left, right }) => {
                debug!("Transfer conjunction {proposition} =>");
                debug!("    [{}, {}]", left, right);
                debug!("    []");
                (vec![(**left).clone(), (**right).clone()], vec![])
            }
        })
    }

    fn inner_prove(&self, graph: &mut PropositionTree, negated: bool) -> Result<ProveResult> {
        let mut changed = false;
        if let Some(unprocessed_node) = self.find_unprocessed_node(graph) {
            let (to_add_left, to_add_right) = Self::transform(&graph[unprocessed_node].0)?;
            let leafs_to_append = unclosed_leaf_nodes_of(graph, unprocessed_node);
            for leaf_node_id in leafs_to_append {
                let mut last_parent_node = leaf_node_id;
                for p in &to_add_left {
                    let new_node_id = graph.add_node((p.clone(), TransformationState::default()));
                    graph.add_edge(last_parent_node, new_node_id, ());
                    last_parent_node = new_node_id;
                }
                last_parent_node = leaf_node_id;
                for p in &to_add_right {
                    let new_node_id = graph.add_node((p.clone(), TransformationState::default()));
                    graph.add_edge(last_parent_node, new_node_id, ());
                    last_parent_node = new_node_id;
                }
            }
            graph[unprocessed_node].1 = TransformationState::Transformed;
            changed |= true;
        }
        if changed {
            self.update_branches_closed_state(graph)?;
        }
        self.check_all_branches_closed(graph, changed, negated)
    }

    fn update_branches_closed_state(&self, graph: &mut PropositionTree) -> Result<ProveResult> {
        let leaf_node_ids = leaf_nodes(graph);
        let mut leaf_nodes_to_close = vec![];
        for leaf_node_id in leaf_node_ids {
            let (_, transformation_state) = &graph[leaf_node_id];
            if *transformation_state == TransformationState::Closed {
                continue;
            }
            // We compare all nodes along the path from the root to this edge node with each other.
            let ancestors = self.ancestors(&*graph, leaf_node_id);
            let pairs = pairwise(&ancestors);
            if pairs.iter().any(|(i, j)| {
                let (a, _) = &graph[**i];
                let (b, _) = &graph[**j];
                match (a, b) {
                    (Proposition::Negation(n), _) => *n.inner == *b,
                    (_, Proposition::Negation(n)) => *n.inner == *a,
                    _ => false,
                }
            }) {
                leaf_nodes_to_close.push(leaf_node_id);
            }
        }
        for leaf_node_id in leaf_nodes_to_close {
            let (_, transformation_state) = &mut graph[leaf_node_id];
            *transformation_state = TransformationState::Closed;
        }
        Ok(ProveResult::Processing)
    }

    fn check_all_branches_closed(
        &self,
        graph: &PropositionTree,
        changed: bool,
        negated: bool,
    ) -> Result<ProveResult> {
        let leaf_node_ids = leaf_nodes(graph);
        let all_closed = leaf_node_ids
            .iter()
            .all(|i| graph[*i].1 == TransformationState::Closed);
        if all_closed {
            // This means all branches contain contradictions!
            Ok(if negated {
                // We used the negated proposition to refute it which indirectly proved it's truth.
                ProveResult::Proven
            } else {
                // We used the original proposition to refute it which directly falsified it.
                ProveResult::Falsified
            })
        } else if changed {
            // We need to continue until no branches can be developed anymore.
            Ok(ProveResult::Processing)
        } else {
            Ok(ProveResult::Contingent)
        }
    }

    fn ancestors(&self, graph: &PropositionTree, node_id: NodeIndex) -> Vec<NodeIndex> {
        let paths = all_simple_paths::<Vec<_>, _, std::hash::RandomState>(
            graph,
            *self.root.borrow(),
            node_id,
            0,
            None,
        )
        .collect::<Vec<_>>();
        // Tree constraint:
        // At most one path should exist from root to this end node.
        debug_assert!(paths.len() < 2, "length was {}", paths.len());
        if paths.is_empty() {
            vec![*self.root.borrow()]
        } else {
            // Path constraint:
            // The target node should be contained in the list of ancestors.
            debug_assert!(paths[0].contains(&node_id));
            paths[0].clone()
        }
    }

    fn find_unprocessed_node(&self, graph: &mut PropositionTree) -> Option<NodeIndex> {
        graph.node_indices().find(|i| {
            let node = &graph[*i];
            node.1 == TransformationState::Unprocessed
        })
    }
}

/// Generate pairs of elements in a slice without redundances.
fn pairwise<T>(v: &[T]) -> Vec<(&T, &T)> {
    let mut result = Vec::with_capacity(v.len());
    for (i, a) in v.iter().enumerate() {
        for b in v.iter().skip(i + 1) {
            result.push((a, b));
        }
    }
    result
}

fn leaf_nodes(graph: &PropositionTree) -> Vec<NodeIndex> {
    graph
        .node_indices()
        .filter(|i| graph.neighbors(*i).count() == 0)
        .collect::<Vec<NodeIndex>>()
}

fn unclosed_leaf_nodes_of(graph: &PropositionTree, start: NodeIndex) -> Vec<NodeIndex> {
    let mut dfs = DfsPostOrder::new(graph, start);
    let mut result = Vec::new();
    while let Some(i) = dfs.next(graph) {
        if graph[i].1 != TransformationState::Closed && graph.neighbors(i).count() == 0 {
            result.push(i)
        }
    }
    result
}

#[cfg(test)]
mod test {

    use crate::{
        conjunction::Conjunction,
        implication::Implication,
        proposition::Proposition,
        prover::{pairwise, ProveResult, Prover},
    };

    #[test]
    fn test_pairwise() {
        let v = vec!['i', 'j', 'k', 'l'];
        let pairs = pairwise(&v);
        assert_eq!(
            vec![
                (&'i', &'j'),
                (&'i', &'k'),
                (&'i', &'l'),
                (&'j', &'k'),
                (&'j', &'l'),
                (&'k', &'l')
            ],
            pairs
        );
    }

    #[test]
    fn test_solve() {
        // Logically True - Modus Ponens
        // p & (p -> q) -> q
        let proposition = Proposition::Implication(Implication {
            left: Box::new(Proposition::Conjunction(Conjunction {
                left: Box::new("p".into()),
                right: Box::new(Proposition::Implication(Implication {
                    left: Box::new("p".into()),
                    right: Box::new("q".into()),
                })),
            })),
            right: Box::new("q".into()),
        });
        assert_eq!(
            ProveResult::Proven,
            Prover::new().prove(&proposition).unwrap()
        );
    }
}