Commit 11b0b876 authored by Mickael Laurent's avatar Mickael Laurent
Browse files

trying some new rules... (wip)

parent 6066a29c
......@@ -16,6 +16,9 @@
\end{array}
\end{equation}
TODO: Only allow variables and both sides of a application / projection? It would simplify
rules...
TODO: the then and else expressions of typecases have no associated variable,
altough the env refinement rules could refine their types...
Is this an issue? Should we require an atomic in the then and else branchs
......@@ -77,15 +80,31 @@ x\in\dom\Gamma\\
{\Gamma\vdash \tcase {x} t {e_1}{e_2}: t'}
{ }
\\
% \Infer[Abs]
% {\Gamma,(x:s)\vdash e\triangleright_x \dt\\
% \textstyle {\dt'=\dt\cup\left\{s\setminus\bigcup_{s'\in\dt}s'\right\}}\\
% T=\{(s',t')\,|\,s'\in\dt' \text{ and } \Gamma,(x:s')\vdash e:t'\}}
% {
% \Gamma\vdash\lambda x:s.e:\textstyle \bigwedge_{(s',t')\in T}\arrow {s'} {t'}
% }
% { }
% \\
\Infer[AbsBase]
{
\textstyle {\dt'=\dt\cup\left\{s\setminus\bigcup_{s'\in\dt}s'\right\}}\\
T=\{(s',t')\,|\,s'\in\dt' \text{ and } \Gamma,(x:s')\vdash e:t'\}}
{
\Gamma\vdash_\dt\lambda x:s.e:\textstyle \bigwedge_{(s',t')\in T}\arrow {s'} {t'}
}
{ }
\\
\Infer[AbsSplit]
{\forall u\in\dt.\ \Gamma,(x:u)\vdash e\triangleright_x\dt_u\\
\Gamma\textstyle\vdash_{\bigcup_{u\in\dt_u}\dt_u}\lambda x:s.e: t
}
{
\Gamma\vdash_\dt\lambda x:s.e: t
}
{ }
\\
\Infer[Abs]
{\Gamma\vdash_{\{s\}} \lambda x:s.e: t}
{
\Gamma\vdash\lambda x:s.e: t
}
{ }
\\
\Infer[LetBase]
{
\Gamma,(x:u)\vdash e:t}
......@@ -148,33 +167,37 @@ TODO: Inter rule needed?
TODO: Algorithmic rules
TODO: Abs rule must be updated (like the let rule)
\subsection{Candidates generation rules}
\begin{mathpar}
\Infer[Var]
{
}
{ \Gamma \vdash y \triangleright_x \{\Gamma(x)\} }
{ \Gamma \vdash y \triangleright_x \{\} }
{}
\hfill
\Infer[Const]
{
}
{ \Gamma \vdash c \triangleright_x \{\Gamma(x)\} }
{ \Gamma \vdash c \triangleright_x \{\} }
{}
\hfill
\Infer[Abs]
{\Gamma,(y:s)\vdash e\triangleright_x\dt}
{
\Gamma\vdash\lambda y:s.\ e\triangleright_x\dt
}
{x\neq y}
\\
% \hfill
% \Infer[Abs]
% {\Gamma,(y:s)\vdash e\triangleright_x\dt}
% {
% \Gamma\vdash\lambda y:s.\ e\triangleright_x\dt
% }
% {x\neq y}
\\
\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\{t_1\land t_2\ |\ t_1\in\dt_1, t_2\in\dt_2\}}
{i\in\{1,2\}\\
\Gamma \vdash a_i\triangleright_x\dt}
{\Gamma \vdash (a_1,a_2)\triangleright_x \dt}
{}
\hfill
\Infer[ProjVar]
{\Gamma \vdash x:\textstyle{\bigvee_{i \in I}t_i}}
{\Gamma \vdash \pi_i x\triangleright_x\textstyle{\bigcup_{i\in I} \{t_i\}}}
{}
\hfill
\Infer[Proj]
......@@ -200,36 +223,26 @@ TODO: Abs rule must be updated (like the let rule)
{\Gamma\vdash \tcase{y}{t}{e_1}{e_2}\triangleright_x\dt}
{}
\\
% \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)\}} }
% {}
% \\
% \Infer[Let]
% {
% \Gamma \cvdash p: \{(t_i,\Gamma_i)\}_{i\in I}\\
% \Gamma, (y:t) \vdash e\triangleright_x\dt
% }
% { \Gamma \vdash\letexp{y}{p}{e}\triangleright_x\dt
% }
% {}
% \\
% \Infer[Let]
% {
% \Gamma \vdash p: t\\
% \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\textstyle{
% \bigcup_{u\in \dt_y}\bigcup_{i\in I_u}\{\Gamma_u^i(x)\}
% }}
% {}
% \\
\Infer[AppVar1]
{
\Gamma \vdash x : \textstyle{\bigvee_{i \in I}t_i}
}
{ \Gamma \vdash x a\triangleright_x\textstyle{\bigcup_{i\in I} \{t_i\}}}
{}
\qquad
\Infer[AppVar2]
{
\Gamma \vdash a : \textstyle{\bigwedge_{i \in I}s_i\to t_i}
}
{ \Gamma \vdash a x\triangleright_x\textstyle{\bigcup_{i\in I} \{s_i\}}}
{}
\qquad
\Infer[App]
{ i\in\{1,2\}\\
\Gamma \vdash a_i\triangleright_x\dt }
{ \Gamma \vdash a_1 a_2\triangleright_x\dt}
{}
\\
\Infer[LetBase]
{
\Gamma, (y:u) \vdash e\triangleright_y\dt\\
......@@ -260,12 +273,7 @@ TODO: Abs rule must be updated (like the let rule)
{ }
\end{mathpar}
TODO: Fix the second Let rule (does the result cover all the initial domain of $x$??)
TODO: App rule must be updated (like the let rule)
TODO: example: application $x y$ with $x$ an union of arrow. Candidates
for $x$ should be all the different union of arrows of its type?
TODO: update rule ABS
TODO: Candidates for a variable should be a special "all splits".
Otherwise, $\letexp{x}{\cdots}{x}$ will never be splitted.
......
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