-
Notifications
You must be signed in to change notification settings - Fork 73
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Spec sequential visibility for globals #420
Conversation
document/core/valid/modules.rst
Outdated
\frac{ | ||
C \vdashglobal \global_1 : \X{gt}_1 | ||
\qquad | ||
C, \CGLOBALS~\X{gt}_1 \vdashglobalseq \global^\ast : \X{gt}^\ast |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Since context extension was originally defined with labels in mind, it prepends the new items to the relevant index space in the context, but here we want to append the new global to the end of the index space. It seems we need to define separate notations for prepending and appending extension, or else define a convention that extension prepends for labels and appends for everything else.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ah, yes, good catch. I'll probably redesign that at some point, but for now I'm using \compose
instead here.
document/core/valid/modules.rst
Outdated
@@ -802,8 +833,7 @@ The :ref:`external types <syntax-externtype>` classifying a module may contain f | |||
However, this recursion is just a specification device. | |||
All types needed to construct :math:`C` can easily be determined from a simple pre-pass over the module that does not perform any actual validation. | |||
|
|||
Globals, however, are not recursive and not accessible within :ref:`constant expressions <valid-const>` when they are defined locally. | |||
The effect of defining the limited context :math:`C'` for validating certain definitions is that they can only access functions and imported globals and nothing else. | |||
Globals, however, are not recursive but eveluated sequentially, such that each :ref:`constant expressions <valid-const>` only has access to imported or priviously defined globals. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Globals, however, are not recursive but eveluated sequentially, such that each :ref:`constant expressions <valid-const>` only has access to imported or priviously defined globals. | |
Globals, however, are not recursive but evaluated sequentially, such that each :ref:`constant expressions <valid-const>` only has access to imported or previously defined globals. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM beyond those comments.
@tlively, PTAL. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should we briefly describe what \compose means in the conventions section? Other than that, LGTM.
It's already described there. ;) |
Also, add a couple of respective test cases.