Commit 2394f896 authored by Mickael Laurent's avatar Mickael Laurent
Browse files

simplify backtyping + some fixes

parent 05f8792a
......@@ -274,8 +274,8 @@ rules, because one branch is already unreachable and retyping only occurs with s
{
\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_1'\bvdash{a}{\Gammap(x)}\{\Gamma_i\}_{i\in I}\\
\forall i\in I.\ \Gamma_1'\subst{x}{\Gamma(x)\land\Gammap(x)}\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
}
......@@ -299,22 +299,22 @@ rules, because one branch is already unreachable and retyping only occurs with s
\begin{mathpar}
\Infer[Var]
{ }
{\Gamma\bvdash x t \{(t, \subst{x}{t})\}}
{\Gamma\bvdash x t \{\{x:t\}\}}
{ }
\qquad
\Infer[Const]
{ }
{\Gamma\bvdash c t \{(t, \{\})\}}
{\Gamma\bvdash c t \{\{\}\}}
{ }
\\
\Infer[Inter]
{\Gamma\vdash e:t' \\ \Gamma\bvdash e {t\wedge t'} \{(t_i, \Gamma_i)\}_{i\in I}}
{\Gamma\bvdash e t \{(t_i, \Gamma_i)\}_{i\in I}}
{ }
\qquad
\Infer[EFQ]
{\Gamma\bvdash e t \{(t_i,\Gamma_i)\}_{i\in I}\cup\{(\Empty, \Gamma')\}}
{\Gamma\bvdash e t \{(t_i,\Gamma_i)\}_{i\in I}}
% \Infer[Inter]
% {\Gamma\vdash e:t' \\ \Gamma\bvdash e {t\wedge t'} \Gammas}
% {\Gamma\bvdash e t \Gammas}
% { }
% \qquad
\Infer[Normalize]
{\Gamma\bvdash e t \Gammas\cup\{\Gamma'\}\\\exists x\in\dom{\Gamma'}.\ \Gamma'(x)=\Empty}
{\Gamma\bvdash e t \Gammas}
{ }
\\
\Infer[Pair]
......@@ -322,53 +322,59 @@ rules, because one branch is already unreachable and retyping only occurs with s
\forall i\in I.\ \Gamma_1^i = \subst{x_1}{t_i}\\
\forall i\in I.\ \Gamma_2^i = \subst{x_2}{s_i}
}
{\Gamma\bvdash {(x_1,x_2)} {\bigcup_{i\in I}(t_i,s_i)} \bigcup_{i\in I}\{(\pair{t_i}{s_i}, \Gamma_1^i\land\Gamma_2^i)\}}
{\Gamma\bvdash {(x_1,x_2)} {\bigcup_{i\in I}(t_i,s_i)} \textstyle\bigcup_{i\in I}\{\Gamma_1^i\land\Gamma_2^i\}}
{ }
\\
\Infer[Proj]
{
i = 1 \Rightarrow t' = \pair{t}{\Any}\\
i = 2 \Rightarrow t' = \pair{\Any}{t}
}
{\Gamma\bvdash {\pi_i x}{t} \{(t,\subst{x}{\Gamma(x)\land t'})\}}
\Infer[Proj1]
{ }
{\Gamma\bvdash {\pi_1 x}{t} \{x:\pair{t}{\Any}\}}
{ }
\qquad
\Infer[Proj2]
{ }
{\Gamma\bvdash {\pi_2 x}{t} \{x:\pair{\Any}{t}\}}
{ }
\\
\Infer[App]
{\Gamma(x_1)\equiv\bigvee_{i\in I}u_i \\ \Gamma(x_2)=t'\\
{\Gamma(x_1)\equiv\textstyle\bigvee_{i\in I}u_i \\
\forall i\in I.\ u_i\leq \arrow{\neg t_i}{s_i} \text{ with } s_i\land t = \varnothing \\
\forall i\in I.\ \Gamma_1^i = \subst{x_1}{u_i}\\
\forall i\in I.\ \Gamma_2^i = \subst{x_2}{t_i\land t'}\\
\forall i\in I.\ u_i\leq\arrow{(t_i\land t')}{s_i}}
\forall i\in I.\ \Gamma_2^i = \subst{x_2}{t_i}
}
{
\Gamma\bvdash {(x_1\ x_2)} {t} \bigcup_{i\in I}\{(s_i\land t, \Gamma_{1}^i\land\Gamma_{2}^i)\}
\Gamma\bvdash {(x_1\ x_2)} {t} \textstyle\bigcup_{i\in I}\{\Gamma_{1}^i\land\Gamma_{2}^i\}
}
{ }
\\
\Infer[Case]
{
\Gamma\subst{x}{t_x\land\Gamma(x)} \bvdash {e_1} {t} \{(t_i,\Gamma_1^i)\}_{i\in I}\\
\Gamma\subst{x}{\neg t_x\land\Gamma(x)} \bvdash {e_2} {t} \{(s_j,\Gamma_2^j)\}_{j\in J}}
{\Gamma\bvdash {\tcase {x} {t_x} {e_1}{e_2}}{t} \{(t_i,\Gamma_1^i\subst{x}{t_x\land\Gamma_1^i(x)})\}_{i\in I}
\cup \{(s_j,\Gamma_2^j\subst{x}{\neg t_x\land\Gamma_2^j(x)})\}_{j\in J}}
\Gamma\subst{x}{t_x\land\Gamma(x)} \bvdash {e_1} {t} \{\Gamma_1^i\}_{i\in I}\\
\Gamma\subst{x}{\neg t_x\land\Gamma(x)} \bvdash {e_2} {t} \{\Gamma_2^j\}_{j\in J}}
{\Gamma\bvdash {\tcase {x} {t_x} {e_1}{e_2}}{t}
\{\Gamma_1^i\land\{x:t_x\}\}_{i\in I}
\cup \{\Gamma_2^j\land\{x:\neg t_x\}\}_{j\in J}}
{ }
\\
\Infer[Abs]
{ }
{\Gamma\bvdash {\lambda x:s.\ e}{t} \{(t,\{\})\}}
{ }
\qquad
\Infer[Abs-]
{t\leq \arrow{t_1}{t_2}\\ t_1\not\leq s}
{\Gamma\bvdash {\lambda x:s.\ e}{t} \{\}}
{ }
\qquad
\Infer[Abs]
{ }
{\Gamma\bvdash {\lambda x:s.\ e}{t} \{\{\}\}}
{ }
\\
\Infer[Let]
{
\Gamma\bvdash{e}{t} \{(t_i,\Gamma_i)\}_{i\in I}\\
\forall i\in I.\ \Gamma\land\Gamma_i\bvdash{a}{\Gamma\land\Gamma_i)(x)} \{(t_i^j,\Gamma_i^j)\}_{j\in J_i}
\Gamma\bvdash{e}{t} \{\Gamma_i\}_{i\in I}\\
\forall i\in I.\ x\in\dom{\Gamma_i}\Rightarrow
\Gamma\land\Gamma_i\bvdash{a}{\Gamma_i(x)} \{\Gamma_i^j\}_{j\in J_i}\\
\forall i\in I.\ x\not\in\dom{\Gamma_i}\Rightarrow
\{\Gamma_i^j\}_{j\in J_i} = \{\{\}\}
}
{
\Gamma\bvdash{\letexp{x}{a}{e}}{t} \{(t_i,\Gamma_i\land\Gamma_i^j)\ \alt\ i\in I,\ j\in J_i\}
\Gamma\bvdash{\letexp{x}{a}{e}}{t} \{\Gamma_i\land\Gamma_i^j\ \alt\ i\in I,\ j\in J_i\}
}
{ }
\end{mathpar}
......@@ -379,11 +385,6 @@ the environment is supposed to already contain a type for $x$.
TODO: Simplify Case rule: as the expression has been typed before backtyping,
$x$ is supposed to be included into $t_x$ or $\neg t_x$.
TODO: No need to return the type of the expression. The definition will be retyped anyway
after the splits.
TODO: The Inter rule seems to be not needed needed anymore (now that result of backtyping must be intersected with the original env)
TODO: Algorithmic App, Inter and EFQ rule
\subsection{Algorithmic typing rules (alternative attempt)}
......@@ -539,8 +540,8 @@ rules, because one branch is already unreachable and retyping only occurs with s
{
\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_1'\bvdash{a}{\Gammap(x)}\{\Gamma_i\}_{i\in I}\\
\forall i\in I.\ \Gamma_1'\subst{x}{\Gamma(x)\land\Gammap(x)}\avdash{(\Gammap\land\Gamma_i)\setminus\{x\}}{[]} \ct[\letexp x a e] : \tree_i}
{
\Gamma\avdash\Gammap\ct\letexp x a e : \Node(\Gamma_1', \{\tree_i\}_{i\in I})
}
......
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