algorithmic type system in progress

new_system3.tex

@@ -237,12 +237,33 @@ t\land\neg(\pair{\Any}{\Any})\neq\Empty\\
 %   {\Gamma\vdash\lambda x:s.e: t}
 %   { }
 % \\
-% \Infer[Let]
-%   {\Gamma\vdash_e a:\{(t_i,\Gamma_i)\}_{i\in I}\\
-%   x\not\in\dom\Gamma \text{ or } \forall i.\ t_i\leq\Gamma(x)\\
-%   \forall i\in I.\ \Gamma_i,(x:t_i)\vdash_e e' : \{(u_j,\Gamma_j)\}_{j\in J_i}}
-%   {
-%   \Gamma\vdash_e\letexp x a e' : \{(u_j,\Gamma_j)\,\alt\,i\in I,\ j\in J_i\}
-%   }
-%   { }
+\Infer[Let]
+  {\Gamma\vdash_e a:\{(t_i,\Gamma_i)\}_{i\in I}\\
+  x\not\in\dom\Gamma \text{ or } \forall i.\ t_i\leq\Gamma(x)\\
+  \forall i\in I.\ \Gamma_i,(x:t_i)\vdash_e e' : \{(u_j,\Gamma_j)\}_{j\in J_i}}
+  {
+  \Gamma\vdash_e\letexp x a e' : \{(u_j,\Gamma_j)\,\alt\,i\in I,\ j\in J_i\}
+  }
+  { }
+  \\
+\Infer[LetRefine]
+  {\Gamma\vdash_e a:\{(t_i,\Gamma_i)\}_{i\in I}\\
+  \Gamma\bvdash{a}{\Gamma(x)}\{(t_j,\Gamma_j)\}_{j\in J}\\
+  \forall j\in J.\ \Gamma_j,(x:t_j)\vdash_e e : \{(u_k,\Gamma_k)\}_{k\in K_j}}
+  {
+  \Gamma\vdash_e\letexp x a e' : \bt\{(u_k,\Gamma_k)\,\alt\,j\in J,\ k\in K_j\}
+  }
+  { }
 \end{mathpar}
+
+TODO: Case rules with Backtrack in hypotheses
+
+TODO: Let rules with Backtrack in hypotheses
+
+TODO: Abs rules (problem??? the different splits for x
+cannot be cannot be retrieved...\\
+solution 1: instead
+of storing the whole expression e, only store what has already been
+typed so that we can retype up to the current expr.\\
+solution 2: rules take ALL the splits as argument
+(it handles all the branches), but more complex...)