scopegraphs_lib/completeness/
mod.rs

1//! This module contains several utilities to guarantee query stability.
2//! Query stability means that the result of a query, once resolved, will remain valid after future
3//! additions to the scope graph.
4//! This allows safe interleaving of name resolution and scope graph construction.
5//!
6//! The main trait of this module is [`Completeness`]. An instance of this trait should be passed
7//! to [`super::ScopeGraph::new`] to obtain a correct scope graph instance.
8//!
9//! Currently the module contains two safe implementations.
10//! [`ImplicitClose`] is the easiest to use, and most likely the preferred choice for simple
11//! sequential type checkers.
12//! [`ExplicitClose`] requires some manual bookkeeping, but allows more flexible handling of
13//! queries. This is the most suitable choice for type checkers that need to do dynamic scheduling.
14
15use crate::{InnerScopeGraph, Scope};
16
17mod future;
18pub use future::*;
19
20mod critical_edge;
21pub use critical_edge::*;
22mod explicit;
23pub use explicit::*;
24mod implicit;
25pub use implicit::*;
26mod unchecked;
27pub use unchecked::*;
28
29mod private {
30    pub trait Sealed {}
31}
32
33use private::Sealed;
34
35/*** Completeness trait ***/
36
37/// Types implementing this trait have the responsibility to guarantee query stability.
38///
39/// This means that the result of a query, once computed, may not be invalidated by later extensions
40/// of the scope graph.
41///
42/// A [`super::ScopeGraph`] will call the handlers of its completeness on each operation.
43/// For scope addition and data access, it can update some internal state.
44/// For edge addition and retrieval, it can override/augment the default result as well.
45///
46/// The way query stability is guaranteed is very flexible. Current implementations use
47/// - critical edges, explicitly closed by the client ([`ExplicitClose`]).
48/// - critical edges, implicitly closed when retrieved ([`ImplicitClose`]).
49///
50/// Future implementations may also:
51/// - delay retrieval of edges until it is closed (by returning a future).
52/// - guarantee stability by retaining residual queries, and checking those do not return any
53///   results for later additions.
54/// - ...
55///
56/// This trait is sealed to ensure only verified implementations are available.
57pub trait Completeness<LABEL, DATA>: Sealed {
58    fn cmpl_new_scope(&self, inner_scope_graph: &InnerScopeGraph<LABEL, DATA>, scope: Scope);
59
60    /// Should initialize a scope without possibility to extend it with edges
61    fn cmpl_new_complete_scope(
62        &self,
63        inner_scope_graph: &InnerScopeGraph<LABEL, DATA>,
64        scope: Scope,
65    ) {
66        self.cmpl_new_scope(inner_scope_graph, scope)
67    }
68
69    type NewEdgeResult;
70    fn cmpl_new_edge(
71        &self,
72        inner_scope_graph: &InnerScopeGraph<LABEL, DATA>,
73        src: Scope,
74        lbl: LABEL,
75        dst: Scope,
76    ) -> Self::NewEdgeResult;
77
78    // type GetDataResult;
79    // fn get_data(&mut self, inner_scope_graph: &InnerScopeGraph<LABEL, DATA>, scope: Scope) -> Self::GetDataResult;
80
81    type GetEdgesResult<'rslv>
82    where
83        Self: 'rslv,
84        LABEL: 'rslv,
85        DATA: 'rslv;
86    fn cmpl_get_edges<'rslv>(
87        &'rslv self,
88        inner_scope_graph: &'rslv InnerScopeGraph<LABEL, DATA>,
89        src: Scope,
90        lbl: LABEL,
91    ) -> Self::GetEdgesResult<'rslv>
92    where
93        LABEL: 'rslv,
94        DATA: 'rslv;
95}
96
97// TODO: Asynchronous Completeness can be a wrapper around the ExplicitClose impl
98
99// TODO: Residual-query-based Completeness requires access to query resolution
scopegraphs_lib/completeness/mod.rs

scopegraphs_lib/completeness/
mod.rs
