Enum RecursionPlan 

pub enum RecursionPlan {
    IntCountdown {
        param_index: usize,
    },
    IntAscending {
        param_index: usize,
        bound: Spanned<Expr>,
    },
    LinearRecurrence2,
    ListStructural {
        param_index: usize,
    },
    SizeOfStructural,
    StringPosAdvance,
    MutualIntCountdown,
    MutualStringPosAdvance {
        rank: usize,
    },
    MutualSizeOfRanked {
        rank: usize,
    },
}

Classification for a single recursive fn (or a whole mutual-recursion SCC, in which case every fn in the SCC gets its own plan from the same family).

Eq is deliberately omitted — IntAscending holds an AST expression which only implements PartialEq (float literals inside it are partially ordered). PartialEq still works for the uses this enum sees (pattern matching, matches!, equality via .eq).

Variants

IntCountdown

Single-fn recursion where an Int parameter decreases by 1. The wrapper supplies n.natAbs + 1 fuel so the helper terminates.

Fields

param_index: usize

IntAscending

Single-fn recursion where an Int param increases by 1 up to a bound. The bound is kept as an Aver AST expression so each backend renders it in its own idiom; the wrapper supplies (bound - n).natAbs + 1 fuel.

Fields

param_index: usize

bound: Spanned<Expr>

LinearRecurrence2

Affine second-order recurrence like fib(n) = fib(n-1) + fib(n-2) with 0 / 1 bases and an n < 0 guard. Emitted through a private Nat helper (pair-state), not a fuel helper.

ListStructural

Single-fn structural recursion on a List<_> parameter; proof backends emit as structural recursion directly (no fuel).

Fields

param_index: usize

SizeOfStructural

Single-fn structural recursion on a recursive user ADT; proof backends emit through a sizeOf-guarded fuel helper.

StringPosAdvance

Single-fn recursion where the first String is preserved and the second Int position parameter strictly advances (pos + k, k ≥ 1). Wrapper fuel is derived from s.length - pos.

MutualIntCountdown

Mutual recursion SCC where the first Int parameter decreases by 1 across every inter-fn call.

MutualStringPosAdvance

Mutual recursion SCC where the first String is preserved and the second Int either advances or stays the same across rank-decreasing edges.

Fields

rank: usize

MutualSizeOfRanked

Generic mutual recursion SCC using sizeOf on structural parameters plus rank for same-measure edges.

Fields

rank: usize

Trait Implementations

impl Clone for RecursionPlan

fn clone(&self) -> RecursionPlan

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for RecursionPlan

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl PartialEq for RecursionPlan

fn eq(&self, other: &RecursionPlan) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for RecursionPlan