Trait SolverDelegateEvalExt

pub trait SolverDelegateEvalExt: SolverDelegate {
    // Required methods
    fn evaluate_root_goal(
        &self,
        goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>,
        span: <Self::Interner as Interner>::Span,
        stalled_on: Option<GoalStalledOn<Self::Interner>>,
    ) -> Result<GoalEvaluation<Self::Interner>, NoSolution>;
    fn root_goal_may_hold_with_depth(
        &self,
        root_depth: usize,
        goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>,
    ) -> bool;
    fn evaluate_root_goal_for_proof_tree(
        &self,
        goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>,
        span: <Self::Interner as Interner>::Span,
    ) -> (Result<(NestedNormalizationGoals<Self::Interner>, GoalEvaluation<Self::Interner>), NoSolution>, GoalEvaluation<Self::Interner>);
}

Required Methods

fn evaluate_root_goal( &self, goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>, span: <Self::Interner as Interner>::Span, stalled_on: Option<GoalStalledOn<Self::Interner>>, ) -> Result<GoalEvaluation<Self::Interner>, NoSolution>

Evaluates a goal from outside of the trait solver.

Using this while inside of the solver is wrong as it uses a new search graph which would break cycle detection.

fn root_goal_may_hold_with_depth( &self, root_depth: usize, goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>, ) -> bool

Check whether evaluating goal with a depth of root_depth may succeed. This only returns false if the goal is guaranteed to not hold. In case evaluation overflows and fails with ambiguity this returns true.

This is only intended to be used as a performance optimization in coherence checking.

fn evaluate_root_goal_for_proof_tree( &self, goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>, span: <Self::Interner as Interner>::Span, ) -> (Result<(NestedNormalizationGoals<Self::Interner>, GoalEvaluation<Self::Interner>), NoSolution>, GoalEvaluation<Self::Interner>)

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors

impl<D, I> SolverDelegateEvalExt for D

where D: SolverDelegate<Interner = I>, I: Interner,