Commit 78ea0c43 authored by Mickael Laurent's avatar Mickael Laurent
Browse files

algorithmic type system in progress

parent 1fb585b9
......@@ -106,7 +106,9 @@ TODO: Which restrictions on types? (cannot test a precise arrow type, etc)
{ }
\end{mathpar}
TODO: Inter rule needed?
TODO: Inter rule needed?\\
TODO: Theorems and proof: no need for rule Inter, etc.
\newpage
\subsection{Algorithmic type system}
......@@ -114,12 +116,12 @@ TODO: Inter rule needed?
\begin{mathpar}
\Infer[EFQ]
{\exists x\in\dom\Gamma.\ \Gamma(x)=\Empty}
{\Gamma \vdash_e e' : \Empty}
{\Gamma \vdash_e e' : \{(\Empty,\Gamma)\}}
{ }
\qquad
\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}}
{\Gamma \vdash_e e : \bt\{t_i,\Gamma_i\}_{i\in I}}
{\Gamma \vdash_e e : \{(t_i,\Gamma_i)\}_{i\in I}}
{ }
\\
\Infer[Const]
......@@ -134,7 +136,7 @@ TODO: Inter rule needed?
\\
\Infer[Proj]
{\Gamma(x)\equiv\pair{t_1}{t_2}}
{\Gamma \vdash_e \pi_i x: \{t_i,\Gamma\}}
{\Gamma \vdash_e \pi_i x: \{(t_i,\Gamma)\}}
{ }
\\
\Infer[Proj*]
......@@ -223,18 +225,20 @@ TODO: Inter rule needed?
}
{\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}}
{ }
% \\
\end{mathpar}
\begin{mathpar}
% \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_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\letexp x a e : t
% \Gamma\vdash_e\letexp x a e' : \{(u_j,\Gamma_j)\,\alt\,i\in I,\ j\in J_i\}
% }
% { }
\end{mathpar}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment