Commit 02d6ecbb authored by Mickael Laurent's avatar Mickael Laurent
Browse files

attempt in progress

parent c658912d
......@@ -113,7 +113,7 @@ TODO: Theorems and proof: no need for rule Inter, etc.
\subsection{Algorithmic type system}
The elements of $\Gamma\avdash\Gammap\ct e:t$ mean:
The elements of $\Gamma\avdash\Gammap\ct e:S$ mean:
\begin{itemize}
\item $\Gamma$ is the environment: it associates to some variables their associated type,
and can also associate types to variables that will be declared later in $e$ (in this case,
......@@ -246,8 +246,6 @@ The elements of $\Gamma\avdash\Gammap\ct e:t$ mean:
NOTE: No need to add the case statement to the context in the premises of the \Rule{CaseThen} and \Rule{CaseElse}
rules, because one branch is already unreachable and retyping only occurs with stronger environments.
TODO: Update rules below
\begin{mathpar}
\Infer[LetFirst]
......@@ -290,12 +288,6 @@ TODO: Update rules below
\Gamma'_i\setminus\{x\})\,\alt\,i\in I'\}}
{ }
\end{mathpar}
TODO: Check abs rule
TODO: The current environments returned by the typing rules are
not adapted at all to type lambda abstractions. The type associated
with a given environment should cover all the cases for this environment.
==> Need for the other refinement type system
\subsection{Backward typing rules}
......@@ -390,3 +382,173 @@ TODO: Algorithmic App, Inter and EFQ rule
TODO: Is the Comp rule needed in this new setting where every application is alone in a let,
and where union-arrow app are backtyped by splitting possibilities?
\subsection{Algorithmic typing rules (alternative attempt)}
\begin{mathpar}
\Infer[NoDef]
{ x\in\dom\Gammap\setminus\bv(e)\\
\Gamma\subst{x}{\Gamma(x)\land\Gammap(x)} \avdash{\Gammap\setminus\{x\}}{\ct} e : \tree}
{\Gamma \avdash\Gammap{\ct} e : \tree}
{ }
\qquad
\Infer[EFQ]
{\exists x\in\dom\Gamma.\ \Gamma(x)=\Empty}
{\Gamma \avdash\Gammap\ct e : \Leaf(\Empty,\Gamma)}
{ }
\\
\Infer[Const]
{ }
{\Gamma\avdash\Gammap\ct c: \Leaf(\basic{c},\Gamma)}
{ }
\quad
\Infer[Var]
{ }
{ \Gamma \avdash\Gammap\ct x: \Leaf(\Gamma(x),\Gamma)}
{ x\in\dom\Gamma }
\\
\Infer[Proj]
{\Gamma(x)\equiv\pair{t_1}{t_2}}
{\Gamma \avdash\Gammap\ct \pi_i x: \Leaf(t_i,\Gamma)}
{ }
\\
\Infer[Proj*]
{\Gamma(x)\equiv\textstyle\bigvee_{i\in I}\pair{t_i}{s_i}\\
\forall i\in I.\ \Gamma\avdash{\Gammap\subst{x}{\pair{t_i}{s_i}}}{[]} \ct[\pi_i x]: \tree_i
}
{\Gamma \avdash\Gammap\ct \pi_i x: \Node(\Gamma,\{\tree_i\}_{i\in I})}
{ }
\\
\Infer[ProjDom]
{\Gamma(x) = t\\
t\land(\pair{\Any}{\Any})\neq\Empty\\
t\land\neg(\pair{\Any}{\Any})\neq\Empty\\
\Gamma\avdash{\Gammap\subst{x}{t\land(\pair{\Any}{\Any})}}{[]} \ct[\pi_i x]: \tree_1\\
\Gamma\avdash{\Gammap\subst{x}{t\land\neg(\pair{\Any}{\Any})}}{[]} \ct[\pi_i x]: \tree_2
}
{\Gamma \avdash\Gammap\ct \pi_i x: \Node(\Gamma,\{\tree_1,\tree_2\})}
{ }
\\
\Infer[Pair]
{ }
{\Gamma \avdash\Gammap\ct (x_1,x_2):\Leaf(\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 \avdash\Gammap\ct {x_1}{x_2}: \Leaf((\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\avdash{\Gammap\subst{x_2}{s\land s_i}}{[]} \ct[{x_1}{x_2}]: \tree_i
}
{ \Gamma \avdash\Gammap\ct {x_1}{x_2}: \Node(\Gamma,\{\tree_i\}_{i\in I}) }
{ }
\\
\Infer[AppRDom]
{
\Gamma(x_1)\equiv \textstyle\bigwedge_{i\in I}\arrow {s_i}{t_i}\\
s_\circ=\textstyle\bigvee_{i\in I}s_i\\
\Gamma(x_2)=s\\s\land s_\circ\neq\Empty\\s\land \neg s_\circ\neq\Empty\\
\Gamma\avdash{\Gammap\subst{x_2}{s\land s_\circ}}{[]} \ct[{x_1}{x_2}]: \tree_1\\
\Gamma\avdash{\Gammap\subst{x_2}{s\land \neg s_\circ}}{[]} \ct[{x_1}{x_2}]: \tree_2
}
{ \Gamma \avdash\Gammap\ct {x_1}{x_2}: \Node(\Gamma,\{\tree_1,\tree_2\}) }
{ }
\\
\Infer[AppL*]
{\Gamma(x_1)\equiv\textstyle\bigvee_{i\in I}t_i\leq\arrow{\Empty}{\Any}\\
\forall i\in I.\ \Gamma\avdash{\Gammap\subst{x_1}{t_i}}{[]} \ct[{x_1}{x_2}]: \tree_i
}
{\Gamma \avdash\Gammap\ct {x_1}{x_2}: \Node(\Gamma,\{\tree_i\}_{i\in I})}
{ }
\\
\Infer[AppLDom]
{\Gamma(x_1) = t\\t\land (\arrow{\Empty}{\Any})\neq\Empty\\t\land \neg (\arrow{\Empty}{\Any})\neq\Empty\\
\Gamma\avdash{\Gammap\subst{x_1}{t\land(\arrow{\Empty}{\Any})}}{[]} \ct[{x_1}{x_2}]: \tree_1\\
\Gamma\avdash{\Gammap\subst{x_1}{t\land\neg(\arrow{\Empty}{\Any})}}{[]} \ct[{x_1}{x_2}]: \tree_2
}
{\Gamma \avdash\Gammap\ct {x_1}{x_2}: \Node(\Gamma,\{\tree_1,\tree_2\})}
{ }
\end{mathpar}
\begin{mathpar}
\Infer[CaseThen]
{
\Gamma(x)=t_\circ\\t_\circ\leq t\\
\Gamma \avdash\Gammap\ct e_1: \tree}
{\Gamma\avdash\Gammap\ct \tcase {x} t {e_1}{e_2}: \tree}
{ }
\\
\Infer[CaseElse]
{
\Gamma(x)=t_\circ\\t_\circ\leq \neg t\\
\Gamma \avdash\Gammap\ct e_2: \tree}
{\Gamma\avdash\Gammap\ct \tcase {x} t {e_1}{e_2}: \tree}
{ }
\\
\Infer[Case*]
{\Gamma(x) = t_\circ\\
\Gamma\avdash{\Gammap\subst{x}{t_\circ\land t}}{[]} \ct[\tcase {x} t {e_1}{e_2}]: \tree_1\\
\Gamma\avdash{\Gammap\subst{x}{t_\circ\land\neg t}}{[]} \ct[\tcase {x} t {e_1}{e_2}]: \tree_2
}
{\Gamma,\avdash\Gammap\ct \tcase {x} t {e_1}{e_2}: \Node(\Gamma,\{\tree_1,\tree_2\})}
{ }
\end{mathpar}
NOTE: No need to add the case statement to the context in the premises of the \Rule{CaseThen} and \Rule{CaseElse}
rules, because one branch is already unreachable and retyping only occurs with stronger environments.
\begin{mathpar}
\Infer[LetFirst]
{
\Gamma\avdash\Gammap\ct a:\tree\\
\{\Leaf(t_i,\Gamma_i)\}_{i\in I} = \tleaves(\tree)\\
\forall i\in I.\ \Gamma_i,(x:t_i)\avdash\Gammap{\ct[\letexp x a {[]}]} e : \tree_i\\
\tree'= \tree\text{ with each leaf } \Leaf(t_i,\Gamma_i) \text{ replaced with } \tree_i
}
{
\Gamma\avdash\Gammap\ct\letexp x a e : \tree'
}
{ x\not\in\dom\Gamma }
\\
\Infer[LetNoRefine]
{
\Gamma\avdash{\Gammap\setminus\{x\}}{\ct[\letexp x a {[]}]} e : \tree
}
{
\Gamma\avdash\Gammap\ct\letexp x a e : \tree
}
{ x\in\dom\Gamma \text{ and } (x\not\in\dom\Gammap \text{ or } \Gamma(x)\leq\Gammap(x)) }
\\
\Infer[LetRefine]
{
\Gamma\bvdash{a}{\Gamma(x)\land\Gammap(x)}\{(t_i,\Gamma_i)\}_{i\in I}\\
\forall i\in I.\ \Gamma\subst{x}{t_i}\avdash{(\Gammap\land\Gamma_i)\setminus\{x\}}{[]} \ct[\letexp x a e] : \tree_i}
{
\Gamma\avdash\Gammap\ct\letexp x a e : \Node(\Gamma, \{\tree_i\}_{i\in I})
}
{ x\in\dom\Gamma \text{ and } x\in\dom\Gammap \text{ and } \Gamma(x) \not\leq \Gammap(x) }
\end{mathpar}
\begin{mathpar}
\Infer[Abs]
{\Gamma,(x:s)\avdash{\Gammap}{\ct} e:\{(t_i,\Gamma_i)\}_{i\in I}\\
\{(t'_i,\Gamma'_i)\}_{i\in I'} = \{ (\textstyle\bigvee_{j\in I\text{ s.t. }\Gamma_i\setminus\bv(e)\equiv\Gamma_j\setminus\bv(e)} t_j,\ \Gamma_i\setminus\bv(e)) \alt i\in I \}\\
\forall i\in I'.\ t''_i = \textstyle\bigvee_{j\in I'\text{ s.t. } \Gamma'_i\land\Gamma'_j\neq\bot}t'_j
}
{\Gamma\vdash\lambda x:s.e: \{(
\textstyle\bigwedge_{j\in I'\text{ s.t. }\Gamma_i\setminus\{x\}\equiv\Gamma_j\setminus\{x\}} \arrow{\Gamma'_j(x)}{t''_j},\
\Gamma'_i\setminus\{x\})\,\alt\,i\in I'\}}
{ }
\end{mathpar}
TODO: Update the Abs rule. In particular, use $\fvdash{e}{t}$ to improve it.
......@@ -300,6 +300,12 @@
\newcommand{\avdash}[2]{\vdash_{#1,\ #2}}
\newcommand{\bt}[0]{\texttt{Backtrack}}
\newcommand{\Gammas}[0]{\bbGamma}
\newcommand{\Tree}[0]{\texttt{T}}
\newcommand{\Node}[0]{\texttt{N}}
\newcommand{\Leaf}[0]{\texttt{L}}
\newcommand{\tree}[0]{\mathcal{T}}
\newcommand{\ttype}[0]{\texttt{type}}
\newcommand{\tleaves}[0]{\texttt{leaves}}
\makeatletter % allow us to mention @-commands
\def\arcr{\@arraycr}
......
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