msyds/rlp
1
0
Fork 0
Code Issues 4 Pull Requests Actions Packages Projects Releases 2 Wiki Activity

lists!

Browse Source
This commit is contained in:
crumbtoo
2023-11-24 00:29:37 -07:00
parent 5e7192fd6e
commit f1f711c9ca
3 changed files with 94 additions and 10 deletions
Download Patch File Download Diff File Expand all files Collapse all files

49
docs/src/commentary/stg.rst
View File

@@ -257,7 +257,7 @@ Evaluate the first argument if necessary
& g
}
{ p : \nillist
& (c : a_1 : a_2 : \nillist) : d
& (a_1 : a_2 : \nillist) : d
& h
& g
}
@@ -287,3 +287,50 @@ Perform the reduction if the first argument is in normal form
& g
}
Lists
-----
Evaluate the scrutinee
.. math::
\transrule
{ c : a_1 : a_2 : a_3 : \nillist
& d
& h
\begin{bmatrix}
c : \mathtt{NPrim} \; \mathtt{CaseListP} \\
a_1 : \mathtt{NAp} \; c \; x
\end{bmatrix}
& g
}
{ x
& (a_1 : a_2 : a_3) : \nillist
& h
& g
}
If the scrutinee is :code:`Nil`, perform the appropriate reduction.
.. math::
\transrule
{ c : a_1 : a_2 : a_3 : s
& d
& h
\begin{bmatrix}
c : \mathtt{NPrim} \; \mathtt{CaseListP} \\
p : \mathtt{NData} \; 1 \; \nillist \\
a_1 : \mathtt{NAp} \; c \; p \\
a_2 : \mathtt{NAp} \; p \; f_\text{nil} \\
a_3 : \mathtt{NAp} \; a_2 \; f_\text{cons}
\end{bmatrix}
& g
}
{ a_3 : s
& d
& h
\begin{bmatrix}
a_3 : \mathtt{NAp} \; f_\text{nil}
\end{bmatrix}
& g
}