Commit 4f9dd98e authored by Mickael Laurent's avatar Mickael Laurent
Browse files

trying some new rules... (wip)

parent 485cee3c
......@@ -330,6 +330,26 @@ TODO: Algorithmic rules
\subsection{Forward refinement rules}
\begin{mathpar}
\Infer[App]
{\Gamma\vdash e_1:\bigvee_{i\in I}u_i \\
\forall i\in I.\ u_i\leq \arrow{t_i}{t}\\
\forall i\in I.\ \Gamma\fvdash{e_1}{u_i}\{(u_i^j, \Gamma_{1,i}^j)\}_{j\in J_i} \\ \forall i\in I.\ \Gamma\fvdash{e_2}{t_i}\{(t_i^k, \Gamma_{2,i}^k)\}_{k\in K_i}\\
\forall i\in I.\ \forall j\in J_i.\ \forall k\in K_i.\ u_i^j\leq\arrow{t_i^k}{s_i^{j,k}}}
{\Gamma\fvdash {(e_1\ e_2)} {t} \bigcup_{i\in I}\{(s_i^{j,k}, \Gamma_{1,i}^j\land\Gamma_{2,i}^k)\ |\ j\in J_i, k\in K_i\}}
{ }
\\
\Infer[Abs]
{\Gamma\vdash \lambda x:s.\ e:t'\\t'\leq t}
{\Gamma\fvdash {\lambda x:s.\ e}{t} \{(t',\Gamma)\}}
{ }
\qquad
\Infer[Abs-]
{ }
{\Gamma\fvdash {\lambda x:s.\ e}{t} \{\}}
{ }
\end{mathpar}
\subsection{Backward refinement rules}
\begin{mathpar}
......@@ -401,6 +421,11 @@ TODO: Algorithmic rules
{\Gamma\vdash \lambda x:s.\ e:t'}
{\Gamma\bvdash {\lambda x:s.\ e}{t} \{(t\land t',\Gamma)\}}
{ }
\qquad
\Infer[Abs-]
{t\leq \arrow{t_1}{t_2}\\ t_1\not\leq s}
{\Gamma\bvdash {\lambda x:s.\ e}{t} \{\}}
{ }
\\
\Infer[LetBase]
{
......@@ -437,5 +462,3 @@ TODO: Is the Comp rule needed in this new setting where every application is alo
and where union-arrow app are backtyped by splitting possibilities?
TODO: rename e to the right element according to the grammar
TODO: Let rule
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