thufschmitt/tix-papers
1
1
Fork 0
mirror of https://github.com/thufschmitt/tix-papers.git synced 2024-08-16 16:20:47 +03:00
Code Issues Projects Releases Wiki Activity

Remove typing judgements from semantics

Browse Source 
Fixes #3
This commit is contained in:
regnat 2017-04-24 16:49:34 +02:00
parent e9d61da64c
commit 8c933d3cb0
1 changed files with 7 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
semantics/semantics.tex
View File

@ -7,19 +7,14 @@ figure~\pref{fig:semantics:nix-light:patterns}
\begin{figure}
\begin{tabular}{rl}
\dstepa{$v.s$}{$e$}{if $\vdash v : \{ e : \lnot\undef; .. \}$ and v(s) = e}
\dstepa{$v.s \text{ or } e'$}{$e$}{if $\vdash v : \{ e : \lnot\undef; .. \}$ and v(s) = e}
\dstepa{$v.s \text{ or } e'$}{$e'$}{if $\vdash v : \lnot\{ e : \lnot\undef; .. \}$}
\dstepa{\{ \s/ = \e/; $\ldots{}$\}.\s/}{$e$}{}
\dstepa{\{ \s/ = \e/; $\ldots{}$\}.\s/ or $e'$}{$e$}{}
\dstepa{$v.s \text{ or } e'$}{$e'$}{if $\v/ \neq$ \{ \s/ = \e/; $\ldots{}$ \}}
\dstepa{$(x:e_1) e_2$}{$\substp{x}{e_2}{e_1}$}{}
\dstepa{$(p:e_1) v$} {$\substp{p}{v}{e_1}$}{}
\dstepa{with \v/ ; \e/}{
\e/[\assign{\xone}{\eone}; ...; \assign{\xn}{\en}]
}{
\parbox[t]{10cm}{
if $\vdash v : \{ \xone : \lnot\undef; .. ; \xn : \not\undef; \}$ \\
and $\forall i \in \discrete{1}{n}, v(x_i) = e_i$
}
}
\dstepa{$(p:e_1) v$} {$\substp{p}{v}{e_1}$}{if $p \neq x$}
\dstepa{with \{ $l_1$ = $e_1$; $\cdots{}$; $l_n$ = $e_n$; \} ; \e/}{
\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\τ$}