Commit 10412c32 authored by Mickael Laurent's avatar Mickael Laurent
Browse files

fix

parent d217479a
......@@ -310,6 +310,11 @@ rules, because one branch is already unreachable and retyping only occurs with s
% {\Gamma\bvdash e t \Gammas}
% { }
% \qquad
\Infer[EFQ]
{\exists x\in\dom{\Gamma}.\ \Gamma(x)=\Empty}
{\Gamma\bvdash e t \{\}}
{ }
\qquad
\Infer[Normalize]
{\Gamma\bvdash e t \Gammas\cup\{\Gamma'\}\\\exists x\in\dom{\Gamma'}.\ \Gamma'(x)=\Empty}
{\Gamma\bvdash e t \Gammas}
......@@ -365,7 +370,7 @@ rules, because one branch is already unreachable and retyping only occurs with s
{ }
\\
\Infer[Abs-]
{t\leq \arrow{t_1}{t_2}\\ t_1\not\leq s}
{\dom t\not\leq s}
{\Gamma\bvdash {\lambda x:s.\ e}{t} \{\}}
{ }
\qquad
......@@ -391,6 +396,8 @@ rules, because one branch is already unreachable and retyping only occurs with s
NOTE: For the Let rule: as the expression $a$ has been typed before backtyping,
the environment is supposed to already contain a type for $x$.
NOTE: The declarative rule for the application is as follows:
\begin{mathpar}
\Infer[App]
{\Gamma(x_1)\equiv\textstyle\bigvee_{i\in I}u_i \\
......@@ -406,6 +413,95 @@ the environment is supposed to already contain a type for $x$.
TODO: Simplify Case and Let rule: as the expression has been typed before backtyping,
$x$ is supposed to be included into $t_x$ or $\neg t_x$.
\newpage
\subsection{Forward refinement rules}
\begin{mathpar}
\Infer[EFQ]
{\exists x\in\dom{\Gamma}.\ \Gamma(x)=\Empty}
{\Gamma\bvdash e t \{\}}
{ }
\qquad
\Infer[Normalize]
{\Gamma\fvdash e t \Gammas\cup\{\Gamma'\}\\\exists x\in\dom{\Gamma'}.\ \Gamma'(x)=\Empty}
{\Gamma\fvdash e t \Gammas}
{ }
\\
\Infer[Var]
{ }
{\Gamma\fvdash x t \{\{x:t\}\}}
{ }
\qquad
\Infer[Const]
{ }
{\Gamma\fvdash c t \{\{\}\}}
{ }
\\
\Infer[Pair]
{
\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\fvdash {(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[Proj1]
{ }
{\Gamma\fvdash {\pi_1 x}{t} \{x:\pair{t}{\Any}\}}
{ }
\qquad
\Infer[Proj2]
{ }
{\Gamma\fvdash {\pi_2 x}{t} \{x:\pair{\Any}{t}\}}
{ }
\\
\Infer[App]
{
\Gamma(x_1) \btr t = s \\
\Gamma_1 = \subst{x_1}{\Gamma(x_1)}\\
\Gamma_2 = \subst{x_2}{s}
}
{
\Gamma\fvdash {(x_1\ x_2)} {t} \{\Gamma_{1}\land\Gamma_{2}\}
}
{ }
\\
\Infer[Case]
{
\Gamma\subst{x}{t_x\land\Gamma(x)} \fvdash {e_1} {t} \{\Gamma_1^i\}_{i\in I}\\
\Gamma\subst{x}{\neg t_x\land\Gamma(x)} \fvdash {e_2} {t} \{\Gamma_2^j\}_{j\in J}}
{\Gamma\fvdash {\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\avdash{\{\}}{[]}\lambda x:s.\ e:\tree\\
\{\Leaf(t_i,\Gamma_i)\}_{i\in I} = \tleaves(\tree)}
{\Gamma\fvdash {\lambda x:s.\ e}{t} \{\Gamma_i\,\alt\,i\in I\text{ s.t. }t_i\leq t\}}
{ }
\qquad
\Infer[Abs-]
{ }
{\Gamma\fvdash {\lambda x:s.\ e}{t} \{\}}
{ }
\\
\Infer[Let]
{
\Gamma\fvdash{e}{t} \{\Gamma_i\}_{i\in I}\\
\forall i\in I.\ x\in\dom{\Gamma_i}\Rightarrow
\Gamma\land\Gamma_i\fvdash{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\fvdash{\letexp{x}{a}{e}}{t} \{\Gamma_i\land\Gamma_i^j\ \alt\ i\in I,\ j\in J_i\}
}
{ }
\end{mathpar}
TODO: Update rule Let (current versions is incorrect)
\newpage
\subsection{Algorithmic typing rules (alternative attempt)}
......
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