Commit bb5e0e86 authored by Mickael Laurent's avatar Mickael Laurent
Browse files

trying some new rules... (wip)

parent 50ac8f98
......@@ -122,53 +122,55 @@ TODO: Which restrictions on types? (cannot test a precise arrow type, etc)
{ }
\\
\Infer[Let]
{\Gamma\cvdash p:\{(t_i,\Gamma_i)\}_{i\in I}\\
\forall i\in I.\ \Gamma_i\vdash_{t_i}\letexp x p e : t}
{%\Gamma\cvdash p:\{(t_i,\Gamma_i)\}_{i\in I}\\
%\forall i\in I.\ \Gamma_i\vdash_{t_i}\letexp x p e : t
\Gamma\vdash p:s\\
\Gamma\vdash_{s}\letexp x p e : t
}
{
\Gamma\vdash\letexp x p e : t
}
{ }
\end{mathpar}
\begin{mathpar}
\Infer[ProjC]
{\Gamma \vdash x:\textstyle\bigcup_{j\in J}\pair{t_1^j}{t_2^j}}
{\Gamma \cvdash \pi_i x: \{(t_i^j, \Gamma\subst{x}{\pair{t_1^j}{t_2^j}})\ \alt\ j\in J\}}
{ }
\\
\Infer[AppC]
{
\Gamma \vdash x: \textstyle\bigcup_{i\in I}t_i\quad
\forall i\in I.\ t_i\leq \arrow{t}{s_i}\quad
\Gamma \vdash y: t
}
{ \Gamma \cvdash {x}{y}: \{(s_i, \Gamma\subst{x}{t_i})\ \alt\ i\in I\} }
{ }
\\
\Infer[CaseC]
{
\Gamma_1 = \Gamma\subst{x}{\Gamma(x)\land t}\\
\Gamma_2 = \Gamma\subst{x}{\Gamma(x)\land \neg t}\\
\Gamma_1 \vdash e_1:t_1\\
\Gamma_2 \vdash e_2:t_2}
{\Gamma\cvdash \tcase {x} t {e_1}{e_2}: \{(t_1, \Gamma_1), (t_2, \Gamma_2)\}}
{ }
\\
\Infer[AtomicC]
{\Gamma \vdash a:t}
{\Gamma \cvdash a: \{(t, \Gamma)\}}
{ }
\end{mathpar}
% \begin{mathpar}
% \Infer[ProjC]
% {\Gamma \vdash x:\textstyle\bigcup_{j\in J}\pair{t_1^j}{t_2^j}}
% {\Gamma \cvdash \pi_i x: \{(t_i^j, \Gamma\subst{x}{\pair{t_1^j}{t_2^j}})\ \alt\ j\in J\}}
% { }
% \\
% \Infer[AppC]
% {
% \Gamma \vdash x: \textstyle\bigcup_{i\in I}t_i\quad
% \forall i\in I.\ t_i\leq \arrow{t}{s_i}\quad
% \Gamma \vdash y: t
% }
% { \Gamma \cvdash {x}{y}: \{(s_i, \Gamma\subst{x}{t_i})\ \alt\ i\in I\} }
% { }
% \\
% \Infer[CaseC]
% {
% \Gamma_1 = \Gamma\subst{x}{\Gamma(x)\land t}\\
% \Gamma_2 = \Gamma\subst{x}{\Gamma(x)\land \neg t}\\
% \Gamma_1 \vdash e_1:t_1\\
% \Gamma_2 \vdash e_2:t_2}
% {\Gamma\cvdash \tcase {x} t {e_1}{e_2}: \{(t_1, \Gamma_1), (t_2, \Gamma_2)\}}
% { }
% \\
% \Infer[AtomicC]
% {\Gamma \vdash a:t}
% {\Gamma \cvdash a: \{(t, \Gamma)\}}
% { }
% \end{mathpar}
TODO: Inter rule needed?
TODO: Algorithmic rules
TODO: AppC rule: what about the argument? We could loose precision there...
In the end, these rules look quite similar to the candidate generation rules.
% TODO: AppC rule: what about the argument? We could loose precision there...
% In the end, these rules look quite similar to the candidate generation rules.
TODO: No need for the "choice" rules if applications of union arrow
are splitted without needing to type them???
TODO: Use the "split rules" for the let (instead of the candidate generation rules)
\subsection{Candidates generation rules}
......@@ -283,11 +285,23 @@ are splitted without needing to type them???
}
{ }
\\
\Infer[LetDef]
{
\Gamma\vdash p\triangleright_x \dt
}
{
\Gamma\vdash\letexp y p e \triangleright_x \dt
}
{ }
\qquad
\Infer[Let]
{\Gamma\cvdash p:\{(t_i,\Gamma_i)\}_{i\in I}\\
\forall i\in I.\ \Gamma_i\vdash_{t_i}\letexp x p e \triangleright_x \dt_i}
{%\Gamma\cvdash p:\{(t_i,\Gamma_i)\}_{i\in I}\\
%\forall i\in I.\ \Gamma_i\vdash_{t_i}\letexp x p e \triangleright_x \dt_i
\Gamma\vdash p:s\\
\Gamma\vdash_{s}\letexp x p e \triangleright_x \dt
}
{
\Gamma\vdash\letexp y p e \triangleright_x \textstyle\bigcup_{i\in I} \dt_i
\Gamma\vdash\letexp y p e \triangleright_x \dt%\textstyle\bigcup_{i\in I} \dt_i
}
{ }
\end{mathpar}
......@@ -298,6 +312,8 @@ are splitted without needing to type them???
TODO: Proj: Actually, all the possible types of the first component should be candidates
(similar to the Var case)
TODO: "split rules" that only split in order for an expression to be typeable
\subsection{Forward refinement rules}
\subsection{Backward refinement rules}
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