trying some new rules... (wip)

new_system2.tex

@@ -25,6 +25,8 @@ TODO: Which restrictions on types? (cannot test a precise arrow type, etc)
 
 TODO: Should we allow expr as let definition?
 
+TODO: Simplify pairs (only with variables) + simplify grammar accordingly (no need to distinguish a and u)
+
 \subsection{Typing rules}
 
 \begin{mathpar}
@@ -82,7 +84,7 @@ TODO: Should we allow expr as let definition?
   {
     \Gamma,(x:t')\vdash e:t}
   {
-  \Gamma\vdash_{t'}\lambda x:s.e:\arrow {t'} {t}
+  \Gamma\vdash_{t'}\lambda x:s.e:\arrow {(t'\land s)} {t}
   }
   { }
 \\
@@ -399,25 +401,32 @@ TODO: Algorithmic rules
    { }
 \\
   \Infer[Pair]
-  {\forall i\in I.\ \Gamma\bvdash{e_1}{t_i}\{(t_i^j,\Gamma_{1,i}^j)\}_{j\in J_i} \\ \forall i\in I.\ \Gamma\bvdash{e_2}{s_i}\{(s_i^k,\Gamma_{2,i}^k)\}_{k\in K_i}}
-  {\Gamma\bvdash {(e_1,e_2)} {\bigcup_{i\in I}(t_i,s_i)} \bigcup_{i\in I}\{(\pair{t_i^j}{s_i^k}, \Gamma_{1,i}^j\land\Gamma_{2,i}^k)\ |\ j\in J_i, k\in K_i\}}
+  {\forall i\in I.\ \Gamma\bvdash{a_1}{t_i}\{(t_i^j,\Gamma_{1,i}^j)\}_{j\in J_i}\\
+   \forall i\in I.\ \Gamma\bvdash{a_2}{s_i}\{(s_i^k,\Gamma_{2,i}^k)\}_{k\in K_i}}
+  {\Gamma\bvdash {(a_1,a_2)} {\bigcup_{i\in I}(t_i,s_i)} \bigcup_{i\in I}\{(\pair{t_i^j}{s_i^k}, \Gamma_{1,i}^j\land\Gamma_{2,i}^k)\ |\ j\in J_i, k\in K_i\}}
   { }
   \\
   \Infer[Proj]
   {
-    j = 1 \Rightarrow t' = \pair{t}{\Any}\\
-    j = 2 \Rightarrow t' = \pair{\Any}{t}\\
-    \Gamma\bvdash {e}{t'} \{(t_i,\Gamma_i)\}_{i\in I}\\
-    \forall i\in I.\ t_i\equiv\pair{s_1^i}{s_2^i}}
-  {\Gamma\bvdash {\pi_j e}{t} \{(s_j^i,\Gamma_i)\}_{i\in I}}
+    i = 1 \Rightarrow t' = \pair{t}{\Any}\\
+    i = 2 \Rightarrow t' = \pair{\Any}{t}
+  }
+  {\Gamma\bvdash {\pi_i x}{t} \{(t,\Gamma\subst{x}{\Gamma(x)\land t'})\}}
   { }
 \\
   \Infer[App]
-  {\Gamma\vdash e_1:\bigvee_{i\in I}u_i \\
+  {\Gamma\vdash x_1:\bigvee_{i\in I}u_i \\ \Gamma\vdash x_2:t'\\ 
   \forall i\in I.\ u_i\leq \arrow{\neg t_i}{s_i} \text{ with } s_i\land t = \varnothing \\
-  \forall i\in I.\ \Gamma\bvdash{e_1}{u_i}\{(u_i^j, \Gamma_{1,i}^j)\}_{j\in J_i} \\ \forall i\in I.\ \Gamma\bvdash{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\bvdash {(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\bvdash{e_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\bvdash{e_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\land t')\\
+  %\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\land t')}{s_i}}
+  {
+    %\Gamma\bvdash {(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[Case]
@@ -470,5 +479,3 @@ TODO: Algorithmic rules
 
 TODO: Is the Comp rule needed in this new setting where every application is alone in a let,
 and where union-arrow app are backtyped by splitting possibilities?
-
-TODO: rename e to the right element according to the grammar