Skip to content

Commit

Permalink
take shared into acct in lien construction
Browse files Browse the repository at this point in the history
  • Loading branch information
@nikomatsakis
nikomatsakis committed Feb 17, 2024
1 parent 3344995 commit 239c502
Show file tree
Hide file tree
Showing 3 changed files with 82 additions and 38 deletions.
6 changes: 6 additions & 0 deletions src/type_system/env.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,12 @@ impl Env {
self.assumptions.extend(assumptions);
}

/// True if the environment contains an assumption that `var` is shared.
/// In the particular case of universal-variables, this can be boolean tested, which is convenient.
pub fn is_shared(&self, var: &UniversalVar) -> bool {
self.assumptions.contains(&Predicate::shared(var))
}

pub fn assumptions(&self) -> &Set<Predicate> {
&self.assumptions
}
Expand Down
93 changes: 55 additions & 38 deletions src/type_system/lien_chains.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -52,33 +52,32 @@ pub struct My();
pub struct Our();

impl LienChain {
fn apply_all(&self, liens: LienChain) -> Self {
fn apply_all(&self, env: &Env, liens: LienChain) -> Self {
let mut this = self.clone();
for lien in liens.vec {
this = this.apply(lien);
this = this.apply(env, lien);
}
this
}

fn apply(&self, lien: Lien) -> Self {
match (self.vec.last(), &lien) {
(_, Lien::Our) => LienChain {
vec: vec![Lien::Our],
},
(Some(Lien::Leased(_)), Lien::Shared(_)) | (Some(Lien::Var(_)), Lien::Shared(_)) => {
LienChain { vec: vec![lien] }
}
(None, _)
| (Some(Lien::Our), _)
| (Some(Lien::Shared(_)), _)
| (Some(Lien::Leased(_)), _)
| (Some(Lien::Var(_)), _) => LienChain {
fn apply(&self, env: &Env, lien: Lien) -> Self {
let lien_is_shared = match &lien {
Lien::Our => true,
Lien::Shared(_) => true,
Lien::Var(v) => env.is_shared(v),
Lien::Leased(_) => false,
};

if lien_is_shared {
LienChain { vec: vec![lien] }
} else {
LienChain {
vec: self.vec.iter().cloned().chain(Some(lien)).collect(),
},
}
}
}

fn apply_lien(&self, lien: Lien, pending: &LienChain) -> (Self, LienChain) {
fn apply_lien(&self, env: &Env, lien: Lien, pending: &LienChain) -> (Self, LienChain) {
let mut this = self.clone();
let mut pending = pending.vec.iter();

Expand All @@ -87,23 +86,33 @@ impl LienChain {
// FIXME: should be "p covers lien" (or the reverse?) something.
break;
}
this = this.apply(p.clone());
this = this.apply(env, p.clone());
}

(
this.apply(lien),
this.apply(env, lien),
LienChain {
vec: pending.cloned().collect(),
},
)
}

fn apply_var(&self, var: impl Upcast<UniversalVar>, pending: &LienChain) -> (Self, LienChain) {
self.apply_lien(Lien::Var(var.upcast()), pending)
fn apply_var(
&self,
env: &Env,
var: impl Upcast<UniversalVar>,
pending: &LienChain,
) -> (Self, LienChain) {
self.apply_lien(env, Lien::Var(var.upcast()), pending)
}

fn apply_leased(&self, place: impl Upcast<Place>, pending: &LienChain) -> (Self, LienChain) {
self.apply_lien(Lien::Leased(place.upcast()), pending)
fn apply_leased(
&self,
env: &Env,
place: impl Upcast<Place>,
pending: &LienChain,
) -> (Self, LienChain) {
self.apply_lien(env, Lien::Leased(place.upcast()), pending)
}

pub fn is_not_my(&self) -> bool {
Expand All @@ -119,6 +128,10 @@ impl Lien {
pub fn leased(place: impl Upcast<Place>) -> Self {
Self::Leased(place.upcast())
}

pub fn var(var: impl Upcast<UniversalVar>) -> Self {
Self::Var(var.upcast())
}
}

impl UpcastFrom<My> for LienChain {
Expand Down Expand Up @@ -193,8 +206,11 @@ where
}
}

pub fn collapse(pairs: Set<(LienChain, LienChain)>) -> Set<LienChain> {
pairs.into_iter().map(|(a, b)| a.apply_all(b)).collect()
pub fn collapse(env: &Env, pairs: Set<(LienChain, LienChain)>) -> Set<LienChain> {
pairs
.into_iter()
.map(|(a, b)| a.apply_all(env, b))
.collect()
}

judgment_fn! {
Expand Down Expand Up @@ -223,15 +239,15 @@ judgment_fn! {
debug(chain, pending, a, env)

(
(let chain = chain.apply_all(pending))
(let chain = chain.apply_all(&env, pending))
----------------------------------- ("named-ty")
(ty_chains_cx(_env, chain, pending, n: NamedTy) => set![TyChain::NamedTy(chain, n)])
(ty_chains_cx(env, chain, pending, n: NamedTy) => set![TyChain::NamedTy(chain, n)])
)

(
(let chain = chain.apply_all(pending))
(let chain = chain.apply_all(&env, pending))
----------------------------------- ("universal-var")
(ty_chains_cx(_env, chain, pending, v: UniversalVar) => set![TyChain::Var(chain, v)])
(ty_chains_cx(env, chain, pending, v: UniversalVar) => set![TyChain::Var(chain, v)])
)

(
Expand Down Expand Up @@ -283,7 +299,7 @@ judgment_fn! {
(
(lien_chain_pairs(&env, My(), cx, a) => pairs)
----------------------------------- ("restrictions")
(lien_chains(env, cx, a) => collapse(pairs))
(lien_chains(env, cx, a) => collapse(&env, pairs))
)
}
}
Expand Down Expand Up @@ -326,10 +342,10 @@ judgment_fn! {
)

(
(if var.kind == Kind::Perm)!
(let pair = chain.apply_var(var, &pending))
(if var.kind == Kind::Perm)
(let pair = chain.apply_var(&env, var, &pending))
----------------------------------- ("perm-var")
(lien_chain_pairs(_env, chain, pending, Variable::UniversalVar(var)) => set![pair])
(lien_chain_pairs(env, chain, pending, Variable::UniversalVar(var)) => set![pair])
)

(
Expand Down Expand Up @@ -374,14 +390,15 @@ judgment_fn! {
}

fn collapse_to_pending(
env: &Env,
chain: impl Upcast<LienChain>,
pending: impl Upcast<Set<(LienChain, LienChain)>>,
) -> Set<(LienChain, LienChain)> {
let chain = chain.upcast();
let pending = pending.upcast();
pending
.into_iter()
.map(|(a, b)| (chain.clone(), a.apply_all(b)))
.map(|(a, b)| (chain.clone(), a.apply_all(env, b)))
.collect()
}

Expand All @@ -404,7 +421,7 @@ judgment_fn! {
(lien_chain_pairs(&env, My(), &pending, ty) => pairs0)
(given_from_places(&env, &chain, &pending, &places) => pairs1)
-------------------------- ("cons")
(given_from_places(env, chain, pending, Cons(place, places)) => (collapse_to_pending(&chain, &pairs0), pairs1))
(given_from_places(env, chain, pending, Cons(place, places)) => (collapse_to_pending(&env, &chain, &pairs0), pairs1))
)
}
}
Expand All @@ -425,11 +442,11 @@ judgment_fn! {

(
(place_ty(&env, &place) => ty)
(let (liens_l, pending_l) = chain.apply_leased(&place, &pending))
(let (liens_l, pending_l) = chain.apply_leased(&env, &place, &pending))
(lien_chain_pairs(&env, My(), &pending_l, ty) => pairs0)
(leased_from_places(&env, &chain, &pending, &places) => pairs1)
-------------------------- ("cons")
(leased_from_places(env, chain, pending, Cons(place, places)) => (collapse_to_pending(&liens_l, &pairs0), pairs1))
(leased_from_places(env, chain, pending, Cons(place, places)) => (collapse_to_pending(&env, &liens_l, &pairs0), pairs1))
)
}
}
Expand All @@ -450,7 +467,7 @@ judgment_fn! {
(lien_chain_pairs(&env, My(), My(), ty) => pairs0)
(shared_from_places(&env, &places) => pairs1)
-------------------------- ("cons")
(shared_from_places(env, Cons(place, places)) => (collapse_to_pending(Lien::shared(&place), &pairs0), pairs1))
(shared_from_places(env, Cons(place, places)) => (collapse_to_pending(&env, Lien::shared(&place), &pairs0), pairs1))
)
}
}
Expand Down
21 changes: 21 additions & 0 deletions src/type_system/tests/cancellation.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -324,3 +324,24 @@ fn forall_leased_P_shared_P_data_to_our_P_data() {
))
.assert_ok(expect_test::expect!["()"]);
}

#[test]
#[allow(non_snake_case)]
fn forall_shared_P_shared_P_data_to_our_P_data() {
check_program(&term(
"
class Data {
}
class Main {
fn test[perm P](my self, data: P Data) -> our P Data
where
shared(P),
{
let p: shared{data} Data = data.share;
p.give;
}
}
",
))
.assert_ok(expect_test::expect!["()"]);
}

0 comments on commit 239c502

Please sign in to comment.