trying some new rules... (wip)

new_system2.tex

@@ -68,14 +68,6 @@ TODO: Which restrictions on types? (cannot test a precise arrow type, etc)
 }
 { \Gamma \vdash {a_1}{a_2}: t_2 }
 { }
-\qquad
-\Infer[Split]
-{
-  \Gamma,(x:t_1) \vdash e: t\quad
-  \Gamma,(x:t_2) \vdash e: t
-}
-{ \Gamma,(x:t_1\lor t_2) \vdash e: t }
-{ }
 \\
 \Infer[Case]
 {
@@ -94,10 +86,9 @@ x\in\dom\Gamma\\
 %   }
 %   { }
 % \\
-\Infer[Let]
+\Infer[LetBase]
   {
-  \Gamma\bvdash{p}{u} (\Gamma_u^i)_{i\in I_u}\\
-  \forall i\in I_u.\ \Gamma_u^i,(x:u)\vdash e:t}
+  \Gamma,(x:u)\vdash e:t}
   {
   \Gamma\vdash_{u}\letexp x p e : t
   }
@@ -106,34 +97,58 @@ x\in\dom\Gamma\\
   \Infer[LetSplit]
   {
   \Gamma,(x:t')\vdash e\triangleright_x\dt\\
-  \forall u\in \dt.\ \Gamma\vdash_{u}\letexp x p e : t}
+  \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}
   {
   \Gamma\vdash_{t'}\letexp x p e : t
   }
   { }
   \\
 \Infer[Let]
-  {\Gamma\vdash p:t'\\
-  \Gamma\vdash_{t'}\letexp x p e : t}
+  {\Gamma\cvdash p:\{(t_i,\Gamma_i)\}_{i\in I}\\
+  \forall i\in I.\ \Gamma_i\vdash_{t_i}\letexp x p e : t}
   {
   \Gamma\vdash\letexp x p e : t
   }
   { }
 \end{mathpar}
 
+\begin{mathpar}
+\Infer[Proj]
+{\Gamma \vdash x:\textstyle\bigcup_{j\in J}\pair{t_1^j}{t_2^j}}
+{\Gamma \cvdash \pi_i x: \{(t_i^j, \Gamma\subst{x}{\pair{t_1^j}{t_2^j}})\ \alt\ j\in J\}}
+{ }
+\\
+\Infer[App]
+{
+  \Gamma \vdash x: \textstyle\bigcup_{i\in I}t_i\quad
+  \forall i\in I.\ t_i\leq \arrow{t}{s_i}\quad
+  \Gamma \vdash a: t
+}
+{ \Gamma \cvdash {x}{a}: \{(s_i, \Gamma\subst{x}{t_i})\ \alt\ i\in I\} }
+{ }
+\\
+\Infer[Case]
+{
+\Gamma_1 = \Gamma\subst{x}{\Gamma(x)\land t}\\
+\Gamma_2 = \Gamma\subst{x}{\Gamma(x)\land \neg t}\\
+\Gamma_1 \vdash e_1:t_1\\
+\Gamma_2 \vdash e_2:t_2}
+{\Gamma\cvdash \tcase {x} t {e_1}{e_2}: \{(t_1, \Gamma_1), (t_2, \Gamma_2)\}}
+{ }
+\\
+\Infer[NoChoice]
+{\Gamma \vdash p:t}
+{\Gamma \cvdash p: \{(t, \Gamma)\}}
+{ }
+\end{mathpar}
+
 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
-without making any approximation (and similarly for the application of a union of arrows).
-
 \subsection{Candidates generation rules}
 
 \begin{mathpar}
@@ -155,7 +170,7 @@ without making any approximation (and similarly for the application of a union o
       \Gamma\vdash\lambda y:s.\ e\triangleright_x\dt
       }
       {x\neq y}
-    \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\{t_1\land t_2\ |\ t_1\in\dt_1, t_2\in\dt_2\}}
@@ -165,13 +180,13 @@ without making any approximation (and similarly for the application of a union o
           {\Gamma \vdash a\triangleright_x\dt}
           {\Gamma \vdash \pi_i a\triangleright_x\dt}
           {}
-  \vspace{-2.3mm}\\        
+  \\        
   \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[CaseRec1]
   {\Gamma\vdash e_1\triangleright_x\dt\\
   \Gamma(y)\leq t}
@@ -183,15 +198,7 @@ without making any approximation (and similarly for the application of a union o
   \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}\\
@@ -201,30 +208,58 @@ without making any approximation (and similarly for the application of a union o
   %     { \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 p: t\\
-        \Gamma, (y:t) \vdash e\triangleright_x\dt
-      }
-      { \Gamma \vdash\letexp{y}{p}{e}\triangleright_x\dt
-      }
-      {}
-      \vspace{-2.3mm}\\
-  \Infer[Let]
-      {
-        \Gamma \vdash p: t\\
-        \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\textstyle{
-        \bigcup_{u\in \dt_y}\bigcup_{i\in I_u}\{\Gamma_u^i(x)\}
-      }}
-      {}
+  % \\
+  % \Infer[Let]
+  %     {
+  %       \Gamma \cvdash p: \{(t_i,\Gamma_i)\}_{i\in I}\\
+  %       \Gamma, (y:t) \vdash e\triangleright_x\dt
+  %     }
+  %     { \Gamma \vdash\letexp{y}{p}{e}\triangleright_x\dt
+  %     }
+  %     {}
+  %     \\
+  % \Infer[Let]
+  %     {
+  %       \Gamma \vdash p: t\\
+  %       \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\textstyle{
+  %       \bigcup_{u\in \dt_y}\bigcup_{i\in I_u}\{\Gamma_u^i(x)\}
+  %     }}
+  %     {}
+  %     \\
+\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}
+  }{
+  \Gamma\vdash_{u}\letexp y p e \triangleright_x \textstyle{
+  \bigcup_{v\in \dt}\bigcup_{i\in I_v}\{\Gamma_v^i(x)\}
+  }}
+  { }
+  \\
+  \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
+  }
+  {
+  \Gamma\vdash_{t'}\letexp y p e \triangleright_x \textstyle\bigcup_{u\in \dt}\bigcup_{i\in I_u} \dt_u^i
+  }
+  { }
+  \\
+\Infer[Let]
+  {\Gamma\cvdash p:\{(t_i,\Gamma_i)\}_{i\in I}\\
+  \forall i\in I.\ \Gamma_i\vdash_{t_i}\letexp x p e \triangleright_x \dt_i}
+  {
+  \Gamma\vdash\letexp y p e \triangleright_x \textstyle\bigcup_{i\in I} \dt_i
+  }
+  { }
   \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: Fix the second Let rule (does the result cover all the initial domain of $x$??)
 
   TODO: App rule must be updated (like the let rule)
 

setup.sty

@@ -287,6 +287,7 @@
 \newcommand{\dt}[0]{\mathbb{T}}
 \newcommand{\fvdash}[2]{\vdash^{\texttt{Env}\rightarrow}_{#1,#2}}
 \newcommand{\bvdash}[2]{\vdash^{\texttt{Env}\leftarrow}_{#1,#2}}
+\newcommand{\cvdash}[0]{\vdash^{\texttt{Choices}}}
 
 \makeatletter % allow us to mention @-commands
 \def\arcr{\@arraycr}