openvet-policy 0.6.0

//! Tree-shaped evaluation diagnostics.
//!
//! Walks an [`Expr`] against a claim-lookup function and produces an
//! [`ExplainNode`] tree carrying the [`Tri`] result at every node.
//! Every child is evaluated (no short-circuiting), so the tree
//! shows the complete reasoning for any input — at query scale the
//! cost is negligible and complete trees are far more useful than
//! the elided ones evaluation's short-circuit would produce.
//!
//! The tree's top-level [`ExplainNode::result`] always equals
//! [`crate::expr::evaluate`] on the same `(expr, lookup)` pair;
//! Kleene semantics are deterministic regardless of evaluation
//! order.
//!
//! Rendering (ASCII / colour / etc.) is a presentation concern and
//! lives in the consumer (currently `openvet query`); this crate
//! exposes only the structured shape.

use crate::expr::{Expr, Tri};

/// One node in the evaluation tree for an expression.
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct ExplainNode {
    /// What kind of expression node this row came from.
    pub label: ExplainLabel,
    /// The Kleene tri-state result for the sub-expression rooted
    /// here. Always agrees with `evaluate(expr, lookup)` for the
    /// corresponding sub-expression.
    pub result: Tri,
    /// Sub-rows beneath this node (one per AST child).
    pub children: Vec<ExplainNode>,
}

/// What an [`ExplainNode`]'s row should display as.
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum ExplainLabel {
    /// A leaf claim name; the row shows that name.
    Claim(String),
    /// A logical negation; the row shows "not" with the negated
    /// sub-expression as a child.
    Not,
    /// An n-ary conjunction; the row shows "all" with each
    /// conjunct as a child.
    All,
    /// An n-ary disjunction; the row shows "any" with each
    /// disjunct as a child.
    Any,
}

/// Walk `expr` against `lookup` and produce an [`ExplainNode`] tree
/// where every node carries its sub-result.
///
/// Children are evaluated eagerly, not short-circuited, so the tree
/// is complete regardless of operator semantics. The Kleene
/// combination at each branch matches [`crate::expr::evaluate`].
pub fn explain<F>(expr: &Expr, lookup: &F) -> ExplainNode
where
    F: Fn(&str) -> Tri,
{
    match expr {
        Expr::Claim(name) => ExplainNode {
            label: ExplainLabel::Claim(name.clone()),
            result: lookup(name),
            children: vec![],
        },
        Expr::Not(inner) => {
            let inner_node = explain(inner, lookup);
            let result = !inner_node.result;
            ExplainNode {
                label: ExplainLabel::Not,
                result,
                children: vec![inner_node],
            }
        }
        Expr::And(children) => {
            let kids: Vec<ExplainNode> = children.iter().map(|c| explain(c, lookup)).collect();
            let result = combine_and(kids.iter().map(|c| c.result));
            ExplainNode {
                label: ExplainLabel::All,
                result,
                children: kids,
            }
        }
        Expr::Or(children) => {
            let kids: Vec<ExplainNode> = children.iter().map(|c| explain(c, lookup)).collect();
            let result = combine_or(kids.iter().map(|c| c.result));
            ExplainNode {
                label: ExplainLabel::Any,
                result,
                children: kids,
            }
        }
    }
}

fn combine_and(iter: impl Iterator<Item = Tri>) -> Tri {
    let mut all_true = true;
    for t in iter {
        match t {
            Tri::False => return Tri::False,
            Tri::True => {}
            Tri::Unknown => all_true = false,
        }
    }
    if all_true { Tri::True } else { Tri::Unknown }
}

fn combine_or(iter: impl Iterator<Item = Tri>) -> Tri {
    let mut all_false = true;
    for t in iter {
        match t {
            Tri::True => return Tri::True,
            Tri::False => {}
            Tri::Unknown => all_false = false,
        }
    }
    if all_false { Tri::False } else { Tri::Unknown }
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::expr::parse;

    fn lookup_from<'a>(claims: &'a [(&'a str, bool)]) -> impl Fn(&str) -> Tri + use<'a> {
        move |name: &str| match claims.iter().find(|(n, _)| *n == name) {
            Some((_, true)) => Tri::True,
            Some((_, false)) => Tri::False,
            None => Tri::Unknown,
        }
    }

    #[test]
    fn claim_leaf() {
        let e = parse("foo").unwrap();
        let node = explain(&e, &lookup_from(&[("foo", true)]));
        assert_eq!(node.label, ExplainLabel::Claim("foo".into()));
        assert_eq!(node.result, Tri::True);
        assert!(node.children.is_empty());
    }

    #[test]
    fn flat_all_tree_for_and_chain() {
        let e = parse("a and b and c").unwrap();
        let node = explain(&e, &lookup_from(&[("a", true), ("b", true), ("c", false)]));
        assert_eq!(node.label, ExplainLabel::All);
        assert_eq!(node.result, Tri::False);
        assert_eq!(node.children.len(), 3);
        assert_eq!(node.children[2].result, Tri::False);
    }

    #[test]
    fn flat_any_tree_for_implies_or_chain() {
        // `a implies b or c` desugars + flattens to Or([Not(a), b, c]).
        let e = parse("a implies b or c").unwrap();
        let node = explain(&e, &lookup_from(&[("a", false), ("b", false), ("c", true)]));
        assert_eq!(node.label, ExplainLabel::Any);
        assert_eq!(node.result, Tri::True);
        assert_eq!(node.children.len(), 3);
        // First child is `Not(a)` → true (since a is false).
        assert_eq!(node.children[0].label, ExplainLabel::Not);
        assert_eq!(node.children[0].result, Tri::True);
        // The Not has its leaf child for `a` underneath.
        assert_eq!(node.children[0].children.len(), 1);
        assert_eq!(
            node.children[0].children[0].label,
            ExplainLabel::Claim("a".into())
        );
        assert_eq!(node.children[0].children[0].result, Tri::False);
    }

    #[test]
    fn top_level_result_agrees_with_evaluate() {
        // Spot-check that the tree's root carries the same result
        // as evaluate() across a few mixed-state assignments.
        let e = parse("(a and b) or (c and not d)").unwrap();
        for &assignment in &[
            &[("a", true), ("b", true)][..],
            &[("a", false), ("c", true), ("d", false)][..],
            &[("a", false), ("c", true), ("d", true)][..],
            &[("a", false), ("c", false)][..],
            &[][..],
        ] {
            let look = lookup_from(assignment);
            let node = explain(&e, &look);
            let direct = crate::expr::evaluate(&e, &look);
            assert_eq!(
                node.result, direct,
                "tree root vs evaluate disagreed for {assignment:?}"
            );
        }
    }
}