Outline

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 X_1, …, X_n is written X_1,...,X_n. 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 T_1,...,T_n are the value sequences V_1,...,V_n where V_1:T_1, …, V_n:T_n. 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 Nth 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*))

 From the PLanCompS Project CBS-beta issues… Suggest an improvement…