Enum ModulePattern 

pub enum ModulePattern {
    RefinementSmartConstructor {
        scope: Option<String>,
        type_name: String,
        carrier_field: String,
        carrier_type: String,
        constructor_fn: String,
        param_name: String,
        predicate: Spanned<Expr>,
    },
    WrapperOverRecursion {
        wrapper_scope: Option<String>,
        wrapper_fn: String,
        inner_scope: Option<String>,
        inner_fn: String,
    },
    ResultPipelineChain {
        scope: Option<String>,
        fn_name: String,
        step_count: usize,
        step_fns: Vec<String>,
    },
    RendererFormatter {
        scope: Option<String>,
        fn_name: String,
    },
    MatchDispatcherFold {
        scope: Option<String>,
        fn_name: String,
        list_param: String,
    },
}

A ModulePattern is a recognized structural fact about a whole module’s surface — the level above per-fn archetypes — carrying the typed payload downstream consumers need to act on it.

The first variant is RefinementSmartConstructor, the canonical refinement-via-opaque shape (single-field record + validating smart constructor) the proof export already recognizes via crate::codegen::common::refinement_info_for. Stage 6 lifts the recognition into the analysis tier so other consumers (aver shape LSP, future inliner, monomorphizer) don’t each re-walk the AST to ask the same question.

Peer-review note from issue #232: “kind == SmartConstructor is too compressed to be source of truth for proof routing — proof needs typed payload”. This enum carries that payload (carrier field + type, constructor fn name, predicate expression).

Stage 6a (this commit) only detects the pattern; the proof export still walks via the legacy refinement_info_for API. Stage 6b refactors that fn into a thin adapter over ProgramShape::patterns. Stage 6c+ adds the next pattern (WrapperOverRecursion, ResultPipelineChain, …).

Variants

RefinementSmartConstructor

refinement-via-opaque shape: a single-field record T { <carrier_field>: <carrier_type> } paired with a validating smart constructor fn <constructor_fn>(<param_name>: <carrier_type>) -> Result<T, _> match <predicate> true -> Result.Ok(T(<carrier_field> = <param_name>)) false -> Result.Err("...")

Fields

scope: Option<String>

Where this pattern lives: None = entry items, Some(prefix) = dep module with that prefix. Lets the scope-aware adapter (refinement_info_for_in_scope) pick the predicate from the right module when two modules declare a refined record with the same bare name (e.g. A.Natural vs B.Natural).

type_name: String

Source-level type name ("Natural", "Positive", …). FnId / TypeId migration deferred — name keys match what the current refinement_info_for adapter uses.

carrier_field: String

Carrier-field name (e.g. "value"). Lean projects through .val on a Subtype; this is the field that gets renamed in the lifted view.

carrier_type: String

Carrier type annotation as written in the record field ("Int", "Float", …). Backends emit it as the subset’s underlying type.

constructor_fn: String

Source-level name of the smart constructor ("fromInt").

param_name: String

Parameter name on the smart constructor signature ("n" in fromInt(n: Int) -> Result<Natural, _>). Used when substituting the law’s quantified variable into the predicate.

predicate: Spanned<Expr>

Cloned bool predicate the smart constructor branches on — the body’s match <predicate> subject. Owned so ProgramShape doesn’t borrow source items.

WrapperOverRecursion

wrapper-over-recursion shape: a non-recursive wrapper_fn whose body’s only recursive call is to a self-recursive inner_fn living in the same scope, with inner_fn taking the wrapper’s parameters as a prefix (literally, as Ident args) plus at least one additional argument (typically an accumulator initial value). fib(n) -> fibTR(n, 0, 1) is the canonical example; aver fmt / proof export use this to route the wrapper through the inner’s induction certificate.

Conservative detection rules (stage 6c):

• wrapper is itself non-recursive (no self-call)
• exactly one inner call to a self-recursive same-scope fn
• every wrapper parameter appears literally (Ident) somewhere in the inner’s argument list
• inner’s arity is strictly greater than the wrapper’s arity

These rules keep false positives near zero on the shipped corpus; mutual recursion across fns isn’t claimed yet (inner_fn must self-recurse, not participate in a larger SCC).

Fields

wrapper_scope: Option<String>

Scope of the wrapper (None = entry, Some(prefix) = dep module). inner_scope is always equal to wrapper_scope in stage 6c — cross-module wrappers aren’t claimed.

wrapper_fn: String

Source-level wrapper fn name (the outer, non-recursive one).

inner_scope: Option<String>

Scope of the recursive inner fn. Mirrors wrapper_scope while stage 6c keeps this same-scope-only.

inner_fn: String

Source-level inner fn name (the recursive one).

ResultPipelineChain

?-propagating Result pipeline: a fn whose body is a sequence of let x = step()? bindings followed by a tail expression (typically Result.Ok(final)). Canonical example: examples/core/result_pipeline.av::validateAndCombine — six ? steps that short-circuit on the first Err.

Detection rules (stage 6d):

• fn return type starts with Result<
• body has at least two Stmt::Binding whose value is Expr::ErrorProp(...) (the ? operator)
• the tail stmt is an expression, not a binding

step_count is the number of ? bindings; downstream consumers can use it to size the staged result type or to pick between inlined and trampoline lowerings. No proof-export consumer yet — this is substrate-only.

Fields

scope: Option<String>

fn_name: String

step_count: usize

step_fns: Vec<String>

Source names of the step fns called via ? in body order. Captured here because the post-pipeline AST desugars ? into nested match arms — downstream consumers that need the original step list (e.g. the proof_lower ResultPipelineChain strategy) read from this field instead of re-walking.

RendererFormatter

Non-recursive pure renderer: a fn whose return type is String, effects list is empty, and body contains an InterpolatedStr or a String-typed + concatenation. Canonical examples are examples/data/rle.av::showRun (single interpolation) and the show* family in examples/data/fibonacci.av.

Detection rules (stage 6e):

• return type is exactly String
• effects list is empty
• fn does not call itself anywhere in its body
• body contains at least one Expr::InterpolatedStr or Expr::BinOp(Add, ..) reachable through nesting

Recursive structural renderers (showRuns, showListIntInner) are intentionally excluded — they belong to a future StructuralRenderer pattern paired with structural induction.

Fields

scope: Option<String>

fn_name: String

MatchDispatcherFold

Self-recursive structural fold over a List<T> parameter: fn body is a single match <param> with at minimum [] -> ... and [head, ..tail] -> ... arms, and the fn calls itself somewhere in its body (typically passing tail to recur). nthOrZero(xs, index) from examples/data/fibonacci.av is the canonical example.

Detection rules (stage 6f):

• body is a single Stmt::Expr(Match)
• subject is Ident(p) where p is one of the fn’s params
• arms include both Pattern::EmptyList and Pattern::Cons
• fn is self-recursive

Aver’s stdlib has no List.map/fold, so this hand-rolled structural fold shows up across the corpus. Recognizing it unlocks two future moves: list-induction proof obligation emission, and a deforestation rewrite that fuses the fold with its consumer.

Fields

scope: Option<String>

fn_name: String

list_param: String

Trait Implementations

impl Clone for ModulePattern

fn clone(&self) -> ModulePattern

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ModulePattern

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

Formats the value using the given formatter.