Commit 298d2bf1 authored by Mickael Laurent's avatar Mickael Laurent
Browse files

trying some new rules... (wip)

parent bb5e0e86
......@@ -114,8 +114,8 @@ TODO: Which restrictions on types? (cannot test a precise arrow type, etc)
{
\Gamma,(x:t')\vdash e\triangleright_x\dt\\
\dt' = \dt\cup\{t'\setminus\textstyle\bigcup_{u\in\dt}u\}\\
\forall u\in \dt'.\ \Gamma\bvdash{p}{u} (\Gamma_u^i)_{i\in I_u}\\
\forall u\in \dt'.\ \forall i\in I_u.\ \Gamma_u^i\vdash_{u}\letexp x p e : t}
\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_u^i\vdash_{t_u^i}\letexp x p e : t}
{
\Gamma\vdash_{t'}\letexp x p e : t
}
......@@ -170,8 +170,6 @@ 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: Use the "split rules" for the let (instead of the candidate generation rules)
\subsection{Candidates generation rules}
\begin{mathpar}
......@@ -277,8 +275,8 @@ TODO: Use the "split rules" for the let (instead of the candidate generation rul
\Infer[LetSplit]
{
\Gamma,(y:t')\vdash e\triangleright_y\dt\\
\forall u\in \dt.\ \Gamma\bvdash{p}{u} (\Gamma_u^i)_{i\in I_u}\\
\forall u\in \dt.\ \forall i\in I_u.\ \Gamma_u^i\vdash_{u}\letexp x p e \triangleright_x \dt_u^i
\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_u^i\vdash_{t_u^i}\letexp x p e \triangleright_x \dt_u^i
}
{
\Gamma\vdash_{t'}\letexp y p e \triangleright_x \textstyle\bigcup_{u\in \dt}\bigcup_{i\in I_u} \dt_u^i
......
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