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

Only allow constants as default values in patterns

Browse Source 
This doesn't change the expressivity of the language, but makes the
typing easier.
This commit is contained in:
regnat 2017-04-26 17:05:24 +02:00
parent 91f34b029a
commit 686e289832
3 changed files with 6 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
grammar/expressions.tex
View File

@ -30,6 +30,6 @@
\alt Cons(\x/, \x/) \| nil
\alt \c/
<f> ::= \x/ \| \x/ ? \e/
<f> ::= \x/ \| \x/ ? \c/
\end{grammar}

3
grammar/grammar.tex
View File

@ -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.

4
semantics/semantics.tex
View File

@ -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'}}{}