Type-Checking Monad: context, state and error.
Typing context (Gamma) and its updater, the type-checking error and its pretty-printer
Depends on module syntax.
| TCS | Type-Checking State , not "Theoretical Computer Science".
This is not present in Mini-TT.
|
| mismatch | |
| update_gamma | Move version of upG in Mini-TT.
$$
\frac{}{\Gamma \vdash x:t=v\Rightarrow \Gamma,x:t}
\quad
\frac{}{\Gamma \vdash _:t=v\Rightarrow \Gamma}
$$
$$
\frac{\Gamma \vdash p_1:t_1=v.1 \Rightarrow \Gamma_1
\quad \Gamma \vdash p_2:\textsf{inst}\ g(v.1)=v.2 \Rightarrow \Gamma_2}
{\Gamma \vdash (p_1,p_2):\Sigma\ t_1\ g=v\Rightarrow \Gamma_2}
$$
Cow is used to simulate immutability.
|
| update_gamma_borrow | Borrow version of upG in Mini-TT.
|
| update_gamma_by_pair | Some minor helper specialized from other functions.
|
| update_gamma_by_var | Some minor helper specialized from other functions.
|
| update_gamma_lazy | Lazy version of upG in Mini-TT.
|
| Gamma | $\Gamma ::= () \ | \ \Gamma, x : t$,
Gamma in Mini-TT.
By aliasing BTreeMap to Gamma, we get lookupG in Mini-TT for free.
|
| GammaRaw | Since we have no place to document lookupG I'll put it here:
$$
\frac{}{(\Gamma, a:t)(x)\rightarrow t}
\quad
\frac{\Gamma(x) \rightarrow t}
{(\Gamma, y:t')(x)\rightarrow t} y \neq x
$$
Type-Checking context. Name as key, type of the declaration as value.
|
| TCM | G in Mini-TT.
Type-Checking Monad.
|