[−][src]Module minitt::check::expr
Expression checker: infer, instance-of check, normal-form comparison, subtyping, etc.
Depends on modules syntax, read_back and tcm.
Functions
| check | $$
\frac{\rho,\Gamma\vdash_l M\Leftarrow ⟦A_i⟧v}
{\rho,\Gamma\vdash_l c_i \ M \Leftarrow \textsf{Sum}
\lang c_1\ A_1 | \dots | c_n\ A_n,v \rang}
$$
$$
\frac{}{\rho,\Gamma\vdash_l 0 \Leftarrow \textbf{1}}
\quad
\frac{}{\rho,\Gamma\vdash_l \textbf{1} \Leftarrow \textsf{U}}
$$
$$
\frac{\rho,\Gamma\vdash_l M_1\Leftarrow \Pi(⟦A_1⟧v)(g \circ c_1)
\dots
\rho,\Gamma\vdash_l M_n\Leftarrow \Pi(⟦A_n⟧v)(g \circ c_n)}
{\rho,\Gamma\vdash_l \textsf{fun}(c_1\rightarrow M_1 | \dots | c_n \rightarrow M_n)
\Leftarrow \Pi(\textsf{Sum}\lang c_1:A_1 | \dots | c_n:A_n,v \rang)g}
$$
$$
\frac{\rho,\Gamma\vdash_l D\Rightarrow \Gamma_1
\quad (\rho,\Gamma),\Gamma_1\vdash_l M\Leftarrow t}
{\rho,\Gamma\vdash_l D; M\Leftarrow t}
$$
$$
\frac{\rho,\Gamma\vdash_l M\Rightarrow t'
\quad \textsf{R}_l\ t =\textsf{R}_l\ t'}
{\rho,\Gamma\vdash_l M\Leftarrow t}
(\textnormal{If other rules are not applicable})
$$
$$
\dots (\textnormal{There are too many, please checkout the original paper for more})
$$
|
| check_fallback | $$
\frac{\rho,\Gamma\vdash_l M \Rightarrow t'
\quad \textsf{R}_l\ t = \textsf{R}_l\ t'}
{\rho,\Gamma\vdash_l M\Leftarrow t}
$$
Fallback rule of instance check. |
| check_infer | $$
\frac{\Gamma(x)\rightarrow t}
{\rho,\Gamma\vdash_l x\Rightarrow t}
\quad
\frac{\rho,\Gamma\vdash_l M \Rightarrow \Pi\ t\ g
\quad \rho,\Gamma\vdash_l N\Leftarrow t}
{\rho,\Gamma\vdash_l M\ N \Rightarrow \textsf{inst}\ g(⟦N⟧\rho)}
$$
$$
\frac{}{\rho,\Gamma\vdash_l 0 \Rightarrow \textbf{1}}
\quad
\frac{}{\rho,\Gamma\vdash_l \textbf{1} \Rightarrow \textsf{U}}
$$
$$
\frac{\rho,\Gamma\vdash_l M\Rightarrow \Sigma\ t\ g}
{\rho,\Gamma\vdash_l M.1\Rightarrow t}
\quad
\frac{\rho,\Gamma\vdash_l M\Rightarrow \Sigma\ t\ g}
{\rho,\Gamma\vdash_l M.2 \Rightarrow \textsf{inst}\ g((⟦M⟧\rho).1)}
$$
|
| check_level | $$ \frac{i < j}{\Gamma\vdash \textsf{U}_i <: \textsf{U}_j} $$ Level comparison. |
| check_merge_type | To reuse code that checks if a merge expression is well-typed between |
| check_sum_type | $$
\frac{\rho,\Gamma\vdash_l A_1\Leftarrow \textsf{U}
\dots
\rho,\Gamma\vdash_l A_n\Leftarrow \textsf{U}}
{\rho,\Gamma\vdash_l
\textsf{Sum}(c_1\ A_1|\dots|c_n\ A_n)\Leftarrow \textsf{U}}
$$
To reuse code that checks if a sum type is well-typed between |
| check_telescoped | $$
\frac{\rho,\Gamma\vdash_l A
\quad \Gamma\vdash p:⟦A⟧\rho=[\textsf{x}_l]\Rightarrow\Gamma_1
\quad (\rho,p=[\textsf{x}_l]), \Gamma_1\vdash_{l+1}B}
{\rho,\Gamma\vdash_l (\Pi /\Sigma) \ p:A.B}
$$
To reuse code that checks if a sigma or a pi type is well-typed between |
| check_type | $$
\frac{}{\rho,\Gamma\vdash_l \textsf{U}}
$$
$$
\frac{\rho,\Gamma\vdash_l A
\quad \Gamma\vdash p:⟦A⟧\rho=[\textsf{x}_l]\Rightarrow\Gamma_1
\quad (\rho,p=[\textsf{x}_l]), \Gamma_1\vdash_{l+1}B}
{\rho,\Gamma\vdash_l \Pi\ p:A.B}
$$
$$
\frac{\rho,\Gamma\vdash_l A
\quad \Gamma\vdash p:⟦A⟧\rho=[\textsf{x}_l]\Rightarrow\Gamma_1
\quad (\rho,p=[\textsf{x}_l]), \Gamma_1\vdash_{l+1}B}
{\rho,\Gamma\vdash_l \Sigma\ p:A.B}
$$
$$
\frac{\rho,\Gamma\vdash_l A\Leftarrow\textsf{U}}
{\rho,\Gamma\vdash_l A}
\textnormal{(if other rules are not applicable)}
$$
|
| generate_for |