Skip to content

Commit 3605d47

Browse files
AZWNAZWN
authored
Merge pull request #62 from metaborg/dwf-bounds-on-query-separate-traits
Dwf bounds on query separate traits
2 parents 6790225 + 65f2689 commit 3605d47

File tree

6 files changed

+190
-64
lines changed

6 files changed

+190
-64
lines changed

‎scopegraphs/src/completeness/implicit.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ use super::Implicit;
1414
/// Unlike [`ExplicitClose`](crate::completeness::ExplicitClose), this implementation will implicitly close edges once traversed.
1515
/// This does not require special attention from the type checker writer.
1616
///
17-
/// Returns [`EdgeClosedError`](EdgeClosedError) when an edge is added to a scope in which the label is already
17+
/// Returns [EdgeClosedError] when an edge is added to a scope in which the label is already
1818
/// closed (because `get_edges(s, l, ...)` was called earlier.
1919
///
2020
/// When edges are retrieved (e.g. during query resolution) the `(src, label)` edge is closed.

‎scopegraphs/src/containers/path.rs

+26-4
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,13 @@
11
use crate::future_wrapper::FutureWrapper;
22
use crate::resolve::{Env, Path, ResolvedPath};
33
use futures::future::join_all;
4+
use std::fmt::Debug;
45
use std::hash::Hash;
56

7+
use super::EnvContainer;
8+
69
/// Interface for path containers that support the operations required for query resolution.
7-
pub trait PathContainer<'sg, 'rslv, LABEL: 'sg, DATA: 'sg>: 'rslv {
10+
pub trait PathContainer<'sg, 'rslv, LABEL: 'sg, DATA: 'sg>: Debug + 'rslv {
811
/// Type returned by resolving a path to its sub-environment.
912
type EnvContainer;
1013

@@ -15,7 +18,26 @@ pub trait PathContainer<'sg, 'rslv, LABEL: 'sg, DATA: 'sg>: 'rslv {
1518
) -> Self::EnvContainer;
1619
}
1720

18-
impl<'rslv, 'sg, LABEL: 'sg, DATA: 'sg> PathContainer<'sg, 'rslv, LABEL, DATA> for Vec<Path<LABEL>>
21+
/// Trait that is auto-implemented for any [PathContainer] implementation that yields a valid [EnvContainer].
22+
pub trait PathContainerWf<'sg, 'rslv, LABEL: 'sg, DATA: 'sg, DWFO>:
23+
PathContainer<'sg, 'rslv, LABEL, DATA, EnvContainer = Self::EnvContainerWf>
24+
{
25+
/// Witness that ```Self::EnvContainer``` is a valid environment container.
26+
type EnvContainerWf: EnvContainer<'sg, 'rslv, LABEL, DATA, DWFO>;
27+
}
28+
29+
impl<'sg, 'rslv, LABEL, DATA, DWFO, T> PathContainerWf<'sg, 'rslv, LABEL, DATA, DWFO> for T
30+
where
31+
LABEL: Debug + 'sg,
32+
DATA: 'sg,
33+
T: PathContainer<'sg, 'rslv, LABEL, DATA>,
34+
Self::EnvContainer: EnvContainer<'sg, 'rslv, LABEL, DATA, DWFO>,
35+
{
36+
type EnvContainerWf = Self::EnvContainer;
37+
}
38+
39+
impl<'rslv, 'sg, LABEL: Debug + 'sg, DATA: 'sg> PathContainer<'sg, 'rslv, LABEL, DATA>
40+
for Vec<Path<LABEL>>
1941
where
2042
Self: 'rslv,
2143
LABEL: Clone + Hash + Eq,
@@ -30,8 +52,8 @@ where
3052

3153
// TODO: can this be generalized to arbitrary results of PathContainers?
3254
// (challenge is converting between the different `::EnvContainer`s.)
33-
impl<'rslv, 'sg, LABEL: 'sg, DATA: 'sg, E: 'rslv> PathContainer<'sg, 'rslv, LABEL, DATA>
34-
for Result<Vec<Path<LABEL>>, E>
55+
impl<'rslv, 'sg, LABEL: Debug + 'sg, DATA: 'sg, E: Debug + 'rslv>
56+
PathContainer<'sg, 'rslv, LABEL, DATA> for Result<Vec<Path<LABEL>>, E>
3557
where
3658
Self: 'rslv,
3759
LABEL: Clone + Hash,

‎scopegraphs/src/containers/scope.rs

+114-6
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,14 @@
1+
use std::fmt::Debug;
2+
use std::hash::Hash;
3+
14
use crate::future_wrapper::FutureWrapper;
25
use crate::resolve::Path;
36
use crate::Scope;
47

