Sequences

### 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₁`, ..., `Xn` is written `X₁,...,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 `T₁,...,Tn` are the value sequences `V₁,...,Vn`
  where `V₁:T₁`, ..., `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′, V₁:T, V₂:T, V*:(T)*) ~> (V₁, V′, intersperse(V′, V₂, V*))