use crate::HostTypes;
pub trait BoundedRecursion<H: HostTypes> {
type DescentMeasure: DescentMeasure<H>;
fn measure(&self) -> &Self::DescentMeasure;
type BaseCase: BaseCase<H>;
fn base_case(&self) -> &Self::BaseCase;
type RecursiveCase: RecursiveCase<H>;
fn recursive_case(&self) -> &Self::RecursiveCase;
type Predicate: crate::kernel::predicate::Predicate<H>;
fn base_predicate(&self) -> &Self::Predicate;
type ComputationDatum: crate::user::morphism::ComputationDatum<H>;
fn recursion_body(&self) -> &Self::ComputationDatum;
fn initial_measure(&self) -> u64;
}
pub trait DescentMeasure<H: HostTypes> {
fn measure_value(&self) -> u64;
}
pub trait BaseCase<H: HostTypes>: crate::kernel::predicate::MatchArm<H> {}
pub trait RecursiveCase<H: HostTypes>: crate::kernel::predicate::MatchArm<H> {}
pub trait RecursiveStep<H: HostTypes> {
type Transform: crate::user::morphism::Transform<H>;
fn step_decomposition(&self) -> &Self::Transform;
type DescentMeasure: DescentMeasure<H>;
fn step_measure_pre(&self) -> &Self::DescentMeasure;
fn step_measure_post(&self) -> &Self::DescentMeasure;
}
pub trait RecursionTrace<H: HostTypes>: crate::bridge::trace::ComputationTrace<H> {}
pub trait StructuralRecursion<H: HostTypes>: BoundedRecursion<H> {}