Skip to content

GitLab

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

attempt in progress

parent 999343fa
Hide whitespace changes
Inline Side-by-side
new_system3.tex
View file @ c658912d
......@@ -126,129 +126,131 @@ The elements of $\Gamma\avdash\Gammap\ct e:t$ mean:
\end{itemize}
\begin{mathpar}
\Infer[EFQ]
{\exists x\in\dom\Gamma.\ \Gamma(x)=\Empty}
{\Gamma \avdash\Gammap\ct e : \{(\Empty,\Gamma)\}}
{ }
\qquad
\Infer[NoDef]
{ x\in\dom\Gammap\setminus\bv(e)\\
\Gamma\subst{x}{\Gamma(x)\land\Gammap(x)} \avdash{\Gammap\setminus\{x\}}{\ct} e : S}
{\Gamma \avdash\Gammap{\ct} e : S}
{ }
\\
\Infer[Const]
{ }
{\Gamma\avdash\Gammap\ct c: \{(\basic{c},\Gamma)\}}
{ }
\quad
\Infer[Var]
{ }
{ \Gamma \avdash\Gammap\ct x: \{(\Gamma(x),\Gamma)\} }
{ x\in\dom\Gamma }
\\
\Infer[Proj]
{\Gamma(x)\equiv\pair{t_1}{t_2}}
{\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\avdash{\Gammap\subst{x}{\pair{t_i}{s_i}}}{[]} \ct[\pi_i x]: \{(u_j,\Gamma_j)\}_{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\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 \avdash\Gammap\ct \pi_i x: \{(u_i,\Gamma_i)\}_{i\in I}\cup\{(u_j,\Gamma_j)\}_{j\in J}}
{ }
\\
\Infer[Pair]
{ }
{\Gamma \avdash\Gammap\ct (x_1,x_2):\{(\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}: \{((\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}]: \{(u_j,\Gamma_j)\}_{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]
{
\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}]: \{(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 \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\avdash{\Gammap\subst{x_1}{t_i}}{[]} \ct[{x_1}{x_2}]: \{(u_j,\Gamma_j)\}_{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\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 \avdash\Gammap\ct {x_1}{x_2}: \{(u_i,\Gamma_i)\}_{i\in I}\cup\{(u_j,\Gamma_j)\}_{j\in J}}
{ }
\end{mathpar}
\begin{mathpar}
\Infer[CaseThen]
{
\Gamma(x)=t_\circ\\t_\circ\leq t\\
\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 \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\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\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}}
{ }
\Infer[NoDef]
{ x\in\dom\Gammap\setminus\bv(e)\\
\Gamma\subst{x}{\Gamma(x)\land\Gammap(x)} \avdash{\Gammap\setminus\{x\}}{\ct} e : S}
{\Gamma \avdash\Gammap{\ct} e : S}
{ }
\qquad
\Infer[EFQ]
{\exists x\in\dom\Gamma.\ \Gamma(x)=\Empty}
{\Gamma \avdash\Gammap\ct e : \{(\Empty,\Gamma)\}}
{ }
\\
\Infer[Const]
{ }
{\Gamma\avdash\Gammap\ct c: \{(\basic{c},\Gamma)\}}
{ }
\quad
\Infer[Var]
{ }
{ \Gamma \avdash\Gammap\ct x: \{(\Gamma(x),\Gamma)\} }
{ x\in\dom\Gamma }
\\
\Infer[Proj]
{\Gamma(x)\equiv\pair{t_1}{t_2}}
{\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\avdash{\Gammap\subst{x}{\pair{t_i}{s_i}}}{[]} \ct[\pi_i x]: S_i
}
{\Gamma \avdash\Gammap\ct \pi_i x: \textstyle\bigcup_{i\in I}S_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]: S_1\\
\Gamma\avdash{\Gammap\subst{x}{t\land\neg(\pair{\Any}{\Any})}}{[]} \ct[\pi_i x]: S_2
}
{\Gamma \avdash\Gammap\ct \pi_i x: S_1\cup S_2}
{ }
\\
\Infer[Pair]
{ }
{\Gamma \avdash\Gammap\ct (x_1,x_2):\{(\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}: \{((\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}]: S_i
}
{ \Gamma \avdash\Gammap\ct {x_1}{x_2}: \textstyle\bigcup_{i\in I}S_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}]: S_1\\
\Gamma\avdash{\Gammap\subst{x_2}{s\land \neg s_\circ}}{[]} \ct[{x_1}{x_2}]: S_2
}
{ \Gamma \avdash\Gammap\ct {x_1}{x_2}: S_1\cup S_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}]: S_i
}
{\Gamma \avdash\Gammap\ct {x_1}{x_2}: \textstyle\bigcup_{i\in I}S_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}]: S_1\\
\Gamma\avdash{\Gammap\subst{x_1}{t\land\neg(\arrow{\Empty}{\Any})}}{[]} \ct[{x_1}{x_2}]: S_2
}
{\Gamma \avdash\Gammap\ct {x_1}{x_2}: S_1\cup S_2}
{ }
\end{mathpar}
\begin{mathpar}
\Infer[CaseThen]
{
\Gamma(x)=t_\circ\\t_\circ\leq t\\
\Gamma \avdash\Gammap\ct e_1: S}
{\Gamma\avdash\Gammap\ct \tcase {x} t {e_1}{e_2}: S}
{ }
\\
\Infer[CaseElse]
{
\Gamma(x)=t_\circ\\t_\circ\leq \neg t\\
\Gamma \avdash\Gammap\ct e_2: S}
{\Gamma\avdash\Gammap\ct \tcase {x} t {e_1}{e_2}: S}
{ }
\\
\Infer[Case*]
{\Gamma(x) = t_\circ\\
\Gamma\avdash{\Gammap\subst{x}{t_\circ\land t}}{[]} \ct[\tcase {x} t {e_1}{e_2}]: S_1\\
\Gamma\avdash{\Gammap\subst{x}{t_\circ\land\neg t}}{[]} \ct[\tcase {x} t {e_1}{e_2}]: S_2
}
{\Gamma,\avdash\Gammap\ct \tcase {x} t {e_1}{e_2}: S_1\cup S_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.
TODO: Update rules below
\begin{mathpar}
\Infer[LetFirst]
\Infer[LetFirst]
{
\Gamma\avdash\Gammap\ct a:\{(t_i,\Gamma_i)\}_{i\in I}\\
\forall i\in I.\ \Gamma_i,(x:t_i)\avdash\Gammap{\ct[\letexp x a {[]}]} e : S_i
......@@ -288,7 +290,6 @@ rules, because one branch is already unreachable and retyping only occurs with s
\Gamma'_i\setminus\{x\})\,\alt\,i\in I'\}}
{ }
\end{mathpar}
TODO: Check abs rule
TODO: The current environments returned by the typing rules are
......
setup.sty
View file @ c658912d
......@@ -299,6 +299,7 @@
\newcommand{\Gammap}[0]{{\Gamma'}}
\newcommand{\avdash}[2]{\vdash_{#1,\ #2}}
\newcommand{\bt}[0]{\texttt{Backtrack}}
\newcommand{\Gammas}[0]{\bbGamma}
\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