Commit 466a3f78 authored by Mickael Laurent's avatar Mickael Laurent
Browse files

fix let rules (definitions should always be retyped when splitting)

parent 02d6ecbb
......@@ -260,21 +260,26 @@ rules, because one branch is already unreachable and retyping only occurs with s
\\
\Infer[LetNoRefine]
{
\Gamma\avdash{\Gammap\setminus\{x\}}{\ct[\letexp x a {[]}]} e : S
\Gamma\avdash{\Gammap}\ct a:\{(t_1,\Gamma_1)\}\\
\Gamma_1'=\Gamma_1\subst{x}{\Gamma_1(x)\land t_1}\\
x\not\in\dom\Gammap\text{ or }\Gamma_1'(x)\leq \Gammap(x)\\
\Gamma_1'\avdash{\Gammap\setminus\{x\}}{\ct[\letexp x a {[]}]} e : S
}
{
\Gamma\avdash\Gammap\ct\letexp x a e : S
}
{ x\in\dom\Gamma \text{ and } (x\not\in\dom\Gammap \text{ or } \Gamma(x)\leq\Gammap(x)) }
{ }
\\
\Infer[LetRefine]
{
\Gamma\bvdash{a}{\Gamma(x)\land\Gammap(x)}\{(t_i,\Gamma_i)\}_{i\in I}\\
\forall i\in I.\ \Gamma\subst{x}{t_i}\avdash{(\Gammap\land\Gamma_i)\setminus\{x\}}{[]} \ct[\letexp x a e] : S_i}
\Gamma\avdash{\Gammap}\ct a:\{(t_1,\Gamma_1)\}\\
\Gamma_1'=\Gamma_1\subst{x}{\Gamma_1(x)\land t_1}\\
\Gamma_1'\bvdash{a}{\Gamma_1'(x)\land\Gammap(x)}\{(t_i,\Gamma_i)\}_{i\in I}\\
\forall i\in I.\ \Gamma_1'\subst{x}{t_i}\avdash{(\Gammap\land\Gamma_i)\setminus\{x\}}{[]} \ct[\letexp x a e] : S_i}
{
\Gamma\avdash\Gammap\ct\letexp x a e : \textstyle\bigcup_{i\in I} S_i
}
{ x\in\dom\Gamma \text{ and } x\in\dom\Gammap \text{ and } \Gamma(x) \not\leq \Gammap(x) }
{ }
\end{mathpar}
\begin{mathpar}
......@@ -289,7 +294,7 @@ rules, because one branch is already unreachable and retyping only occurs with s
{ }
\end{mathpar}
\subsection{Backward typing rules}
\subsection{Backward refinement rules}
\begin{mathpar}
\Infer[Var]
......@@ -522,21 +527,26 @@ rules, because one branch is already unreachable and retyping only occurs with s
\\
\Infer[LetNoRefine]
{
\Gamma\avdash{\Gammap\setminus\{x\}}{\ct[\letexp x a {[]}]} e : \tree
\Gamma\avdash{\Gammap}\ct a:\Node(t_1,\Gamma_1)\\
\Gamma_1'=\Gamma_1\subst{x}{\Gamma_1(x)\land t_1}\\
x\not\in\dom\Gammap\text{ or }\Gamma_1'(x)\leq \Gammap(x)\\
\Gamma_1'\avdash{\Gammap\setminus\{x\}}{\ct[\letexp x a {[]}]} e : \tree
}
{
\Gamma\avdash\Gammap\ct\letexp x a e : \tree
}
{ x\in\dom\Gamma \text{ and } (x\not\in\dom\Gammap \text{ or } \Gamma(x)\leq\Gammap(x)) }
{ }
\\
\Infer[LetRefine]
{
\Gamma\bvdash{a}{\Gamma(x)\land\Gammap(x)}\{(t_i,\Gamma_i)\}_{i\in I}\\
\forall i\in I.\ \Gamma\subst{x}{t_i}\avdash{(\Gammap\land\Gamma_i)\setminus\{x\}}{[]} \ct[\letexp x a e] : \tree_i}
\Gamma\avdash{\Gammap}\ct a:\{(t_1,\Gamma_1)\}\\
\Gamma_1'=\Gamma_1\subst{x}{\Gamma_1(x)\land t_1}\\
\Gamma_1'\bvdash{a}{\Gamma_1'(x)\land\Gammap(x)}\{(t_i,\Gamma_i)\}_{i\in I}\\
\forall i\in I.\ \Gamma_1'\subst{x}{t_i}\avdash{(\Gammap\land\Gamma_i)\setminus\{x\}}{[]} \ct[\letexp x a e] : \tree_i}
{
\Gamma\avdash\Gammap\ct\letexp x a e : \Node(\Gamma, \{\tree_i\}_{i\in I})
\Gamma\avdash\Gammap\ct\letexp x a e : \Node(\Gamma_1', \{\tree_i\}_{i\in I})
}
{ x\in\dom\Gamma \text{ and } x\in\dom\Gammap \text{ and } \Gamma(x) \not\leq \Gammap(x) }
{ }
\end{mathpar}
\begin{mathpar}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment