Commit ca61d22c authored by Mickael Laurent's avatar Mickael Laurent
Browse files

let rule in progress

parent 2f394a80
......@@ -113,47 +113,59 @@ TODO: Theorems and proof: no need for rule Inter, etc.
\subsection{Algorithmic type system}
The elements of $\Gamma\avdash\Gammap\ct e:t$ 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,
it can be seen as an assumption that we can make about the type of a future variable)
\item $\ct$ is the context in which $e$ is located
(it is used when backtyping: the whole context is retyped)
\item $\Gammap$ is an additional environment that maps some "future" variables
to a type. It can be seen as an assumption we make about the type of a future variable,
but that hasn't been propagated yet.
\end{itemize}
\begin{mathpar}
\Infer[EFQ]
{\exists x\in\dom\Gamma.\ \Gamma(x)=\Empty}
{\Gamma \vdash_\ct e : \{(\Empty,\Gamma)\}}
{\Gamma \avdash\Gammap\ct e : \{(\Empty,\Gamma)\}}
{ }
\qquad
\Infer[Const]
{ }
{\Gamma\vdash_\ct c: \{(\basic{c},\Gamma)\}}
{\Gamma\avdash\Gammap\ct c: \{(\basic{c},\Gamma)\}}
{ }
\quad
\Infer[Var]
{ }
{ \Gamma \vdash_\ct x: \{(\Gamma(x),\Gamma)\} }
{ \Gamma \avdash\Gammap\ct x: \{(\Gamma(x),\Gamma)\} }
{ x\in\dom\Gamma }
\\
\Infer[Proj]
{\Gamma(x)\equiv\pair{t_1}{t_2}}
{\Gamma \vdash_\ct \pi_i x: \{(t_i,\Gamma)\}}
{\Gamma \avdash\Gammap\ct \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_{[]} \ct[\pi_i x]: \{(u_j,\Gamma_j)\}_{j\in J_i}
\forall i\in I.\ \Gamma\avdash{\Gammap\subst{x}{\pair{t_i}{s_i}}}{[]} \ct[\pi_i x]: \{(u_j,\Gamma_j)\}_{j\in J_i}
}
{\Gamma \vdash_\ct \pi_i x: \{(u_j,\Gamma_j)\,\alt\,i\in I,\ j\in J_i\}}
{\Gamma \avdash\Gammap\ct \pi_i x: \{(u_j,\Gamma_j)\,\alt\,i\in I,\ j\in J_i\}}
{ }
\\
\Infer[ProjDom]
{\Gamma(x) = t\\
t\land(\pair{\Any}{\Any})\neq\Empty\\
t\land\neg(\pair{\Any}{\Any})\neq\Empty\\
\Gamma\subst{x}{t\land(\pair{\Any}{\Any})}\vdash_{[]} \ct[\pi_i x]: \{(u_i,\Gamma_i)\}_{i\in I}\\
\Gamma\subst{x}{t\land\neg(\pair{\Any}{\Any})}\vdash_{[]} \ct[\pi_i x]: \{(u_j,\Gamma_j)\}_{j\in J}
\Gamma\avdash{\Gammap\subst{x}{t\land(\pair{\Any}{\Any})}}{[]} \ct[\pi_i x]: \{(u_i,\Gamma_i)\}_{i\in I}\\
\Gamma\avdash{\Gammap\subst{x}{t\land\neg(\pair{\Any}{\Any})}}{[]} \ct[\pi_i x]: \{(u_j,\Gamma_j)\}_{j\in J}
}
{\Gamma \vdash_\ct \pi_i x: \{(u_i,\Gamma_i)\}_{i\in I}\cup\{(u_j,\Gamma_j)\}_{j\in J}}
{\Gamma \avdash\Gammap\ct \pi_i x: \{(u_i,\Gamma_i)\}_{i\in I}\cup\{(u_j,\Gamma_j)\}_{j\in J}}
{ }
\\
\Infer[Pair]
{ }
{\Gamma \vdash_\ct (x_1,x_2):\{(\pair {\Gamma(x_1)} {\Gamma(x_2)},\Gamma)\}}
{\Gamma \avdash\Gammap\ct (x_1,x_2):\{(\pair {\Gamma(x_1)} {\Gamma(x_2)},\Gamma)\}}
{ }
\\
\Infer[App]
......@@ -162,7 +174,7 @@ t\land\neg(\pair{\Any}{\Any})\neq\Empty\\
\Gamma(x_2)=s\\
\exists i\in I.\ s\leq s_i
}
{ \Gamma \vdash_\ct {x_1}{x_2}: \{((\textstyle\bigwedge_{i\in I}\arrow {s_i}{t_i}) \circ s,\Gamma)\} }
{ \Gamma \avdash\Gammap\ct {x_1}{x_2}: \{((\textstyle\bigwedge_{i\in I}\arrow {s_i}{t_i}) \circ s,\Gamma)\} }
{ }
\\
\Infer[AppR*]
......@@ -170,9 +182,9 @@ t\land\neg(\pair{\Any}{\Any})\neq\Empty\\
\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_{[]} \ct[{x_1}{x_2}]: \{(u_j,\Gamma_j)\}_{j\in J_i}
\forall i\in I.\ \Gamma\avdash{\Gammap\subst{x_2}{s\land s_i}}{[]} \ct[{x_1}{x_2}]: \{(u_j,\Gamma_j)\}_{j\in J_i}
}
{ \Gamma \vdash_\ct {x_1}{x_2}: \{(u_j,\Gamma_j)\,\alt\,i\in I,\ j\in J_i\} }
{ \Gamma \avdash\Gammap\ct {x_1}{x_2}: \{(u_j,\Gamma_j)\,\alt\,i\in I,\ j\in J_i\} }
{ }
\\
\Infer[AppRDom]
......@@ -180,25 +192,25 @@ t\land\neg(\pair{\Any}{\Any})\neq\Empty\\
\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\subst{x_2}{s\land s_\circ}\vdash_{[]} \ct[{x_1}{x_2}]: \{(u_i,\Gamma_i)\}_{i\in I}\\
\Gamma\subst{x_2}{s\land \neg s_\circ}\vdash_{[]} \ct[{x_1}{x_2}]: \{(u_j,\Gamma_j)\}_{j\in J}
\Gamma\avdash{\Gammap\subst{x_2}{s\land s_\circ}}{[]} \ct[{x_1}{x_2}]: \{(u_i,\Gamma_i)\}_{i\in I}\\
\Gamma\avdash{\Gammap\subst{x_2}{s\land \neg s_\circ}}{[]} \ct[{x_1}{x_2}]: \{(u_j,\Gamma_j)\}_{j\in J}
}
{ \Gamma \vdash_\ct {x_1}{x_2}: \{(u_i,\Gamma_i)\}_{i\in I}\cup\{(u_j,\Gamma_j)\}_{j\in J} }
{ \Gamma \avdash\Gammap\ct {x_1}{x_2}: \{(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}t_i\leq\arrow{\Empty}{\Any}\\
\forall i\in I.\ \Gamma\subst{x_1}{t_i}\vdash_{[]} \ct[{x_1}{x_2}]: \{(u_j,\Gamma_j)\}_{j\in J_i}
\forall i\in I.\ \Gamma\avdash{\Gammap\subst{x_1}{t_i}}{[]} \ct[{x_1}{x_2}]: \{(u_j,\Gamma_j)\}_{j\in J_i}
}
{\Gamma \vdash_\ct {x_1}{x_2}: \{(u_j,\Gamma_j)\,\alt\,i\in I,\ j\in J_i\}}
{\Gamma \avdash\Gammap\ct {x_1}{x_2}: \{(u_j,\Gamma_j)\,\alt\,i\in I,\ j\in J_i\}}
{ }
\\
\Infer[AppLDom]
{\Gamma(x_1) = t\\t\land (\arrow{\Empty}{\Any})\neq\Empty\\t\land \neg (\arrow{\Empty}{\Any})\neq\Empty\\
\Gamma\subst{x_1}{t\land(\arrow{\Empty}{\Any})}\vdash_{[]} \ct[{x_1}{x_2}]: \{(u_i,\Gamma_i)\}_{i\in I}\\
\Gamma\subst{x_1}{t\land\neg(\arrow{\Empty}{\Any})}\vdash_{[]} \ct[{x_1}{x_2}]: \{(u_j,\Gamma_j)\}_{j\in J}
\Gamma\avdash{\Gammap\subst{x_1}{t\land(\arrow{\Empty}{\Any})}}{[]} \ct[{x_1}{x_2}]: \{(u_i,\Gamma_i)\}_{i\in I}\\
\Gamma\avdash{\Gammap\subst{x_1}{t\land\neg(\arrow{\Empty}{\Any})}}{[]} \ct[{x_1}{x_2}]: \{(u_j,\Gamma_j)\}_{j\in J}
}
{\Gamma \vdash_\ct {x_1}{x_2}: \{(u_i,\Gamma_i)\}_{i\in I}\cup\{(u_j,\Gamma_j)\}_{j\in J}}
{\Gamma \avdash\Gammap\ct {x_1}{x_2}: \{(u_i,\Gamma_i)\}_{i\in I}\cup\{(u_j,\Gamma_j)\}_{j\in J}}
{ }
\end{mathpar}
......@@ -206,23 +218,23 @@ t\land\neg(\pair{\Any}{\Any})\neq\Empty\\
\Infer[CaseThen]
{
\Gamma(x)=t_\circ\\t_\circ\leq t\\
\Gamma \vdash_\ct e_1:\{(u_i,\Gamma_i)\}_{i\in I}}
{\Gamma\vdash_\ct \tcase {x} t {e_1}{e_2}: \{(u_i,\Gamma_i)\}_{i\in I}}
\Gamma \avdash\Gammap\ct e_1:\{(u_i,\Gamma_i)\}_{i\in I}}
{\Gamma\avdash\Gammap\ct \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_\ct e_2:\{(u_i,\Gamma_i)\}_{i\in I}}
{\Gamma\vdash_\ct \tcase {x} t {e_1}{e_2}: \{(u_i,\Gamma_i)\}_{i\in I}}
\Gamma \avdash\Gammap\ct e_2:\{(u_i,\Gamma_i)\}_{i\in I}}
{\Gamma\avdash\Gammap\ct \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_{[]} \ct[\tcase {x} t {e_1}{e_2}]: \{(u_i,\Gamma_i)\}_{i\in I}\\
\Gamma\subst{x}{t_\circ\land\neg t}\vdash_{[]} \ct[\tcase {x} t {e_1}{e_2}]: \{(u_j,\Gamma_j)\}_{j\in J}
\Gamma\avdash{\Gammap\subst{x}{t_\circ\land t}}{[]} \ct[\tcase {x} t {e_1}{e_2}]: \{(u_i,\Gamma_i)\}_{i\in I}\\
\Gamma\avdash{\Gammap\subst{x}{t_\circ\land\neg t}}{[]} \ct[\tcase {x} t {e_1}{e_2}]: \{(u_j,\Gamma_j)\}_{j\in J}
}
{\Gamma\vdash_\ct \tcase {x} t {e_1}{e_2}: \{(u_i,\Gamma_i)\}_{i\in I}\cup\{(u_j,\Gamma_j)\}_{j\in J}}
{\Gamma\avdash\Gammap\ct \tcase {x} t {e_1}{e_2}: \{(u_i,\Gamma_i)\}_{i\in I}\cup\{(u_j,\Gamma_j)\}_{j\in J}}
{ }
\end{mathpar}
......@@ -235,27 +247,20 @@ rules, because one branch is already unreachable and retyping only occurs with s
% {\Gamma\vdash\lambda x:s.e: t}
% { }
% \\
\Infer[Let]
{\Gamma\vdash_\ct 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_{\ct[\letexp x a {[]}]} e : \{(u_j,\Gamma_j)\}_{j\in J_i}}
{
\Gamma\vdash_\ct\letexp x a e : \{(u_j,\Gamma_j)\,\alt\,i\in I,\ j\in J_i\}
}
{ }
\\
\Infer[LetRefine]
{\Gamma\vdash_\ct a:\{(t_i,\Gamma_i)\}_{i\in I}\\
\forall i\in I.\ \Gamma_i\bvdash{a}{\Gamma(x)}\{(t_j,\Gamma_j)\}_{j\in J_i}\\
\forall i\in I.\ \forall j\in J_i.\ \Gamma_j,(x:t_j)\vdash_{[]} \ct[\letexp x a e] : \{(u_k,\Gamma_k)\}_{k\in K_j}}
{
\Gamma\vdash_\ct\letexp x a e : \{(u_k,\Gamma_k)\,\alt\,i\in I,\ j\in J_i,\ k\in K_j\}
x\in\dom\Gamma\Rightarrow t=\Gamma(x)\\x\not\in\dom\Gamma\Rightarrow t=\Any\\
x\in\dom\Gamma'\Rightarrow t'=\Gamma'(x)\\x\not\in\dom\Gamma'\Rightarrow t'=\Any\\
\Gamma\avdash\Gammap\ct a:\{(t_i,\Gamma_i)\}_{i\in I}\\
\forall i\in I.\ t_i\land t\leq t' \Rightarrow \Gamma_i\subst{x}{t_i\land t}\avdash{\Gammap}{\ct[\letexp x a {[]}]} e : S_i\\
\forall i\in I.\ t_i\land t\not\leq t' \Rightarrow\Gamma_i\land\Gamma'\bvdash{a}{t'\land t\land t_i}\{(t_j,\Gamma_j)\}_{j\in J_i}\\
\forall i\in I.\ \forall j\in J_i.\ \Gamma_i\subst{x}{t_j}\avdash{\Gammap_j}{[]} \ct[\letexp x a e] : S_j}
{
\Gamma\avdash\Gammap\ct\letexp x a e : \textstyle\bigcup S_i \cup \textstyle\bigcup\bigcup S_j
}
{ }
\end{mathpar}
TODO: Let rules: not well-founded: we have to store only
hypotheses in the left-hand-side Gamma, and "wanted" types in
another Gamma (underscript?)
TODO: Check let rule and divide it into simpler rules
TODO: Abs rules
......@@ -294,6 +294,8 @@
\newcommand{\cvdash}[0]{\vdash^{\texttt{Choices}}}
\newcommand{\ct}[0]{\mathcal{C}}
\newcommand{\Gammap}[0]{{\Gamma'}}
\newcommand{\avdash}[2]{\vdash_{#1,\ #2}}
\newcommand{\bt}[0]{\texttt{Backtrack}}
\makeatletter % allow us to mention @-commands
......
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