Skip to main content

glb_perms

Function glb_perms 

Source
pub fn glb_perms<'db>(
    env: &Env<'db>,
    perm1: RedPerm<'db>,
    perm2: RedPerm<'db>,
) -> Option<RedPerm<'db>>
Expand description

The greatest lower bound (GLB) of two permissions (perm1, perm2), if it exists. The GLB perm3 is a permission such that perm3 <: perm1 and perm3 <: perm2 but also there is no other mutual lower bound perm4 where perm3 <: perm4. In other words, if perm1 and perm2 represent upper bounds in inference (i.e., for some inference variable ?X, ?X <: perm1 and ?X <: perm2), then perm3 combines those two bounds on ?X into a single bound ?X <: perm3 that must also hold (because there is no possible value for ?X that wouldn’t satisfy it).

§Examples

  • glb_perms([our], [ref[x]]) = [our]
  • glb_perms([ref[x] mut[y.z]], [ref[x.y] mut[y]]) = [ref[x.y] mut[y.z]]