Module voile::check::eval

Tooling functions that depends on neither decl nor expr. $$ \llbracket a \rrbracket = \alpha $$

Functions

compile_cons	Evaluate a single constructor as a lambda.
evaluate	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{\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} \\ & && \\ & \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 \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{\ty} &&= \ty \end{alignedat} $$
expand_global	Expand global references to concrete values, like meta references or global references due to recursion.