Operational semantics of visibility resolution
Prelimiaries:
- It is desirable to be able to build a module incrementally, e.g. by sequentially compiling several source files that each contain part of the module text, or by adding pieces incrementally with multiple invocations of [user]. There should not be any rules that require knowledge of the full module text, as this implies multi-pass compilation and inability to extend a module.
- On the other hand, a completely dynamic visibility system (allowing arbitrary changes, like un-importing, etc) is also problematic, in particular when different calling conventions exist (e.g. meta-predicates, or inlined predicates).
We therefore describe a system where declarations, definitions and uses of predicates can be encountered by the system in an arbitrary order.
We consider the following visibility states for a predicate during this process:
- UNKNOWN - visibility and origin not yet resolved
- LIMPORT - latently imported, after "import module" (or use_module/1) declaration
- IMPORT - explicitly imported from a particular module, after "import pred from module" (or use_module/2) declaration
- LOCAL - after definition or explicit local-declaration
- EXPORT - exported, after export-declaration or module-header
- REXPORT - imported and re-exported, after reexport-declaration
and the following events
- import-module declaration
- import-pred-from-module declaration
- export-declaration (possibly implicit in module header)
- reexport-declaration (import and export combined)
- local-declaration (if supported)
- definition (compilation of clauses)
- call-compilation (occurrence as a compiled subgoal)
- meta-call (e.g. non-ISO directive in file, toplevel query, etc)
The table below specifies the resulting predicate visibility after each encounter. The general idea is to allow only changes towards "more precise" visibility information.
| Old state | UNKNOWN | LIMPORT | IMPORT | REXPORT | LOCAL | EXPORT |
|---|
| Event | | | | | | |
|---|
| import-module | LIMPORT | LIMPORT 2 | = | = | = | = |
| import-pred | IMPORT | IMPORT 3 | eidm | eidm | error | error |
| reexport | REXPORT | REXPORT 3 | REXPORT 6 | eidm | error | error |
| export | EXPORT | EXPORT 4 | error | error | EXPORT | = |
| local-decl | LOCAL | LOCAL 4 | error | error | = | = |
| definition | LOCAL | LOCAL 4 | error | error | = | = |
| compiled call | = 1 | IMPORT 5 | = | = | = | = |
| meta-call | = | IMPORT 5 | = | = | = | = |
where
- error - error message, declaration ignored, old state retained
- eidm - error if different module, otherwise ignored as duplicate declaration
- = silent, no state change
Notes:
- may need to commit to a particular calling convention here.
- multiple latent imports from different modules are possible (and silent).
- either confirming one (of possibly multiple) latent imports, or silently overriding them with a different one.
- silently overriding the latent import.
- confirming a unique latent import, or error if multiple latent imports.
- if import and reexport were from same module, otherwise error
Not every system may support every transition (e.g. when explicit local or export declarations are not present).
Abolish
[separate section because possibly more controversial]
In keeping with restrictions motivated by the calling convention problem, abolishing should not be able to undo established import-export links:
| Old state | UNKNOWN | LIMPORT | IMPORT | REXPORT | LOCAL | EXPORT |
|---|
| Event | | | | | | |
|---|
| abolish | = | = | error | error | = | = |
As a result, abolish basically removes a predicate's clauses but leaves its identity and visibility intact. It can neither affect the clauses of imported predicates, nor remove a predicate's visibility once it has been established.
Implementation
The above is essentially what is implemented in the ECLiPSe system since version 5.0 (2000), when the module system was redesigned in the light of experience with the earlier, more dynamic system, and with a view to better support of inlining.
Joachim Schimpf, March 2012
