Commit 11ec4aef authored by Mickael Laurent's avatar Mickael Laurent
Browse files

several fixes

parent af650565
......@@ -130,7 +130,8 @@ The elements of $\Gamma\avdash\Gammap\ct e:S$ mean:
(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.
but that hasn't been propagated yet. Variables in $\Gammap$ should not refer to variables defined in $\ct$,
but only to future variables (defined in $e$ or in a bigger expression from which $e$ comes from).
\end{itemize}
\begin{mathpar}
......@@ -139,7 +140,7 @@ The elements of $\Gamma\avdash\Gammap\ct e:S$ mean:
\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)\}}
......@@ -231,14 +232,14 @@ The elements of $\Gamma\avdash\Gammap\ct e:S$ mean:
\begin{mathpar}
\Infer[CaseThen]
{
\Gamma(x)=t_\circ\\t_\circ\leq t\\
\Gamma(x)\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(x)\leq\neg t\\
\Gamma \avdash\Gammap\ct e_2: S}
{\Gamma\avdash\Gammap\ct \tcase {x} t {e_1}{e_2}: S}
{ }
......@@ -268,10 +269,10 @@ rules, because one branch is already unreachable and retyping only occurs with s
\\
\Infer[LetNoRefine]
{
\Gamma\avdash{\Gammap}\ct a:\{(t_1,\Gamma_1)\}\\
\Gamma_1'=\Gamma_1\subst{x}{\Gamma_1(x)\land t_1}\\
x\not\in\dom\Gammap\text{ or }\Gamma_1'(x)\leq \Gammap(x)\\
\Gamma_1'\avdash{\Gammap\setminus\{x\}}{\ct[\letexp x a {[]}]} e : S
\Gamma\avdash{\Gammap}\ct a:\{(t_1,\_)\}\\
\Gamma_\circ=\Gamma\subst{x}{\Gamma(x)\land t_1}\\
x\not\in\dom\Gammap\text{ or }\Gamma_\circ(x)\leq \Gammap(x)\\
\Gamma_\circ\avdash{\Gammap\setminus\{x\}}{\ct[\letexp x a {[]}]} e : S
}
{
\Gamma\avdash\Gammap\ct\letexp x a e : S
......@@ -280,10 +281,10 @@ rules, because one branch is already unreachable and retyping only occurs with s
\\
\Infer[LetRefine]
{
\Gamma\avdash{\Gammap}\ct a:\{(t_1,\Gamma_1)\}\\
\Gamma_1'=\Gamma_1\subst{x}{\Gamma_1(x)\land t_1}\\
\Gamma_1'\bvdash{a}{\Gammap(x)}\{\Gamma_i\}_{i\in I}\\
\forall i\in I.\ \Gamma_1'\subst{x}{\Gamma(x)\land\Gammap(x)}\avdash{(\Gammap\land\Gamma_i)\setminus\{x\}}{[]} \ct[\letexp x a e] : S_i}
\Gamma\avdash{\Gammap}\ct a:\{(t_1,\_)\}\\
\Gamma_\circ=\Gamma\subst{x}{\Gamma(x)\land t_1}\\
\Gamma_\circ\bvdash{a}{\Gammap(x)}\{\Gamma_i\}_{i\in I}\\
\forall i\in I.\ \Gamma_\circ\subst{x}{\Gamma_\circ(x)\land\Gammap(x)}\avdash{(\Gammap\land\Gamma_i)\setminus\{x\}}{[]} \ct[\letexp x a e] : S_i}
{
\Gamma\avdash\Gammap\ct\letexp x a e : \textstyle\bigcup_{i\in I} S_i
}
......@@ -491,17 +492,18 @@ $x$ is supposed to be included into $t_x$ or $\neg t_x$.
\Infer[Let]
{
\Gamma\fvdash{e}{t} \{\Gamma_i\}_{i\in I}\\
\forall i\in I.\ x\in\dom{\Gamma_i}\Rightarrow
\Gamma\land\Gamma_i\fvdash{a}{\Gamma_i(x)} \{\Gamma_i^j\}_{j\in J_i}\\
\forall i\in I.\ x\not\in\dom{\Gamma_i}\Rightarrow
\Gamma_\circ = \Gamma\subst{x}{\Empty}\\
I' = I\cup\{\circ\}\\
\forall i\in I'.\ x\in\dom{\Gamma_i}\Rightarrow
(\Gamma\land\Gamma_i)\setminus\{x\}\fvdash{a}{\Gamma_i(x)} \{\Gamma_i^j\}_{j\in J_i}\\
\forall i\in I'.\ x\not\in\dom{\Gamma_i}\Rightarrow
\{\Gamma_i^j\}_{j\in J_i} = \{\{\}\}
}
{
\Gamma\fvdash{\letexp{x}{a}{e}}{t} \{\Gamma_i\land\Gamma_i^j\ \alt\ i\in I,\ j\in J_i\}
\Gamma\fvdash{\letexp{x}{a}{e}}{t} \{(\Gamma_i\land\Gamma_i^j)\setminus\{x\}\ \alt\ i\in I',\ j\in J_i\}
}
{ }
\end{mathpar}
TODO: Update rule Let (current versions is incorrect)
\newpage
\subsection{Algorithmic typing rules (alternative attempt)}
......@@ -512,32 +514,32 @@ TODO: Update rule Let (current versions is incorrect)
\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)}
{\Gamma \avdash\Gammap\ct e : \Leaf(\Empty,\Gamma\land\Gammap)}
{ }
\\
\Infer[Const]
{ }
{\Gamma\avdash\Gammap\ct c: \Leaf(\basic{c},\Gamma)}
{\Gamma\avdash\Gammap\ct c: \Leaf(\basic{c},\Gamma\land\Gammap)}
{ }
\quad
\Infer[Var]
{ }
{ \Gamma \avdash\Gammap\ct x: \Leaf(\Gamma(x),\Gamma)}
{ \Gamma \avdash\Gammap\ct x: \Leaf(\Gamma(x),\Gamma\land\Gammap)}
{ 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)}
{\Gamma \avdash\Gammap\ct \pi_i x: \Leaf(t_i,\Gamma\land\Gammap)}
{ }
\\
\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})}
{\Gamma \avdash\Gammap\ct \pi_i x: \Node(\Gamma\land\Gammap,\{\tree_i\}_{i\in I})}
{ }
\\
\Infer[ProjDom]
......@@ -547,12 +549,12 @@ TODO: Update rule Let (current versions is incorrect)
\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\})}
{\Gamma \avdash\Gammap\ct \pi_i x: \Node(\Gamma\land\Gammap,\{\tree_1,\tree_2\})}
{ }
\\
\Infer[Pair]
{ }
{\Gamma \avdash\Gammap\ct (x_1,x_2):\Leaf(\pair {\Gamma(x_1)} {\Gamma(x_2)},\Gamma)}
{\Gamma \avdash\Gammap\ct (x_1,x_2):\Leaf(\pair {\Gamma(x_1)} {\Gamma(x_2)},\Gamma\land\Gammap)}
{ }
\\
\Infer[App]
......@@ -561,7 +563,7 @@ TODO: Update rule Let (current versions is incorrect)
\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) }
{ \Gamma \avdash\Gammap\ct {x_1}{x_2}: \Leaf((\textstyle\bigwedge_{i\in I}\arrow {s_i}{t_i}) \circ s, \Gamma\land\Gammap) }
{ }
\\
\Infer[AppR*]
......@@ -571,7 +573,7 @@ TODO: Update rule Let (current versions is incorrect)
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}) }
{ \Gamma \avdash\Gammap\ct {x_1}{x_2}: \Node(\Gamma\land\Gammap,\{\tree_i\}_{i\in I}) }
{ }
\\
\Infer[AppRDom]
......@@ -582,14 +584,14 @@ TODO: Update rule Let (current versions is incorrect)
\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\}) }
{ \Gamma \avdash\Gammap\ct {x_1}{x_2}: \Node(\Gamma\land\Gammap,\{\tree_1,\tree_2\}) }
{ }
\\
\Infer[AppL*]
{\Gamma(x_1)\equiv\textstyle\bigvee_{i\in I}u_i\leq\arrow{\Empty}{\Any}\\
\forall i\in I.\ \Gamma\avdash{\Gammap\subst{x_1}{u_i}}{[]} \ct[{x_1}{x_2}]: \tree_i
}
{\Gamma \avdash\Gammap\ct {x_1}{x_2}: \Node(\Gamma,\{\tree_i\}_{i\in I})}
{\Gamma \avdash\Gammap\ct {x_1}{x_2}: \Node(\Gamma\land\Gammap,\{\tree_i\}_{i\in I})}
{ }
\\
\Infer[AppLDom]
......@@ -597,21 +599,21 @@ TODO: Update rule Let (current versions is incorrect)
\Gamma\avdash{\Gammap\subst{x_1}{u\land(\arrow{\Empty}{\Any})}}{[]} \ct[{x_1}{x_2}]: \tree_1\\
\Gamma\avdash{\Gammap\subst{x_1}{u\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\})}
{\Gamma \avdash\Gammap\ct {x_1}{x_2}: \Node(\Gamma\land\Gammap,\{\tree_1,\tree_2\})}
{ }
\end{mathpar}
\begin{mathpar}
\Infer[CaseThen]
{
\Gamma(x)=t_\circ\\t_\circ\leq t\\
\Gamma(x)\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(x)\leq\neg t\\
\Gamma \avdash\Gammap\ct e_2: \tree}
{\Gamma\avdash\Gammap\ct \tcase {x} t {e_1}{e_2}: \tree}
{ }
......@@ -621,7 +623,7 @@ TODO: Update rule Let (current versions is incorrect)
\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\})}
{\Gamma,\avdash\Gammap\ct \tcase {x} t {e_1}{e_2}: \Node(\Gamma\land\Gammap,\{\tree_1,\tree_2\})}
{ }
\end{mathpar}
......@@ -643,10 +645,10 @@ rules, because one branch is already unreachable and retyping only occurs with s
\\
\Infer[LetNoRefine]
{
\Gamma\avdash{\Gammap}\ct a:\Leaf(t_1,\Gamma_1)\\
\Gamma_1'=\Gamma_1\subst{x}{\Gamma_1(x)\land t_1}\\
x\not\in\dom\Gammap\text{ or }\Gamma_1'(x)\leq \Gammap(x)\\
\Gamma_1'\avdash{\Gammap\setminus\{x\}}{\ct[\letexp x a {[]}]} e : \tree
\Gamma\avdash{\Gammap}\ct a:\Leaf(t_1,\_)\\
\Gamma_\circ=\Gamma\subst{x}{\Gamma(x)\land t_1}\\
x\not\in\dom\Gammap\text{ or }\Gamma_\circ(x)\leq \Gammap(x)\\
\Gamma_\circ\avdash{\Gammap\setminus\{x\}}{\ct[\letexp x a {[]}]} e : \tree
}
{
\Gamma\avdash\Gammap\ct\letexp x a e : \tree
......@@ -655,10 +657,10 @@ rules, because one branch is already unreachable and retyping only occurs with s
\\
\Infer[LetRefine]
{
\Gamma\avdash{\Gammap}\ct a:\Leaf(t_1,\Gamma_1)\\
\Gamma_1'=\Gamma_1\subst{x}{\Gamma_1(x)\land t_1}\\
\Gamma_1'\bvdash{a}{\Gammap(x)}\{\Gamma_i\}_{i\in I}\\
\forall i\in I.\ \Gamma_1'\subst{x}{\Gamma(x)\land\Gammap(x)}\avdash{(\Gammap\land\Gamma_i)\setminus\{x\}}{[]} \ct[\letexp x a e] : \tree_i}
\Gamma\avdash{\Gammap}\ct a:\Leaf(t_1,\_)\\
\Gamma_\circ=\Gamma\subst{x}{\Gamma(x)\land t_1}\\
\Gamma_\circ\bvdash{a}{\Gammap(x)}\{\Gamma_i\}_{i\in I}\\
\forall i\in I.\ \Gamma_\circ\subst{x}{\Gamma_\circ(x)\land\Gammap(x)}\avdash{(\Gammap\land\Gamma_i)\setminus\{x\}}{[]} \ct[\letexp x a e] : \tree_i}
{
\Gamma\avdash\Gammap\ct\letexp x a e : \Node(\Gamma_1', \{\tree_i\}_{i\in I})
}
......@@ -678,3 +680,6 @@ rules, because one branch is already unreachable and retyping only occurs with s
\end{mathpar}
TODO: Update the Abs rule. In particular, use $\fvdash{e}{t}$ to improve it.
TODO: Allow Gammap to be non-empty initially. For that, LetFirst should call recursively LetNoRefine
or LetRefine, and the environments associated to the leaves should not be itersected with Gammap.
\ No newline at end of file
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