Support include for libraries, to "merge" several libraries into one single namespace
#691
Comments
|
The following question may need to be spun off as a separate issue at some point: should we shift the focus of the F* standard list library from effectful to total functions? In other words, instead of having
|
|
Isn't it just a matter of having an |
|
I was expecting that this could be supported purely as a namespacing mechanism. If we have |
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.
|
|
tahina-pro
changed the title
export for libraries, to "merge" several libraries into one single namespaceinclude for libraries, to "merge" several libraries into one single namespace
|
In fact, the new branch taramana_include that I just pushed deprecates the old branch taramana_export, thanks to the name resolution improvements merged in pull request #772 . |
|
The branch taramana_include_seq, descending from taramana_include, illustrates the use of and all client code only uses |
|
@tahina-pro So can this be closed now? |
|
Done for sequences (see above) and also for lists ( Are there any further instances in the standard library where |
|
Closing this as suggested by @catalin-hritcu and now follow-up on @tahina-pro's question for further instances. |
Consider a series of libraries pertaining to a data structure, e.g. FStar.Seq and FStar.SeqProperties for finite sequences. Then, to use finite sequences in their programs, end users would have to explicitly import all libraries through:
open FStar.Seqopen FStar.SeqPropertiesIdeally, we would like to provide the user with a single library which would be enough for them to import, regardless of how and why the other underlying libraries are organized.
In our example, we would rename
FStar.SeqintoFStar.SeqBase, and we would like to provide the user with a singleFStar.Seqlibrary so thatopen FStar.Seqwould automatically importFStar.SeqBaseandFStar.SeqProperties. The contents ofFStar.Seqwould be something like:module FStar.Seqinclude FStar.SeqBaseinclude FStar.SeqPropertiesThis solution would be enough for the user to import all definitions of
FStar.SeqBaseandFStar.SeqPropertiesinto the unqualified namespace.(It would be actually similar to
Exportin Coq, to this respect, see for instanceZArithin the Coq standard library for mathematical integers.)However, what if the user wants to use both finite sequences and lists in their programs? In particular, what if the user wants to use
lengthandappendfrom bothFStar.SeqandFStar.List.Tot, and their associated lemmas? Then, the user will need to explicitly qualify their uses ofappendwith correct namespaces.In this case, the user will need to figure out that the
appendrelated to lists is actually defined inFStar.List.Tot, which is vulnerable to any refactoring of the underlying list libraries.Ideally we would like to define
FStar.Listso that the user can access the list-relatedappendusingFStar.List.append, regardless of which underlying library it is actually defined in.BEGIN DIGRESSION
In Coq, this is possible thanks to nested modules. For instance, for mathematical integers, one can do
Import ZArithwhich provides the user with aZnamespace giving access to all operators and lemmas related to mathematical integers, such asZ.add(addition) andZ.add_0_r(the fact that x+0=x.)In fact, this
Znamespace is made of two modules calledZ, one defined inBinIntDefand providingZ.add, and another defined inBinIntand providingZ.add_0_r.BinIntDefandBinIntare both exported byZArith.Now, if the user only wants to use mathematical integers, they can
Import ZArithandImport Zonce and getaddandadd_0_rboth in the unqualified namespace, sinceBinInt.ZhasInclude BinIntDef.Z.END DIGRESSION
Of course this is not currently possible in F*. So, we would like to have the proposed
includemechanism take care of this namespace issue as well, so that, renamingFStar.ListintoFstar.ListBaseand defining
FStar.Listas:module FStar.Listinclude FStar.List.Totinclude FStar.ListBaseinclude FStar.ListPropertiesThe text was updated successfully, but these errors were encountered: