pub trait Delegate {
    type Cx: Cx;
    type ProofTreeBuilder: ProofTreeBuilder<Self::Cx>;

    const FIXPOINT_STEP_LIMIT: usize;

    // Required methods
    fn recursion_limit(cx: Self::Cx) -> usize;
    fn initial_provisional_result(
        cx: Self::Cx,
        kind: CycleKind,
        input: <Self::Cx as Cx>::Input,
    ) -> <Self::Cx as Cx>::Result;
    fn reached_fixpoint(
        cx: Self::Cx,
        kind: UsageKind,
        input: <Self::Cx as Cx>::Input,
        provisional_result: Option<<Self::Cx as Cx>::Result>,
        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 step_is_coinductive(cx: Self::Cx, input: <Self::Cx as Cx>::Input) -> bool;
}

Required Associated Types§

Required Associated Constants§

Required Methods§

source

fn recursion_limit(cx: Self::Cx) -> usize

source

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

source

fn reached_fixpoint( cx: Self::Cx, kind: UsageKind, input: <Self::Cx as Cx>::Input, provisional_result: Option<<Self::Cx as Cx>::Result>, result: <Self::Cx as Cx>::Result, ) -> bool

source

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

source

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

source

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

Object Safety§

This trait is not object safe.

Implementors§