diff --git a/grammar/expressions.tex b/grammar/expressions.tex index 45e5991..6bb37b5 100644 --- a/grammar/expressions.tex +++ b/grammar/expressions.tex @@ -30,6 +30,6 @@ \alt Cons(\x/, \x/) \| nil \alt \c/ - ::= \x/ \| \x/ ? \e/ + ::= \x/ \| \x/ ? \c/ \end{grammar} diff --git a/grammar/grammar.tex b/grammar/grammar.tex index 94416db..fb16856 100644 --- a/grammar/grammar.tex +++ b/grammar/grammar.tex @@ -32,6 +32,9 @@ modifications: \item Let bindings are not recursive by default anymore; a special \emph{let rec} construct is introduced equivalent to the recursive \emph{let} of Nix. + \item Default values in patterns may only be constants. This makes typing of + patterns easier, without impact on the expressivity. + \item The last notable change is that the opaque list construct of nix is replaced by the classical \texttt{nil} and \texttt{cons}. This avoids having over-complicated typing and evaluation rules for lists. diff --git a/semantics/semantics.tex b/semantics/semantics.tex index 950974e..6e6949f 100644 --- a/semantics/semantics.tex +++ b/semantics/semantics.tex @@ -42,8 +42,8 @@ figure~\pref{fig:semantics:nix-light:patterns} \begin{tabular}{rl} \eqdefa{\assignp{q@x}{e}}{\assign{x}{e}; \assignp{q}{e}}{} \eqdefa{\assignp{(\{ x \} \orthplus q)}{(\{ x = e; \} \orthplus v)}}{\assignp{x}{e}; \assignp{q}{v}}{} - \eqdefa{\assignp{(\{ x ? e' \} \orthplus q)}{(\{ x = e; \} \orthplus v)}}{\assignp{x}{e}; \assignp{q}{v}}{} - \eqdefa{\assignp{(\{ x ? e \} \orthplus q)}{(v_1 \orthplus v_2)}}{\assignp{x}{e}; \assignp{q}{\left( v_1 \orthplus v_2\right)}}{if $v_1 \neq \{ x = e'; \}$} + \eqdefa{\assignp{(\{ x ? c' \} \orthplus q)}{(\{ x = e; \} \orthplus v)}}{\assignp{x}{e}; \assignp{q}{v}}{} + \eqdefa{\assignp{(\{ x ? c \} \orthplus q)}{(v_1 \orthplus v_2)}}{\assignp{x}{c}; \assignp{q}{\left( v_1 \orthplus v_2\right)}}{if $v_1 \neq \{ x = e'; \}$} \eqdefa{\assignp{\{\}}{\{ \}}}{ø}{} \eqdefa{\assignp{\{ .. \}}{v}}{ø}{} \eqdefa{\assignp{Cons(x, x')}{Cons(e, e')}}{\assign{x}{e}; \assign{x'}{e'}}{}