Expand description
Auto-generated module
🤖 Generated with SplitRS
Structs§
- EtaCanon
Map - Eta canonicalization: maps expression ids to their canonical eta-normal form.
- EtaCategorizer
- Batch eta-categorization results.
- EtaChange
Entry - EtaChange
Log - A change log for an eta-normalization session.
- EtaDepth
Tracker - Tracks depth of eta-expansion nesting.
- EtaEquality
Oracle - A simple equality oracle for eta-normal forms.
- EtaExpanded
- Eta-expanded form: a record constructed from its own projections.
- EtaGraph
- A dependency graph tracking which expressions depend on eta-normal forms.
- EtaLong
Checker - Checks eta-long status for a set of expressions.
- EtaNorm
RunSummary - Summary for a completed eta-normalization run.
- EtaNormal
Form Checker - Checks whether an expression is in eta-normal form for a given structure.
- EtaNormalization
Pass - A worklist-based eta-normalization pass.
- EtaPass
Config - Configuration for an eta-normalization pass.
- EtaPass
Result - Final result of running the eta normalization pass.
- EtaRedex
- An occurrence of an eta-redex within a larger expression.
- EtaRedex
Collector - Collects all eta-redexes found during a traversal.
- EtaReduction
- An eta-reduction opportunity: a constructor applied to its own projections.
- EtaRewrite
Engine - A simple eta rewrite engine that applies a set of rules iteratively.
- EtaState
Machine - Eta-expansion state machine for iterative expansion.
- EtaStats
- Counts eta-expansion and reduction events for instrumentation.
- EtaUnification
Hint - A struct-eta unification hint: suggests which struct to eta-expand to unify.
- Field
Bounds Checker - Validates that field access indices are in-bounds for a structure.
- Field
Descriptor - A record field descriptor for eta-expansion analysis.
- Injectivity
Checker - Structural injectivity analysis: can a constructor be distinguished by its arguments?
- KReduction
Table - Maps structure names to their singleton-K reduction status.
- Projection
Descriptor - A structure projection descriptor mapping projector name to field index.
- Projection
Rewrite - A projection normalization rewrite: projector applied to constructor.
- Projection
Rewrite Set - A set of projection rewrite rules for a kernel.
- Record
Update - A record update: replace one field of a structure expression.
- Record
Update Batch - Accumulates record updates to be applied in a batch.
- Shape
Equivalence - A simple structural equivalence oracle based on shape matching.
- SingletonK
Reducer - Performs K-like reduction on singleton types.
- Struct
Flattening Pass - A pass that flattens nested structure constructor applications.
- Structure
Def - Structure
Eta - Performs η-expansion for structure (record) types.
- Structure
Registry - Registry of structure types and their fields.
Enums§
- Coherence
Result - A structural coherence check result.
- EtaCategory
- Categorizes expressions by their structural type for eta purposes.
- EtaChange
Kind - EtaLong
Status - Represents whether an expression is in eta-long normal form.
- Struct
Shape - Represents the shape of a structure expression for comparison.