Commit 53eb81a8 authored by Mickael Laurent's avatar Mickael Laurent
Browse files

several fixes

parent a6dfd671
......@@ -163,9 +163,9 @@ The elements of $\Gamma\avdash\Gammap\ct e:S$ mean:
\\
\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
\forall i\in I.\ \Gamma\avdash{\Gammap\subst{x}{\pair{t_i}{s_i}}}{[]} \ct[\pi_j x]: S_i
}
{\Gamma \avdash\Gammap\ct \pi_i x: \textstyle\bigcup_{i\in I}S_i}
{\Gamma \avdash\Gammap\ct \pi_j x: \textstyle\bigcup_{i\in I}S_i}
{ }
\\
\Infer[ProjDom]
......@@ -260,7 +260,7 @@ rules, because one branch is already unreachable and retyping only occurs with s
\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
\forall i\in I.\ \Gamma_i,(x:t_i)\avdash\Gammap{\ct} \letexp x a e : S_i
}
{
\Gamma\avdash\Gammap\ct\letexp x a e : \textstyle\bigcup_{i\in I}S_i
......@@ -517,29 +517,29 @@ $x$ is supposed to be included into $t_x$ or $\neg t_x$.
\\
\Infer[EFQ]
{\exists x\in\dom\Gamma.\ \Gamma(x)=\Empty}
{\Gamma \avdash\Gammap\ct e : \Leaf(\Empty,\Gamma\land\Gammap)}
{\Gamma \avdash\Gammap\ct e : \Leaf(\Empty,\Gamma)}
{ }
\\
\Infer[Const]
{ }
{\Gamma\avdash\Gammap\ct c: \Leaf(\basic{c},\Gamma\land\Gammap)}
{\Gamma\avdash\Gammap\ct c: \Leaf(\basic{c},\Gamma)}
{ }
\quad
\Infer[Var]
{ }
{ \Gamma \avdash\Gammap\ct x: \Leaf(\Gamma(x),\Gamma\land\Gammap)}
{ \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\land\Gammap)}
{\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
\forall i\in I.\ \Gamma\avdash{\Gammap\subst{x}{\pair{t_i}{s_i}}}{[]} \ct[\pi_j x]: \tree_i
}
{\Gamma \avdash\Gammap\ct \pi_i x: \Node(\Gamma\land\Gammap,\{\tree_i\}_{i\in I})}
{\Gamma \avdash\Gammap\ct \pi_j x: \Node(\Gamma\land\Gammap,\{\tree_i\}_{i\in I})}
{ }
\\
\Infer[ProjDom]
......@@ -554,7 +554,7 @@ $x$ is supposed to be included into $t_x$ or $\neg t_x$.
\\
\Infer[Pair]
{ }
{\Gamma \avdash\Gammap\ct (x_1,x_2):\Leaf(\pair {\Gamma(x_1)} {\Gamma(x_2)},\Gamma\land\Gammap)}
{\Gamma \avdash\Gammap\ct (x_1,x_2):\Leaf(\pair {\Gamma(x_1)} {\Gamma(x_2)},\Gamma)}
{ }
\\
\Infer[App]
......@@ -563,7 +563,7 @@ $x$ is supposed to be included into $t_x$ or $\neg t_x$.
\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\land\Gammap) }
{ \Gamma \avdash\Gammap\ct {x_1}{x_2}: \Leaf((\textstyle\bigwedge_{i\in I}\arrow {s_i}{t_i}) \circ s, \Gamma) }
{ }
\\
\Infer[AppR*]
......@@ -635,7 +635,7 @@ rules, because one branch is already unreachable and retyping only occurs with s
{
\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\\
\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
}
{
......@@ -662,7 +662,7 @@ rules, because one branch is already unreachable and retyping only occurs with s
\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})
\Gamma\avdash\Gammap\ct\letexp x a e : \Node(\Gamma_\circ\land\Gammap, \{\tree_i\}_{i\in I})
}
{ }
\end{mathpar}
......@@ -680,6 +680,3 @@ 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