|
| 1 | +use crate::{ |
| 2 | + completeness::private::Sealed, |
| 3 | + completeness::{ |
| 4 | + Completeness, CriticalEdgeBasedCompleteness, CriticalEdgeSet, Delay, EdgeClosedError, |
| 5 | + EdgesOrDelay, |
| 6 | + }, |
| 7 | + label::Label, |
| 8 | + InnerScopeGraph, Scope, ScopeGraph, |
| 9 | +}; |
| 10 | +use std::{collections::HashSet, hash::Hash}; |
| 11 | + |
| 12 | +/// Critical-edge based [`Completeness`] implementation. |
| 13 | +/// |
| 14 | +/// Unlike [`ImplicitClose`], this implementation shifts responsibility of closing edges to the |
| 15 | +/// _type checker writer_. I.e., they have to insert `sg.close(scope, label)` statements at the |
| 16 | +/// appropriate positions in the code. |
| 17 | +/// |
| 18 | +/// Returns [`EdgeClosedError`] when an edge is added to a scope in which the label is already |
| 19 | +/// closed (by an explicit close of the type checker writer). |
| 20 | +/// |
| 21 | +/// Returns [`Delay`] when edges are retrieved (e.g. during query resolution) for an edge that is |
| 22 | +/// not yet closed. |
| 23 | +pub struct ExplicitClose<LABEL> { |
| 24 | + critical_edges: CriticalEdgeSet<LABEL>, |
| 25 | +} |
| 26 | + |
| 27 | +impl<LABEL> Default for ExplicitClose<LABEL> { |
| 28 | + fn default() -> Self { |
| 29 | + ExplicitClose { |
| 30 | + critical_edges: CriticalEdgeSet::default(), |
| 31 | + } |
| 32 | + } |
| 33 | +} |
| 34 | + |
| 35 | +impl<LABEL> Sealed for ExplicitClose<LABEL> {} |
| 36 | + |
| 37 | +impl<LABEL: Hash + Eq + Label, DATA> Completeness<LABEL, DATA> for ExplicitClose<LABEL> { |
| 38 | + fn cmpl_new_scope(&mut self, _: &InnerScopeGraph<LABEL, DATA>, _: Scope) { |
| 39 | + <ExplicitClose<LABEL> as CriticalEdgeBasedCompleteness<LABEL, DATA>>::init_scope_with( |
| 40 | + self, |
| 41 | + LABEL::iter().collect(), // init with all labels: programmer is responsible for closing edges |
| 42 | + ) |
| 43 | + } |
| 44 | + |
| 45 | + fn cmpl_new_complete_scope(&mut self, _: &InnerScopeGraph<LABEL, DATA>, _: Scope) { |
| 46 | + <ExplicitClose<LABEL> as CriticalEdgeBasedCompleteness<LABEL, DATA>>::init_scope_with( |
| 47 | + self, |
| 48 | + HashSet::new(), // init with empty label set to prevent extension |
| 49 | + ) |
| 50 | + } |
| 51 | + |
| 52 | + type NewEdgeResult = Result<(), EdgeClosedError<LABEL>>; |
| 53 | + |
| 54 | + fn cmpl_new_edge( |
| 55 | + &mut self, |
| 56 | + inner_scope_graph: &mut InnerScopeGraph<LABEL, DATA>, |
| 57 | + src: Scope, |
| 58 | + lbl: LABEL, |
| 59 | + dst: Scope, |
| 60 | + ) -> Self::NewEdgeResult { |
| 61 | + if self.critical_edges.is_open(src, &lbl) { |
| 62 | + inner_scope_graph.add_edge(src, lbl, dst); |
| 63 | + Ok(()) |
| 64 | + } else { |
| 65 | + Err(EdgeClosedError { |
| 66 | + scope: src, |
| 67 | + label: lbl, |
| 68 | + }) |
| 69 | + } |
| 70 | + } |
| 71 | + |
| 72 | + type GetEdgesResult = EdgesOrDelay<Vec<Scope>, LABEL>; |
| 73 | + |
| 74 | + fn cmpl_get_edges( |
| 75 | + &mut self, |
| 76 | + inner_scope_graph: &InnerScopeGraph<LABEL, DATA>, |
| 77 | + src: Scope, |
| 78 | + lbl: LABEL, |
| 79 | + ) -> Self::GetEdgesResult { |
| 80 | + if self.critical_edges.is_open(src, &lbl) { |
| 81 | + Err(Delay { |
| 82 | + scope: src, |
| 83 | + label: lbl, |
| 84 | + }) |
| 85 | + } else { |
| 86 | + Ok(inner_scope_graph.get_edges(src, lbl)) |
| 87 | + } |
| 88 | + } |
| 89 | +} |
| 90 | + |
| 91 | +impl<LABEL: Hash + Eq + Label, DATA> CriticalEdgeBasedCompleteness<LABEL, DATA> |
| 92 | + for ExplicitClose<LABEL> |
| 93 | +{ |
| 94 | + fn init_scope_with(&mut self, open_labels: HashSet<LABEL>) { |
| 95 | + self.critical_edges.init_scope(open_labels) |
| 96 | + } |
| 97 | +} |
| 98 | + |
| 99 | +impl<LABEL: Hash + Eq> ExplicitClose<LABEL> { |
| 100 | + fn close(&mut self, scope: Scope, label: &LABEL) { |
| 101 | + self.critical_edges.close(scope, label); |
| 102 | + } |
| 103 | +} |
| 104 | + |
| 105 | +impl<LABEL: Hash + Eq, DATA> ScopeGraph<LABEL, DATA, ExplicitClose<LABEL>> { |
| 106 | + /// Closes an edge, (i.e., prohibit future new |
| 107 | + /// |
| 108 | + /// For example, the following program will return an error. |
| 109 | + /// ``` |
| 110 | + /// # use scopegraphs_lib::completeness::ExplicitClose; |
| 111 | + /// # use scopegraphs_lib::ScopeGraph; |
| 112 | + /// # use scopegraphs_macros::Label; |
| 113 | + /// # #[derive(Eq, Hash, PartialEq, Label)] enum Lbl { Def } |
| 114 | + /// # use Lbl::*; |
| 115 | + /// let mut sg = ScopeGraph::<Lbl, usize, _>::new(ExplicitClose::default()); |
| 116 | + /// |
| 117 | + /// let s1 = sg.add_scope_with(0, [Def]); |
| 118 | + /// let s2 = sg.add_scope_closed(42); |
| 119 | + /// |
| 120 | + /// sg.close(s1, &Def); |
| 121 | + /// sg.add_edge(s1, Def, s2).expect_err("cannot add edge after closing edge"); |
| 122 | + /// ``` |
| 123 | + /// |
| 124 | + /// Closing is required to permit queries to traverse these edges: |
| 125 | + /// ``` |
| 126 | + /// |
| 127 | + /// # use scopegraphs_lib::completeness::ExplicitClose; |
| 128 | + /// # use scopegraphs_lib::ScopeGraph; |
| 129 | + /// # use scopegraphs_lib::resolve::{DefaultDataEquiv, DefaultLabelOrder, EdgeOrData, Resolve}; |
| 130 | + /// # use scopegraphs_macros::{compile_regex, Label}; |
| 131 | + /// # |
| 132 | + /// # #[derive(Eq, Hash, PartialEq, Label, Debug, Copy, Clone)] |
| 133 | + /// # enum Lbl { Def } |
| 134 | + /// # use Lbl::*; |
| 135 | + /// # type LblD = EdgeOrData<Lbl>; |
| 136 | + /// # |
| 137 | + /// # compile_regex!(type Regex<Lbl> = Def); |
| 138 | + /// let mut sg = ScopeGraph::<Lbl, usize, _>::new(ExplicitClose::default()); |
| 139 | + /// |
| 140 | + /// let s1 = sg.add_scope_with(0, [Def]); |
| 141 | + /// let s2 = sg.add_scope_closed(42); |
| 142 | + /// |
| 143 | + /// // Note: not calling `sg.close(s1, &Def)` |
| 144 | + /// |
| 145 | + /// let query_result = sg.query() |
| 146 | + /// .with_path_wellformedness(Regex::new()) // regex: `Def` |
| 147 | + /// .with_data_wellformedness(|x: &usize| *x == 42) // match `42` |
| 148 | + /// .resolve(s1); |
| 149 | + /// |
| 150 | + /// query_result.expect_err("require s1/Def to be closed"); |
| 151 | + /// ``` |
| 152 | + /// |
| 153 | + /// Closing allows queries to resolve: |
| 154 | + /// ``` |
| 155 | + /// |
| 156 | + /// # use scopegraphs_lib::completeness::ExplicitClose; |
| 157 | + /// # use scopegraphs_lib::ScopeGraph; |
| 158 | + /// # use scopegraphs_lib::resolve::{DefaultDataEquiv, DefaultLabelOrder, EdgeOrData, Resolve}; |
| 159 | + /// # use scopegraphs_macros::{compile_regex, Label}; |
| 160 | + /// # |
| 161 | + /// # #[derive(Eq, Hash, PartialEq, Label, Debug, Copy, Clone)] |
| 162 | + /// # enum Lbl { Def } |
| 163 | + /// # use Lbl::*; |
| 164 | + /// # type LblD = EdgeOrData<Lbl>; |
| 165 | + /// # |
| 166 | + /// # compile_regex!(type Regex<Lbl> = Def); |
| 167 | + /// let mut sg = ScopeGraph::<Lbl, usize, _>::new(ExplicitClose::default()); |
| 168 | + /// |
| 169 | + /// let s1 = sg.add_scope_with(0, [Def]); |
| 170 | + /// let s2 = sg.add_scope_closed(42); |
| 171 | + /// |
| 172 | + /// // Note: closing the edge *after* creating all edges, *before* doing the query |
| 173 | + /// sg.close(s1, &Def); |
| 174 | + /// |
| 175 | + /// let query_result = sg.query() |
| 176 | + /// .with_path_wellformedness(Regex::new()) // regex: `Def` |
| 177 | + /// .with_data_wellformedness(|x: &usize| *x == 42) // match `42` |
| 178 | + /// .resolve(s1); |
| 179 | + /// |
| 180 | + /// query_result.expect("query should return result"); |
| 181 | + /// ``` |
| 182 | + pub fn close(&self, scope: Scope, label: &LABEL) { |
| 183 | + self.completeness.borrow_mut().close(scope, label) |
| 184 | + } |
| 185 | +} |
0 commit comments