Commit 15f67411 authored by Mickael Laurent's avatar Mickael Laurent
Browse files

trying some new rules... (wip)

parent 27973961
......@@ -329,3 +329,58 @@ TODO: Algorithmic rules
\subsection{Forward refinement rules}
\subsection{Backward refinement rules}
\begin{mathpar}
\Infer[Var]
{ }
{\Gamma\bvdash x t \{(t, \Gamma\subst{x}{t})\}}
{ }
\qquad
\Infer[Const]
{ }
{\Gamma\bvdash c t \{(t, \Gamma)\}}
{ }
\\
% \Infer[Comp]
% {\Gamma\bvdash e t \{(t_i, \Gamma_i)\}_{i\in I} \\ \forall i.\ \Gamma_i\bvdash e {t_i} \{(t_i^j, \Gamma_i^j)\}_{j\in J_i}}
% {\Gamma\bvdash e t \{(t_i^j, \Gamma_i^j)\ \alt\ i\in I, j\in J_i\}}
% { }
%\qquad
\Infer[Inter]
%{\Gamma\vdash e:t' \\ \Gamma\subst{e}{t\wedge t'}\bvdash e {t\wedge t'} \bbGamma}
{\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}}
{ }
\\
\Infer[EFQ]
{ }
{\Gamma,(x:\Empty)\bvdash e t \{\}}
{ }
\qquad
\Infer[Pair]
{\forall i\in I.\ \Gamma\bvdash{e_1}{t_i}\{(t_i^j,\Gamma_{1,i}^j)\}_{j\in J_i} \\ \forall i\in I.\ \Gamma\bvdash{e_2}{s_i}\{(s_i^k,\Gamma_{2,i}^k)\}_{k\in K_i}}
{\Gamma\bvdash {(e_1,e_2)} {\bigcup_{i\in I}(t_i,s_i)} \bigcup_{i\in I}\{(\pair{t_i^j}{s_i^k}, \Gamma_{1,i}^j\land\Gamma_{2,i}^k)\ |\ j\in J_i, k\in K_i\}}
{ }
\\
\Infer[App]
{\Gamma\vdash e_1:\bigvee_{i\in I}u_i \\ \Gamma\vdash e_2:t_2\\
\forall i\in I.\ u_i\leq \arrow{(\neg t_i \land t_2)}{s_i'} \text{ with } s_i'\land t = \varnothing \\
\forall i\in I.\ u_i\leq \arrow{t_i}{s_i}\\
\forall i\in I.\ \Gamma\bvdash{e_1}{u_i}\{(\_, \Gamma_{1,i}^j)\}_{j\in J_i} \\ \forall i\in I.\ \Gamma\bvdash{e_2}{t_i}\{(\_, \Gamma_{2,i}^k)\}_{k\in K_i}}
{\Gamma\bvdash {(e_1\ e_2)} {t} \bigcup_{i\in I}\{(s_i, \Gamma_{1,i}^j\land\Gamma_{2,i}^k)\ |\ j\in J_i, k\in K_i\}}
{ }
\\
\Infer[Case]
{
\Gamma,(x:t_e\land\Gamma(t_e)) \bvdash {e_1} {t} \{(t_i,\Gamma_1^i)\}_{i\in I}\\
\Gamma,(x:\neg t_e\land\Gamma(t_e)) \bvdash {e_2} {t} \{(s_j,\Gamma_2^j)\}_{j\in J}}
{\Gamma\bvdash {\tcase {x} {t_e} {e_1}{e_2}}{t} \{(t_i,\Gamma_1^i)\}_{i\in I} \cup \{(s_j,\Gamma_2^j)\}_{j\in J}}
{ }
\end{mathpar}
TODO: Is the Comp rule needed in this new setting where every application is alone in a let,
and where union-arrow app are backtyped by splitting possibilities?
TODO: rename e to the right element according to the grammar
TODO: Let rule
......@@ -36,7 +36,7 @@
{ }
\\
\Infer[App]
{\Gamma\vdash e_1:\bigcup_{i\in I}t_i \\ \forall i\in I.\ t_i\leq \arrow{\neg s_i}{s_i'} \text{ with } s_i'\land t = \varnothing \\ \forall i\in I.\ \Gamma\evdash{e_1}{t_i}\bbGamma_1^i \\ \forall i\in I.\ \Gamma\evdash{e_2}{s_i}\bbGamma_2^i}
{\Gamma\vdash e_1:\bigvee_{i\in I}t_i \\ \forall i\in I.\ t_i\leq \arrow{\neg s_i}{s_i'} \text{ with } s_i'\land t = \varnothing \\ \forall i\in I.\ \Gamma\evdash{e_1}{t_i}\bbGamma_1^i \\ \forall i\in I.\ \Gamma\evdash{e_2}{s_i}\bbGamma_2^i}
{\Gamma\evdash {(e_1\ e_2)} {t} \bigcup_{i\in I}\{\Gamma_1\land\Gamma_2\ |\ \Gamma_1\in\bbGamma_1^i, \Gamma_2\in\bbGamma_2^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