Struct StructuralRecursion 

pub struct StructuralRecursion {
    pub block: MutualBlock,
    pub recursive_args: HashMap<Name, Vec<usize>>,
}

Encoder for structurally recursive definitions.

Transforms structurally recursive definitions into applications of the recursor (eliminator) for the decreasing argument’s type.

Fields

block: MutualBlock

The mutual block being processed

recursive_args: HashMap<Name, Vec<usize>>

For each function, which argument indices are recursive

Implementations

impl StructuralRecursion

pub fn new(block: MutualBlock) -> Self

Create a new structural recursion encoder.

pub fn detect_structural_recursion(&mut self) -> Result<(), MutualElabError>

Detect which arguments are structurally decreasing.

pub fn encode_as_recursor_application( &self, ) -> Result<MutualBlock, MutualElabError>

Encode the structural recursion as recursor applications.

In a full implementation, this would replace each recursive function with an application of the appropriate recursor/eliminator.

pub fn get_recursive_args(&self) -> &HashMap<Name, Vec<usize>>

Get the detected recursive arguments.

Trait Implementations

impl Clone for StructuralRecursion

fn clone(&self) -> StructuralRecursion

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for StructuralRecursion

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

Formats the value using the given formatter.