[−][src]Module voile::check::expr
Expression/Type relevant checking. $$ \newcommand{\tyck}[0]{\vdash_\texttt{c}} \newcommand{\Gtyck}[0]{\Gamma \tyck} \newcommand{\infer}[0]{\vdash_\texttt{i}} \newcommand{\Ginfer}[0]{\Gamma \infer} \Ginfer a \Rightarrow o \quad \Gtyck a:m \Rightarrow o \quad \Gamma \vdash A <: B $$
Functions
| check | Check an abstract term against an expected type and produce a well-typed term. $$ \newcommand{\tyck}[4]{#1 \vdash_\texttt{c} #2 : #3 \Rightarrow #4} \newcommand{\Gtyck}[3]{\tyck{\Gamma}{#1}{#2}{#3}} \newcommand{\eval}[1]{\llbracket #1 \rrbracket} % {\texttt{eval}(#1)} \newcommand{\cheval}[3]{#1 \vdash_\texttt{e} #2 \Rightarrow #3} \newcommand{\Gcheval}[2]{\cheval{\Gamma}{#1}{#2}} \newcommand{\subt}[0]{<:} \newcommand{\xx}[0]{\texttt{x}} \newcommand{\ty}[0]{\tau} \newcommand{\piTy}[1]{\Pi \langle #1 \rangle} \newcommand{\sigTy}[1]{\Sigma \langle #1 \rangle} \newcommand{\recordext}[2]{\record{#1 \mid #2}} \newcommand{\recExt}[1]{\mid #1} \newcommand{\variant}[1]{\textbf{Sum}\ { #1 }} \newcommand{\record}[1]{\textbf{Rec}\ { #1 }} \newcommand{\nocases}[0]{\textbf{whatever}} \newcommand{\case}[4]{\textbf{case}\ #1\ #2: #3\ \textbf{or}\ #4} \newcommand{\variantext}[2]{\variant{#1 \mid #2}} \newcommand{\ctyLab}[0]{\gamma} \newcommand{\cA}[0]{\mathcal A} \newcommand{\cB}[0]{\mathcal B} \cfrac{ \Gtyck{a}{\cA}{\alpha} \quad \Gtyck{b}{\cB[\xx := \alpha]}{\beta} }{ \Gcheval{a, b}{\sigTy{\xx : \cA . \cB}} } \quad \cfrac{ \tyck{\Gamma, \xx : \cB}{a}{\cA}{\alpha} }{ \Gtyck{ \lambda \xx. \alpha}{\piTy{\xx : \cB . \cA} }{ \lambda \langle \xx . \alpha \rangle } } \\ \space \\ \cfrac{ \Gtyck{B}{\ty}{\cB} \quad \Gcheval{b}{\cB} }{ \cfrac{ \Gcheval{a}{\record{\ctyLab}} }{ \Gcheval{ \{ n = b\recExt{a} \} }{ \record{n : \cB, \ctyLab} } } \quad \cfrac{ \Gcheval{a}{[k]} }{ \Gcheval{ \{ n = b\recExt{a} \} }{ [\recordext{n : \cB}{k}] } } } \\ \space \\ \cfrac{ \Gtyck{A}{\ty}{\cA} }{ \Gcheval{\nocases}{ \piTy{\xx : \variant{} . \cA} } \quad \cfrac{ \Gtyck{a}{\variant{}}{\alpha} }{ \Gtyck{\nocases\ a}{\cA}{\alpha} } } \\ \space \\ \cfrac{ \cheval{\Gamma,\xx : \cA_1}{b}{\cB} \quad \Gtyck{A_1}{\ty}{\cA_1} }{ \cfrac{ \Gcheval{a}{\piTy{\xx : \variant{\ctyLab} . \cB}} }{ \Gcheval{ (\case{n}{\xx}{b}{a}) }{ \piTy{\xx : \variant{n : \cA_1, \ctyLab} . \cB} } } \quad \cfrac{ \Gcheval{a}{\piTy{\xx : [k] . \cB}} }{ \Gcheval{ (\case{n}{\xx}{b}{a}) }{ \piTy{\xx : [\variantext{n : \cA_1}{k}] . \cB} } } } $$ |
| check_app_type | Recursive function to insert meta for implicit argument |
| check_fallback | |
| check_fields | |
| check_fields_no_more | |
| check_row_polymorphic_type | Extracted from |
| infer | Infer type of an abstract term, if it's well-typed. $$ \newcommand{\tyck}[4]{#1 \vdash_\texttt{c} #2 : #3 \Rightarrow #4} \newcommand{\Gtyck}[3]{\tyck{\Gamma}{#1}{#2}{#3}} \newcommand{\eval}[1]{\llbracket #1 \rrbracket} % {\texttt{eval}(#1)} \newcommand{\infer}[3]{#1 \vdash_\texttt{i} #2 \Leftarrow #3} \newcommand{\Ginfer}[2]{\infer{\Gamma}{#1}{#2}} \newcommand{\subt}[0]{<:} \newcommand{\xx}[0]{\texttt{x}} \newcommand{\ty}[0]{\tau} \newcommand{\piTy}[1]{\Pi \langle #1 \rangle} \newcommand{\sigTy}[1]{\Sigma \langle #1 \rangle} \newcommand{\tyLab}[0]{\bar \gamma} \newcommand{\ctyLab}[0]{\gamma} \newcommand{\labVal}[0]{\bar \delta} \newcommand{\record}[1]{\textbf{Rec}\ \{ #1 \}} \newcommand{\cA}[0]{\mathcal A} \newcommand{\cB}[0]{\mathcal B} \cfrac{ \Gtyck{A}{\ty}{\cA}\quad \tyck{\Gamma, (\xx : \cA)}{B}{\ty}{\cB} }{ \Ginfer{\piTy{\xx : A . B}}{\ty} \quad \Ginfer{\sigTy{\xx : A . B}}{\ty} } \quad \cfrac{}{\Ginfer{\ty}{\ty}} \\ \space \\ \cfrac{ \Ginfer{a}{\sigTy{\xx : \cA . \cB}} }{ \Ginfer{a.1}{\cA} \quad \Ginfer{a.2}{\cB[\xx := \eval{a.1}]} } \quad \cfrac{ \Ginfer{a}{\piTy{\xx : \cB . \cA}} \quad \Gtyck{b}{\cB}{\beta} }{ \Ginfer{a\ b}{\cA [\xx := \eval{b}]} } \\ \space \\ \cfrac{ \Ginfer{a}{\cA} \quad \Ginfer{ \{\labVal\} }{ \record{\ctyLab} } \quad (n : \cA) \notin \ctyLab }{ \Ginfer{ \{n = a, \labVal\} }{ \record{n : \cA, \ctyLab} } } \quad \cfrac{ \Ginfer{a}{\record{n : \cA, \ctyLab}} }{ \Ginfer{a .n}{\cA} } $$ |
| mock_for | |
| subtype | Check if |