Commit 09d1fdf2 authored by Mickael Laurent's avatar Mickael Laurent
Browse files

some fixes in the record part

parent eb6838d1
......@@ -47,13 +47,9 @@ e_0e_1& i.\varpi & \occ{e_i}\varpi\qquad i=0,1\\
\]
undefined otherwise
Let $e$ be an expression, $t$ a type, $\Gamma$ a type environment, $\varpi\in\{0,1\}^*$ and $p\in\{+,-\}$, we define $\typep p \varpi {\Gamma,e,t}$as follows
Let $e$ be an expression, $t$ a type, $\Gamma$ a type environment, $\varpi\in\{0,1\}^*$ and $p\in\{+,-\}$, we extend $\typep p \varpi {\Gamma,e,t}$ as follows
\[
\begin{array}{lcl}
\typep+\epsilon{\Gamma,e,t} & = & t\\
\typep-\epsilon{\Gamma,e,t} & = & \neg t\\
\typep{p}{\varpi.0}{\Gamma,e,t} & = & \arrow{\tyof{\occ e{\varpi.1}}\Gamma}{\Gp p {\Gamma,e,t} (\varpi)}\\
\typep{p}{\varpi.1}{\Gamma,e,t} & = & \worra{\tyof{\occ e{\varpi.0}}\Gamma}{\Gp p {\Gamma,e,t} (\varpi)}\\ \\
\typep{p}{\varpi.l}{\Gamma,e,t} & = & \bpl{\Gp p {\Gamma,e,t} (\varpi)}\\
\typep{p}{\varpi.r}{\Gamma,e,t} & = & \bpr{\Gp p {\Gamma,e,t} (\varpi)}\\
\typep{p}{\varpi.f}{\Gamma,e,t} & = & \pair{\Gp p {\Gamma,e,t} (\varpi)}\Any\\
......@@ -129,7 +125,7 @@ We add the following syntactic sugars:
We define the following operators on record types:
\begin{eqnarray}
\proj \ell t & = & \min \{ u \alt t\leq \orecord{\ell=u}\}\\
\proj \ell t & = & \begin{array}{ll}\min \{ u \alt t\leq \orecord{\ell=u}\} &\text{if } t \leq \orecord{\ell = \Any}\\ &\text{undefined otherwise}\end{array}\\
t_1 + t_2 & = & \min \left\{
\begin{split}
&u \alt \forall \ell \in \Labels.\\
......@@ -168,13 +164,13 @@ We can then extend $\typep p \varpi {\Gamma,e,t}$ as follows:
\[
\begin{array}{lcl}
\typep{p}{\varpi.a_\ell}{\Gamma,e,t} & = & \orecord {\ell: \Gp p {\Gamma,e,t} (\varphi)}\\
\typep{p}{\varpi.u_\ell^1}{\Gamma,e,t} & = & \Gp p {\Gamma,e,t} (\varpi) + \crecord{\ell \eqq \Any}\\
\typep{p}{\varpi.u_\ell^1}{\Gamma,e,t} & = & \recdel {(\Gp p {\Gamma,e,t} (\varpi))} \ell + \crecord{\ell \eqq \Any}\\
\typep{p}{\varpi.u_\ell^2}{\Gamma,e,t} & = & \proj \ell {(\Gp p {\Gamma,e,t} (\varpi))}\\
\typep{p}{\varpi.r_\ell}{\Gamma,e,t} & = & \Gp p {\Gamma,e,t} (\varpi) + \crecord{\ell \eqq \Any}\\ \\
\typep{p}{\varpi.r_\ell}{\Gamma,e,t} & = & \recdel {(\Gp p {\Gamma,e,t} (\varpi))} \ell + \crecord{\ell \eqq \Any}\\ \\
\Gp p {\Gamma,e,t}(\varpi) &=& \typep p \varpi{\Gamma,e,t} \wedge \tyof {\occ e\varpi}\Gamma
\end{array}
\]
Notice that the effect of doing $t + \crecord{\ell \eqq \Any}$
Notice that the effect of doing $\recdel t \ell + \crecord{\ell \eqq \Any}$
corresponds to setting the field $\ell$ of the (record) type $t$ to the type
$\Any\vee\Undef$, that is, to the type of all undefined fields in an open
record.
......@@ -192,7 +188,7 @@ Finally, we add the following typing rules:
\begin{mathpar}
\Infer[Proj]
{\Gamma \vdash e:t\and t\leq\orecord {}}
{\Gamma \vdash e:t\and t\leq\orecord{\ell = \Any}}
{\Gamma \vdash e.\ell:\proj \ell {t}}
{e.\ell\not\in\dom\Gamma}
......
......@@ -71,11 +71,11 @@ Let $e$ be an expression, $t$ a type, $\Gamma$ a type environment, $\varpi\in\{0
\begin{array}{lcl}
\typep+\epsilon{\Gamma,e,t} & = & t\\
\typep-\epsilon{\Gamma,e,t} & = & \neg t\\
\color{blue}\typep{p}{\varpi.0}{\Gamma,e,t} & = & \color{blue}\arrow{\tyof{\occ e{\varpi.1}}\Gamma}{\typep p \varpi{\Gamma,e,t}}\\
\color{red} \typep{p}{\varpi.0}{\Gamma,e,t} & = & \color{red}(\arrow{\tyof{\occ e{\varpi.1}}\Gamma}{\typep p \varpi{\Gamma,e,t}})\setminus\\
&&\color{red}(\arrow{\tyof{\occ e{\varpi.1}}\Gamma}{((\tyof{\occ e{\varpi.0}}\Gamma\circ\tyof{\occ e{\varpi.1}}\Gamma)\setminus\typep{p}{\varpi}{\Gamma,e,t})})\\
\typep{p}{\varpi.1}{\Gamma,e,t} & = & \worra{\tyof{\occ e{\varpi.0}}\Gamma}{\typep p \varpi{\Gamma,e,t}}\\ \\
\typep{p}{\varpi.0}{\Gamma,e,t} & = & \arrow{\tyof{\occ e{\varpi.1}}\Gamma}{\Gp p {\Gamma,e,t} (\varpi)}\\
\color{blue}\typep{p}{\varpi.0}{\Gamma,e,t} & = & \color{blue}\arrow{\tyof{\occ e{\varpi.1}}\Gamma}{\Gp p {\Gamma,e,t} (\varpi)}\\
\color{red} \typep{p}{\varpi.0}{\Gamma,e,t} & = & \color{red}(\arrow{\tyof{\occ e{\varpi.1}}\Gamma}{\Gp p {\Gamma,e,t} (\varpi)})\setminus\\
&&\color{red}(\arrow{\tyof{\occ e{\varpi.1}}\Gamma}{(\tyof{\occ e{\varpi}}\Gamma\setminus\Gp p {\Gamma,e,t} (\varpi))})\\
\color{purple} \typep{p}{\varpi.0}{\Gamma,e,t} & = & \color{purple}(\arrow{\tyof{\occ e{\varpi.1}}\Gamma}{\Gp p {\Gamma,e,t} (\varpi)})\setminus\\
&&\color{purple}(\arrow{\tyof{\occ e{\varpi.1}}\Gamma}{\neg \Gp p {\Gamma,e,t} (\varpi)})\\
\typep{p}{\varpi.1}{\Gamma,e,t} & = & \worra{\tyof{\occ e{\varpi.0}}\Gamma}{\Gp p {\Gamma,e,t} (\varpi)}\\ \\
\Gp p {\Gamma,e,t}(\varpi) &=& \typep p \varpi{\Gamma,e,t} \wedge \tyof {\occ e\varpi}\Gamma\\
\end{array}
......
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