add backward typing rules

new_system3.tex

@@ -269,13 +269,105 @@ rules, because one branch is already unreachable and retyping only occurs with s
 \Infer[LetRefine]
   {
   \Gamma\land\Gammap\bvdash{a}{\Gamma(x)\land\Gammap(x)}\{(t_i,\Gamma_i)\}_{i\in I}\\
-  \forall i\in I.\ \Gamma\subst{x}{t_i}\avdash{\Gamma_i\setminus\{x\}}{[]} \ct[\letexp x a e] : S_i}
+  \forall i\in I.\ \Gamma\subst{x}{t_i}\avdash{(\Gammap\land\Gamma_i)\setminus\{x\}}{[]} \ct[\letexp x a e] : S_i}
   {
   \Gamma\avdash\Gammap\ct\letexp x a e : \textstyle\bigcup_{i\in I} S_i
   }
   { x\in\dom\Gamma \text{ and } x\in\dom\Gammap \text{ and } \Gamma(x) \not\leq \Gammap(x) }
 \end{mathpar}
 
-TODO: Check let rule and optimize $\Gammap$ (it should be minimal but it isn't as output of $\bvdash{t}{a}$)
+TODO: Check let rule
 
 TODO: Abs rules
+
+\subsection{Backward typing rules}
+
+\begin{mathpar}
+  \Infer[Var]
+  { }
+  {\Gamma\bvdash x t \{(t, \subst{x}{t})\}}
+  { }
+\qquad
+\Infer[Const]
+{ }
+{\Gamma\bvdash c t \{(t, \{\})\}}
+{ }
+\\
+  \Infer[Inter]
+  {\Gamma\vdash e:t' \\ \Gamma\bvdash e {t\wedge t'} \{(t_i, \Gamma_i)\}_{i\in I}}
+  {\Gamma\bvdash e t \{(t_i, \Gamma_i)\}_{i\in I}}
+  { }
+\qquad
+  \Infer[EFQ]
+   {\Gamma\bvdash e t \{(t_i,\Gamma_i)\}_{i\in I}\cup\{(\Empty, \Gamma')\}}
+   {\Gamma\bvdash e t \{(t_i,\Gamma_i)\}_{i\in I}}
+   { }
+\\
+  \Infer[Pair]
+  {
+   \forall i\in I.\ \Gamma_1^i = \subst{x_1}{t_i}\\
+   \forall i\in I.\ \Gamma_2^i = \subst{x_2}{s_i}
+  }
+  {\Gamma\bvdash {(x_1,x_2)} {\bigcup_{i\in I}(t_i,s_i)} \bigcup_{i\in I}\{(\pair{t_i}{s_i}, \Gamma_1^i\land\Gamma_2^i)\}}
+  { }
+  \\
+  \Infer[Proj]
+  {
+    i = 1 \Rightarrow t' = \pair{t}{\Any}\\
+    i = 2 \Rightarrow t' = \pair{\Any}{t}
+  }
+  {\Gamma\bvdash {\pi_i x}{t} \{(t,\subst{x}{\Gamma(x)\land t'})\}}
+  { }
+\\
+  \Infer[App]
+  {\Gamma(x_1)\equiv\bigvee_{i\in I}u_i \\ \Gamma(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_1^i = \subst{x_1}{u_i}\\
+  \forall i\in I.\ \Gamma_2^i = \subst{x_2}{t_i\land t'}\\
+  \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, \Gamma_{1}^i\land\Gamma_{2}^i)\}
+  }
+  { }
+\\
+  \Infer[Case]
+  {
+   \Gamma\subst{x}{t_x\land\Gamma(x)} \bvdash {e_1} {t} \{(t_i,\Gamma_1^i)\}_{i\in I}\\
+   \Gamma\subst{x}{\neg t_x\land\Gamma(x)} \bvdash {e_2} {t} \{(s_j,\Gamma_2^j)\}_{j\in J}}
+  {\Gamma\bvdash {\tcase {x} {t_x} {e_1}{e_2}}{t} \{(t_i,\Gamma_1^i\subst{x}{t_x\land\Gamma_1^i(x)})\}_{i\in I}
+  \cup \{(s_j,\Gamma_2^j\subst{x}{\neg t_x\land\Gamma_2^j(x)})\}_{j\in J}}
+  { }
+  \\
+  \Infer[Abs]
+  { }
+  {\Gamma\bvdash {\lambda x:s.\ e}{t} \{(t,\{\})\}}
+  { }
+  \qquad
+  \Infer[Abs-]
+  {t\leq \arrow{t_1}{t_2}\\ t_1\not\leq s}
+  {\Gamma\bvdash {\lambda x:s.\ e}{t} \{\}}
+  { }
+  \\
+  \Infer[Let]
+  {
+    \Gamma\bvdash{e}{t} \{(t_i,\Gamma_i)\}_{i\in I}\\
+    \forall i\in I.\ \Gamma\land\Gamma_i\bvdash{a}{\Gamma\land\Gamma_i)(x)} \{(t_i^j,\Gamma_i^j)\}_{j\in J_i}
+  }
+  {
+    \Gamma\bvdash{\letexp{x}{a}{e}}{t} \{(t_i,\Gamma_i\land\Gamma_i^j)\ \alt\ i\in I,\ j\in J_i\}
+  }
+  { }
+\end{mathpar}
+
+NOTE: For the Let rule: as the expression $a$ has been typed before backtyping,
+the environment is supposed to already contain a type for $x$.
+
+TODO: Simplify Case rule: as the expression has been typed before backtyping,
+$x$ is supposed to be included into $t_x$ or $\neg t_x$.
+
+TODO: Improve Abs rule
+
+TODO: Algorithmic App, Inter and EFQ rule
+
+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?