Propagate state names through ModuleContext's bind#1062
Open
nanavati wants to merge 2 commits into
Open
Conversation
A module expression can carry more than one state-naming layer: for
example, an explicit setStateName (or the one BSV's typechecker inserts
for bound instantiations) wrapped by a naming layer from a module
monad's bind. The PrimStateName handler re-heads the IStateLoc for
each layer -- a sibling of the previous stack, not a child -- so
instance naming collapses the layers and the innermost name wins. But
each handler also pushed one schedule-name-scope frame, leaving a stale
frame whose IStateLoc prefix the final rule names do not extend.
remIStateLocPrefix then poisons the frame's name map -- lazily, so the
internalError only fires if something forces the map, such as a
scheduling attribute that names a submodule rule, and only visibly when
the two layers carry different names (e.g. old-style instantiation
where the instance name differs from the binder).
Collapse the layers in pushModuleSchedNameScope too: a push that
re-names the still-open scope described by the frame on top of the
stack renames that frame in place (bumping its ignore count for the
extra pop) instead of stacking a second frame.
The push is a re-naming exactly when all of the following hold; each
condition is pinned by a counterexample in the testsuite:
- the new IStateLoc and the top frame's have equal tails: the same
parent position. A child scope's tail is the parent's full stack,
which is strictly longer, and a completed sibling's frame has
already been popped, so only a re-heading of the open scope can
present an equal tail;
- the tails are non-empty: primBuildModule scopes are fresh singleton
stacks and nest dynamically (the primitive is forced lazily, even
mid-rule), so two empty tails are two unrelated build-module scopes;
- the heads have the same isl_ifc_id: the same binding. The
PrimStateName handler preserves the ifc id when it re-heads the
stack, while a child that reaches the same tail (by escaping a
naming level) carries its own;
- the frame has no rules registered and no rule/interface elaboration
in progress: the scope's body has not begun. Rule names only reach
the map in addRules, after rule bodies elaborate, so the
elabProgress check covers immediate registration;
- no rules are saved for deferred registration: under moduleFix,
addRules only saves the rules and replays them after the body
finishes, so a saved rule is already named under the current prefix
while both frame-local checks pass -- renaming the frame would
orphan it.
Known limits, unchanged from the previous behavior (each crashes the
compiler identically before and after this change): user binders that
squat on the internal element names ("_elements"/"_velements") hijack
the IStateLoc classification and escape a naming level; and an
explicit setStateName directly around a primBuildModule scope stacks
rather than collapses (blocked by the non-empty-tail condition).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01BaLzQyHtX6CvXty92voyM8
State naming never worked for Classic (BH) code using ModuleContext or ModuleCollect: BSV's typechecker inserts a setStateName wrapper on every bound module statement, but Classic has no such insertion -- the name can only ride the monad's bind, and ModuleContext's bind dropped it. Registers bound in a Classic [ModuleCollect] module came out as "ec"/"ec_1" instead of "ec_count"/"ec_flag". Use the standard approach (see ReaderModule in the testsuite): bind extracts the continuation's parameter name with primGetParamName and wraps the bound computation in setStateName. For BSV code the typechecker's wrapper is still present, so one module now carries two stacked naming layers; the previous commit teaches the schedule name scope to collapse them. Tests: a Classic ModuleCollect naming test; the pong-distilled regression (old-style instantiation, where the instance name differs from the binder, plus an urgency attribute that forces the name maps); and pins for the collapse condition's non-empty-tail and same-ifc-id conjuncts (a nested primBuildModule, and a user binder squatting on the internal "_elements" name). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BaLzQyHtX6CvXty92voyM8
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
State naming never worked for Classic (BH) code using
ModuleContextorModuleCollect: BSV's typechecker inserts asetStateNamewrapper on every bound module statement, but Classic has no such insertion — the name can only ride the monad's bind, andModuleContext's bind dropped it. Registers bound in a Classic[ModuleCollect]module came out asec/ec_1instead ofec_count/ec_flag.Commit 1 — Collapse re-naming layers in the module schedule name scope. A module expression can carry more than one state-naming layer (an explicit
setStateName, or the BSV typechecker's inserted one, wrapped by a naming layer from a module monad's bind). Instance naming already collapses the layers (thePrimStateNamehandler re-heads theIStateLocper layer, innermost name wins), but each handler also pushed one schedule-name-scope frame, leaving a stale frame whoseIStateLocprefix the final rule names do not extend;remIStateLocPrefixthen poisons that frame's name map, and a scheduling attribute naming a submodule rule turns it into an internalError. The push now renames the still-open frame in place when it is a re-naming of that same scope; each conjunct of the re-naming condition is pinned by a counterexample test.Commit 2 — the fix itself.
ModuleContext's bind extracts the continuation's parameter name withprimGetParamNameand wraps the bound computation insetStateName(the standard approach; seeReaderModulein the testsuite). For BSV code the typechecker's wrapper is still present, so one module now carries two stacked naming layers — which commit 1 makes safe.Tests: a Classic
ModuleCollectnaming test; a pong-distilled regression (old-style instantiation where the instance name differs from the binder, plus an urgency attribute that forces the name maps); and pins for the collapse condition's non-empty-tail and same-ifc-id conjuncts (a nestedprimBuildModule, and a user binder squatting on the internal_elementsname).Known limits (unchanged behavior, crash identically before and after): user binders squatting on
_elements/_velements, and an explicitsetStateNamedirectly around aprimBuildModulescope.🤖 Generated with Claude Code
https://claude.ai/code/session_01QFFuSAof9Rp8Zye97fCpAG