### Giving
[ Entity given-value Funcon initialise-giving Funcon give Funcon given Funcon no-given Funcon left-to-right-map Funcon interleave-map Funcon left-to-right-repeat Funcon interleave-repeat Funcon left-to-right-filter Funcon interleave-filter Funcon fold-left Funcon fold-right ] Meta-variables T, T′ <: values T? <: values? Entity given-value(_:values?) |- _ ---> _
*/
/* `initialise-giving(X)` ensures that the entities used by the funcons for
giving are properly initialised.
*/ Funcon give(_:T, _:T=>T′) : =>T′
/* `give(X, Y)` executes `X`, possibly referring to the current `given` value,
to compute a value `V`. It then executes `Y` with `V` as the `given` value,
to compute the result.
*/
Rulegiven-value(V) |- Y ---> Y′ ------------------------------------------------ given-value(_?) |- give(V:T, Y) ---> give(V, Y′) Rule give(_:T, W:T′) ~> W
Funcon given : T=>T
/* `given` refers to the current given value.
*/
Rulegiven-value(V:values) |- given ---> V Rule given-value( ) |- given ---> fail
Funcon no-given(_:( )=>T′) : ( )=>T′
/* `no-given(X)` computes `X` without references to the current given value.
*/
Rulegiven-value( ) |- X ---> X′ ------------------------------------------------ given-value(_?) |- no-given(X) ---> no-given(X′) Rule no-given(U:T′) ~> U
#### Mapping
/* Maps on collection values can be expressed directly, e.g.,
`list(left-to-right-map(F, list-elements(L)))`.
*/ Funcon left-to-right-map(_:T=>T′, _:(T)*) : =>(T′)*
/* `left-to-right-map(F, V*)` computes `F` for each value in `V*` from left
to right, returning the sequence of resulting values.
*/
Ruleleft-to-right-map(F, V:T, V*:(T)*) ~> left-to-right(give(V, F), left-to-right-map(F, V*)) Rule left-to-right-map(_, ( )) ~> ( )
Funcon interleave-map(_:T=>T′, _:(T)*) : =>(T′)*
/* `interleave-map(F, V*)` computes `F` for each value in `V*` interleaved,
returning the sequence of resulting values.
*/
Ruleinterleave-map(F, V:T, V*:(T)*) ~> interleave(give(V, F), interleave-map(F, V*)) Rule interleave-map(_, ( )) ~> ( )
Funcon left-to-right-repeat(_:integers=>T′, _:integers, _:integers) : =>(T′)*
/* `left-to-right-repeat(F, M, N)` computes `F` for each value from `M` to `N`
sequentially, returning the sequence of resulting values.
*/
Ruleis-less-or-equal(M, N) == true ------------------------------------------------------------------------- left-to-right-repeat(F, M:integers, N:integers) ~> left-to-right(give(M, F), left-to-right-repeat(F, int-add(M, 1), N)) Rule is-less-or-equal(M, N) == false ---------------------------------------------- left-to-right-repeat(_, M:integers, N:integers) ~> ( )
Funcon interleave-repeat(_:integers=>T′, _:integers, _:integers) : =>(T′)*
/* `interleave-repeat(F, M, N)` computes `F` for each value from `M` to `N`
interleaved, returning the sequence of resulting values.
*/
Ruleis-less-or-equal(M, N) == true ------------------------------------------------------------------- interleave-repeat(F, M:integers, N:integers) ~> interleave(give(M, F), interleave-repeat(F, int-add(M, 1), N)) Rule is-less-or-equal(M, N) == false ------------------------------------------- interleave-repeat(_, M:integers, N:integers) ~> ( )
#### Filtering
/* Filters on collections of values can be expressed directly, e.g.,
`list(left-to-right-filter(P, list-elements(L)))` to filter a list `L`.
*/ Funcon left-to-right-filter(_:T=>booleans, _:(T)*) : =>(T)*
/* `left-to-right-filter(P, V*)` computes `P` for each value in `V*` from left
to right, returning the sequence of argument values for which the result is
`true`.
*/
Ruleleft-to-right-filter(P, V:T, V*:(T)*) ~> left-to-right(when-true(give(V, P), V), left-to-right-filter(P, V*)) Rule left-to-right-filter(_) ~> ( )
Funcon interleave-filter(_:T=>booleans, _:(T)*) : =>(T)*
/* `interleave-filter(P, V*)` computes `P` for each value in `V*` interleaved,
returning the sequence of argument values for which the result is `true`.
*/
Ruleinterleave-filter(P, V:T, V*:(T)*) ~> interleave(when-true(give(V, P), V), interleave-filter(P, V*)) Rule interleave-filter(_) ~> ( )
#### Folding
Funcon fold-left(_:tuples(T,T′)=>T, _:T, _:(T′)*) : =>T
/* `fold-left(F, A, V*)` reduces a sequence `V*` to a single value by folding it
from the left, using `A` as the initial accumulator value, and iteratively
updating the accumulator by giving `F` the pair of the accumulator value and
the first of the remaining arguments.
*/
Rulefold-left(_, A:T, ( )) ~> A Rule fold-left(F, A:T, V:T′, V*:(T′)*) ~> fold-left(F, give(tuple(A, V), F), V*)
Funcon fold-right(_:tuples(T,T′)=>T′, _:T′, _:(T)*) : =>T′
/* `fold-right(F, A, V*)` reduces a sequence `V*` to a single value by folding it
from the right, using `A` as the initial accumulator value, and iteratively
updating the accumulator by giving `F` the pair of the the last of the
remaining arguments and the accumulator value.
*/
Rulefold-right(_, A:T′, ( )) ~> A Rule fold-right(F, A:T′, V*:(T)*, V:T) ~> give(tuple(V, fold-right(F, A, V*)), F)
/*The given-value entity allows a computation to refer to a single previously-computed `V:values`. The given value `( )` represents the absence of a current given value.