algorithmic type system in progress

new_system3.tex

@@ -110,3 +110,126 @@ TODO: Inter rule needed?
 \newpage
 
 \subsection{Algorithmic type system}
+
+\begin{mathpar}
+  \Infer[Const]
+  { }
+  {\Gamma\vdash_e c: \{(\basic{c},\Gamma)\}}
+  { }
+  \quad
+  \Infer[Var]
+{ }
+{ \Gamma \vdash_e x: \{(\Gamma(x),\Gamma)\} }
+{ x\in\dom\Gamma }
+\\
+\Infer[Backtrack]
+{\Gamma \vdash_e e': \bt\{t_i,\Gamma_i\}_{i\in I}}
+{\Gamma \vdash_e e : \{t_i,\Gamma_i\}_{i\in I}}
+{ }
+\qquad
+\Infer[Proj]
+{\Gamma(x)\equiv\pair{t_1}{t_2}}
+{\Gamma \vdash_e \pi_i x: \{t_i,\Gamma\}}
+{ }
+\\
+\Infer[Proj*]
+{\Gamma(x)\equiv\textstyle\bigvee_{i\in I}\pair{t_i}{s_i}\\
+\forall i\in I.\ \Gamma\subst{x}{\pair{t_i}{s_i}}\vdash_e e: \{(u_j,\Gamma_j)\}_{j\in J_i}
+}
+{\Gamma \vdash_e \pi_i x: \bt\{(u_j,\Gamma_j)\,\alt\,i\in I,\ j\in J_i\}}
+{ }
+\\
+\Infer[ProjDom]
+{\Gamma(x) = t\\
+\Gamma\subst{x}{t\land(\pair{\Any}{\Any})}\vdash_e e: \{(u_i,\Gamma_i)\}_{i\in I}\\
+\Gamma\subst{x}{t\land\neg(\pair{\Any}{\Any})}\vdash_e e: \{(u_j,\Gamma_j)\}_{j\in J}
+}
+{\Gamma \vdash_e \pi_i x: \bt\{(u_i,\Gamma_i)\}_{i\in I}\cup\{(u_j,\Gamma_j)\}_{j\in J}}
+{ }
+\\
+\Infer[Pair]
+{ }
+{\Gamma \vdash_e (x_1,x_2):\{(\pair {\Gamma(x_1)} {\Gamma(x_2)},\Gamma)\}}
+{ }
+\\
+\Infer[App]
+{
+  \Gamma(x_1)\equiv \textstyle\bigwedge_{i\in I}\arrow {s_i}{t_i}\\
+  \Gamma(x_2)=s\\
+  \exists i\in I.\ s\leq s_i
+}
+{ \Gamma \vdash_e {x_1}{x_2}: \{((\textstyle\bigwedge_{i\in I}\arrow {s_i}{t_i}) \circ s,\Gamma)\} }
+{ }
+\\
+\Infer[AppR*]
+{
+  \Gamma(x_1)\equiv \textstyle\bigwedge_{i\in I}\arrow {s_i}{t_i}\\
+  \Gamma(x_2)=s\\
+  s\leq \textstyle\bigvee_{i\in I}s_i\\
+  \forall i\in I.\ \Gamma\subst{x_2}{s\land s_i}\vdash_e e: \{(u_j,\Gamma_j)\}_{j\in J_i}
+}
+{ \Gamma \vdash_e {x_1}{x_2}: \bt\{(u_j,\Gamma_j)\,\alt\,i\in I,\ j\in J_i\} }
+{ }
+\\
+\Infer[AppRDom]
+{
+  \Gamma(x_1)\equiv \textstyle\bigwedge_{i\in I}\arrow {s_i}{t_i}\\
+  \Gamma(x_2)=s\\
+  s_\circ=\textstyle\bigvee_{i\in I}s_i\\
+  \Gamma\subst{x_2}{s\land s_\circ}\vdash_e e: \{(u_i,\Gamma_i)\}_{i\in I}\\
+  \Gamma\subst{x_2}{s\land \neg s_\circ}\vdash_e e: \{(u_j,\Gamma_j)\}_{j\in J}
+}
+{ \Gamma \vdash_e {x_1}{x_2}: \bt\{(u_i,\Gamma_i)\}_{i\in I}\cup\{(u_j,\Gamma_j)\}_{j\in J} }
+{ }
+\\
+\Infer[AppL*]
+{\Gamma(x_1)\equiv\textstyle\bigvee_{i\in I}\arrow{s_i}{t_i}\\
+\forall i\in I.\ \Gamma\subst{x_1}{\arrow{s_i}{t_i}}\vdash_e e: \{(u_j,\Gamma_j)\}_{j\in J_i}
+}
+{\Gamma \vdash_e {x_1}{x_2}: \bt\{(u_j,\Gamma_j)\,\alt\,i\in I,\ j\in J_i\}}
+{ }
+\\
+\Infer[AppLDom]
+{\Gamma(x_1) = t\\
+\Gamma\subst{x_1}{t\land(\arrow{\Empty}{\Any})}\vdash_e e: \{(u_i,\Gamma_i)\}_{i\in I}\\
+\Gamma\subst{x_1}{t\land\neg(\arrow{\Empty}{\Any})}\vdash_e e: \{(u_j,\Gamma_j)\}_{j\in J}
+}
+{\Gamma \vdash_e {x_1}{x_2}: \bt\{(u_i,\Gamma_i)\}_{i\in I}\cup\{(u_j,\Gamma_j)\}_{j\in J}}
+{ }
+\\
+\Infer[CaseThen]
+{
+\Gamma(x)=t_\circ\\t_\circ\leq t\\
+\Gamma \vdash_e e_1:\{(u_i,\Gamma_i)\}_{i\in I}}
+{\Gamma\vdash \tcase {x} t {e_1}{e_2}: \{(u_i,\Gamma_i)\}_{i\in I}}
+{ }
+\\
+\Infer[CaseElse]
+{
+\Gamma(x)=t_\circ\\t_\circ\leq \neg t\\
+\Gamma \vdash_e e_2:\{(u_i,\Gamma_i)\}_{i\in I}}
+{\Gamma\vdash \tcase {x} t {e_1}{e_2}: \{(u_i,\Gamma_i)\}_{i\in I}}
+{ }
+\\
+\Infer[Case*]
+{\Gamma(x) = t_\circ\\
+\Gamma\subst{x}{t_\circ\land t}\vdash_e e: \{(u_i,\Gamma_i)\}_{i\in I}\\
+\Gamma\subst{x}{t_\circ\land\neg t}\vdash_e e: \{(u_j,\Gamma_j)\}_{j\in J}
+}
+{\Gamma\vdash \tcase {x} t {e_1}{e_2}: \bt\{(u_i,\Gamma_i)\}_{i\in I}\cup\{(u_j,\Gamma_j)\}_{j\in J}}
+{ }
+% \\
+% \Infer[Abs]
+%   {\Gamma,(x:s)\vdash e:t}
+%   {\Gamma\vdash\lambda x:s.e: t}
+%   { }
+% \qquad
+% \Infer[Let]
+%   {\Gamma\vdash a:t_\circ\\
+%   \Gamma,(x:t_\circ)\vdash e:t}
+%   {
+%   \Gamma\vdash\letexp x a e : t
+%   }
+%   { }
+\end{mathpar}
+

setup.sty

@@ -293,6 +293,8 @@
 \newcommand{\ubvdash}[3]{\vdash^{{#1},\texttt{ Env}\leftarrow}_{#2,#3}}
 \newcommand{\cvdash}[0]{\vdash^{\texttt{Choices}}}
 
+\newcommand{\bt}[0]{\texttt{Backtrack}}
+
 \makeatletter % allow us to mention @-commands
 \def\arcr{\@arraycr}
 \makeatother
\ No newline at end of file