Module scopegraphs::completeness

This module contains several utilities to guarantee query stability.

Query stability means that the result of a query, once resolved, will remain valid after future additions to the scope graph. This allows safe interleaving of name resolution and scope graph construction.

The main trait of this module is Completeness. An implementation of this trait should be passed to ScopeGraph::new to obtain a scope graph instance.

Currently, the module contains three safe implementations.

• ImplicitClose is the easiest to use, and most likely the preferred choice for simple sequential type checkers.
• ExplicitClose requires some manual bookkeeping, but allows more flexible handling of queries. This is the most suitable choice for type checkers that need to do dynamic scheduling. Running queries can return an error, because scopes relevant to the query weren’t closed yet.
• FutureCompleteness is like ExplicitClose, except queries can no longer error. Instead, queries return a Future that resolves when all scopes related to the query are closed.

Structs

• Delay
  Value returned when a query cannot yet be computed because some edge it depends on is still closed.
• EdgeClosedError
  Error returned when attempting to add an edge with a label that is already closed in that scope.
• ExplicitClose
  Critical-edge based Completeness implementation.
• FutureCompleteness
  A completeness strategy that makes queries return a Future in case one of the scopes that the query runs over was not yet closed. The future resolves once all such scopes are closed.
• ImplicitClose
  Critical-edge based Completeness implementation.
• UncheckedCompleteness
  No-Op implementation of Completeness.

Traits

• Completeness
  Types implementing this trait have the responsibility to guarantee query stability.
• CriticalEdgeBasedCompleteness
  Sub-trait of Completeness that uses critical edges (scope-label pairs) to manage completeness. // TODO: link to “concepts”

Type Aliases

• EdgesOrDelay
  Convenience alias for the type of Result returned from queries using critical edge based completion