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,
    },
    AccumulatorFold {
        scope: Option<String>,
        wrapper_fn: String,
        loop_fn: String,
        list_param: String,
        acc_param: String,
        step_fn: Option<String>,
        step_op: Option<BinOp>,
        finish_fn: Option<String>,
        driver_type: Option<String>,
        step_value_first: bool,
    },
}

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

AccumulatorFold

accumulator-fold shape: the role-bearing refinement of WrapperOverRecursion for a tail-recursive LIST fold. A non-recursive wrapper(xs) = loop(xs, neutral) whose loop is match list { [] -> finish(acc); h::t -> loop(t, step) }, where step is either a named fold fn step_fn(acc, h) or an inline binop acc <step_op> h, and the nil arm is either finish_fn(acc) or acc itself (finish_fn = None, an identity finish).

This is the single shape both the codec-roundtrip and the monoidal spec-equivalence proofs key on — the accumulator-generalization schema. Carrying the roles here lets BOTH the --discover lemma chains (codegen::lemma_discovery) and the normal-path ProofStrategy (codegen::proof_lower::detect_wrapper_over_recursion) read them from one recognizer instead of each re-walking the loop. fib(n) = fibTR(n, 0, 1) is a WrapperOverRecursion but NOT an AccumulatorFold (its inner recurs on an Int, not a match list), so the two patterns are distinct.

Fields

scope: Option<String>

wrapper_fn: String

loop_fn: String

list_param: String

acc_param: String

step_fn: Option<String>

Named fold step step_fn(acc, h), or None when the step is an inline binop (then step_op is set).

step_op: Option<BinOp>

Inline additive fold step acc <op> h, or None when the step is a named fn (then step_fn is set).

finish_fn: Option<String>

Nil-arm finishing fn finish_fn(acc), or None for an identity finish (the nil arm returns acc unchanged).

driver_type: Option<String>

None for the original List<_> structural fold. Some(ty) for a Peano-Nat countdown fold (match n { Z -> acc; S(m) -> loop(m, step) }) over the ADT named ty — factTR’s shape, where the step multiplies/adds the matched subject value rather than a list head. The two share the role-extraction but need different backend induction skeletons.

step_value_first: bool

For a Peano-Nat fold whose step is combine(subject, acc), true when the folded subject is the combine fn’s FIRST argument (mul(n, acc)), false for mul(acc, n). Ignored for List.

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.