mirror of
https://github.com/thufschmitt/tix-papers.git
synced 2024-08-16 16:20:47 +03:00
Add variable substitution in typecases
This allows to explicit how to do occurence typing Fixes #6
This commit is contained in:
parent
b2c8475bde
commit
ef5b2c837d
@ -6,7 +6,7 @@
|
||||
\alt \p/:\e/ \| \e/ \e/
|
||||
\alt \{ \e/ = \e/ \}
|
||||
\alt with \e/; \e/
|
||||
\alt (\e/ $\bm{\in}$ \t/) ? \e/ : \e/
|
||||
\alt (\x/ := \e/ $\bm{\in}$ \t/) ? \e/ : \e/
|
||||
\alt let \x/ = \e/; $\cdots{}$; \x/ = \e/; in \e/
|
||||
\alt let rec \x/ = \e/; $\cdots{}$; \x/ = \e/; in \e/
|
||||
\alt \o/
|
||||
|
@ -16,8 +16,8 @@ figure~\pref{fig:semantics:nix-light:patterns}
|
||||
\e/[\assign{l_1}{\eone}; ...; \assign{l_n}{\en}]
|
||||
}{}
|
||||
\dstepa{raise \e/}{$\bot$}{}
|
||||
\dstepa{($v \in \τ$ ? \eone : $e_2$)}{\eone}{if $\vdash v : \τ$}
|
||||
\dstepa{($v \in \τ$ ? \eone : $e_2$)}{$e_2$}{if $\vdash v : \lnot\τ$}
|
||||
\dstepa{($x := v \in \τ$ ? \eone : $e_2$)}{\subst{x}{v}{\eone}}{if $\vdash v : \τ$}
|
||||
\dstepa{($x := v \in \τ$ ? \eone : $e_2$)}{\subst{x}{v}{$e_2$}}{if $\vdash v : \lnot\τ$}
|
||||
\dstepa{let \xone = \eone; $\cdots{}$; \xn = \en; in \e/}{%
|
||||
\e/[\assign{x_1}{\eone}; ...; \assign{x_n}{\en}]
|
||||
}{}
|
||||
|
@ -28,13 +28,10 @@
|
||||
\and
|
||||
\inferrule{%
|
||||
\Gamma \vdash e : \tau \\
|
||||
% TODO: fix display of cases here
|
||||
\begin{cases}
|
||||
\tau \not\subtype \lnot t \Rightarrow \Gamma \vdash e_1 : \sigma_1 &
|
||||
\tau \not\subtype t \Rightarrow \Gamma \vdash e_2 : \sigma_2
|
||||
\end{cases}
|
||||
\Γ; x : \τ \wedge t \vdash e_1 : \sigma_1 \\
|
||||
\Γ; x : \τ \wedge \lnot t \vdash e_2 : \sigma_2
|
||||
}{%
|
||||
\Gamma \vdash ((e \in t) ? e_1 : e_2) : \sigma_1 \vee \sigma_2
|
||||
\Gamma \vdash ((x := e \in t) ? e_1 : e_2) : \sigma_1 \vee \sigma_2
|
||||
}
|
||||
(Tcase)
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user