mirror of
https://github.com/thufschmitt/tix-papers.git
synced 2024-10-05 17:17:55 +03:00
Remove \x/ syntax for meta-variables
Those are typeset in math mode anyway, so they can as well be written $x$
This commit is contained in:
regnat
parent
56365fba22
commit
914328e8ca
@ -39,22 +39,6 @@
|
||||
\renewcommand{\grammarlabel}[2]{\meta{#1 #2}}
|
||||
\newcommand{\meta}[1]{\ensuremath{#1}} % For meta syntax
|
||||
\renewcommand{\|}{\textrm{|}}
|
||||
% Define shortcuts for all meta variables
|
||||
\def\a/{\meta{a}}
|
||||
\def\b/{\meta{b}}
|
||||
\def\c/{\meta{c}}
|
||||
\def\e/{\meta{e}}
|
||||
\def\E/{\meta{E}}
|
||||
\def\f/{\meta{f}}
|
||||
\def\o/{\meta{o}}
|
||||
\def\p/{\meta{p}}
|
||||
\def\q/{\meta{q}}
|
||||
\def\r/{\meta{r}}
|
||||
\def\s/{\meta{s}}
|
||||
\def\t/{\meta{t}}
|
||||
\def\u/{\meta{u}}
|
||||
\def\v/{\meta{v}}
|
||||
\def\x/{\meta{x}}
|
||||
|
||||
\newcommand{\assign}[2]{\ensuremath{\sfrac{#2}{#1}}}
|
||||
\newcommand{\assignp} [2] {\assign{#1}{#2}}
|
||||
|
||||
@ -1,37 +1,37 @@
|
||||
\begin{grammar}
|
||||
\bfseries
|
||||
<e> ::=
|
||||
\x/ \| \c/
|
||||
\alt \e/.\a/ \| \e/.\a/ or \e/
|
||||
\alt $\λ$\p/.\e/ \| \e/ \e/
|
||||
\alt \{ \e/ = \e/ \}
|
||||
\alt with \e/; \e/
|
||||
\alt (\x/ := \e/ $\bm{\in}$ \t/) ? \e/ : \e/
|
||||
\alt let \x/ = \e/; $\cdots{}$; \x/ = \e/; in \e/
|
||||
\alt let rec \r/ = \e/; $\cdots{}$; \r/ = \e/; in \e/
|
||||
\alt \o/
|
||||
$x$ \| $c$
|
||||
\alt $e$.$a$ \| $e$.$a$ or $e$
|
||||
\alt $\λ$$p$.$e$ \| $e$ $e$
|
||||
\alt \{ $e$ = $e$ \}
|
||||
\alt with $e$; $e$
|
||||
\alt ($x$ := $e$ $\bm{\in}$ $t$) ? $e$ : $e$
|
||||
\alt let $x$ = $e$; $\cdots{}$; $x$ = $e$; in $e$
|
||||
\alt let rec $r$ = $e$; $\cdots{}$; $r$ = $e$; in $e$
|
||||
\alt $o$
|
||||
|
||||
<o> ::= attrNames(\e/) \| listToAttrs(\e/)
|
||||
\alt \e/ + \e/ \| \e/ $\orthplus$ \e/ \| \e/ \textbackslash \e/
|
||||
\alt deepSeq(\e/, \e/)
|
||||
\alt functionArgs(\e/)
|
||||
<o> ::= attrNames($e$) \| listToAttrs($e$)
|
||||
\alt $e$ + $e$ \| $e$ $\orthplus$ $e$ \| $e$ \textbackslash $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/)
|
||||
\alt Cons($e$, $e$)
|
||||
|
||||
<a> ::= \e/. $\cdots{}$ .\e/
|
||||
<a> ::= $e$. $\cdots{}$ .$e$
|
||||
|
||||
<c> ::= \meta{s} \| \meta{i} \| $\cdots{}$
|
||||
\alt nil
|
||||
\alt $\cdots{}$
|
||||
|
||||
<p> ::= \q/ \| \q/@\x/ \| \r/
|
||||
<p> ::= $q$ \| $q$@$x$ \| $r$
|
||||
|
||||
<q> ::= \{ \f/, $\cdots{}$, \f/ \} \| \{ \f/, $\cdots{}$, \f/ , \ldots{}\}
|
||||
\alt Cons(\r/, \r/) \| nil
|
||||
\alt \q/:\τ
|
||||
<q> ::= \{ $f$, $\cdots{}$, $f$ \} \| \{ $f$, $\cdots{}$, $f$ , \ldots{}\}
|
||||
\alt Cons($r$, $r$) \| nil
|
||||
\alt $q$:\τ
|
||||
|
||||
<r> ::= \x/ | \x/:\τ
|
||||
<r> ::= $x$ | $x$:\τ
|
||||
|
||||
<f> ::= \r/ \| \r/ ? \c/
|
||||
<f> ::= $r$ \| $r$ ? $c$
|
||||
|
||||
\end{grammar}
|
||||
|
||||
@ -1,21 +1,21 @@
|
||||
\begin{grammar}
|
||||
\bfseries
|
||||
<t> ::= \c/ \| \t/ $\bm{\rightarrow}$ \t/
|
||||
\alt \t/ $\bm{\vee}$ \t/ \| \t/ $\bm{\wedge}$ \t/ \| \t/ $\bm{\backslash}$ \t/
|
||||
<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/; $\cdots{}$; \s/ = \u/; _ = \u/ \}
|
||||
\alt \{ $s$ = $u$; $\cdots{}$; $s$ = $u$; _ = $u$ \}
|
||||
\alt bool \| int \| string
|
||||
|
||||
<u> ::= \t/ \| ?\t/
|
||||
<u> ::= $t$ \| ?$t$
|
||||
|
||||
<R> ::= \t/ \| \meta{R^{\bm{+}}} \| \meta{R}* \| \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
|
||||
<\τ> ::= $t$ % No polymorphism for now
|
||||
\end{grammar}
|
||||
|
||||
We write \textbf{\{ \s/ = \u/; $\cdots{}$; \s/ = \u/; \}} as
|
||||
syntactic sugar for \textbf{\{ \s/ = \u/; $\cdots{}$; \s/ = \u/; _ =
|
||||
$\undef$ \}}, and \textbf{\{ \s/ = \u/; $\cdots{}$; \s/ = \u/;.. \}}
|
||||
as syntactic sugar for \textbf{\{ \s/ = \u/; $\cdots{}$; \s/ = \u/; _
|
||||
We write \textbf{\{ $s$ = $u$; $\cdots{}$; $s$ = $u$; \}} as
|
||||
syntactic sugar for \textbf{\{ $s$ = $u$; $\cdots{}$; $s$ = $u$; _ =
|
||||
$\undef$ \}}, and \textbf{\{ $s$ = $u$; $\cdots{}$; $s$ = $u$;.. \}}
|
||||
as syntactic sugar for \textbf{\{ $s$ = $u$; $\cdots{}$; $s$ = $u$; _
|
||||
= \textmd{\emph{Any}} \}}
|
||||
|
||||
@ -2,8 +2,8 @@
|
||||
\bfseries
|
||||
|
||||
<v> ::=
|
||||
\c/
|
||||
\alt $\λ$\p/:\τ.\e/
|
||||
\alt \{ \v/ = \e/ \} $\orthplus{} \cdots{} \orthplus$ \{ \v/ = \e/ \}
|
||||
\alt Cons(\e/, \e/) \| nil
|
||||
$c$
|
||||
\alt $\λ$$p$:\τ.$e$
|
||||
\alt \{ $v$ = $e$ \} $\orthplus{} \cdots{} \orthplus$ \{ $v$ = $e$ \}
|
||||
\alt Cons($e$, $e$) \| nil
|
||||
\end{grammar}
|
||||
|
||||
@ -7,24 +7,24 @@ figure~\pref{fig:semantics:nix-light:patterns}
|
||||
|
||||
\begin{figure}
|
||||
\begin{tabular}{rl}
|
||||
\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{\{ $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}$}{if $p \neq x$}
|
||||
\dstepa{with \{ $l_1$ = $e_1$; $\cdots{}$; $l_n$ = $e_n$; \}; \e/}{
|
||||
\e/[\assign{l_1}{\eone}; $\cdots$; \assign{l_n}{\en}]
|
||||
\dstepa{with \{ $l_1$ = $e_1$; $\cdots{}$; $l_n$ = $e_n$; \}; $e$}{
|
||||
$e$[\assign{l_1}{\eone}; $\cdots$; \assign{l_n}{\en}]
|
||||
}{}
|
||||
\dstepa{raise \e/}{$\bot$}{}
|
||||
\dstepa{raise $e$}{$\bot$}{}
|
||||
\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}; $\cdots$; \assign{x_n}{\en}]
|
||||
\dstepa{let \xone{} = \eone; $\cdots{}$; \xn{} = \en; in $e$}{%
|
||||
$e$[\assign{x_1}{\eone}; $\cdots$; \assign{x_n}{\en}]
|
||||
}{}
|
||||
\dstepa{let rec $x$: $\τ$ = $e$; in $e'$}{%
|
||||
\subst{x}{\text{let $x$ = $e$; in $x$}}{$e'$}
|
||||
}{}
|
||||
\dstepa{let rec \xone: $\τ_1$ = \eone; $\cdots{}$; \xn: $\τ_n$ = \en; in \e/}{%
|
||||
\dstepa{let rec \xone: $\τ_1$ = \eone; $\cdots{}$; \xn: $\τ_n$ = \en; in $e$}{%
|
||||
\parbox[t]{10cm}{%
|
||||
(let rec $r$: \{ $x'_1$ = $\τ_1$; $\cdots$; $x'_n$ = $\τ_n$; \} = \\
|
||||
\{ $x'_1$ = \eone; $\cdots$; $x'_n$ = \en{} \}; in e)
|
||||
@ -86,10 +86,10 @@ figure~\pref{fig:semantics:nix-light:patterns}
|
||||
\bfseries
|
||||
<E> ::= [] \| \meta{E} \meta{e}
|
||||
\alt \meta{E.a} \| \meta{E.a} or \meta{e} \| \meta{v.F} \| \meta{v.F} or \meta{e}
|
||||
\alt \{ \v/ = \e/; $\cdots{}$; \v/ = \e/; \E/ = \e/; $\cdots{}$; \e/ = \e/ \}
|
||||
\alt with \E/; \e/ | if \E/ then \e/ else \e/
|
||||
\alt \{ $v$ = $e$; $\cdots{}$; $v$ = $e$; $E$ = $e$; $\cdots{}$; $e$ = $e$ \}
|
||||
\alt with $E$; $e$ | if $E$ then $e$ else $e$
|
||||
|
||||
<F> ::= \E/.\a/ \| \v/.\meta{F}
|
||||
<F> ::= $E$.$a$ \| $v$.\meta{F}
|
||||
\end{grammar}
|
||||
\caption{Reduction contexts for nix-light\label{fig:semantics:nix-light:reduction-contexts}}
|
||||
\end{figure}
|
||||
|
||||
@ -9,11 +9,11 @@
|
||||
We assume a record language, whose grammar is defined as follows:
|
||||
|
||||
\begin{grammar}
|
||||
<e> ::= \{ \e/ = \e/ ; \} \| \{\}
|
||||
\| \e/ + \e/
|
||||
\| \e/ $\orthplus{}$ \e/
|
||||
\| \e/ \textbackslash{} \e/
|
||||
\| \e/.\e/
|
||||
<e> ::= \{ $e$ = $e$ ; \} \| \{\}
|
||||
\| $e$ + $e$
|
||||
\| $e$ $\orthplus{}$ $e$
|
||||
\| $e$ \textbackslash{} $e$
|
||||
\| $e$.$e$
|
||||
\| s
|
||||
\end{grammar}
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user