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

Unify the typesetting of grammar

Browse Source 
Fixes #1
This commit is contained in:
regnat 2017-04-24 16:20:34 +02:00
parent 923e4e1995
commit 1b5d5748fe
4 changed files with 16 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
grammar/expressions.tex
View File

@ -4,7 +4,7 @@
\x/ \| \c/
\alt \e/.\a/ \| \e/.\a/ or \e/
\alt \p/:\e/ \| \e/ \e/
\alt \{ \e/ = \e/; \}
\alt \{ \e/ = \e/ \}
\alt with \e/; \e/
\alt (\e/ $\bm{\in}$ \t/) ? \e/ : \e/
\alt let \x/ = \e/; $\cdots{}$; \x/ = \e/; in \e/
@ -12,7 +12,7 @@
<o> ::= attrNames(\e/) \| listToAttrs(\e/)
\alt \e/ + \e/ \| \e/ $\orthplus$ \e/ \| \e/ \textbackslash \e/
\alt deepSeq(\e/, \e/) \| seq(\e/, \e/)
\alt deepSeq(\e/, \e/)
\alt functionArgs(\e/)
% Maybe this can be typed as a function, but it is rather unlikely
\alt Cons(\e/, \e/)

7
grammar/types.tex
View File

@ -3,12 +3,13 @@
<t> ::= \c/ \| \t/ $\bm{\rightarrow}$ \t/
\alt \t/ $\bm{\vee}$ \t/ \| \t/ $\bm{\wedge}$ \t/ \| \t/ $\bm{\backslash}$ \t/
\alt [\meta{R}]
\alt \{ \s/ = \u/; \ldots{}; \s/ = \u/; _ = \u/ \}
\alt \{ \s/ = \u/; $\cdots{}$; \s/ = \u/; _ = \u/ \}
\alt bool \| int \| str
<u> ::= \t/ \| ?\t/
<R> ::= \t/ \| \meta{R^{\bm{+}}} \| \meta{R}?
\| \meta{R} $\bm{\vee}$ \meta{R} \| \meta{R} $\bm{\wedge}$ \meta{R}
<R> ::= \t/ \| \meta{R^{\bm{+}}} \| \meta{R}* \| \meta{R}?
\| \meta{R} \meta{R} \| \meta{R}\texttt{|}\meta{R}
<\τ> ::= \t/ % No polymorphism for now
\end{grammar}

2
grammar/values.tex
View File

@ -4,6 +4,6 @@
<v> ::=
\c/
\alt \p/:\e/
\alt \{ \v/ = \e/; \} $\orthplus \cdots{} \orthplus$ \{ \v/ = \e/; \}
\alt \{ \v/ = \e/ \} $\orthplus \cdots{} \orthplus$ \{ \v/ = \e/ \}
\alt Cons(\e/, \e/) \| nil
\end{grammar}

18
semantics/semantics.tex
View File

@ -7,20 +7,20 @@ 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 or e'}{e}{if $\vdash v : \{ e : \lnot\undef; .. \}$ and v(s) = e}
\dstepa{v.s or e'}{e'}{if $\vdash v : \lnot\{ e : \lnot\undef; .. \}$}
\dstepa{(x:e1) e2}{\substp{x}{e2}{e1}}{}
\dstepa{(p:e1) v} {\substp{p}{v} {e1}}{}
\dstepa{with v; e}{
e[\assign{\xone}{\eone}; ...; \assign{\xn}{\en}]
\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{$(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{raise e}{$\bot$}{}
\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{let $x$ = $e$; in $e'$}{%
@ -56,7 +56,7 @@ figure~\pref{fig:semantics:nix-light:patterns}
\begin{grammar}
\bfseries
<E> ::= [] \| \meta{E e}
\alt \meta{E.w} \| \meta{E.w} or \meta{e} \| \meta{v.F} \| \meta{v.F} or \meta{e}
\alt \meta{E.a} \| \meta{E.a} or \meta{e} \| \meta{v.F} \| \meta{v.F} or \meta{e}
\alt \{ \x/ = \e/; \ldots{}; \x/ = \e/; \E/ = \e/; \ldots{}; \e/ = \e/ \}
\alt with \E/; \e/ | if \E/ then \e/ else \e/