Lifetime Projections

Generalized Lifetimes

A generalized lifetime $gr$ is either a region $r$ or $\text{RegionsIn}(\tau )$, where $\tau$ is either:

1. a type parameter, or
2. a type alias that cannot be normalized

Generalized Lifetime Projections

A generalized lifetime projection $grp$ takes the form $b\downarrow gr$ where $b$ is a base having an associated type $\tau$. The index $\text{index}(grp)$ of a lifetime projection is the index of the occurence of $gr$ in the generalized lifetime list $GR(\tau )$ (the list of generalized lifetimes in $\tau$, occurring in the order they appear in $\tau$, and with duplicates removed).

A lifetime projection is a generalized lifetime projection of the form $b\downarrow r$ (that is, a generalized lifetime projection where the associated generalized lifetime is a region).

PCG Lifetime Projections

PCG lifetime projections take the following form

$$\begin{array}{llr}rp& ::=& \text{(Lifetime Projection)}\\ & \mid \hat{p}\downarrow r& \text{(Place Projection)}\\ & \mid \hat{p}\downarrow r\text{at}\ell & \text{(Snapshot of Place Projection)}\\ & \mid \hat{p}\downarrow r\text{at}\text{FUTURE}& \text{(Placeholder Projection)}\\ & \mid c\downarrow r& \text{(Constant Projection)}\end{array}$$

Lifetime Projection Lifetime

The lifetime $r(rp)$ of a lifetime projection $rp$ is conceptually the lifetime $r$ on the right of the $\downarrow$, i.e:

• $r(\hat{p}\downarrow r)=r$
• $r(\hat{p}\downarrow r\text{at}\ell )=r$
• $r(\hat{p}\downarrow r\text{at}\text{FUTURE})=r$
• $r(c\downarrow r)=r$

Lifetime Projection Base

The base $base(rp)$ of a lifetime projection $rp$ is conceptually the part on the left of the $\downarrow$, i.e. defined as follows:

• $base(\hat{p}\downarrow r)=\hat{p}$
• $base(\hat{p}\downarrow r\text{at}\ell )=\hat{p}$
• $base(\hat{p}\downarrow r\text{at}\text{FUTURE})=\hat{p}$
• $base(c\downarrow r)=c$