simplify backtyping

new_system3.tex

@@ -113,6 +113,13 @@ TODO: Theorems and proof: no need for rule Inter, etc.
 
 \subsection{Algorithmic type system}
 
+\begin{eqnarray*}
+  \dom{t}    & = & \bigwedge_{i\in I}\bigvee_{p\in P_i}s_p\\[4mm]
+  \apply t s & = & \bigvee_{i\in I}\left(\bigvee_{\{Q\subsetneq P_i\alt s\not\leq\bigvee_{q\in Q}s_q\}}\left(\bigwedge_{p\in P_i\setminus Q}t_p\right)\right)\hspace*{1cm}\makebox[0cm][l]{(for $s\leq\dom{t}$)}\\[4mm]
+  %\worra t s & = & \dom t \wedge\bigvee_{i\in I}\left(\bigwedge_{\{P \subseteq P_i\alt s \leq \bigvee_{p \in P} \neg t_p\}} \left(\bigvee_{p \in P} \neg s_p \right)\right)\\[4mm]
+  \worra t s & = & \left\{\left(\bigwedge_{p\in P_i}(s_p\to t_p)\bigwedge_{n\in N_i}\neg(s_n'\to t_n'),\ \dom t \wedge\bigwedge_{\{P \subseteq P_i\alt s \leq \bigvee_{p \in P} \neg t_p\}} \left(\bigvee_{p \in P} \neg s_p \right)\right)\ |\ i\in I\right\}
+\end{eqnarray*}
+
 The elements of $\Gamma\avdash\Gammap\ct e:S$ mean:
 \begin{itemize}
   \item $\Gamma$ is the environment: it associates to some variables their associated type,
@@ -297,6 +304,16 @@ rules, because one branch is already unreachable and retyping only occurs with s
 \subsection{Backward refinement rules}
 
 \begin{mathpar}
+%   \Infer[Inter]
+%   {\Gamma\vdash e:t' \\ \Gamma\bvdash e {t\wedge t'} \Gammas}
+%   {\Gamma\bvdash e t \Gammas}
+%   { }
+% \qquad
+\Infer[Normalize]
+{\Gamma\bvdash e t \Gammas\cup\{\Gamma'\}\\\exists x\in\dom{\Gamma'}.\ \Gamma'(x)=\Empty}
+{\Gamma\bvdash e t \Gammas}
+{ }
+\\
   \Infer[Var]
   { }
   {\Gamma\bvdash x t \{\{x:t\}\}}
@@ -306,16 +323,6 @@ rules, because one branch is already unreachable and retyping only occurs with s
 { }
 {\Gamma\bvdash c t \{\{\}\}}
 { }
-\\
-%   \Infer[Inter]
-%   {\Gamma\vdash e:t' \\ \Gamma\bvdash e {t\wedge t'} \Gammas}
-%   {\Gamma\bvdash e t \Gammas}
-%   { }
-% \qquad
-  \Infer[Normalize]
-   {\Gamma\bvdash e t \Gammas\cup\{\Gamma'\}\\\exists x\in\dom{\Gamma'}.\ \Gamma'(x)=\Empty}
-   {\Gamma\bvdash e t \Gammas}
-   { }
 \\
   \Infer[Pair]
   {
@@ -336,8 +343,7 @@ rules, because one branch is already unreachable and retyping only occurs with s
   { }
 \\
   \Infer[App]
-  {\Gamma(x_1)\equiv\textstyle\bigvee_{i\in I}u_i \\
-  \forall i\in I.\ u_i\leq \arrow{\neg t_i}{s_i} \text{ with } s_i\land t = \varnothing \\
+  {\worra{\Gamma(x_1)}t = \{ (u_i, t_i) \}_{i\in I} \\
   \forall i\in I.\ \Gamma_1^i = \subst{x_1}{u_i}\\
   \forall i\in I.\ \Gamma_2^i = \subst{x_2}{t_i}
   }
@@ -382,10 +388,21 @@ rules, because one branch is already unreachable and retyping only occurs with s
 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$.
+\begin{mathpar}
+  \Infer[App]
+  {\Gamma(x_1)\equiv\textstyle\bigvee_{i\in I}u_i \\
+  \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}
+  }
+  {
+    \Gamma\bvdash {(x_1\ x_2)} {t} \textstyle\bigcup_{i\in I}\{\Gamma_{1}^i\land\Gamma_{2}^i\}
+  }
+  { }
+\end{mathpar}
 
-TODO: Algorithmic App, Inter and EFQ rule
+TODO: Simplify Case and Let rule: as the expression has been typed before backtyping,
+$x$ is supposed to be included into $t_x$ or $\neg t_x$.
 
 \subsection{Algorithmic typing rules (alternative attempt)}