Commit 6a0f5a27 authored by Iavor S. Diatchki's avatar Iavor S. Diatchki
Browse files

fixed rule (g) of pattern semantics to avoid duplicating the evaluation of e'

parent aaf9a1d5
......@@ -1576,11 +1576,12 @@ $x_1$@ })@ $\ldots$ @(case @$v$@ of { @$p$@ -> @$x_n$@})@\\
\outlinec{\small
\begin{tabular}{@@{}cl}
(g)&@case @$v$@ of { @$K\ p_1 \ldots p_n$@ -> @$e$@; _ -> @$e'$@ }@\\
&$=$@ case @$v$@ of {@\\
&$=$@ case @$e'$@ of { @$y$@ ->@\\
&@ case @$v$@ of {@\\
&@ @$K\ x_1 \ldots x_n$@ -> case @$x_1$@ of {@\\
&@ @$p_1$@ -> @$\ldots$@ case @$x_n$@ of { @$p_n$@ -> @$e$@ ; _ -> @$e'$@ } @$\ldots$\\
&@ _ -> @$e'$@ }@\\
&@ _ -> @$e'$@ }@\\[2pt]
&@ @$p_1$@ -> @$\ldots$@ case @$x_n$@ of { @$p_n$@ -> @$e$@ ; _ -> @$y$@ } @$\ldots$\\
&@ _ -> @$y$@ }@\\
&@ _ -> @$y$@ }}@\\[2pt]
&{\rm at least one of $p_1, \ldots, p_n$ is not a variable; $x_1, \ldots, x_n$ are new variables}\\[4pt]
%\\
(h)&@case @$v$@ of { @$k$@ -> @$e$@; _ -> @$e'$@ } @$=$@ if (@$v$@==@$k$@) then @$e$@ else @$e'$ \\
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment