Trait Delegate

pub trait Delegate {
    type Cx: Cx;
    type ValidationScope;
    type ProofTreeBuilder;

    const ENABLE_PROVISIONAL_CACHE: bool;
    const FIXPOINT_STEP_LIMIT: usize;
    const DIVIDE_AVAILABLE_DEPTH_ON_OVERFLOW: usize;

    // Required methods
    fn enter_validation_scope(
        cx: Self::Cx,
        input: <Self::Cx as Cx>::Input,
    ) -> Option<Self::ValidationScope>;
    fn inspect_is_noop(inspect: &mut Self::ProofTreeBuilder) -> bool;
    fn initial_provisional_result(
        cx: Self::Cx,
        kind: PathKind,
        input: <Self::Cx as Cx>::Input,
    ) -> <Self::Cx as Cx>::Result;
    fn is_initial_provisional_result(
        cx: Self::Cx,
        kind: PathKind,
        input: <Self::Cx as Cx>::Input,
        result: <Self::Cx as Cx>::Result,
    ) -> bool;
    fn on_stack_overflow(
        cx: Self::Cx,
        inspect: &mut Self::ProofTreeBuilder,
        input: <Self::Cx as Cx>::Input,
    ) -> <Self::Cx as Cx>::Result;
    fn on_fixpoint_overflow(
        cx: Self::Cx,
        input: <Self::Cx as Cx>::Input,
    ) -> <Self::Cx as Cx>::Result;
    fn is_ambiguous_result(result: <Self::Cx as Cx>::Result) -> bool;
    fn propagate_ambiguity(
        cx: Self::Cx,
        for_input: <Self::Cx as Cx>::Input,
        from_result: <Self::Cx as Cx>::Result,
    ) -> <Self::Cx as Cx>::Result;
    fn step_is_coinductive(cx: Self::Cx, input: <Self::Cx as Cx>::Input) -> bool;
}

Required Associated Constants

const ENABLE_PROVISIONAL_CACHE: bool

Whether to use the provisional cache. Set to false by a fuzzer when validating the search graph.

const FIXPOINT_STEP_LIMIT: usize

const DIVIDE_AVAILABLE_DEPTH_ON_OVERFLOW: usize

Required Associated Types

type Cx: Cx

type ValidationScope

type ProofTreeBuilder

Required Methods

fn enter_validation_scope( cx: Self::Cx, input: <Self::Cx as Cx>::Input, ) -> Option<Self::ValidationScope>

Returning Some disables the global cache for the current goal.

The ValidationScope is used when fuzzing the search graph to track for which goals the global cache has been disabled. This is necessary as we may otherwise ignore the global cache entry for some goal G only to later use it, failing to detect a cycle goal and potentially changing the result.

fn inspect_is_noop(inspect: &mut Self::ProofTreeBuilder) -> bool

fn initial_provisional_result( cx: Self::Cx, kind: PathKind, input: <Self::Cx as Cx>::Input, ) -> <Self::Cx as Cx>::Result

fn is_initial_provisional_result( cx: Self::Cx, kind: PathKind, input: <Self::Cx as Cx>::Input, result: <Self::Cx as Cx>::Result, ) -> bool

fn on_stack_overflow( cx: Self::Cx, inspect: &mut Self::ProofTreeBuilder, input: <Self::Cx as Cx>::Input, ) -> <Self::Cx as Cx>::Result

fn on_fixpoint_overflow( cx: Self::Cx, input: <Self::Cx as Cx>::Input, ) -> <Self::Cx as Cx>::Result

fn is_ambiguous_result(result: <Self::Cx as Cx>::Result) -> bool

fn propagate_ambiguity( cx: Self::Cx, for_input: <Self::Cx as Cx>::Input, from_result: <Self::Cx as Cx>::Result, ) -> <Self::Cx as Cx>::Result

fn step_is_coinductive(cx: Self::Cx, input: <Self::Cx as Cx>::Input) -> bool

Object Safety

This trait is not object safe.

Implementors