trying some new rules... (wip)

new_system2.tex

@@ -85,15 +85,15 @@ x\in\dom\Gamma\\
 {\Gamma\vdash \tcase {x} t {e_1}{e_2}: t'}
 { }
 \\
-\Infer[Abs]
-  {\Gamma,(x:s)\vdash e\triangleright_x \dt\\
-  \textstyle {\dt'=\dt\cup\left\{s\setminus\bigcup_{s'\in\dt}s'\right\}}\\
-  T=\{(s',t')\,|\,s'\in\dt' \text{ and } \Gamma,(x:s')\vdash e:t'\}}
-  {
-  \Gamma\vdash\lambda x:s.e:\textstyle \bigwedge_{(s',t')\in T}\arrow {s'} {t'}
-  }
-  { }
-\\
+% \Infer[Abs]
+%   {\Gamma,(x:s)\vdash e\triangleright_x \dt\\
+%   \textstyle {\dt'=\dt\cup\left\{s\setminus\bigcup_{s'\in\dt}s'\right\}}\\
+%   T=\{(s',t')\,|\,s'\in\dt' \text{ and } \Gamma,(x:s')\vdash e:t'\}}
+%   {
+%   \Gamma\vdash\lambda x:s.e:\textstyle \bigwedge_{(s',t')\in T}\arrow {s'} {t'}
+%   }
+%   { }
+% \\
 \Infer[Let]
   {
   \Gamma\bvdash{p}{u} (\Gamma_u^i)_{i\in I_u}\\
@@ -125,6 +125,10 @@ TODO: Inter rule needed?
 
 TODO: Algorithmic rules
 
+TODO: Abs rule must be updated (like the let rule)
+
+TODO: Case rule can suppose that x is a subtype of $t$ or $\neg t$?
+
 NOTE: In the algorithmic system, the Split rule can be guaranteed by stronger
 typing rules for the application and the typecase: it should return a list of
 pair (typ, env). It allows us to consider the two possibilities of a typecase
@@ -136,13 +140,13 @@ without making any approximation (and similarly for the application of a union o
   \Infer[Var]
       {
       }
-      { \Gamma \vdash y \triangleright_x \varnothing }
+      { \Gamma \vdash y \triangleright_x \{\Gamma(x)\} }
       {}
   \hfill
   \Infer[Const]
       {
       }
-      { \Gamma \vdash c \triangleright_x \varnothing }
+      { \Gamma \vdash c \triangleright_x \{\Gamma(x)\} }
       {}
   \hfill
   \Infer[Abs]
@@ -154,7 +158,7 @@ without making any approximation (and similarly for the application of a union o
     \vspace{-2.3mm}\\ 
     \Infer[Pair]
           {\Gamma \vdash a_1\triangleright_x\dt_1 \and \Gamma \vdash a_2\triangleright_x\dt_2}
-          {\Gamma \vdash (a_1,a_2)\triangleright_x\dt_1\cup\dt_2}
+          {\Gamma \vdash (a_1,a_2)\triangleright_x\{t_1\land t_2\ |\ t_1\in\dt_1, t_2\in\dt_2\}}
           {}
   \hfill
    \Infer[Proj]
@@ -162,41 +166,68 @@ without making any approximation (and similarly for the application of a union o
           {\Gamma \vdash \pi_i a\triangleright_x\dt}
           {}
   \vspace{-2.3mm}\\        
-  \Infer[Case]
-        {\Gamma\subst{y}{\Gamma(y)\land t}\vdash e_1\triangleright_x\dt_1\\
-        \Gamma\subst{y}{\Gamma(y)\land \neg t}\vdash e_2\triangleright_x\dt_2}
-        {\Gamma\vdash \tcase{y}{t}{e_1}{e_2}\triangleright_x\dt_1\cup\dt_2\cup
-            \left\{
-              \begin{array}{l}
-                \{\Gamma(x)\land t,\Gamma(x)\land\neg t\} \text{ if } y=x\arcr
-                \varnothing\text{ otherwise}
-              \end{array}
-            \right.}
+  \Infer[CaseTest]
+        { }
+        {\Gamma\vdash \tcase{x}{t}{e_1}{e_2}\triangleright_x
+        \{\Gamma(x)\land t,\Gamma(x)\land\neg t\}}
         {}
   \vspace{-2.3mm}\\
-  \Infer[App]
+  \Infer[CaseRec1]
+  {\Gamma\vdash e_1\triangleright_x\dt\\
+  \Gamma(y)\leq t}
+  {\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\vdash \tcase{y}{t}{e_1}{e_2}\triangleright_x\dt}
+  {}
+  \vspace{-2.3mm}\\
+  \Infer[Split]
+{
+  \Gamma,(y:t_1) \vdash e\triangleright_x \dt_1\quad
+  \Gamma,(y:t_2) \vdash e\triangleright_x \dt_2
+}
+{ \Gamma,(y:t_1\lor t_2) \vdash e\triangleright_x \{t_1\land t_2\ |\ t_1\in\dt_1, t_2\in\dt_2\} }
+{ y\neq x }
+\vspace{-2.3mm}\\
+  % \Infer[App]
+  %     {
+  %       \Gamma \vdash a_1 : \textstyle{\bigvee \bigwedge_{i \in I}s_i\to t_i}\\
+  %       \Gamma \vdash a_1\triangleright_x\dt_1\\
+  %       \forall i\in I.\ \Gamma\fvdash{a_2}{s_i}\{\Gamma_i^j\}_{j\in J_i}
+  %     }
+  %     { \Gamma \vdash a_1 a_2\triangleright_x\dt_1\cup\textstyle{\bigcup_{i\in I}
+  %       \bigcup_{j\in J_i}\{\Gamma_i^j(x)\}} }
+  %     {}
+  % \vspace{-2.3mm}\\
+  \Infer[Let]
       {
-        \Gamma \vdash a_1 : \textstyle{\bigvee \bigwedge_{i \in I}s_i\to t_i}\\
-        \Gamma \vdash a_1\triangleright_x\dt_1\\
-        \forall i\in I.\ \Gamma\fvdash{a_2}{s_i}\{\Gamma_i^j\}_{j\in J_i}
+        \Gamma \vdash p: t\\
+        \Gamma, (y:t) \vdash e\triangleright_x\dt
+      }
+      { \Gamma \vdash\letexp{y}{p}{e}\triangleright_x\dt
       }
-      { \Gamma \vdash a_1 a_2\triangleright_x\dt_1\cup\textstyle{\bigcup_{i\in I}
-        \bigcup_{j\in J_i}\{\Gamma_i^j(x)\}} }
       {}
-  \vspace{-2.3mm}\\
+      \vspace{-2.3mm}\\
   \Infer[Let]
       {
         \Gamma \vdash p: t\\
-        \Gamma, (y:t) \vdash e\triangleright_x\dt_x\\
         \Gamma, (y:t) \vdash e\triangleright_y\dt_y\\
         \forall u\in \dt_y.\ \Gamma\fvdash{p}{u}\{\Gamma_u^i\}_{i\in I_u}
       }
-      { \Gamma \vdash\letexp{y}{p}{e}\triangleright_x\dt_x\cup\textstyle{
+      { \Gamma \vdash\letexp{y}{p}{e}\triangleright_x\textstyle{
         \bigcup_{u\in \dt_y}\bigcup_{i\in I_u}\{\Gamma_u^i(x)\}
       }}
       {}
   \end{mathpar}
 
+  TODO: Fix the second Let rule (it does not allow to split the type of $y$ when necessary
+  + does the result cover all the initial domain of $x$??)
+
+  TODO: App rule must be updated (like the let rule)
+
   TODO: example: application $x y$ with $x$ an union of arrow. Candidates
   for $x$ should be all the different union of arrows of its type?