'Modul(term)' -> 'Modul.(term)' ; 'Dcon.prm' -> 'Dcon?.prm', 'is_Dcon' -> 'Dcon?' ; improved name resolution #772
Conversation
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
The goal of this syntax change is to ensure that, for any name
of the form Namespace.ident or Namespace.Name, the Namespace part
is always a valid module name (except if Namespace.Name is itself
the name of a module.)
So far, this property was not holding for the following two
cases:
- many occurrences of Some.v to project the formal parameter v
of an option value that is known to be Some;
Formally, whenever an inductive type t is defined:
type t = | Datacon : param: u -> t | ...
then, for any value vt : t {is_Datacon v} , it is valid to
use (Datacon.param vt), of type u, to extract the value of
the formal parameter.
This introduces a spurious dependency on a hypothetical
module called Some (and a clash if any Some module is
reachable from open namespaces.)
- STATE.pre, STATE.post, and other effect members, similarly
introducing spurious dependencies on a hypothetical STATE
module.
As mentioned, the main consequence of those data constructor and
effect namespaces not being true modules are spurious dependency
generation and potential clashes with modules. I claim that this
current situation also gets in the way of any improvement on
name resolution, e.g. potential support for `include', currently
being discussed as `export' at:
#691
Thus, we need to introduce new syntax to change these
data constructor projector and effect member notations.
While I arbitrarily chose .. for testing purposes, discussions
about the final concrete syntax are still ongoing at:
http://doodle.com/poll/enadrtwqb6vhu2tr
However, independently of the actual choice for concrete syntax,
this syntax change implies the following deeper changes:
1. The projector for a formal parameter of a data constructor
has been renamed, both internally and on the extracted code.
Previously, Datacon.param was added as a fully qualified
name for the corresponding projector. To avoid clashes with
name resolution in open namespaces, it is now renamed as
__proj__Datacon__item__param
We could have used the reserved prefix uu___ (defined as
reserved_prefix in src/basic/ident.fs), but using such
prefix actually makes the verification of
examples/preorders/MRefHeap.fst fail when replaying hints,
for an unknown reason so far.
2. The fields of a record have been renamed similarly in
extracted code.
This is for two reasons. First, a record field is treated in
the same way as a formal parameter of a data constructor,
for internal purposes. In particular, given the following
record type:
type reco = { field: unit; ... }
the elaborator actually turned any field access of the form
expr.field intro (Mk_reco.field expr) where Mk_reco is the
name of the data constructor created by transforming the
record type into an inductive type, and so Mk_reco.field was
exactly the data constructor projector for the 'field'
formal parameter of the Mk_reco (unique) data constructor.
We preserve this elaboration as a projector, but now using
the new projector name instead.
However, the second reason is that, since such projector
calls are turned back to field accesses in extracted ML code,
we do not want to rely on the extracted language's shadowing
mechanism (for two different record types in the same module,
each of which having a field with the same name in both),
and so we use our field renaming as a way to resolve any such
shadowing in advance.
3. The fields (pre, post, reflect, return, bind, and actions)
of an effect have been renamed similarly, both internally
and in extracted code.
In this process, we took extra care to preserve the monad scope
while defining the members and actions of an effect, in such
a way that those names need not be qualified by the effect name
while being defined. However, once defined, such a member is
now required to be qualified with its MonadName.. instead of
MonadName. In particular, this new mechanism now forbids
`open Monad' ---opening the namespace of a monad to access its
members through unqualified names outside of the monad
definition. Fortunately, this happens nowhere in any examples.
The main purpose of these renamings is to guarantee that, for any
global definition whose fully qualified name is of the shape
Namespace.ident, Namespace is now always a valid module, which
was not the case until now for data constructor projectors and
effect fields.
Needed by 'make -C src test', namely 'make -C examples/unit-tests sall', more exactly examples/unit-tests/Unit1.Basic.fst
…te"" This reverts commit 5e2138d.
…na_projectors Remaining conflicts on compiler files were solved by automatically regenerating them.
Now, scopes are handled more intuitively, very much like OCaml: local opens really shadow previous local definitions, etc. The elaborator now relies on a cleaner implementation for name resolution in src/parser/env.fs, based on keeping one single list with all declarations interleaved, instead of keeping separate lists for local definitions, recursive definitions, open namespaces and module abbrevs. Thus, this commit also fixes some spurious shadowings, which were missed in some examples. This commit heavily relies on the fact that, whenever a name of the form Namespace.ident shows up, Namespace is always the name of a valid module (not an effect or a data constructor). So, now, Namespace is first separately resolved as a module, then the definition is looked up into the given module. This commit currently allows module name resolution at open, let open, and module abbrevs, but I claim that this can be easily changed and reverted to the previous behavior of requiring fully qualified module names.
Reported by failing builds 2411 to 2413
…mana_local_open Conflicts: src/parser/parse.fsi src/parser/parse.fsy Resolved as "take theirs" (discard conflicting changes coming from taramana_local_open).
…na_projectors Conflicts: src/ocaml-output/FStar_Parser_AST.ml src/parser/parse.fsi src/parser/parse.fsy Resolved as "take theirs" (discard taramana_projectors) ***NO_CI***
…mana_local_open
…mana_local_open Conflicts resolved by regenerating the parser using: make -C src/ocaml-output parser
***CI***
…mana_local_open
into taramana_projectors Conflicts: doc/tutorial/code/solutions/Ex11a.fst.hints examples/low-level/crypto/Buffer.Utils.fst.hints examples/low-level/crypto/Crypto.AEAD.AES256GCM.fst.hints examples/low-level/crypto/Crypto.AEAD.Encoding.fst.hints examples/low-level/crypto/Crypto.AEAD.Invariant.fst.hints examples/low-level/crypto/Crypto.AEAD.Lemmas.fst.hints examples/low-level/crypto/Crypto.AEAD.fst.hints examples/low-level/crypto/Crypto.Symmetric.AES.fst.hints examples/low-level/crypto/Crypto.Symmetric.Bytes.fst.hints examples/low-level/crypto/Crypto.Symmetric.GCM.fst.hints examples/low-level/crypto/Crypto.Symmetric.GF128.fst.hints examples/low-level/crypto/Crypto.Symmetric.PRF.fst.hints examples/low-level/crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part3.fst.hints examples/low-level/crypto/Crypto.Symmetric.Poly1305.Bignum.fst.hints examples/low-level/crypto/Crypto.Symmetric.Poly1305.Spec.fst.hints examples/low-level/crypto/Crypto.Symmetric.Poly1305.fst.hints ulib/FStar.Math.Lib.fst.hints Resolved by discarding taramana_projectors in favor of master (git checkout --theirs) ***CI***
At this point, Crypto.AEAD.Lemmas succeeds, but Ex07c still fails. In fact, Ex07c succeeds if hints are disabled altogether, but even if hints are produced when disabled (yielding the .hints file as reflected in this commit), rechecking Ex07c with them ultimately fails, for an unknown reason so far.
…StarLang/FStar into taramana_discriminators
This reverts commit 3826b71.
…g/FStar into taramana_name_resolution Conflicts: - *.hints: --theirs - *.ml: make -C src ocaml - *.fst: manual edits
Now, 'open M' for module M again requires that M be fully qualified, or a module abbrev, and 'module A = M' requires that M be fully qualified.
49 tasks
***CI***
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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 long-awaited pull request introduces invasive, non-backwards-compatible syntax changes, as announced in #770.
Namespace (term)becomesNamespace.(term)(similarly to OCaml, restores pull request Syntax change: 'Modul term' -> 'Modul.(term)', parsed as 'let open Modul in term' #757 that was reverted because of the PLDI deadline)Datacon.parambecomesDatacon?.paramEffect.actionbecomesEffect?.action(and similarly forreflect, etc.)is_DataconbecomesDatacon?The goal of these syntax changes is to introduce an invariant in name resolution: for any identifier (except module names) of the form
Namespace.ident,Namespaceshall always be a valid module name (in particular, it can no longer be a data constructor or effect name). This pull request introduces an improved name resolution with this invariant.The improved name resolution mechanism brought by this pull request now honors shadowing in a more intuitive way, similarly to OCaml. Thus, in the following example:
In the above example,
ywill have value 18, sincexnow takes the value ofA.xas expected, instead of the local variablex, as was the case previously.NOTE: This may break existing code with
let open FStar.UInt32and the like, which will shadown, sincenis defined in such integer library modules.These improvements are necessary to implement long-awaited enhancements (upcoming, not yet included in this pull request):
includefor libraries, to "merge" several libraries into one single namespace #691)