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

new attempt for the ABS rule

parent a2a1d786
......@@ -539,17 +539,17 @@ $x$ is supposed to be included into $t_x$ or $\neg t_x$.
{\Gamma(x)\equiv\textstyle\bigvee_{i\in I}\pair{t_i}{s_i}\\
\forall i\in I.\ \Gamma\avdash{\Gammap\subst{x}{\pair{t_i}{s_i}}}{[]} \ct[\pi_j x]: \tree_i
}
{\Gamma \avdash\Gammap\ct \pi_j x: \Node(\Gamma\land\Gammap,\{\tree_i\}_{i\in I})}
{\Gamma \avdash\Gammap\ct \pi_j x: \Node(\Gamma,\{(\{\{x:\pair{t_i}{s_i}\}\}, \tree_i)\}_{i\in I})}
{ }
\\
\Infer[ProjDom]
{\Gamma(x) = t\\
t\land(\pair{\Any}{\Any})\neq\Empty\\
t\land\neg(\pair{\Any}{\Any})\neq\Empty\\
\Gamma\avdash{\Gammap\subst{x}{t\land(\pair{\Any}{\Any})}}{[]} \ct[\pi_i x]: \tree_1\\
\Gamma\avdash{\Gammap\subst{x}{t\land\neg(\pair{\Any}{\Any})}}{[]} \ct[\pi_i x]: \tree_2
{\Gamma(x) = t\\t_1 = t\land(\pair{\Any}{\Any})\\
t_2 = t\land\neg(\pair{\Any}{\Any})\\
t_1\neq\Empty\\t_2\neq\Empty\\
\Gamma\avdash{\Gammap\subst{x}{t_1}}{[]} \ct[\pi_i x]: \tree_1\\
\Gamma\avdash{\Gammap\subst{x}{t_2}}{[]} \ct[\pi_i x]: \tree_2
}
{\Gamma \avdash\Gammap\ct \pi_i x: \Node(\Gamma\land\Gammap,\{\tree_1,\tree_2\})}
{\Gamma \avdash\Gammap\ct \pi_i x: \Node(\Gamma,\{(\{\{x:t_1\}\}, \tree_1),(\{\{x:t_2\}\},\tree_2)\})}
{ }
\\
\Infer[Pair]
......@@ -573,7 +573,7 @@ $x$ is supposed to be included into $t_x$ or $\neg t_x$.
s\leq \textstyle\bigvee_{i\in I}s_i\\
\forall i\in I.\ \Gamma\avdash{\Gammap\subst{x_2}{s\land s_i}}{[]} \ct[{x_1}{x_2}]: \tree_i
}
{ \Gamma \avdash\Gammap\ct {x_1}{x_2}: \Node(\Gamma\land\Gammap,\{\tree_i\}_{i\in I}) }
{ \Gamma \avdash\Gammap\ct {x_1}{x_2}: \Node(\Gamma,\{(\{\{x_2:s\land s_i\}\},\tree_i)\}_{i\in I}) }
{ }
\\
\Infer[AppRDom]
......@@ -584,22 +584,24 @@ $x$ is supposed to be included into $t_x$ or $\neg t_x$.
\Gamma\avdash{\Gammap\subst{x_2}{s\land s_\circ}}{[]} \ct[{x_1}{x_2}]: \tree_1\\
\Gamma\avdash{\Gammap\subst{x_2}{s\land \neg s_\circ}}{[]} \ct[{x_1}{x_2}]: \tree_2
}
{ \Gamma \avdash\Gammap\ct {x_1}{x_2}: \Node(\Gamma\land\Gammap,\{\tree_1,\tree_2\}) }
{ \Gamma \avdash\Gammap\ct {x_1}{x_2}: \Node(\Gamma,\{(\{\{x_2:s\land s_\circ\}\},\tree_1),(\{\{x_2:s\land \neg s_\circ\}\},\tree_2)\}) }
{ }
\\
\Infer[AppL*]
{\Gamma(x_1)\equiv\textstyle\bigvee_{i\in I}u_i\leq\arrow{\Empty}{\Any}\\
\forall i\in I.\ \Gamma\avdash{\Gammap\subst{x_1}{u_i}}{[]} \ct[{x_1}{x_2}]: \tree_i
}
{\Gamma \avdash\Gammap\ct {x_1}{x_2}: \Node(\Gamma\land\Gammap,\{\tree_i\}_{i\in I})}
{\Gamma \avdash\Gammap\ct {x_1}{x_2}: \Node(\Gamma,\{(\{\{x_1:u_i\}\},\tree_i)\}_{i\in I})}
{ }
\\
\Infer[AppLDom]
{\Gamma(x_1) = u\\u\land (\arrow{\Empty}{\Any})\neq\Empty\\u\land \neg (\arrow{\Empty}{\Any})\neq\Empty\\
\Gamma\avdash{\Gammap\subst{x_1}{u\land(\arrow{\Empty}{\Any})}}{[]} \ct[{x_1}{x_2}]: \tree_1\\
\Gamma\avdash{\Gammap\subst{x_1}{u\land\neg(\arrow{\Empty}{\Any})}}{[]} \ct[{x_1}{x_2}]: \tree_2
{\Gamma(x_1) = u\\t_1=u\land (\arrow{\Empty}{\Any})\\
t_2=u\land \neg (\arrow{\Empty}{\Any})\\
t_1\neq\Empty\\t_2\neq\Empty\\
\Gamma\avdash{\Gammap\subst{x_1}{t_1}}{[]} \ct[{x_1}{x_2}]: \tree_1\\
\Gamma\avdash{\Gammap\subst{x_1}{t_2}}{[]} \ct[{x_1}{x_2}]: \tree_2
}
{\Gamma \avdash\Gammap\ct {x_1}{x_2}: \Node(\Gamma\land\Gammap,\{\tree_1,\tree_2\})}
{\Gamma \avdash\Gammap\ct {x_1}{x_2}: \Node(\Gamma,\{(\{\{x_1:t_1\}\},\tree_1),(\{\{x_1:t_2\}\},\tree_2)\})}
{ }
\end{mathpar}
......@@ -623,7 +625,7 @@ $x$ is supposed to be included into $t_x$ or $\neg t_x$.
\Gamma\avdash{\Gammap\subst{x}{t_\circ\land t}}{[]} \ct[\tcase {x} t {e_1}{e_2}]: \tree_1\\
\Gamma\avdash{\Gammap\subst{x}{t_\circ\land\neg t}}{[]} \ct[\tcase {x} t {e_1}{e_2}]: \tree_2
}
{\Gamma,\avdash\Gammap\ct \tcase {x} t {e_1}{e_2}: \Node(\Gamma\land\Gammap,\{\tree_1,\tree_2\})}
{\Gamma,\avdash\Gammap\ct \tcase {x} t {e_1}{e_2}: \Node(\Gamma,\{(\{\{x:t_\circ\land t\}\},(\{\{x:t_\circ\land\neg t\}\},\tree_1)),\tree_2\})}
{ }
\end{mathpar}
......@@ -636,10 +638,15 @@ rules, because one branch is already unreachable and retyping only occurs with s
\Gamma\avdash\Gammap\ct a:\tree\\
\{\Leaf(t_i,\Gamma_i)\}_{i\in I} = \tleaves(\tree)\\
\forall i\in I.\ \Gamma_i,(x:t_i)\avdash\Gammap{\ct} \letexp x a e : \tree_i\\
\tree'= \tree\text{ with each leaf } \Leaf(t_i,\Gamma_i) \text{ replaced with } \tree_i
\tree'= \tree\text{ with, for each } i\in I\text{, the leaf } \Leaf(t_i,\Gamma_i) \text{ replaced by } \tree_i\\
\{(\Gamma_i',\{\Gamma_{i,j}'\}_{j\in J_i})\}_{i\in I'} = \tlabels(\tree')\\
\forall i\in I'.\ \forall j\in J_i.\ x\in\dom{\Gamma_{i,j}'} \Rightarrow (\Gamma_i'\land\Gamma_{i,j}')\setminus\{x\} \fvdash{a}{\Gamma_{i,j}'(x)} \{\Gamma_{i,j,k}'\}_{k\in K_j}\\
\forall i\in I'.\ \forall j\in J_i.\ x\not\in\dom{\Gamma_{i,j}'} \Rightarrow \{\Gamma_{i,j,k}'\}_{k\in K_j} = \{\{\}\} \\
\tree''= \tree'\text{ with, for each } i\in I' \text{, the label } \{\Gamma_{i,j}'\}_{j\in J_i}
\text{ replaced by } \{(\Gamma_{i,j,k}'\land\Gamma_{i,j}')\setminus\{x\}\,\alt\,j\in J_i, k\in K_j\}
}
{
\Gamma\avdash\Gammap\ct\letexp x a e : \tree'
\Gamma\avdash\Gammap\ct\letexp x a e : \tree''
}
{ x\not\in\dom\Gamma }
\\
......@@ -662,21 +669,20 @@ rules, because one branch is already unreachable and retyping only occurs with s
\Gamma_\circ\bvdash{a}{\Gammap(x)}\{\Gamma_i\}_{i\in I}\\
\forall i\in I.\ \Gamma_\circ\subst{x}{\Gamma_\circ(x)\land\Gammap(x)}\avdash{(\Gammap\land\Gamma_i)\setminus\{x\}}{[]} \ct[\letexp x a e] : \tree_i}
{
\Gamma\avdash\Gammap\ct\letexp x a e : \Node(\Gamma_\circ\land\Gammap, \{\tree_i\}_{i\in I})
\Gamma\avdash\Gammap\ct\letexp x a e : \Node(\Gamma,\{(\{\}, \tree_i)\}_{i\in I})
}
{ }
\end{mathpar}
\begin{mathpar}
\Infer[Abs]
{\Gamma,(x:s)\avdash{\Gammap}{\ct} e:\{(t_i,\Gamma_i)\}_{i\in I}\\
\{(t'_i,\Gamma'_i)\}_{i\in I'} = \{ (\textstyle\bigvee_{j\in I\text{ s.t. }\Gamma_i\setminus\bv(e)\equiv\Gamma_j\setminus\bv(e)} t_j,\ \Gamma_i\setminus\bv(e)) \alt i\in I \}\\
\forall i\in I'.\ t''_i = \textstyle\bigvee_{j\in I'\text{ s.t. } \Gamma'_i\land\Gamma'_j\neq\bot}t'_j
{\Gamma,(x:s)\avdash{\Gammap}{\ct} e:\tree\\
\{(t_i,\Gamma_i)\}_{i\in I} = \tflatten(\tree)\\
\{\Gamma_j'\}_{j\in J} = \{\Gamma_i\setminus\{x\}\,\alt\,i\in I\}
}
{\Gamma\vdash\lambda x:s.e: \{(
\textstyle\bigwedge_{j\in I'\text{ s.t. }\Gamma_i\setminus\{x\}\equiv\Gamma_j\setminus\{x\}} \arrow{\Gamma'_j(x)}{t''_j},\
\Gamma'_i\setminus\{x\})\,\alt\,i\in I'\}}
{\Gamma\vdash\lambda x:s.e: \Node(\Gamma,\{(\{\Gamma_j'\},
\textstyle\bigwedge_{i\in I\text{ s.t. }\Gamma_i\leq\Gamma_j'} \arrow{\Gamma_i(x)}{t_i}
)\,\alt\,j\in J\})}
{ }
\end{mathpar}
TODO: Update the Abs rule. In particular, use $\fvdash{e}{t}$ to improve it.
......@@ -306,6 +306,9 @@
\newcommand{\tree}[0]{\mathcal{T}}
\newcommand{\ttype}[0]{\texttt{type}}
\newcommand{\tleaves}[0]{\texttt{leaves}}
\newcommand{\tnodes}[0]{\texttt{nodes}}
\newcommand{\tlabels}[0]{\texttt{labels}}
\newcommand{\tflatten}[0]{\texttt{flatten}}
\newcommand{\btr}[0]{\blacktriangleright}
\makeatletter % allow us to mention @-commands
......
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