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

trying some new rules... (wip)

parent 4f9dd98e
......@@ -221,32 +221,30 @@ TODO: Algorithmic rules
{\Gamma \vdash x:t}
{\Gamma \vdash \pi_i x\triangleright_x\{t\land (\pair{\Any}{\Any})\}}
{}
\hfill
\Infer[ProjTypX]
{\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]
{ }
{\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[CaseTest]
\Infer[CaseTest*]
{ }
{\Gamma\vdash \tcase{x}{t}{e_1}{e_2}\triangleright_x
\{\Gamma(x)\land t,\Gamma(x)\land\neg t\}}
{}
\\
\Infer[CaseRec1]
{\Gamma\vdash e_1\triangleright_x\dt\\
\Gamma(y)\leq t}
{\Gamma,(y:\Gamma(y)\land t)\vdash e_1\triangleright_x\dt}
{\Gamma\vdash \tcase{y}{t}{e_1}{e_2}\triangleright_x\dt}
{}
\qquad
\Infer[CaseRec2]
{\Gamma\vdash e_2\triangleright_x\dt\\
\Gamma(y)\leq \neg t}
{\Gamma,(y:\Gamma(y)\land \neg t)\vdash e_2\triangleright_x\dt}
{\Gamma\vdash \tcase{y}{t}{e_1}{e_2}\triangleright_x\dt}
{}
\\
......@@ -270,7 +268,7 @@ TODO: Algorithmic rules
{ \Gamma \vdash y z\triangleright_x\{\}}
{}
\\
\Infer[AppTyp2]
\Infer[App2*]
{
\Gamma \vdash y : \textstyle{\bigwedge_{i \in I}s_i\to t_i}
}
......@@ -319,14 +317,12 @@ TODO: Algorithmic rules
{ }
\end{mathpar}
TODO: Candidates for a variable should be a special "all splits".
Otherwise, $\letexp{x}{\cdots}{x}$ will never be splitted.
TODO: Proj: Actually, all the possible types of the first component should be candidates
(similar to the Var case)
TODO: The hypothesis of the LetDef rule should not use the * rules
(it should only ensure the expression is typeable and shouldn't worry about its precise type).
TODO: The hypothesis of the LetDef rule should not use the xxxTyp rules
(it shoudl 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
that allows * rules. Otherwise, $\letexp{x}{\cdots}{x}$ will never be splitted.
\subsection{Forward refinement rules}
......
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