Function voile::check::eval::evaluate

fn evaluate(tcs: TCS, abs: Abs) -> (ValInfo, TCS)

Evaluation rules. $$ \newcommand{\xx}[0]{\texttt{x}} \newcommand{\ty}[0]{\tau} \newcommand{\eval}[1]{\llbracket #1 \rrbracket} % {\texttt{eval}(#1)} \newcommand{\piTy}[1]{\Pi \langle #1 \rangle} \newcommand{\sigTy}[1]{\Sigma \langle #1 \rangle} \newcommand{\variant}[1]{\textbf{Sum}\ \{ #1 \}} \newcommand{\record}[1]{\textbf{Rec}\ \{ #1 \}} \newcommand{\variantR}[1]{\mathbb{Sum}\ #1} \newcommand{\recordR}[1]{\mathbb{Rec}\ #1} \newcommand{\cA}[0]{\mathcal A} \newcommand{\cB}[0]{\mathcal B} \newcommand{\labels}[1]{\texttt{labels}(#1)} \newcommand{\fields}[1]{\texttt{fields}(#1)} \newcommand{\tyLab}[0]{\bar \gamma} \newcommand{\labVal}[0]{\bar \delta} \newcommand{\ctyLab}[0]{\gamma} \newcommand{\clabVal}[0]{\delta} \newcommand{\caseTr}[0]{\text{ct}} \newcommand{\caseS}[1]{\langle #1 \rangle} \newcommand{\case}[4]{\textbf{case}\ #1\ #2: #3\ \textbf{or}\ #4} \newcommand{\casevS}[2]{\textbf{split}\ #1\ (#2)} \newcommand{\oneCase}[2]{#1\ #2} \newcommand{\oneCaseL}[2]{\oneCase{#1}{\langle #2 \rangle}} \newcommand{\caseextS}[2]{\textbf{split}\ (#1)\ \textbf{or}\ #2} \newcommand{\nocases}[0]{\textbf{whatever}} \newcommand{\recordext}[2]{\record{#1 \mid #2}} \newcommand{\recExt}[1]{\mid #1} \newcommand{\variantextS}[2]{\variant{#1, \ldots = #2}} \newcommand{\recordextS}[2]{\record{#1, \ldots = #2}} \newcommand{\variantext}[2]{\variant{#1 \mid #2}} \begin{alignedat}{2} & \labels{\emptyset} &&= \emptyset \\ & \labels{n : a, \tyLab} &&= n : \eval{a}, \labels{\tyLab} \\ & \fields{\emptyset} &&= \emptyset \\ & \fields{n = a, \labVal} &&= n = \eval{a}, \fields{\labVal} \\ & && \\ & \eval{a, b} &&= \eval{a}, \eval{b} \\ & \eval{a.1} &&= \left\{\begin{matrix} [k.1] & \text{if} & \eval{a} = [k] \\ \alpha_0 & \text{if} & \eval{a} = \alpha_0, \alpha_1 \end{matrix}\right\} \\ & \eval{a.2} &&= \left\{\begin{matrix} [k.2] & \text{if} & \eval{a} = [k] \\ \alpha_1 & \text{if} & \eval{a} = \alpha_0, \alpha_1 \end{matrix}\right\} \\ & \eval{\lambda \xx. a} &&= \lambda \langle \xx . \eval{a} \rangle \\ & \eval{\xx} &&= [\xx] \\ & \eval{a\ b} &&= \left\{\begin{matrix} [k\ \eval{b}] & \text{if} & \eval{a} = [k] \\ \alpha [\xx := \eval{b}] & \text{if} & \eval{a} = \lambda \langle \xx . \alpha \rangle \\ \left\{\begin{matrix} \alpha [\xx := \beta] & \text{if} & \eval{b} = n\ \beta \\ [\casevS{k}{\oneCaseL{n}{\xx. \alpha}, \caseTr}] & \text{if} & \eval{b} = [k] \\ \end{matrix}\right\} & \text{if} & \eval{a} = \lambda \langle \oneCaseL{n}{\xx. \alpha}, \caseTr \rangle \end{matrix}\right\} \\ & \eval{\piTy{\xx : a.b}} &&= \Pi\ \eval{a}\ \langle \xx . \eval{b} \rangle \\ & \eval{\sigTy{\xx : a.b}} &&= \Sigma\ \eval{a}\ \langle \xx . \eval{b} \rangle \\ & \eval{\variantR{ns}} &&= \variantR{ns} \\ & \eval{\recordR{ns}} &&= \recordR{ns} \\ & \eval{\variant{\tyLab}} &&= \variant{\labels{\tyLab}} \\ & \eval{\record{\tyLab}} &&= \record{\labels{\tyLab}} \\ & \eval{\variantextS{\tyLab_0}{a}} &&= \left\{\begin{matrix} [\variantext{\labels{\tyLab_0}}{k}] & \text{if} & \eval{a} = [k] \\ \variant{\labels{\tyLab_0} \cup \ctyLab_1} & \text{if} & \eval{a} = \variant{\ctyLab_1} \\ [\variantext{\labels{\tyLab_0} \cup \ctyLab_1}{k}] & \text{if} & \eval{a} = [\variantext{\ctyLab_1}{k}] \\ \end{matrix}\right\} \\ & \eval{\recordextS{\tyLab_0}{a}} &&= \left\{\begin{matrix} [\recordext{\labels{\tyLab_0}}{k}] & \text{if} & \eval{a} = [k] \\ \record{\labels{\tyLab_0} \cup \ctyLab_1} & \text{if} & \eval{a} = \record{\ctyLab_1} \\ [\recordext{\labels{\tyLab_0} \cup \ctyLab_1}{k}] & \text{if} & \eval{a} = [\recordext{\ctyLab_1}{k}] \\ \end{matrix}\right\} \\ & \eval{n\ a} &&= n\ \eval{a} \\ & \eval{\{ \labVal \}} &&= \{ \fields{\labVal} \} \\ & \eval{\{ \labVal_0\recExt{a} \}} &&= \left\{\begin{matrix} \{ \fields{\labVal_0} \cup \clabVal_1 \} & \text{if} & \eval{a} = \{ \clabVal_1 \} \\ [\{ \fields{\labVal_0} \cup \clabVal_1\recExt{k} \}] & \text{if} & \eval{a} = [\{ n = \alpha, \ctyLab_1\recExt{k} \}] \\ [\{ \fields{\labVal_0}\recExt{k} \}] & \text{if} & \eval{a} = [k] \\ \end{matrix}\right\} \\ & \eval{a.n} &&= \left\{\begin{matrix} [k.n] & \text{if} & \eval{a} = [k] \\ \alpha & \text{if} & \eval{a} = \{ n = \alpha, \ctyLab \} \\ \end{matrix}\right\} \\ & \eval{\nocases} &&= \lambda \langle \rangle \\ & \eval{\case{n}{\xx}{a}{b}} &&= \left\{\begin{matrix} \lambda \langle \oneCaseL{n}{\xx. \eval{a}}, \caseTr \rangle & \text{if} & \eval{b} = \lambda \langle \caseTr \rangle \\ \caseextS{\oneCaseL{n}{\xx. \eval{a}}}{k} & \text{if} & \eval{b} = [k] \\ \end{matrix}\right\} \\ & \eval{\ty} &&= \ty \end{alignedat} $$

Ensure abs is well-typed before invoking this, otherwise this function may panic or produce ill-typed core term.