Commit 7e11b6a6 authored by Mickael Laurent's avatar Mickael Laurent
Browse files

rewrite algorithmic type system with contexts (a lot simpler)

parent b1d8f3df
......@@ -116,49 +116,49 @@ TODO: Theorems and proof: no need for rule Inter, etc.
\begin{mathpar}
\Infer[EFQ]
{\exists x\in\dom\Gamma.\ \Gamma(x)=\Empty}
{\Gamma \vdash_e e' : \{(\Empty,\Gamma)\}}
{\Gamma \vdash_\ct 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}}
{ }
\\
% \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}}
% { }
% \\
\Infer[Const]
{ }
{\Gamma\vdash_e c: \{(\basic{c},\Gamma)\}}
{\Gamma\vdash_\ct c: \{(\basic{c},\Gamma)\}}
{ }
\quad
\Infer[Var]
{ }
{ \Gamma \vdash_e x: \{(\Gamma(x),\Gamma)\} }
{ \Gamma \vdash_\ct x: \{(\Gamma(x),\Gamma)\} }
{ x\in\dom\Gamma }
\\
\Infer[Proj]
{\Gamma(x)\equiv\pair{t_1}{t_2}}
{\Gamma \vdash_e \pi_i x: \{(t_i,\Gamma)\}}
{\Gamma \vdash_\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_e e: \{(u_j,\Gamma_j)\}_{j\in J_i}
\forall i\in I.\ \Gamma\subst{x}{\pair{t_i}{s_i}}\vdash_\ct \ct[\pi_i x]: \{(u_j,\Gamma_j)\}_{j\in J_i}
}
{\Gamma \vdash_e \pi_i x: \bt\{(u_j,\Gamma_j)\,\alt\,i\in I,\ j\in J_i\}}
{\Gamma \vdash_\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_e e: \{(u_i,\Gamma_i)\}_{i\in I}\\
\Gamma\subst{x}{t\land\neg(\pair{\Any}{\Any})}\vdash_e e: \{(u_j,\Gamma_j)\}_{j\in J}
\Gamma\subst{x}{t\land(\pair{\Any}{\Any})}\vdash_\ct \ct[\pi_i x]: \{(u_i,\Gamma_i)\}_{i\in I}\\
\Gamma\subst{x}{t\land\neg(\pair{\Any}{\Any})}\vdash_\ct \ct[\pi_i x]: \{(u_j,\Gamma_j)\}_{j\in J}
}
{\Gamma \vdash_e \pi_i x: \bt\{(u_i,\Gamma_i)\}_{i\in I}\cup\{(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}}
{ }
\\
\Infer[Pair]
{ }
{\Gamma \vdash_e (x_1,x_2):\{(\pair {\Gamma(x_1)} {\Gamma(x_2)},\Gamma)\}}
{\Gamma \vdash_\ct (x_1,x_2):\{(\pair {\Gamma(x_1)} {\Gamma(x_2)},\Gamma)\}}
{ }
\\
\Infer[App]
......@@ -167,7 +167,7 @@ t\land\neg(\pair{\Any}{\Any})\neq\Empty\\
\Gamma(x_2)=s\\
\exists i\in I.\ s\leq s_i
}
{ \Gamma \vdash_e {x_1}{x_2}: \{((\textstyle\bigwedge_{i\in I}\arrow {s_i}{t_i}) \circ s,\Gamma)\} }
{ \Gamma \vdash_\ct {x_1}{x_2}: \{((\textstyle\bigwedge_{i\in I}\arrow {s_i}{t_i}) \circ s,\Gamma)\} }
{ }
\\
\Infer[AppR*]
......@@ -175,9 +175,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_e e: \{(u_j,\Gamma_j)\}_{j\in J_i}
\forall i\in I.\ \Gamma\subst{x_2}{s\land s_i}\vdash_\ct \ct[{x_1}{x_2}]: \{(u_j,\Gamma_j)\}_{j\in J_i}
}
{ \Gamma \vdash_e {x_1}{x_2}: \bt\{(u_j,\Gamma_j)\,\alt\,i\in I,\ j\in J_i\} }
{ \Gamma \vdash_\ct {x_1}{x_2}: \{(u_j,\Gamma_j)\,\alt\,i\in I,\ j\in J_i\} }
{ }
\\
\Infer[AppRDom]
......@@ -185,25 +185,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_e e: \{(u_i,\Gamma_i)\}_{i\in I}\\
\Gamma\subst{x_2}{s\land \neg s_\circ}\vdash_e e: \{(u_j,\Gamma_j)\}_{j\in J}
\Gamma\subst{x_2}{s\land s_\circ}\vdash_\ct \ct[{x_1}{x_2}]: \{(u_i,\Gamma_i)\}_{i\in I}\\
\Gamma\subst{x_2}{s\land \neg s_\circ}\vdash_\ct \ct[{x_1}{x_2}]: \{(u_j,\Gamma_j)\}_{j\in J}
}
{ \Gamma \vdash_e {x_1}{x_2}: \bt\{(u_i,\Gamma_i)\}_{i\in I}\cup\{(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} }
{ }
\\
\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_e e: \{(u_j,\Gamma_j)\}_{j\in J_i}
\forall i\in I.\ \Gamma\subst{x_1}{t_i}\vdash_\ct \ct[{x_1}{x_2}]: \{(u_j,\Gamma_j)\}_{j\in J_i}
}
{\Gamma \vdash_e {x_1}{x_2}: \bt\{(u_j,\Gamma_j)\,\alt\,i\in I,\ j\in J_i\}}
{\Gamma \vdash_\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_e e: \{(u_i,\Gamma_i)\}_{i\in I}\\
\Gamma\subst{x_1}{t\land\neg(\arrow{\Empty}{\Any})}\vdash_e e: \{(u_j,\Gamma_j)\}_{j\in J}
\Gamma\subst{x_1}{t\land(\arrow{\Empty}{\Any})}\vdash_\ct \ct[{x_1}{x_2}]: \{(u_i,\Gamma_i)\}_{i\in I}\\
\Gamma\subst{x_1}{t\land\neg(\arrow{\Empty}{\Any})}\vdash_\ct \ct[{x_1}{x_2}]: \{(u_j,\Gamma_j)\}_{j\in J}
}
{\Gamma \vdash_e {x_1}{x_2}: \bt\{(u_i,\Gamma_i)\}_{i\in I}\cup\{(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}}
{ }
\end{mathpar}
......@@ -211,59 +211,52 @@ t\land\neg(\pair{\Any}{\Any})\neq\Empty\\
\Infer[CaseThen]
{
\Gamma(x)=t_\circ\\t_\circ\leq t\\
\Gamma \vdash_e e_1:\{(u_i,\Gamma_i)\}_{i\in I}}
{\Gamma\vdash \tcase {x} t {e_1}{e_2}: \{(u_i,\Gamma_i)\}_{i\in I}}
\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}}
{ }
\\
\Infer[CaseElse]
{
\Gamma(x)=t_\circ\\t_\circ\leq \neg t\\
\Gamma \vdash_e e_2:\{(u_i,\Gamma_i)\}_{i\in I}}
{\Gamma\vdash \tcase {x} t {e_1}{e_2}: \{(u_i,\Gamma_i)\}_{i\in I}}
\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}}
{ }
\\
\Infer[Case*]
{\Gamma(x) = t_\circ\\
\Gamma\subst{x}{t_\circ\land t}\vdash_e e: \{(u_i,\Gamma_i)\}_{i\in I}\\
\Gamma\subst{x}{t_\circ\land\neg t}\vdash_e e: \{(u_j,\Gamma_j)\}_{j\in J}
\Gamma\subst{x}{t_\circ\land t}\vdash_\ct \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 \ct[\tcase {x} t {e_1}{e_2}]: \{(u_j,\Gamma_j)\}_{j\in J}
}
{\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}}
{\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}}
{ }
\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[Abs]
% {\Gamma,(x:s)\vdash e:t}
% {\Gamma\vdash\lambda x:s.e: t}
% { }
% \\
\Infer[Let]
{\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_e\letexp x a e' : \{(u_j,\Gamma_j)\,\alt\,i\in I,\ j\in J_i\}
}
{ }
\\
\Infer[LetRefine]
{\Gamma\vdash_e a:\{(t_i,\Gamma_i)\}_{i\in I}\\
\Gamma\bvdash{a}{\Gamma(x)}\{(t_j,\Gamma_j)\}_{j\in J}\\
\forall j\in J.\ \Gamma_j,(x:t_j)\vdash_e e : \{(u_k,\Gamma_k)\}_{k\in K_j}}
{
\Gamma\vdash_e\letexp x a e' : \bt\{(u_k,\Gamma_k)\,\alt\,j\in J,\ k\in K_j\}
}
{ }
% \Infer[Let]
% {\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_e\letexp x a e' : \{(u_j,\Gamma_j)\,\alt\,i\in I,\ j\in J_i\}
% }
% { }
% \\
% \Infer[LetRefine]
% {\Gamma\vdash_e a:\{(t_i,\Gamma_i)\}_{i\in I}\\
% \Gamma\bvdash{a}{\Gamma(x)}\{(t_j,\Gamma_j)\}_{j\in J}\\
% \forall j\in J.\ \Gamma_j,(x:t_j)\vdash_e e : \{(u_k,\Gamma_k)\}_{k\in K_j}}
% {
% \Gamma\vdash_e\letexp x a e' : \bt\{(u_k,\Gamma_k)\,\alt\,j\in J,\ k\in K_j\}
% }
% { }
\end{mathpar}
TODO: Case rules with Backtrack in hypotheses
TODO: Let rules with Backtrack in hypotheses
TODO: Abs rules (problem??? the different splits for x
cannot be cannot be retrieved...\\
solution 1: instead
of storing the whole expression e, only store what has already been
typed so that we can retype up to the current expr.\\
solution 2: rules take ALL the splits as argument
(it handles all the branches), but more complex...)
TODO: Abs and Let rules
......@@ -293,6 +293,7 @@
\newcommand{\ubvdash}[3]{\vdash^{{#1},\texttt{ Env}\leftarrow}_{#2,#3}}
\newcommand{\cvdash}[0]{\vdash^{\texttt{Choices}}}
\newcommand{\ct}[0]{\mathcal{C}}
\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