Documentation for incremental module definitions#1087
Open
Gustavo2622 wants to merge 2 commits into
Open
Conversation
…ases
`module M' = B with {...}` re-rooted references using only the TOP path
of the base mpath, appending the reference's arguments to the
destination's. Consequences:
- a sub-module base P.O had every P-rooted reference re-rooted onto M':
the enclosing module's state (P.g -> M'.g) and even the sub-module's
own state (P.O.x -> M'.O.x) became dangling globals, silently changing
the program's semantics while remaining fully usable by the program
logics;
- a functor base F(A) whose body contains self-calls crashed the
elaborator (assertion failure in EcEnv.Fun.by_xpath): the self-call
F(A).h, unsuspended at A, was rewritten to M'(A).h with M' not a
functor.
The substitution entry now records the full base expression (top path,
arguments, inner path) and rewrites a reference iff it lies at or below
the base's inner path AND its arguments extend the base's (references
to program variables carry no arguments); the remainders are
transplanted onto the destination. Non-matching references (an
enclosing module's state, sibling sub-modules, other applications)
denote state that is not copied along with the base's items, and are
left untouched.
This makes updates of sub-modules (P.O), applied functors (F(A)), and
sub-modules of applied functors (F(A).O) all well-defined: the base's
items are copied, everything else is shared, and the application is
baked into the copy. Behavior for plain top-level bases and for
section-exit alias inlining is unchanged (empty argument and inner-path
components).
Also: reject abstract-module bases with a proper error instead of an
assertion, and add regression tests covering every base shape.
Adds doc/language/module-update.rst, documenting `module M' = M with
{...}`: syntax, the copy/share semantics, restrictions, and worked
examples (ghost-state instrumentation, statement and result rewrites,
loop edits, match-branch collapse, functor and sub-module updates).
The code-position language (shared by the program tactics and by module
updates) is factored out into its own page,
doc/language/code-positions.rst, which module-update.rst references.
The section on sub-module and applied-functor bases documents the
semantics introduced by the parent commit (sound module updates on
sub-module and applied-functor bases); its example is executable and
mirrors the regression tests in tests/module-update-bases.ec. This
change is meant to be merged after that fix.
Both pages are marked :orphan: until a language-reference toctree
lands.
Gustavo2622
force-pushed
the
doc-module-update
branch
from
July 24, 2026 11:27
c1e8d7b to
108648c
Compare
Gustavo2622
marked this pull request as ready for review
July 24, 2026 11:28
Member
|
Change the target branch to avoid the commit count failure. The target will automatically change when we merge the other PR. |
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
2 participants
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.
This adds documentation for the incremental / fine-grained module definition syntax / functionality.
It depends on #1086