pub struct ProgramShape {
pub per_fn: HashMap<FnId, FnRecognition>,
pub sccs: HashSet<FnId>,
pub patterns: Vec<ModulePattern>,
pub inductable_sum_types: HashSet<String>,
}Expand description
Whole-program shape facts produced by analyze_program.
Stage 4 of issue #232 (0.23 “Shape”). This is the recognition
substrate every downstream consumer reads from — aver shape CLI,
proof_lower’s strategy router, future inliner / monomorphizer.
Stage 6 will grow patterns: Vec<ModulePattern> and
relations: Vec<FnRelation> next to per_fn for the higher-arity
recognitions (WrapperOverRecursion, RefinementSmartConstructor,
ResultPipelineChain, …).
Computed once per compilation per the peer-review note (“compute ProgramShape once per compilation / per HIR snapshot — don’t persistent-cache per FnId yet”). Threaded as a read-only borrow from the call site; the analysis tier never mutates it.
Fields§
§per_fn: HashMap<FnId, FnRecognition>Per-fn recognition keyed by stable FnId.
sccs: HashSet<FnId>Multi-node SCC participants in the local call graph. Kept here so consumers don’t have to recompute Tarjan to ask “is this fn part of a mutual-recursion group?”.
patterns: Vec<ModulePattern>Whole-module typed patterns (stage 6 of #232). Populated by
analyze_program_with_modules; analyze_program leaves
this empty since it only sees the resolved-fn snapshot, not
the source items needed to detect module-level shapes like
RefinementSmartConstructor.
inductable_sum_types: HashSet<String>Source-level sum type names that are eligible as induction
targets: directly self-referential in at least one variant
and not indirectly recursive through nested generics the
per-variant emit can’t case-split (e.g. Some(List<Self>)).
Mirrors proof_lower::detect_induction_target’s inline
scan so the detector can read this set instead of
re-walking type defs.
Implementations§
Source§impl ProgramShape
impl ProgramShape
Sourcepub fn for_fn(&self, fn_id: FnId) -> Option<&FnRecognition>
pub fn for_fn(&self, fn_id: FnId) -> Option<&FnRecognition>
Recognition for one fn by id. Returns None for fns that
weren’t included in the call to analyze_program (e.g. an
out-of-tree id or a stale lookup against a refreshed view).
Trait Implementations§
Source§impl Clone for ProgramShape
impl Clone for ProgramShape
Source§fn clone(&self) -> ProgramShape
fn clone(&self) -> ProgramShape
1.0.0 (const: unstable) · Source§fn clone_from(&mut self, source: &Self)
fn clone_from(&mut self, source: &Self)
source. Read more