The basic functions for the abstract data type of sequences.
List of Import References :
See BOOL
See DENOTATION
See Nat
See Option
SIGNATURE Seq [data]
$Date: 2012-02-08 21:11:24 +0100 (Mi, 08. Feb 2012) $ ($Revision: 807 $)
IMPORT Nat ONLY nat
Option[data] ONLY option
SORT data
TYPE seq == <>
::(ft:data, rt:seq)
Alternate (alphabetic) names for constructors and discriminators. Note that you can not use them in pattern-based definitions.
FUN empty: seq
FUN cons: data ** seq -> seq
FUN empty?
cons? : seq -> bool
%(e_0, ..., e_n-1) = <e_0, ..., e_n-1>
FUN % : data ->seq
% : data ** data -> seq
% : data ** data ** data -> seq
% : data ** data ** data ** data -> seq
% : data ** data ** data ** data ** data -> seq
% : data ** data ** data ** data ** data ** data -> seq
% : data ** data ** data ** data ** data ** data ** data -> seq
% : data ** data ** data ** data ** data ** data ** data ** data -> seq
Append an element to the beginning (::, cons) or to the end
(+%) of a sequence.
FUN :: : data ** seq -> seq FUN cons: data ** seq -> seq FUN +% : seq ** data -> seq
(n_1 .. n_2)(f) = <f(n1), f(n1 +1), ..., f(n2)>
FUN .. : nat ** nat -> (nat -> data) -> seq
iter(start, it, P) = <start, it(start), ... it^n(start)>,
where n+1 is the smallest number such that
~P(it^(n+1)(start)).
FUN iter : data ** (data -> data) ** (data -> bool) -> seq
Concatenate sequences.
FUN ++ : seq ** seq -> seq
Concatenate: +/+(d)(s1, s2) concatenate sequences, put
d inbetween, if both are nonempty.
FUN +/+ : data -> seq ** seq -> seq FUN +/+ : seq -> seq ** seq -> seq
Concatenate: +%+(d)(s1, s2) concatenate sequences, put
d inbetween unconditionally.
FUN +%+ : data -> seq ** seq -> seq FUN +%+ : seq -> seq ** seq -> seq
Take or drop the first k elements of a sequence. split
performs both operations simultaneously: split (n, s) = (take
(n,s), drop (n,s)). These functions adjust the index to the length of
the sequence if it is too great.
FUN take : nat ** seq -> seq FUN drop : nat ** seq -> seq FUN split : nat ** seq -> seq ** seq
Drop the last element (front) or the first
(rt). These functions abort on empty sequences.
FUN front : seq -> seq FUN rt : seq -> seq FUN revert : seq -> seq
FUN ft last : seq -> data
FUN # : seq -> nat -- length
Existence of elements fulfilling predicate: exist? checks if at least
one element of the sequence fulfills a predicate; exist1? checks if exactly one
element of the sequence fulfills a predicate.
FUN exist? : (data -> bool) ** seq -> bool FUN exist1? : (data -> bool) ** seq -> bool
Check if all elements of a sequence fulfill a predicate.
FUN forall? : (data -> bool) ** seq -> bool
Find and return an element fulfilling a predicate, if it exists.
FUN find? : (data -> bool) ** seq -> option[data]
If called with an total strict order on its elements, < is
a lexicographic total strict order on sequences. = is similar
for equality (equivalence) relations.
FUN < : (data ** data -> bool) -> (seq ** seq -> bool) FUN = : (data ** data -> bool) -> (seq ** seq -> bool)
next node: SeqCompare,
prev node: Subsystem Sequences Proper,
up to node: Subsystem Sequences Proper