Commit 7dbfdd36 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

removed files moved in new repository

parent 87797484
\withcommentstrue
\ifwithcomments
\renewcommand{\ignore}[1]{{\color{red}\textbf{DELETED:}#1}}
\renewcommand{\beppe}[1]{{\color{blue}\textbf{Beppe:} #1}}
\renewcommand{\mick}[1]{{\bf\color{gray}Mickael: #1}}
\renewcommand{\kim}[1]{{\bf\color{pink}Kim: #1}}
\renewcommand{\victor}[1]{{\bf\color{purple}Victor: #1}}
\else
\renewcommand{\ignore}[1]{}
\renewcommand{\beppe}[1]{}
\renewcommand{\mick}[1]{}
\renewcommand{\kim}[1]{}
\renewcommand{\victor}[1]{}
\fi
The idea here is to modify the inference of Section~\ref{sec:refining}
so that it infers \emph{sets of type environments}---that we denote as
$\{\Gamma_i\alt i\in I\}$ or equivalently $\{\Gamma_i\}_{i\in
I}$---rather than sets $\psi$ of single mappings from expression variables to types.
The advantage is that by using type environments we can record the
correlations of distinct expression variables and, by introducing an
explicit \p{let} construction, we can capture (part/all? of) the flow analysis
performed by~\citet{THF10}.
As in Section~\ref{sec:refining} there are two distinct (but mutally
recursive) systems: one is the system to infer the type environments, whose
judgements are of the form $\Gamma\vdash e\triangleright
\{\Gamma_i\}_{i\in I}$; the other is the type inference system we
presented in Section~\ref{sec:static} which we modify/extend to
exploit the results of the inference of $\Gamma\vdash e\triangleright
\{\Gamma_i\}_{i\in I}$.
For what concerns the type inference system we have to modify the rule
for typing $\lambda$-abstractions and add a rule for
\p{let}-expressions:
\begin{mathpar}
\Infer[AbsInf+] {\forall i\in I\hspace*{2mm}
T_i = \{ (u, w) ~|~ \exists j\in J_i. u=\Gamma^j_i(x) \text{ and }
\Gamma, x:u\vdash e : w\}\\
\Gamma,x:s_i\vdash e\triangleright\{\Gamma_i^j\alt j\in J_i\}
\qquad
\Gamma,x:s_i\vdash
e : t_i
} {\textstyle \Gamma\vdash\lambda^{\bigwedge_{i\in
I}s_i\to t_i} x.e:\bigwedge_{i\in I}((s_i\to
t_i)\land\bigwedge_{(u, w)\in T_i}(u\to w)) } {}
\\
\Infer[Let]{
\Gamma\vdash e\triangleright \{\Gamma_i\}_{i\in I}\and
\forall i\in I \quad\Gamma_i\vdash e_1:t_i\and\Gamma_i,x:t_i\vdash
e_2: t
}{
\Gamma \vdash \letexp{x}{e_1}{e_2}:t
}{}
\end{mathpar}
The rule \Rule{AbsInf+} is a straightforward modification of the
corresponding rule in Section~\ref{sec:static}, where instead of
picking the different type assignements for $x$ in $\psi_i$ we pick
them in the distinct $\Gamma_i^j$ for $j\in J_i$. The rule \Rule{Let}
refines the classic rule for \p{let} by inferring all the different
type assignements for the variables free in $e_1$; each type assignement
can yield a different typing for $e_2$ and, thus, for $x$; these
different type assignements are then
used to type $e_2$. The multiple check in this rule is what allow us
to record the flow of
information from $e_1$ to $x$: instead of deducing from $\Gamma$ a monolytic type $t$ for
$e_1$ and use it as typing hypothesis for $x$ to type $e_2$, the rule decomposes this $t$ into
a set of types $\{\Gamma_i(x)\}_{i\in I}$ so that $t(= or
\leq??)\bigvee_{i\in I}\Gamma_i(x)$ and then uses this decomposition of
$t$ to perform a finer-grained analysis of the type of $e_2$ and,
thus, of the \p{let} expression. It is
clear that the most precise typing of a \p{let} expression would be obtained by checking the
let constructions for all possible bindings of $x$ to a value that may
be produced by $e_1$. That is the most precise rule for \p{let} would be:
\begin{mathpar}
\Infer[Let]{
\Gamma\vdash e_1:t\and
\forall v:t \quad\Gamma,x:v\vdash
e_2: t
}{
\Gamma \vdash \letexp{x}{e_1}{e_2}:t
}{}
\end{mathpar}
Since this decomposition is impossible we decompose $t$ into
a union type whose summands are the types that are suggested by
analysing $e_1$:(REWRITE)
\begin{mathpar}
\Infer[Let]{\textstyle
\Gamma\vdash e_1:\bigvee_{i\in I}t_i\and
\forall i\in I \quad\Gamma,x:t_i\vdash
e_2: t
}{
\Gamma \vdash \letexp{x}{e_1}{e_2}:t
}{}
\end{mathpar}
The various $\Gamma_i(x)$'s collected by the analysis are approximations of these $t_i$ (actually
they are supertypes since they are used contravariantly). \beppe{Are
they? The point is whether the analysis lose any information or
not. In other terms if we infer $\Gamma\vdash
e\triangleright \{\Gamma_i\}_{i\in I}$ do we have for every $x$
in $\dom{\Gamma}$ either $\bigvee_{i\in i}\Gamma_i(x)\leq\Gamma(x)$ or
rather $\bigvee_{i\in i}\Gamma_i(x)=\Gamma(x)$? I tend to think that
is the second option, but we have to check it}.
Next we have to define the system to infer the judgements of the form
$\Gamma\vdash e\triangleright \{\Gamma_i\}_{i\in I}$. The idea is that when
we infer such a judgement it means that we have used the expression
$e$ to refine the environment $\Gamma$ by \emph{slicing} it into a set of environments $\{\Gamma_i\}_{i\in I}$ that
(should?) satisfy the following properties:
\begin{enumerate}
\item $\forall i \in I.\dom{\Gamma_i} = \dom{\Gamma}$
\item $\forall x \in \dom\Gamma. \bigvee_{i\in I}\Gamma_i(x)\leq
\Gamma(x)$ \beppe{(does equality holds? It may not be so since we
restrict the type of $x$ only to the result of the analysis, but
probably equality holds ... to check)}
\end{enumerate}
As for the systems in Section~\ref{sec:refining} the actual slicing of
an environment is performed when an overloaded function is applied to
an expression variable, but also by the let expression, as shown by the following (rather complicated)
rules:
\begin{mathpar}
\Infer[OverApp]
{
\Gamma \vdash e\triangleright\{\Gamma_i\}_{i\in I}\\
\forall i{\in}I\quad \Gamma_i \vdash e : \textstyle\bigvee_{h\in H(i)} \bigwedge_{j \in J(h,i)}t_j^{hi}\to{}s_j^{hi}\\
}
{ \Gamma \vdash\textstyle
{e}{~x}\triangleright\{\Gamma_i,x:\Gamma_i(x)\wedge t_j^{hi}\alt
i\in I, h\in H(i), j\in J(h,i),\Gamma_i(x)\wedge t_j^{hi}\not\simeq\Empty \}
}
{}
\\
\Infer[Let]
{\Gamma\vdash e_1\triangleright\{\Gamma_i\}_{i\in I}\\
\forall i\in I\quad\Gamma_i\vdash e_1:t_i\\
\Gamma_i, x:t_i\vdash e_2\triangleright\{\Gamma_j^i\}_{j\in J_i}
}{
\Gamma\vdash \letexp x{e_1}{e_2}\triangleright\{\Gamma_j^i\alt
i\in I, j\in J_i\}
}{}
\end{mathpar}
The idea for \Rule{OverApp} is that we take all the $\Gamma_i$
generated by using $e$ to slice $\Gamma$ and we use each of them to
deduce a (possibly overloaded) type for $e$. Then we use the
overloaded type obtained from $\Gamma_i$ to slice $\Gamma_i$ itself: we do it by
refining the type of $x$ via the intersection of each input type that
is compatible with the type of $x$. \beppe{Pas clair du tout n'est pas?}
The rule \Rule{Let} is subtler ... but do we really need such a
precision or would be the following simpler rule enough?
\begin{mathpar}
\Infer[Let(simple)]
{\Gamma\vdash e_1:t_1\\
\Gamma, x:t_1\vdash e_2\triangleright\{\Gamma_i\}_{i\in I}
}{
\Gamma\vdash \letexp x{e_1}{e_2}\triangleright\{\Gamma_i\}_{i\in I}
}{}
\end{mathpar}
the \p{test2} at the end seems to suggest that we need the better rule
(or not?)
\beppe{Food for you thoughts: why the slicing is for generic let but
only for a specific application (of an overloaded function to a
variable)? As a matter of fact, a generic let is just a generic
application of a $\lambda$-abstraction to a generic expression and
not the application of an overloaded function to a variable. Do we
really perform slicing in let or it is more akin to the other rules
that propagate (cf rules for application and pairs)}
The rules for the remaining expressions just compose and propagate the
slicing of their sub-expressions:
\begin{mathpar}
\Infer[Var]
{
}
{ \Gamma \vdash x \triangleright\{\Gamma\}}
{}
\hfill
\Infer[Const]
{
}
{ \Gamma \vdash c \triangleright \{\Gamma\}}
{}
\hfill
\Infer[Abs]
{\Gamma,x:s_i\vdash e\triangleright\{\Gamma_j^i\}_{j\in J_i}}
{
\Gamma\vdash\lambda^{\bigwedge_{i\in
I}s_i\to t_i}x.e\triangleright\{\Gamma_j^i\setminus\{x\}\alt
i\in I,j\in J_i\}
}
{}
\\
\Infer[App]
{
\Gamma \vdash e_1\triangleright \{\Gamma_i\}_{i\in I} \\
\Gamma_i\vdash e_2\triangleright\{\Gamma_j^i\}_{j\in J_i}
}
{ \Gamma \vdash {e_1}{e_2}\triangleright\{\Gamma_j^i\alt
i\in I, j\in J_i\}}
{(e_2\not\equiv x)}
\hfill
\Infer[Pair]
{
\Gamma \vdash e_1\triangleright \{\Gamma_i\}_{i\in I} \\
\Gamma_i\vdash e_2\triangleright\{\Gamma_j^i\}_{j\in J_i}
}
{ \Gamma \vdash ({e_1},{e_2})\triangleright\{\Gamma_j^i\alt
i\in I, j\in J_i\}
}
{}
\\
\Infer[Proj]
{\Gamma \vdash e\triangleright \{\Gamma_i\}_{i\in I}}
{\Gamma \vdash \pi_i e\triangleright \{\Gamma_i\}_{i\in I}}
{}
\\
\Infer[Case]
{\Gamma\vdash e\triangleright \{\Gamma_i\}_{i\in I}\\
\Gamma \evdash e t \Gamma_1\\ \Gamma_1\vdash e_1\triangleright \{\Gamma_j\}_{j\in J}\\
\Gamma \evdash e {\neg t} \Gamma_2 \\ \Gamma_2\vdash e_2\triangleright \{\Gamma_h\}_{h\in H}}
{\Gamma\vdash \ifty{e}{t}{e_1}{e_2}\triangleright \{\Gamma_k\}_{k\in I\cup H\cup J}}
{}
\end{mathpar}
\subsection{DOUBT ABOUT Case}
Not sure that the rule case is the right one. The various
slicing shoud compose (as for the \p{let}) I suspect, not just be
superposed (if $\Gamma_1$ and $\Gamma_2$ are specializations of
$\Gamma$ then we just remove $I$ from the union?). Check the
difference below between \p{test1} and \p{test2}.
The more I think of it the more I am sure it is not correct. The point
is that slicing is very important, we do not have to \textbf{add} a
type environment to the existing one but we have to \textbf{slice} the
existing one (since all environments must type-check, then having the
original one in the sliced set makes slicing useless). So I think that
the minimal informatio is obtained by the following rule:
\begin{mathpar}
\Infer[Case]
{%\Gamma\vdash e\triangleright \{\Gamma_i\}_{i\in I}\\
\Gamma \evdash e t \Gamma_1\\ \Gamma_1\vdash e_1\triangleright \{\Gamma_j\}_{j\in J}\\
\Gamma \evdash e {\neg t} \Gamma_2 \\ \Gamma_2\vdash e_2\triangleright \{\Gamma_h\}_{h\in H}}
{\Gamma\vdash \ifty{e}{t}{e_1}{e_2}\triangleright \{\Gamma_k\}_{k\in
H\cup J}}
{}
\end{mathpar}
and I suspect that if we want a more precise analysis then we have to
use the slicing of $e$ for generating the new slicings:
\begin{mathpar}
\Infer[Case]
{\Gamma\vdash e\triangleright \{\Gamma_i\}_{i\in I}\\
\forall i\in I\quad \Gamma_i \evdash e t \Gamma^i_1\\ \Gamma_1^i\vdash e_1\triangleright \{\Gamma^i_j\}_{j\in J_i}\\
\Gamma_i \evdash e {\neg t} \Gamma^i_2 \\ \Gamma^i_2\vdash e_2\triangleright \{\Gamma_h^i\}_{h\in H_i}}
{\Gamma\vdash \ifty{e}{t}{e_1}{e_2}\triangleright \{\Gamma_k\alt
i\in I, k\in
H_i\cup J_i\}}
{}
\end{mathpar}
but then I think we have to change the typing rule for the case
accordingly, I think:
\begin{mathpar}
\Infer[Case]
{\Gamma\vdash e:t_0\\
\Gamma\vdash e\triangleright \{\Gamma_i\}_{i\in I}\\
\forall i\in I\quad \Gamma_i \evdash e t \Gamma^i_1\\
\Gamma_1^i\vdash e_1:t'\\
\Gamma_i \evdash e {\neg t} \Gamma^i_2 \\ \Gamma^i_2\vdash e_2:t'}
{\Gamma\vdash \ifty{e}{t}{e_1}{e_2}:t'}
{}
\end{mathpar}
if it is so then \Rule{Case} would be the third typing rule to use
slicing and the third analysis rule to generate slicing.
\paragraph{QUESTION:} in the rules \Rule{App} \Rule{Pair} we performed a left to
right slicing: we first sliced $\Gamma$ by using $e_1$ and then sliced
the resulting slices by using $e_2$. Would a right-to-left slicing
give the same results (thanks to the commutativity of intersections)?
\paragraph{SMALL DETAIL:} since our environments map also generic expressions to
types, should we restric the $\Gamma$s in the rules \Rule{Var} and
\Rule{Const} just to variables?
\paragraph{NOTE:}
We should change the name of the rules to reflect that they belong to
type-checking or to the flow analysis. For
instance \Rule{Case$_{\mathcal{T}}$} \Rule{Case$_{\mathcal{F}}$}
\paragraph{EXAMPLES TO TEST:}
\begin{alltt}
let is_int = fun ( x : Any ) ->
if x is Int then true else false
(* the following should type check *)
let test1 = fun( y : Int | Bool) ->
let x = is_int y in
if x is True then y + 1 else lnot y
(* here we inline is_int *)
let test2 = fun( y : Int | Bool) ->
let x = if y is Int then true else false in
if x is True then y + 1 else lnot y
\end{alltt}
\subsection{Syntax}
\[
\begin{array}{lrcl}
\textbf{Types} & t & ::= & b\alt t\to t\alt t\times t\alt t\vee t \alt \neg t \alt \Empty
\end{array}
\]
\begin{equation}\label{expressions2}
\begin{array}{lrclr}
\textbf{Atomic Expr} &a &::=& c\alt x\alt\lambda x:t.e\alt (a,a)\\[.3mm]
\textbf{U-Expr} &u &::=& a a\alt \tcase{x}{t}{e}{e}\alt \pi_i a\\[.3mm]
\textbf{P-Expr} &p &::=& u\alt a\\[.3mm]
\textbf{Expressions} &e &::=& \letexp{x}{p}{e}\alt p \\[.3mm]
\textbf{Values} &v &::=& c\alt\lambda x:t.e\alt (v,v)\\
\end{array}
\end{equation}
TODO: the then and else expressions of typecases have no associated variable,
altough the env refinement rules could refine their types...
Is this an issue? Should we require an atomic in the then and else branchs
(seems difficult: there would be no equivalent normal form)?
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}
\begin{mathpar}
\Infer[Var]
{
}
{ \Gamma \vdash y \triangleright_x \varnothing }
{}
\hfill
\Infer[Const]
{
}
{ \Gamma \vdash c \triangleright_x \varnothing }
{}
\hfill
\Infer[Abs]
{\Gamma,(y:s)\vdash e\triangleright_x\dt}
{
\Gamma\vdash\lambda y:s.\ e\triangleright_x\dt
}
{x\neq y}
\vspace{-2.3mm}\\
\Infer[Pair]
{\Gamma \vdash a_1\triangleright_x\dt_1 \and \Gamma \vdash a_2\triangleright_x\dt_2}
{\Gamma \vdash (a_1,a_2)\triangleright_x\dt_1\cup\dt_2}
{}
\hfill
\Infer[Proj]
{\Gamma \vdash a\triangleright_x\dt}
{\Gamma \vdash \pi_i a\triangleright_x\dt}
{}
\vspace{-2.3mm}\\
\Infer[Case]
{\Gamma\subst{y}{\Gamma(y)\land t}\vdash e_1\triangleright_x\dt_1\\
\Gamma\subst{y}{\Gamma(y)\land \neg t}\vdash e_2\triangleright_x\dt_2}
{\Gamma\vdash \tcase{y}{t}{e_1}{e_2}\triangleright_x\dt_1\cup\dt_2\cup
\left\{
\begin{array}{l}
\{\Gamma(x)\land t,\Gamma(x)\land\neg t\} \text{ if } y=x\arcr
\varnothing\text{ otherwise}
\end{array}
\right.}
{}
\vspace{-2.3mm}\\
\Infer[App]
{
\Gamma \vdash a_1 : \textstyle{\bigvee \bigwedge_{i \in I}s_i\to t_i}\\
\Gamma \vdash a_1\triangleright_x\dt_1\\
\forall i\in I.\ \Gamma\fvdash{a_2}{s_i}\{\Gamma_i^j\}_{j\in J_i}
}
{ \Gamma \vdash a_1 a_2\triangleright_x\dt_1\cup\textstyle{\bigcup_{i\in I}
\bigcup_{j\in J_i}\{\Gamma_i^j(x)\}} }
{}
\vspace{-2.3mm}\\
\Infer[Let]
{
\Gamma \vdash p: t\\
\Gamma, (y:t) \vdash e\triangleright_x\dt_x\\
\Gamma, (y:t) \vdash e\triangleright_y\dt_y\\
\forall u\in \dt_y.\ \Gamma\fvdash{p}{u}\{\Gamma_u^i\}_{i\in I_u}
}
{ \Gamma \vdash\letexp{y}{p}{e}\triangleright_x\dt_x\cup\textstyle{
\bigcup_{u\in \dt_y}\bigcup_{i\in I_u}\{\Gamma_u^i(x)\}
}}
{}
\end{mathpar}
TODO: example: application $x y$ with $x$ an union of arrow. Candidates
for $x$ should be all the different union of arrows of its type?
TODO: Candidates for a variable should be a special "all splits".
Otherwise, $\letexp{x}{\cdots}{x}$ will never be splitted.
TODO: test type system with $\lambda x:\pair{\Int}{\Int}\lor\pair{\Bool}{\Bool}. (\pi_1 x, \pi_2 x)$
TODO: Problem when typing the following:\\
\begin{lstlisting}
x: Bool
let y = x in
let z = if y is True then (fun (z:True) -> true) else (fun (z:False) -> false)
in z x
\end{lstlisting}\vspace{1em}
The typing rules should return a list of pair (type, environments) in order to be
as precise as possible (= remember correlations). When typing a let, the candidates of $e_2$
should be computed under each possible environment of $e_1$ (in this way, we are sure that the
next operation will type (if possible)). Then, the candidate operator should return as soon
as it finds a required split, and it should be applied again and again until there
is no new split.
\subsection{Forward refinement rules}
\subsection{Backward refinement rules}
\subsection{Syntax}
\[
\begin{array}{lrcl}
\textbf{Types} & t & ::= & b\alt t\to t\alt t\times t\alt t\vee t \alt \neg t \alt \Empty
\end{array}
\]
\begin{equation}\label{expressions2}
\begin{array}{lrclr}
\textbf{Atomic expr} &a &::=& c\alt x\alt\lambda x:t.e\alt (x,x)
\alt x x\alt \tcase{x}{t}{e}{e}\alt \pi_i x\\[.3mm]
\textbf{Expressions} &e &::=& \letexp{x}{a}{e}\alt a \\[.3mm]
\textbf{Values} &v &::=& c\alt\lambda x:t.e\alt (v,v)\\
\end{array}
\end{equation}
TODO: the then and else expressions of typecases have no associated variable,
altough the env refinement rules could refine their types...
Is this an issue? Should we require an atomic in the then and else branchs
(seems difficult: there would be no equivalent normal form)?
TODO: Which restrictions on types? (cannot test a precise arrow type, etc)
TODO: Should we allow expr as let definition?
\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 x:\pair{t_1}{t_2}}
{\Gamma \vdash \pi_i x:t_i}
{ }
\qquad
\Infer[Pair]
{\Gamma \vdash x_1:t_1 \and \Gamma \vdash x_2:t_2}
{\Gamma \vdash (x_1,x_2):\pair {t_1} {t_2}}
{ }
\\
\Infer[App]
{
\Gamma \vdash x_1: \arrow {t_1}{t_2}\quad
\Gamma \vdash x_2: t_1
}
{ \Gamma \vdash {x_1}{x_2}: t_2 }
{ }
\\
\Infer[Case]
{
\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'}
{ x\in\dom\Gamma }
\\
\Infer[AbsBase]
{
\Gamma,(x:t')\vdash e:t}
{
\Gamma\vdash_{t'}\lambda x:s.e:\arrow {(t'\land s)} {t}
}
{ }
\\
\Infer[AbsSplit]
{
\Gamma,(x:t')\vdash e\triangleright_x\dt\\
\textstyle {\dt'=\dt\cup\left\{t'\setminus\bigcup_{s'\in\dt}s'\right\}}\\
\forall u\in\dt'.\ \Gamma\textstyle\vdash_u \lambda x:s.e: t_u
}
{
\Gamma\vdash_{t'}\lambda x:s.e: \textstyle\bigwedge_{u\in\dt'}t_u
}
{ }
\\
\Infer[Abs]
{\Gamma\vdash_{s} \lambda x:s.e: t}
{
\Gamma\vdash\lambda x:s.e: t
}
{ }
\\
\Infer[LetBase]
{
\Gamma,(x:u)\vdash e:t}
{
\Gamma\vdash_{u}\letexp x a e : t
}
{ }
\\
\Infer[LetSplit]
{
\Gamma,(x:t')\vdash e\triangleright_x\dt\\