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

trying some new rules... (wip)

parent c834c39d
......@@ -23,7 +23,7 @@ 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?
TODO: Should we allow expr as let definition?
\subsection{Typing rules}
......@@ -181,6 +181,12 @@ TODO: Algorithmic rules
{ \Gamma \vdash y \triangleright_x \{\} }
{}
\hfill
\Infer[Var*]
{
}
{ \Gamma \vdash y \triangleright_x \{\} }
{}
\hfill
\Infer[Const]
{
}
......@@ -217,7 +223,7 @@ TODO: Algorithmic rules
{\Gamma \vdash (a_1,a_2)\triangleright_x \dt}
{}
\\
\Infer[ProjX]
\Infer[ProjDom]
{\Gamma \vdash x:t}
{\Gamma \vdash \pi_i x\triangleright_x\{t\land (\pair{\Any}{\Any})\}}
{}
......@@ -227,10 +233,10 @@ TODO: Algorithmic rules
{\Gamma \vdash \pi_i y\triangleright_x\{\}}
{y\neq x}
\hfill
\Infer[ProjX*]
{\Gamma \vdash x:\textstyle{\bigvee_{i \in I}t_i}}
{\Gamma \vdash \pi_i x\triangleright_x\textstyle{\bigcup_{i\in I} \{t_i\}}}
{}
\Infer[Proj*]
{\Gamma \vdash x:\textstyle{\bigvee_{i \in I}t_i}}
{\Gamma \vdash \pi_i x\triangleright_x\textstyle{\bigcup_{i\in I} \{t_i\}}}
{}
\\
\Infer[CaseTest*]
{ }
......@@ -278,7 +284,7 @@ TODO: Algorithmic rules
\Infer[LetBase]
{
\Gamma, (y:u) \vdash e\triangleright_y\dt\\
\forall v\in \dt.\ \Gamma\fvdash{p}{v}\{\Gamma_v^i\}_{i\in I_v}
\forall v\in \dt.\ \Gamma\fvdash{p}{v}\{(\_,\Gamma_v^i)\}_{i\in I_v}
}{
\Gamma\vdash_{u}\letexp y p e \triangleright_x \textstyle{
\bigcup_{v\in \dt}\bigcup_{i\in I_v}\{\Gamma_v^i(x)\}
......@@ -321,18 +327,26 @@ TODO: Algorithmic rules
(it should only ensure the expression is typeable and shouldn't worry about its precise type).
TODO: In the context of the previous todo,
candidates for a variable and a proj should add a special "all splits" flag
candidates for Var* and a Proj* should add a special "all splits" flag
that allows * rules. Otherwise, $\letexp{x}{\cdots}{x}$ will never be splitted.
\subsection{Forward refinement rules}
\begin{mathpar}
\Infer[App]
{\Gamma\vdash e_1:\bigvee_{i\in I}u_i \\
{\Gamma\vdash x_1:\bigvee_{i\in I}u_i \\
\forall i\in I.\ u_i\leq \arrow{t_i}{t}\\
\forall i\in I.\ \Gamma\fvdash{e_1}{u_i}\{(u_i^j, \Gamma_{1,i}^j)\}_{j\in J_i} \\ \forall i\in I.\ \Gamma\fvdash{e_2}{t_i}\{(t_i^k, \Gamma_{2,i}^k)\}_{k\in K_i}\\
\forall i\in I.\ \forall j\in J_i.\ \forall k\in K_i.\ u_i^j\leq\arrow{t_i^k}{s_i^{j,k}}}
{\Gamma\fvdash {(e_1\ e_2)} {t} \bigcup_{i\in I}\{(s_i^{j,k}, \Gamma_{1,i}^j\land\Gamma_{2,i}^k)\ |\ j\in J_i, k\in K_i\}}
%\forall i\in I.\ \Gamma\fvdash{x_1}{u_i}\{(u_i^j, \Gamma_{1,i}^j)\}_{j\in J_i}\\
\forall i\in I.\ \Gamma_1^i = \Gamma,(x_1:u_i)\\
%\forall i\in I.\ \Gamma\fvdash{x_2}{t_i}\{(t_i^k, \Gamma_{2,i}^k)\}_{k\in K_i}\\
\forall i\in I.\ \Gamma_2^i = \Gamma,(x_2:t_i)\\
%\forall i\in I.\ \forall j\in J_i.\ \forall k\in K_i.\ u_i^j\leq\arrow{t_i^k}{s_i^{j,k}}
\forall i\in I.\ u_i\leq\arrow{t_i}{s_i}
}
{
%\Gamma\fvdash {(x_1\ x_2)} {t} \bigcup_{i\in I}\{(s_i^{j,k}, \Gamma_{1,i}^j\land\Gamma_{2,i}^k)\ |\ j\in J_i, k\in K_i\}
\Gamma\fvdash {(x_1\ x_2)} {t} \bigcup_{i\in I}\{(s_i, \Gamma_{1}^i\land\Gamma_{2}^i)\}
}
{ }
\\
\Infer[Abs]
......
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