The current documentation regarding imports, scoping, and loading (in SAWScript) is both lacking and out of date.
* Import, Load, and Scope
** Thoughts re scope; terminology
- notions/terms
- scope :: the scope of variable (in terms of a point in Cryptol source)
- per four namespaces
- what's in scope at a point in Cryptol module
- point in SAWScript module
- bindees :: the set of (qualified) names we add to scope with binders
- let, bind, import, magic-Cryptolmodule-bind
- context/? ::
- ? the env at the top-level of a module
- ? : the env at a given point of a module
- in Cryptol, we can only *move* the focus (between modules and submodules).
- standard scoping concepts in Cryptol
- the importer: gets names that a module exports.
- non-standard scoping concepts in Cryptol
- submodules are special, reference to can be private/public
- if we have reference to a submodule, we can import it (in
Cryptol, in SAWScript)
** Explaining scope in SAWScript
Note that at the Cryptol command line, one cannot create an
environment that does not correspond to a point in the source code,
due to the command line only allowing one module (or submodule) to be
in focus.
- Alternatives
A. SAWScript works like Cryptol *command line*:
- one module/submodule is *the* focus (not two)
B. SAWScript imports work exactly the same as in Cryptol *code*
- we have access to public submodules
- we can access *public* elements of these submodules with =::=
- we can extend the Env with =import submodule SM=
- just the public, cannot see private
C. Like approach B., but the imports include the private vars
- the env added is
- the "top-level env" of the imported module
- thus top-level privates in =M= are added
- we can access *public* elements of these submodules with =::=
- DESIGN CHOICES
A. we work as if all the "private" annotations did not exist.
- for any any all imports,
- and future =import submodule= *NIY*
(this is not absolutely necessary as we can always access anything
with qualifiers).
B. we have some further granularity wrt exposing "private"
A. each import can choose Pub/All.
- =import submodule= does not have this choice
B. As A, but =import submodule= might have "PRIVATE TOO"
C. we have a different mechanism for referencing private vars
SAWScript is different /by design/:
- Two values may not overlap in their scope at any one place in the
code. But we may want to use or relate these values together in
SAWScript. SAWScript allows use to do this /without/ having to
create an ad hoc Cryptol module for creating a scope where both
values are in scope.
- Thus the simplicity of Cryptol's =:focus <MODULE>= is not desirable.
We choose alternative C, design choice A.
** Current (new branch) behavior
- In SAWScript there are two ways to bring Cryptol modules into scope:
the =import= command and the =cryptol_load= command.
- =import=
- works like an =import= inside a Cryptol program (and it shares
identical *?* syntax), except that all "private annotations" are
ignored.
- Note that it doesn't work identically to =:load= in Cryptol:
- where an environment is created that is identical to the
top-level environment in the loaded Cryptol module, thus
- private definitions (and submodules) at top-level are visible
- private definitions inside submodules are *not* visible,
unless we change to focus to that submodule with =:focus=
- is a SAWScript construct, not a CLI command
- the syntax is *TODO...*
- can only appear at the top-level
- as with Cryptol
- we can qualify multiple modules to the same name
- we can import duplicate [qualified] names without error (the error only
comes when we try to reference one of those names)
- =cryptol_load=
: String -> TopLevel CryptolModule
- it parses, loads, and translates the file (as import does)
- it is a command, can *...*
- *UNLESS* you bind the value, this is effectively a NOP (except
for printing a summary display).
- the magic occurs when you do this (at the top level)
: M <- cryptol_load "M.cry"
- (If not done at the top level, results might be wrong or
unintuitive [?]: a little unclear as to what's happening
here.)
- The magic occurs anytime you bind a value of type
=CryptolModule= at the top-level (with "<-" or "let")
- useful for the (only) other way to create =CryptolModule=:
: cryptol_prims : () -> CryptolModule
- This will
- bind "M" as a SAWScript value of type `CryptolModule` (of course)
- Extend the Cryptol environment with the given module
where the contents of the module are all qualified with "M".
- i.e., *TODO...*
- Using the =M : CryptolModule= SAWScript value
- you can view the public names of "M.cry" with print
(i.e., the default show function for `CryptolModule`
- you can `cryptol_extract` the definitions in it thus
: cryptol_extract M "d2"
this works just as if one had written
: return {{M::d2}}
** Current (branch) compared to previous behavior (on master)
- Changes :: =cryptol_load=:
- *Previously*
- given this
: A <- cryptol_load "A.cry" -- A::** are added to {{A::**}}
: A <- cryptol_load "A2.cry" -- A2:** are added to {{A::**}}
- the `A` in 2nd line would shadow the first `A`.
- for each symbol 's' from A2.cry:
- 's' may shadow any duplicate symbol 's' from `A.cry`
- and it would also
- leave symbols from A.cry in the Cryptol environment, i.e.,
{{A::*}}.
- *NOW*,
- given this
: A <- cryptol_load "A.cry" -- A::** are added to {{A::**}}
: A <- cryptol_load "A2.cry" -- A2:** are added to {{A::**}}
- works identical to
: import "A.cry" as A
: import "A2.cry" as A
- thus,
- no shadowing occurs
- importing ambiguous symbols is allowed
- referring to ambiguous (qualified) symbols is an error.
- : A <- cryptol_load "A2.cry" --
- accessing =A= in SAWScript gives us "A2.cry"
- Changes ::
- cryptol_export is defined in terms of ={{A::name}}=, thus no more
gratuitous differences.
- OLD behavior
- import put privates in scope (as it does now)
- private var in submodules: N/A
- =cryptol_load= did not put top-level privates in scope
- =cryptol_export= cannot not access privates
** Future
- [ ] getting rid of the /magic-CryptolModule-bind/
- [ ] doing import and being able to view!
: x <- qimport <...same as import>
: addtoscope x ...
The Need
The current documentation regarding imports, scoping, and loading (in SAWScript) is both lacking and out of date.
The Destination
This new documentation should make its way to various places:
sawscript/doc/developer/*Rough thoughts