pub fn lub_perms<'db>(
env: &Env<'db>,
perm1: RedPerm<'db>,
perm2: RedPerm<'db>,
) -> RedPerm<'db>Expand description
The least upper bound (LUB) of two permissions (perm1, perm2).
The LUB perm3 is a permission such that perm1 <: perm3 and perm1 <: perm3
but also there is no other mutual upper bound perm4 where perm4 <: perm3.
In other words, if perm1 and perm2 represent lower bounds in inference
(i.e., for some inference variable ?X, perm1 <: ?X and perm2 <: ?X),
then perm3 combines those two bounds on ?X into a single bound perm3 <: ?X
that must also hold (because there is no possible value for ?X that wouldn’t
satisfy it).
Computing the LUB is fairly trivial for us because we can just union the chains. This is not necessarily the most compact representation of the LUB but it is correct. We do some minimal simplification.
§Examples
lub_perms([our], [ref[x]]) = [ref[x]].- The union would be
[our, ref[x]]but just[ref[x]]is equivalent and more compact.- Equivalent because
(our | ref[x]) <: ref[x]andref[x] <: (our | ref[x]))
- Equivalent because
- The union would be
lub_perms([ref[x.y]], [ref[x]]) = [ref[x]].- Another example where the union
[ref[x], ref[x.y]]contains redundancies.
- Another example where the union
lub_perms([ref[x.y]], [ref[x.z]]) = [ref[x.y], ref[x.z]].- Union suffices.
lub_perms([ref[x.y]], [ref[x.z]]) = [ref[x.y], ref[x.z]].