add typing rules

new_system.tex

@@ -20,6 +20,83 @@ TODO: Which restrictions on types? (cannot test a precise arrow type, etc)
 
 \subsection{Typing rules}
 
+\begin{mathpar}
+  \Infer[Const]
+  { }
+  {\Gamma\vdash c:\basic{c}}
+  { }
+  \quad
+  \Infer[Var]
+{ }
+{ \Gamma \vdash x: \Gamma(x) }
+{ x\in\dom\Gamma }
+% \qquad
+% \Infer[Inter]
+% { \Gamma \vdash e:t_1\\\Gamma \vdash e:t_2 }
+% { \Gamma \vdash e: t_1 \wedge t_2 }
+% { }
+\qquad
+\Infer[Subs]
+{ \Gamma \vdash e:t\\t\leq t' }
+{ \Gamma \vdash e: t' }
+{ }
+\\
+\Infer[Efq]
+{ \exists x\in\dom{\Gamma}.\ \Gamma(x)=\Empty }
+{ \Gamma \vdash e: t }
+{ }
+\qquad
+\Infer[Proj]
+{\Gamma \vdash a:\pair{t_1}{t_2}}
+{\Gamma \vdash \pi_i a:t_i}
+{ }
+\qquad
+\Infer[Pair]
+{\Gamma \vdash a_1:t_1 \and \Gamma \vdash a_2:t_2}
+{\Gamma \vdash (a_1,a_2):\pair {t_1} {t_2}}
+{ }
+\\
+\Infer[App]
+{
+  \Gamma \vdash a_1: \arrow {t_1}{t_2}\quad
+  \Gamma \vdash a_2: t_1
+}
+{ \Gamma \vdash {a_1}{a_2}: t_2 }
+{ }
+\\
+\Infer[Case]
+{
+x\in\dom\Gamma\\  
+\Gamma\subst{x}{\Gamma(x)\land t} \vdash e_1:t'\\
+\Gamma\subst{x}{\Gamma(x)\land \neg t} \vdash e_2:t'}
+{\Gamma\vdash \tcase {x} t {e_1}{e_2}: t'}
+{ }
+\\
+\Infer[Abs]
+  {\Gamma,(x:s)\vdash e\triangleright_x \dt\\
+  \textstyle {\dt'=\dt\cup\left\{s\setminus\bigcup_{s'\in\dt}s'\right\}}\\
+  T=\{(s',t')\,|\,s'\in\dt' \text{ and } \Gamma,(x:s')\vdash e:t'\}}
+  {
+  \Gamma\vdash\lambda x:s.e:\textstyle \bigwedge_{(s',t')\in T}\arrow {s'} {t'}
+  }
+  { }
+\\
+\Infer[Let]
+  {\Gamma\vdash p:t_x\\
+  \Gamma,(x:t_x)\vdash e\triangleright_x\dt\\
+  \textstyle {\dt'=\dt\cup\left\{t_x\setminus\bigcup_{u\in\dt}u\right\}}\\
+  \forall u\in\dt'.\ \Gamma\bvdash{p}{u} (\Gamma_u^i)_{i\in I_u}\\
+  \forall u\in\dt'.\ \forall i\in I_u.\ \Gamma_u^i,(x:u)\vdash e:t}
+  {
+  \Gamma\vdash\letexp x p e : t
+  }
+  { }
+\end{mathpar}
+
+TODO: Inter rule needed?
+
+TODO: Algorithmic rules
+
 \subsection{Candidates generation rules}
 
 \subsection{Forward refinement rules}

setup.sty

@@ -284,3 +284,6 @@
 \newcommand{\RRefine}[1]{\textsf{Refine}_{#1}}
 \newcommand{\lfp}[1]{\textsf{lfp}_{#1}}
 \newcommand{\RRefineStep}[1]{\textsf{RefineStep}_{#1}}
+\newcommand{\dt}[0]{\mathbb{T}}
+\newcommand{\fvdash}[2]{\vdash^{\texttt{Env}\rightarrow}_{#1,#2}}
+\newcommand{\bvdash}[2]{\vdash^{\texttt{Env}\leftarrow}_{#1,#2}}
\ No newline at end of file