158 lines
3.9 KiB
Plaintext
158 lines
3.9 KiB
Plaintext
### Sequences of values
|
|
|
|
[
|
|
Funcon length
|
|
Funcon index
|
|
Funcon is-in
|
|
Funcon first
|
|
Funcon second
|
|
Funcon third
|
|
Funcon first-n
|
|
Funcon drop-first-n
|
|
Funcon reverse
|
|
Funcon n-of
|
|
Funcon intersperse
|
|
]
|
|
|
|
/*
|
|
Sequences of two or more values are not themselves values, nor is the empty
|
|
sequence a value. However, sequences can be provided to funcons as arguments,
|
|
and returned as results. Many operations on composite values can be expressed
|
|
by extracting their components as sequences, operating on the sequences, then
|
|
forming the required composite values from the resulting sequences.
|
|
|
|
A sequence with elements `X1`, ..., `Xn` is written `X1,...,Xn`.
|
|
A sequence with a single element `X` is identified with (and written) `X`.
|
|
An empty sequence is indicated by the absence of a term.
|
|
Any sequence `X*` can be enclosed in parentheses `(X*)`, e.g.:
|
|
`( )`, `(1)`, `(1,2,3)`. Superfluous commas are ignored.
|
|
|
|
The elements of a type sequence `T1,...,Tn` are the value sequences `V1,...,Vn`
|
|
where `V1:T1`, ..., `Vn:Tn`. The only element of the empty type sequence `( )`
|
|
is the empty value sequence `( )`.
|
|
|
|
`(T)^N` is equivalent to `T,...,T` with `N` occurrences of `T`.
|
|
`(T)*` is equivalent to the union of all `(T)^N` for `N`>=0,
|
|
`(T)+` is equivalent to the union of all `(T)^N` for `N`>=1, and
|
|
`(T)?` is equivalent to `T | ( )`.
|
|
The parentheses around `T` above can be omitted when they are not needed for
|
|
disambiguation.
|
|
|
|
(Non-trivial) sequence types are not values, so not included in `types`.
|
|
*/
|
|
|
|
|
|
Meta-variables
|
|
T, T' <: values
|
|
|
|
|
|
Funcon
|
|
length(_:values*) : =>natural-numbers
|
|
/*
|
|
`length(V*)` gives the number of elements in `V*`.
|
|
*/
|
|
Rule
|
|
length( ) ~> 0
|
|
Rule
|
|
length(V:values, V*:values*) ~> natural-successor(length(V*))
|
|
|
|
|
|
Funcon
|
|
is-in(_:values, _:values*) : =>booleans
|
|
Rule
|
|
is-in(V:values ,V':values, V*:values*) ~> or(is-equal(V, V'), is-in(V, V*))
|
|
Rule
|
|
is-in(V:values, ( )) ~> false
|
|
|
|
|
|
#### Sequence indexing
|
|
|
|
Funcon
|
|
index(_:natural-numbers, _:values*) : =>values?
|
|
/*
|
|
`index(N, V*)` gives the `N`th element of `V*`, if it exists, otherwise `( )`.
|
|
*/
|
|
Rule
|
|
index(1, V:values, V*:values*) ~> V
|
|
Rule
|
|
natural-predecessor(N) ~> N'
|
|
-----------------------------------------------------------------
|
|
index(N:positive-integers, _:values, V*:values*) ~> index(N', V*)
|
|
Rule
|
|
index(0, V*:values*) ~> ( )
|
|
Rule
|
|
index(_:positive-integers, ( )) ~> ( )
|
|
|
|
|
|
/* Total indexing funcons: */
|
|
|
|
Funcon
|
|
first(_:T, _:values*) : =>T
|
|
Rule
|
|
first(V:T, V*:values*) ~> V
|
|
|
|
Funcon
|
|
second(_:values, _:T, _:values*) : =>T
|
|
Rule
|
|
second(_:values, V:T, V*:values*) ~> V
|
|
|
|
Funcon
|
|
third(_:values, _:values, _:T, _:values*) : =>T
|
|
Rule
|
|
third(_:values, _:values, V:T, V*:values*) ~> V
|
|
|
|
|
|
#### Homogeneous sequences
|
|
|
|
|
|
Funcon
|
|
first-n(_:natural-numbers, _:(T)*) : =>(T)*
|
|
Rule
|
|
first-n(0, V*:(T)*) ~> ( )
|
|
Rule
|
|
natural-predecessor(N) ~> N'
|
|
-----------------------------------------------------------------
|
|
first-n(N:positive-integers, V:T, V*:(T)*) ~> (V,first-n(N', V*))
|
|
Rule
|
|
first-n(N:positive-integers, ( )) ~> ( )
|
|
|
|
|
|
Funcon
|
|
drop-first-n(_:natural-numbers, _:(T)*) : =>(T)*
|
|
Rule
|
|
drop-first-n(0, V*:(T)*) ~> V*
|
|
Rule
|
|
natural-predecessor(N) ~> N'
|
|
-----------------------------------------------------------------------
|
|
drop-first-n(N:positive-integers, _:T, V*:(T)*) ~> drop-first-n(N', V*)
|
|
Rule
|
|
drop-first-n(N:positive-integers, ( )) ~> ( )
|
|
|
|
|
|
Funcon
|
|
reverse(_:(T)*) : =>(T)*
|
|
Rule
|
|
reverse( ) ~> ( )
|
|
Rule
|
|
reverse(V:T, V*:(T)*) ~> (reverse(V*), V)
|
|
|
|
|
|
Funcon
|
|
n-of(N:natural-numbers, V:T) : =>(T)*
|
|
Rule
|
|
n-of(0, _:T) ~> ( )
|
|
Rule
|
|
natural-predecessor(N) ~> N'
|
|
--------------------------------------------------
|
|
n-of(N:positive-integers, V:T) ~> (V, n-of(N', V))
|
|
|
|
|
|
Funcon
|
|
intersperse(_:T', _:(T)*) : =>(T, (T', T)*)?
|
|
Rule
|
|
intersperse(_:T', ( )) ~> ( )
|
|
Rule
|
|
intersperse(_:T', V) ~> V
|
|
Rule
|
|
intersperse(V':T', V1:T, V2:T, V*:(T)*) ~> (V1, V', intersperse(V', V2, V*))
|