pr4xis 0.22.0

use super::action::Action;
use super::precondition::Precondition;
use super::trace::{Trace, TraceEntry};
use crate::logic::proof::{Counterexample, Verdict};

/// Error returned by `Engine::next()`.
#[derive(Debug)]
pub enum EngineError<A: Action> {
    /// Preconditions blocked the action.
    Violated {
        engine: Engine<A>,
        violations: Vec<Box<dyn Counterexample>>,
    },
    /// Preconditions passed but apply contradicted them — ontological inconsistency.
    /// The counterexample describes the apply failure.
    LogicalError {
        engine: Engine<A>,
        counterexample: Box<dyn Counterexample>,
    },
}

/// The enforcement engine — applies actions to situations with precondition checking.
///
/// Implements the `.next()` pattern with back/forward history:
/// ```text
/// let engine = Engine::new(initial_situation, preconditions, apply_fn);
/// let engine = engine.next(action1)?;   // validates + applies
/// let engine = engine.next(action2)?;   // validates + applies
/// let engine = engine.back()?;          // undo
/// let engine = engine.forward()?;       // redo
/// engine.trace()                         // full history (typed Trace<A>)
/// ```
#[allow(clippy::type_complexity)]
pub struct Engine<A: Action> {
    situation: A::Sit,
    past: Vec<A::Sit>,
    future: Vec<A::Sit>,
    preconditions: Vec<Box<dyn Precondition<A>>>,
    apply_fn: Box<dyn Fn(&A::Sit, &A) -> Result<A::Sit, Box<dyn Counterexample>>>,
    trace: Trace<A>,
}

impl<A: Action> core::fmt::Debug for Engine<A> {
    fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
        f.debug_struct("Engine")
            .field("situation", &self.situation)
            .field("step", &self.step())
            .field("back_depth", &self.back_depth())
            .field("forward_depth", &self.forward_depth())
            .field("trace_entries", &self.trace.entries().len())
            .finish()
    }
}

impl<A: Action> Engine<A> {
    /// Create a new engine with an initial situation, preconditions, and apply function.
    pub fn new(
        situation: A::Sit,
        preconditions: Vec<Box<dyn Precondition<A>>>,
        apply_fn: impl Fn(&A::Sit, &A) -> Result<A::Sit, Box<dyn Counterexample>> + 'static,
    ) -> Self {
        Self {
            situation,
            past: Vec::new(),
            future: Vec::new(),
            preconditions,
            apply_fn: Box::new(apply_fn),
            trace: Trace::new(),
        }
    }

    /// Current step number (derived from history depth).
    pub fn step(&self) -> usize {
        self.past.len()
    }

    /// The current situation.
    pub fn situation(&self) -> &A::Sit {
        &self.situation
    }

    /// The full trace of all actions.
    pub fn trace(&self) -> &Trace<A> {
        &self.trace
    }

    /// Apply an action — the `.next()` method.
    ///
    /// Checks all preconditions. If any return `Err` (Counterexample),
    /// returns `EngineError::Violated`. If all pass but apply fails,
    /// returns `EngineError::LogicalError` carrying the apply
    /// counterexample. Both variants return the engine for rollback.
    #[allow(clippy::result_large_err)]
    pub fn next(mut self, action: A) -> Result<Self, EngineError<A>> {
        let situation_before = self.situation.clone();
        let step = self.step();

        // Check all preconditions — each returns a typed Verdict (#161).
        let verdicts: Vec<Verdict> = self
            .preconditions
            .iter()
            .map(|p| p.check(&self.situation, &action))
            .collect();

        // Collect violations (the counterexamples). A Verdict is Err → violation.
        let any_violation = verdicts.iter().any(|v| v.is_err());

        if any_violation {
            // Re-check to move out the counterexamples — verdicts above
            // is borrowed in the filter; simplest is to re-run.
            let rechecked: Vec<Verdict> = self
                .preconditions
                .iter()
                .map(|p| p.check(&self.situation, &action))
                .collect();
            let violations: Vec<Box<dyn Counterexample>> =
                rechecked.into_iter().filter_map(|v| v.err()).collect();

            self.trace.record(TraceEntry {
                step,
                situation_before,
                action,
                precondition_verdicts: verdicts,
                situation_after: None,
            });
            return Err(EngineError::Violated {
                engine: self,
                violations,
            });
        }

        // Apply the action.
        match (self.apply_fn)(&self.situation, &action) {
            Ok(new_situation) => {
                self.trace.record(TraceEntry {
                    step,
                    situation_before,
                    action,
                    precondition_verdicts: verdicts,
                    situation_after: Some(new_situation.clone()),
                });

                self.past.push(self.situation.clone());
                self.future.clear();
                self.situation = new_situation;
                Ok(self)
            }
            Err(counterexample) => {
                self.trace.record(TraceEntry {
                    step,
                    situation_before,
                    action,
                    precondition_verdicts: verdicts,
                    situation_after: None,
                });
                Err(EngineError::LogicalError {
                    engine: self,
                    counterexample,
                })
            }
        }
    }

    /// Go back one step. The current situation moves to the redo stack.
    pub fn back(mut self) -> Result<Self, Self> {
        match self.past.pop() {
            Some(previous) => {
                self.future.push(self.situation.clone());
                self.situation = previous;
                Ok(self)
            }
            None => Err(self),
        }
    }

    /// Go forward one step (redo). Only available after back().
    pub fn forward(mut self) -> Result<Self, Self> {
        match self.future.pop() {
            Some(next) => {
                self.past.push(self.situation.clone());
                self.situation = next;
                Ok(self)
            }
            None => Err(self),
        }
    }

    /// How many steps back are available.
    pub fn back_depth(&self) -> usize {
        self.past.len()
    }

    /// How many steps forward are available (after back).
    pub fn forward_depth(&self) -> usize {
        self.future.len()
    }
}