@@ -33,24 +33,36 @@ rule, inspired by views in ``Epigram`` [1]_, which takes account of
3333the fact that matching on a value in a dependently typed language can
3434affect what we know about the forms of other values. In its simplest
3535form, the ``with`` rule adds another argument to the function being
36−defined, e.g. we have already seen a vector filter function, defined
37−as follows:
36+defined.
37+
38+We have already seen a vector filter function. This time, we define it
39+using ``with`` as follows:
3840
3941.. code-block:: idris
4042
4143 filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
4244 filter p [] = ( _ ** [] )
4345 filter p (x :: xs) with (filter p xs)
44− | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
46+ filter p (x :: xs) | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
4547
4648Here, the ``with`` clause allows us to deconstruct the result of
47−``filter p xs``. Effectively, it adds this value as an extra argument,
48−which we place after the vertical bar.
49+``filter p xs``. The view refined argument pattern ``filter p (x ::
50+xs)`` goes beneath the ``with`` clause, followed by a vertical bar
51+``|``, followed by the deconstructed intermediate result ``( _ ** xs'
52+)``. If the view refined argument pattern is unchanged from the
53+original function argument pattern, then the left side of ``|`` is
54+extraneous and may be omitted:
55+
56+.. code-block:: idris
57+
58+ filter p (x :: xs) with (filter p xs)
59+ | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
4960
5061If the intermediate computation itself has a dependent type, then the
5162result can affect the forms of other arguments — we can learn the form
52−of one value by testing another. For example, a ``Nat`` is either even
53−or odd. If it’s even it will be the sum of two equal ``Nat``.
63+of one value by testing another. In these cases, view refined argument
64+patterns must be explicit. For example, a ``Nat`` is either even or
65+odd. If it is even it will be the sum of two equal ``Nat``.
5466Otherwise, it is the sum of two equal ``Nat`` plus one:
5567
5668.. code-block:: idris
@@ -80,14 +92,29 @@ rule:
8092 natToBin (j + j) | Even = False :: natToBin j
8193 natToBin (S (j + j)) | Odd = True :: natToBin j
8294
83−The value of the result of ``parity k`` affects the form of ``k``,
84−because the result of ``parity k`` depends on ``k``. So, as well as
85−the patterns for the result of the intermediate computation (``Even``
86−and ``odd``) right of the ``|``, we also write how the results
87−affect the other patterns left of the ``|``. Note that there is
88−a function in the patterns (``+``) and repeated occurrences of
89−``j``—this is allowed because another argument has determined the form
90−of these patterns.
95+The value of ``parity k`` affects the form of ``k``, because the
96+result of ``parity k`` depends on ``k``. So, as well as the patterns
97+for the result of the intermediate computation (``Even`` and ``Odd``)
98+right of the ``|``, we also write how the results affect the other
99+patterns left of the ``|``. That is:
100+
101+- When ``parity k`` evaluates to ``Even``, we can refine the original
102+ argument ``k`` to a refined pattern ``(j + j)`` according to
103+ ``Parity (n + n)`` from the ``Even`` constructor definition. So
104+ ``(j + j)`` replaces ``k`` on the left side of ``|``, and the
105+ ``Even`` constructor appears on the right side. The natural number
106+ ``j`` in the refined pattern can be used on the ride side of the
107+ ``=`` sign.
108+
109+- Otherwise, when ``parity k`` evaluates to ``Odd``, the original
110+ argument ``k`` is refined to ``S (j + j)`` according to ``Parity (S
111+ (n + n))`` from the ``Odd`` constructor definition, and ``Odd`` now
112+ appears on the ride side of ``|``, again with the natural number
113+ ``j`` used on the ride side of the ``=`` sign.
114+
115+Note that there is a function in the patterns (``+``) and repeated
116+occurrences of ``j`` - this is allowed because another argument has
117+determined the form of these patterns.
91118
92119We will return to this function in the next section :ref:`sect-parity` to
93120complete the definition of ``parity``.