Commit 6f988c52 authored by Mickael Laurent's avatar Mickael Laurent
Browse files

candidate generation rules

parent aad136ff
......@@ -99,6 +99,80 @@ TODO: Algorithmic rules
\subsection{Candidates generation rules}
\begin{mathpar}
\Infer[Var]
{
}
{ \Gamma \vdash y \triangleright_x \varnothing }
{}
\hfill
\Infer[Const]
{
}
{ \Gamma \vdash c \triangleright_x \varnothing }
{}
\hfill
\Infer[Abs]
{\Gamma,(y:s)\vdash e\triangleright_x\dt}
{
\Gamma\vdash\lambda y:s.\ e\triangleright_x\dt
}
{x\neq y}
\vspace{-2.3mm}\\
\Infer[Pair]
{\Gamma \vdash a_1\triangleright_x\dt_1 \and \Gamma \vdash a_2\triangleright_x\dt_2}
{\Gamma \vdash (a_1,a_2)\triangleright_x\dt_1\cup\dt_2}
{}
\hfill
\Infer[Proj]
{\Gamma \vdash a\triangleright_x\dt}
{\Gamma \vdash \pi_i a\triangleright_x\dt}
{}
\vspace{-2.3mm}\\
\Infer[Case]
{\Gamma\subst{y}{\Gamma(y)\land t}\vdash e_1\triangleright_x\dt_1\\
\Gamma\subst{y}{\Gamma(y)\land \neg t}\vdash e_2\triangleright_x\dt_2}
{\Gamma\vdash \tcase{y}{t}{e_1}{e_2}\triangleright_x\dt_1\cup\dt_2\cup
\left\{
\begin{array}{l}
\{\Gamma(x)\land t,\Gamma(x)\land\neg t\} \text{ if } y=x\arcr
\varnothing\text{ otherwise}
\end{array}
\right.}
{}
\vspace{-2.3mm}\\
\Infer[App]
{
\Gamma \vdash a_1 : \textstyle{\bigvee \bigwedge_{i \in I}s_i\to t_i}\\
\Gamma \vdash a_1\triangleright_x\dt_1\\
\forall i\in I.\ \Gamma\fvdash{a_2}{s_i}\{\Gamma_i^j\}_{j\in J_i}
}
{ \Gamma \vdash a_1 a_2\triangleright_x\dt_1\cup\textstyle{\bigcup_{i\in I}
\bigcup_{j\in J_i}\{\Gamma_i^j(x)\}} }
{}
\vspace{-2.3mm}\\
\Infer[Let]
{
\Gamma \vdash p: t\\
\Gamma, (y:t) \vdash e\triangleright_x\dt_x\\
\Gamma, (y:t) \vdash e\triangleright_y\dt_y\\
\forall u\in \dt_y.\ \Gamma\fvdash{p}{u}\{\Gamma_u^i\}_{i\in I_u}
}
{ \Gamma \vdash\letexp{y}{p}{e}\triangleright_x\dt_x\cup\textstyle{
\bigcup_{u\in \dt_y}\bigcup_{i\in I_u}\{\Gamma_u^i(x)\}
}}
{}
\end{mathpar}
TODO: example: application $x y$ with $x$ an union of arrow. Candidates
of a variable with a function type should be all the union of arrows of its type?\\
More generally, a variable that can be written only has an union should be splitted
along this union. Otherwise, $\letexp{x}{\cdots}{x}$ will never be splitted. Or better:
there should be a special split that means "all splits" (it will also be useful when
we will add polymorphism).
TODO: test type system with $\lambda x:\pair{\Int}{\Int}\lor\pair{\Bool}{\Bool}. (\pi_1 x, \pi_2 x)$
\subsection{Forward refinement rules}
\subsection{Backward refinement rules}
......@@ -286,4 +286,8 @@
\newcommand{\RRefineStep}[1]{\textsf{RefineStep}_{#1}}
\newcommand{\dt}[0]{\mathbb{T}}
\newcommand{\fvdash}[2]{\vdash^{\texttt{Env}\rightarrow}_{#1,#2}}
\newcommand{\bvdash}[2]{\vdash^{\texttt{Env}\leftarrow}_{#1,#2}}
\ No newline at end of file
\newcommand{\bvdash}[2]{\vdash^{\texttt{Env}\leftarrow}_{#1,#2}}
\makeatletter % allow us to mention @-commands
\def\arcr{\@arraycr}
\makeatother
\ No newline at end of file
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