Commit 485cee3c authored by Mickael Laurent's avatar Mickael Laurent
Browse files

trying some new rules... (wip)

parent 7fbe6d4e
......@@ -23,6 +23,8 @@ Is this an issue? Should we require an atomic in the then and else branchs
TODO: Which restrictions on types? (cannot test a precise arrow type, etc)
TODO: Should we allow ezpr as let definition?
\subsection{Typing rules}
\begin{mathpar}
......@@ -370,6 +372,15 @@ TODO: Algorithmic rules
{\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[Proj]
{
j = 1 \Rightarrow t' = \pair{t}{\Any}\\
j = 2 \Rightarrow t' = \pair{\Any}{t}\\
\Gamma\bvdash {e}{t'} \{(t_i,\Gamma_i)\}_{i\in I}\\
\forall i\in I.\ t_i\equiv\pair{s_1^i}{s_2^i}}
{\Gamma\bvdash {\pi_j e}{t} \{(s_j^i,\Gamma_i)\}_{i\in I}}
{ }
\\
\Infer[App]
{\Gamma\vdash e_1:\bigvee_{i\in I}u_i \\
......@@ -390,6 +401,36 @@ TODO: Algorithmic rules
{\Gamma\vdash \lambda x:s.\ e:t'}
{\Gamma\bvdash {\lambda x:s.\ e}{t} \{(t\land t',\Gamma)\}}
{ }
\\
\Infer[LetBase]
{
\Gamma,(x:s)\bvdash{e}{t} \{(t_i,\Gamma_i)\}_{i\in I}
}
{
\Gamma\ubvdash{s}{\letexp{x}{p}{e}}{t} \{(t_i,\Gamma_i)\}_{i\in I}
}
{ }
\\
\Infer[LetSplit]
{
\Gamma,(x:s)\vdash e\triangleright_x\dt\\
\dt' = \dt\cup\{s\setminus\textstyle\bigcup_{u\in\dt}u\}\\
\forall u\in \dt'.\ \Gamma\bvdash{p}{u} \{t_u^i, \Gamma_u^i\}_{i\in I_u}\\
\forall u\in \dt'.\ \forall i\in I_u.\ \Gamma\ubvdash{u}{\letexp{x}{p}{e}}{t} \{(t_i^j,\Gamma_i^j)\}_{j\in J_i}}
{
\Gamma\ubvdash{s}{\letexp{x}{p}{e}}{t} \bigcup_{u\in\dt'}\bigcup_{i\in I_u} \{(t_i^j,\Gamma_i^j)\}_{j\in J_i}
}
{ }
\\
\Infer[Let]
{
\Gamma\vdash p:s\\
\Gamma\ubvdash{s}{\letexp{x}{p}{e}}{t} \{(t_i,\Gamma_i)\}_{i\in I}
}
{
\Gamma\bvdash{\letexp{x}{p}{e}}{t} \{(t_i,\Gamma_i)\}_{i\in I}
}
{ }
\end{mathpar}
TODO: Is the Comp rule needed in this new setting where every application is alone in a let,
......
......@@ -287,6 +287,10 @@
\newcommand{\dt}[0]{\mathbb{T}}
\newcommand{\fvdash}[2]{\vdash^{\texttt{Env}\rightarrow}_{#1,#2}}
\newcommand{\bvdash}[2]{\vdash^{\texttt{Env}\leftarrow}_{#1,#2}}
% \newcommand{\ufvdash}[3]{{\underset{#1}\vdash}^{\texttt{Env}\rightarrow}_{#2,#3}}
% \newcommand{\ubvdash}[3]{{\underset{#1}\vdash}^{\texttt{Env}\leftarrow}_{#2,#3}}
\newcommand{\ufvdash}[3]{\vdash^{{#1},\texttt{ Env}\rightarrow}_{#2,#3}}
\newcommand{\ubvdash}[3]{\vdash^{{#1},\texttt{ Env}\leftarrow}_{#2,#3}}
\newcommand{\cvdash}[0]{\vdash^{\texttt{Choices}}}
\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