8+
use super::{PathContainer, PathContainerWf};
9+
510
/// Interface for scope containers that support the operations required for query resolution.
6-
pub trait ScopeContainer<LABEL> {
11+
pub trait ScopeContainer<'sg, 'rslv, LABEL: Debug + 'sg, DATA: 'sg>: Debug {
712
/// The type containing paths obtained after stepping to this scope.
813
type PathContainer;
914

@@ -14,7 +19,95 @@ pub trait ScopeContainer<LABEL> {
1419
fn lift_step(self, lbl: LABEL, prefix: Path<LABEL>) -> Self::PathContainer;
1520
}
1621

17-
impl<LABEL: Copy> ScopeContainer<LABEL> for Vec<Scope> {
22+
/// Trait that is auto-implemented for any [ScopeContainer] implementation that yields a valid [PathContainer].
23+
///
24+
/// This trait is implemented for:
25+
/// - `Vec<Scope>`,
26+
/// - [Result] of scope containers, and
27+
/// - [FutureWrapper] of scope containers.
28+
/// ```
29+
/// # use scopegraphs::containers::ScopeContainerWf;
30+
/// # use scopegraphs::future_wrapper::FutureWrapper;
31+
/// # use scopegraphs::Scope;
32+
/// # use std::fmt::Debug;
33+
/// # use std::hash::Hash;
34+
///
35+
/// # trait LBound<'sg>: Copy + Hash + Eq + Debug + 'sg {}
36+
/// # trait DBound<'sg>: Hash + Eq + 'sg {}
37+
///
38+
/// fn test<'sg, 'rslv, LABEL: LBound<'sg>, DATA: DBound<'sg>, DWFO>(
39+
/// cont: impl ScopeContainerWf<'sg, 'rslv, LABEL, DATA, DWFO>
40+
/// ) { }
41+
///
42+
/// # fn scope_vec<'sg, 'rslv, LABEL: LBound<'sg>, DATA: DBound<'sg>>() {
43+
/// let vec: Vec<Scope> = todo!();
44+
/// test::<'_, '_, LABEL, DATA, bool>(vec);
45+
/// # }
46+
///
47+
/// # fn result<'sg, 'rslv, LABEL: LBound<'sg>, DATA: DBound<'sg>, E: Debug + Clone>() {
48+
/// let result: Result<Vec<Scope>, E> = todo!();
49+
/// test::<'_, '_, LABEL, DATA, bool>(result);
50+
/// test::<'_, '_, LABEL, DATA, Result<bool, E>>(result);
51+
/// # }
52+
///
53+
/// # fn future<'sg, 'rslv, LABEL: LBound<'sg>, DATA: DBound<'sg>>() {
54+
/// let future: FutureWrapper<Vec<Scope>> = todo!();
55+
/// test::<'_, '_, LABEL, DATA, bool>(future);
56+
/// test::<'_, '_, LABEL, DATA, FutureWrapper<'_, bool>>(future);
57+
/// # }
58+
/// ```
59+
///
60+
/// ```no_run
61+
/// # use scopegraphs::containers::ScopeContainerWf;
62+
/// # use scopegraphs::Scope;
63+
/// # use std::fmt::Debug;
64+
/// # use std::hash::Hash;
65+
///
66+
///
67+
/// fn test<'sg, 'rslv, LABEL: Hash + Eq + Debug + 'sg, DATA: Hash + Eq + 'sg, DWFO>(cont: impl ScopeContainerWf<'sg, 'rslv, LABEL, DATA, DWFO>) {
68+
///
69+
/// }
70+
/// ```
71+
///
72+
/// ```no_run
73+
/// # use scopegraphs::containers::ScopeContainerWf;
74+
/// # use scopegraphs::Scope;
75+
/// # use std::fmt::Debug;
76+
/// # use std::hash::Hash;
77+
///
78+
/// test::<'_, '_, (), (), bool>(Result::<_, ()>::Ok(Vec::<Scope>::new()));
79+
/// test::<'_, '_, (), (), Result<bool, ()>>(Result::<_, ()>::Ok(Vec::<Scope>::new()));
80+
///
81+
/// fn test<'sg, 'rslv, LABEL: Hash + Eq + Debug + 'sg, DATA: Hash + Eq + 'sg, DWFO>(cont: impl ScopeContainerWf<'sg, 'rslv, LABEL, DATA, DWFO>) {
82+
///
83+
/// }
84+
/// ```
85+
///
86+
pub trait ScopeContainerWf<'sg, 'rslv, LABEL, DATA, DWFO>:
87+
ScopeContainer<'sg, 'rslv, LABEL, DATA, PathContainer = Self::PathContainerWf>
88+
where
89+
LABEL: Debug + 'sg,
90+
DATA: 'sg,
91+
{
92+
/// Refinement of `Self::PathContainer`, carrying proof that this scope container resolves to valid path containers.
93+
type PathContainerWf: PathContainerWf<'sg, 'rslv, LABEL, DATA, DWFO>;
94+
}
95+
96+
impl<'sg, 'rslv, LABEL, DATA, DWFO, T> ScopeContainerWf<'sg, 'rslv, LABEL, DATA, DWFO> for T
97+
where
98+
LABEL: Debug + 'sg,
99+
DATA: 'sg,
100+
T: ScopeContainer<'sg, 'rslv, LABEL, DATA>,
101+
Self::PathContainer: PathContainerWf<'sg, 'rslv, LABEL, DATA, DWFO>,
102+
{
103+
type PathContainerWf = Self::PathContainer;
104+
}
105+
106+
impl<'sg: 'rslv, 'rslv, LABEL: Debug + Copy + Eq + Hash + 'sg, DATA: Eq + Hash + 'sg>
107+
ScopeContainer<'sg, 'rslv, LABEL, DATA> for Vec<Scope>
108+
where
109+
Vec<Path<LABEL>>: PathContainer<'sg, 'rslv, LABEL, DATA>,
110+
{
18111
type PathContainer = Vec<Path<LABEL>>;
19112

20113
fn lift_step(self, lbl: LABEL, prefix: Path<LABEL>) -> Self::PathContainer {
@@ -24,21 +117,36 @@ impl<LABEL: Copy> ScopeContainer<LABEL> for Vec<Scope> {
24117
}
25118
}
26119

27-
impl<LABEL, SC: ScopeContainer<LABEL>, E> ScopeContainer<LABEL> for Result<SC, E> {
120+
impl<
121+
'sg: 'rslv,
122+
'rslv,
123+
LABEL: Debug + Copy + Eq + Hash + 'sg,
124+
DATA: Eq + Hash + 'sg,
125+
SC: ScopeContainer<'sg, 'rslv, LABEL, DATA>,
126+
E: Debug,
127+
> ScopeContainer<'sg, 'rslv, LABEL, DATA> for Result<SC, E>
128+
where
129+
Result<SC::PathContainer, E>: PathContainer<'sg, 'rslv, LABEL, DATA>,
130+
{
28131
type PathContainer = Result<SC::PathContainer, E>;
29132

30133
fn lift_step(self, lbl: LABEL, prefix: Path<LABEL>) -> Self::PathContainer {
31134
self.map(|sc| sc.lift_step(lbl, prefix))
32135
}
33136
}
34137

35-
impl<'rslv, LABEL, SC: ScopeContainer<LABEL> + Clone> ScopeContainer<LABEL>
36-
for FutureWrapper<'rslv, SC>
138+
impl<
139+
'sg: 'rslv,
140+
'rslv,
141+
LABEL: Debug + Copy + Eq + Hash + 'sg,
142+
DATA: Eq + Hash + 'sg,
143+
SC: ScopeContainer<'sg, 'rslv, LABEL, DATA> + Clone,
144+
> ScopeContainer<'sg, 'rslv, LABEL, DATA> for FutureWrapper<'rslv, SC>
37145
where
38146
LABEL: Copy,
39-
SC::PathContainer: Clone,
40147
Self: 'rslv,
41148
LABEL: 'rslv,
149+
SC::PathContainer: Clone,
42150
{
43151
type PathContainer = FutureWrapper<'rslv, SC::PathContainer>;
44152

‎scopegraphs/src/future_wrapper.rs

+5-2
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
1+
//! Defines a cloneable pointer to a future.
2+
13
use futures::future::Shared;
24
use futures::FutureExt;
35
use std::fmt::{Debug, Formatter};
@@ -7,8 +9,8 @@ use std::{
79
task::{Context, Poll},
810
};
911

10-
// TODO: fork futures and create our own shared future that can have a
11-
// ?Sized inner type (this should be possible)
12+
// FIXME: only expose futures on tests
13+
/// Shared pointer to a future, useful to make functions parametric over the type of future they are invoked with.
1214
pub struct FutureWrapper<'fut, T>(pub Shared<Pin<Box<dyn Future<Output = T> + 'fut>>>);
1315

1416
impl<T> Clone for FutureWrapper<'_, T> {
@@ -18,6 +20,7 @@ impl<T> Clone for FutureWrapper<'_, T> {
1820
}
1921

2022
impl<'fut, T: Clone> FutureWrapper<'fut, T> {
23+
/// Creates shared pointer to `f`.
2124
pub fn new(f: impl Future<Output = T> + 'fut) -> Self {
2225
let f: Pin<Box<dyn Future<Output = T> + 'fut>> = Box::pin(f);
2326
Self(f.shared())

‎scopegraphs/src/lib.rs

+4-1
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,10 @@ pub use scopegraphs_regular_expressions::*;
2929

3030
pub mod completeness;
3131
pub mod containers;
32-
mod future_wrapper;
32+
// #[cfg(test)]
33+
pub mod future_wrapper;
34+
// #[cfg(not(test))]
35+
// mod future_wrapper;
3336

3437
pub mod resolve;
3538

0 commit comments

Comments
 (0)