From 1b5d5748fe05720e823ce166d55f26b50aff288b Mon Sep 17 00:00:00 2001
From: regnat <rg@regnat.ovh>
Date: Mon, 24 Apr 2017 16:20:34 +0200
Subject: [PATCH] Unify the typesetting of grammar

Fixes #1
---
 grammar/expressions.tex |  4 ++--
 grammar/types.tex       |  7 ++++---
 grammar/values.tex      |  2 +-
 semantics/semantics.tex | 18 +++++++++---------
 4 files changed, 16 insertions(+), 15 deletions(-)

diff --git a/grammar/expressions.tex b/grammar/expressions.tex
index 65961cb..ae7c4e5 100644
--- a/grammar/expressions.tex
+++ b/grammar/expressions.tex
@@ -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/)
diff --git a/grammar/types.tex b/grammar/types.tex
index a243fc7..885641b 100644
--- a/grammar/types.tex
+++ b/grammar/types.tex
@@ -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}
diff --git a/grammar/values.tex b/grammar/values.tex
index 2f41a62..0270313 100644
--- a/grammar/values.tex
+++ b/grammar/values.tex
@@ -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}
diff --git a/semantics/semantics.tex b/semantics/semantics.tex
index f5bf4a3..ae0cb59 100644
--- a/semantics/semantics.tex
+++ b/semantics/semantics.tex
@@ -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/