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

trying some new rules... (wip)

parent 298d2bf1
......@@ -214,8 +214,13 @@ TODO: Algorithmic rules
\Gamma \vdash a_i\triangleright_x\dt}
{\Gamma \vdash (a_1,a_2)\triangleright_x \dt}
{}
\hfill
\\
\Infer[ProjX]
{\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\}}}
{}
......@@ -224,7 +229,7 @@ TODO: Algorithmic rules
{ }
{\Gamma \vdash \pi_i y\triangleright_x\{\}}
{y\neq x}
\\
\\
\Infer[CaseTest]
{ }
{\Gamma\vdash \tcase{x}{t}{e_1}{e_2}\triangleright_x
......@@ -243,25 +248,33 @@ TODO: Algorithmic rules
{\Gamma\vdash \tcase{y}{t}{e_1}{e_2}\triangleright_x\dt}
{}
\\
\Infer[AppVar1]
\Infer[App1]
{
\Gamma \vdash x : \textstyle{\bigvee_{i \in I}t_i}
\Gamma \vdash x : t\\
t\land(\arrow{\Empty}{\Any}) \equiv \textstyle{\bigvee_{i \in I}t_i}
}
{ \Gamma \vdash x y\triangleright_x\textstyle{\bigcup_{i\in I} \{t_i\}}}
{}
\qquad
\Infer[AppVar2]
\Infer[App2]
{
\Gamma \vdash y : \arrow{s}{t}
}
{ \Gamma \vdash y x\triangleright_x \{s\}}
{}
\qquad
\Infer[App]
{ }
{ \Gamma \vdash y z\triangleright_x\{\}}
{}
\\
\Infer[AppTyp2]
{
\Gamma \vdash y : \textstyle{\bigwedge_{i \in I}s_i\to t_i}
}
{ \Gamma \vdash y x\triangleright_x\textstyle{\bigcup_{i\in I} \{s_i\}}}
{}
\qquad
\Infer[App]
{ }
{ \Gamma \vdash y z\triangleright_x\{\}}
{}
\\
\\
\Infer[LetBase]
{
\Gamma, (y:u) \vdash e\triangleright_y\dt\\
......@@ -310,7 +323,8 @@ TODO: Algorithmic rules
TODO: Proj: Actually, all the possible types of the first component should be candidates
(similar to the Var case)
TODO: "split rules" that only split in order for an expression to be typeable
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).
\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