sequence {XB : TYPE; xb : XB, max : NATURAL} : CONTEXT =
BEGIN

%% The sequence context, which models Z sequences as total SAL functions
%% from the positive natural numbers to elements, using a bottom element
%% to represent unused indices.  Sequences must be declared with a fixed 
%% max length, and use xb as the bottom element.  This context defines only
%% the additional sequence operations; other function and set operations 
%% are defined in the function context.

%% A sequence is identical to a function, whose domain type is Index, a 
%% subrange from 1..max, and whose range type is XB, which extends the type
%% X with a bottom element xb.

%% Version revised by A J H Simons on 1 September 2011.

%% Local types - do not export; for internal use within this context only.

	Size : TYPE = [0..max];
	Index : TYPE = {x : Size | x /= 0};

	X : TYPE = {x : XB | x /= xb};

	Domain : TYPE = [Index -> BOOLEAN];	%% set{Index;}!Set
	Range : TYPE = [X -> BOOLEAN];		%% set{X;}!Set

	NX : Type = [Index, X];
	Bag : TYPE = [X -> Size];
	Relation : Type = [NX -> BOOLEAN];	%% set{XN;}!Set

%% Exported type - use only if you don't want to apply operations from the
%% function context as well.  If you do, use the base type [Index -> XB].

	Sequence : TYPE = [Index -> XB];

%% Assert that a sequence is valid only if it is filled contiguously from
%% the low end. If any operation attempts to construct a sequence with 
%% greater than the max length, an *invalid* sequence is returned.  Apply
%% valid?() after each insert, append, and concat to ensure that the 
%% representation has not overflowed.

	valid? (seq : Sequence) : BOOLEAN =
		FORALL (i : Index) :
			IF seq(i) = xb
			THEN (i = max OR seq(i+1) = xb)
			ELSE (i = 1 OR seq(i-1) /= xb)
			ENDIF;

%% Sequence constructors.  An empty sequence is a function where every index
%% maps to the undefined element.  A singleton sequence is one containing
%% exactly one element, at the index 1.

	empty : Sequence = LAMBDA (n : Index) : xb;

	singleton (val : X) : Sequence =
		LAMBDA (i : Index) : 
			IF i = 1 THEN val ELSE xb ENDIF;

%% Set-like predicates on a sequence.  Containment tests for the presence of
%% elements, rather than pairs.  Use where Z tests for the presence of values
%% in the range of the sequence.  Other set-like predicates are defined in
%% the function context.

	empty? (seq : Sequence) : BOOLEAN =
		FORALL (i : Index) : seq(i) = xb;

	contains? (seq : Sequence, elem : X) : BOOLEAN = 
		EXISTS (i : Index) : seq(i) = elem;

%% Sequence-type predicates on a sequence.  These are provided for use where
%% Z declares different sequence types, and may be added to the invariant.
%% By default, sequences are partial functions, but may grow to become total.
%% The non-empty sequence type SEQ1 is translated by adding the notEmpty?()
%% predicate to the invariant.  Likewise, the injective sequence type ISEQ
%% is translated by adding injective?() to the invariant.  An injective
%% sequence maps every *valid* index to a unique value.  Other properties
%% may be asserted using the function-types in the function context.

	notEmpty? (seq : Sequence) : BOOLEAN =
		seq(1) /= xb;

	injective? (seq : Sequence) : BOOLEAN =
		FORALL (i, j : Index) : LET x : XB = seq(i) IN
			x = xb OR (x /= seq(j) OR i = j);

%% Calculate the length of a sequence.  This recursive definition seems
%% to succeed because SAL can determine an upper limit to the recursions.

	sizeAux (seq : Sequence, i : Index) : Size =
		IF seq(i) = xb THEN i-1
		ELSIF i = max THEN max
		ELSE sizeAux(seq, i+1) ENDIF;

	size? (seq : Sequence) : Size = sizeAux(seq, 1);

%% Relational operations for domain and range of a sequence.  These are 
%% replicated for convenience, but work exactly as in the function context.
%% The domain is the set of occupied indices (from 1..n).  The range is the 
%% set of elements contained in the sequence.  Other relational operations
%% such as image, inverse are defined in the function context.

	domain (seq : Sequence) : Domain =
		LAMBDA (i : Index) : seq(i) /= xb;

	range (seq : Sequence) : Range =
		LAMBDA (x : X) : EXISTS (i : Index) : seq(i) = x;

%% Concatenate two arbitrary sequences.  Note that max must always be chosen
%% to exceed (or equal) the length of the longest concatenated sequence 
%% created by this operation.  Special optimised versions insert(val, seq)
%% and append(seq, val) are given, for use where Z has concatenation with a
%% prior, or posterior singleton sequence.  If overflow occurs, the result
%% is an invalid sequence.

	concat (first, second : Sequence) : Sequence =
		LET s : Size = size? (first) IN
		IF s + size?(second) <= max
		THEN LAMBDA (i : Index) :
			IF first(i) /= xb THEN first(i)
			ELSE second(i - s) ENDIF
		ELSE LAMBDA (i : Index) :
			IF i = 1 THEN xb ELSE first(i-1) ENDIF	%% invalid
		ENDIF;

	insert (val : X, seq : Sequence) : Sequence =
		IF seq(max) = xb
		THEN LAMBDA (i : Index) :
			IF i = 1 THEN val ELSE seq(i-1) ENDIF
		ELSE LAMBDA (i : Index) :
			IF i = 1 THEN xb ELSE seq(i) ENDIF	%% invalid
		ENDIF;

	append (seq : Sequence, val : X) : Sequence =
		IF seq(max) = xb
		THEN LAMBDA (i : Index) :
			IF seq(i) = xb AND (i = 1 OR seq(i-1) /= xb) 
			THEN val
			ELSE seq(i) ENDIF
		ELSE LAMBDA (i : Index) :
			IF i = 1 THEN xb ELSE seq(i) ENDIF	%% invalid
	    	ENDIF;

%% Deconstruct a sequence at the front and back ends.  In Z, these are
%% defined over the type SEQ1, the non-empty sequence.  This must be 
%% asserted separately using nonEmpty(seq) in SAL.  These SAL versions
%% are totalised, returning unchanged or undefined values for an empty
%% sequence.

	head (seq : Sequence) : X =
		seq(1);

	tail (seq : Sequence) : Sequence =
		LAMBDA (i : Index) :
			IF i = max THEN xb 
			ELSE seq(i+1) ENDIF;

	last (seq : Sequence) : X =
		seq(size? (seq));

	front (seq : Sequence) : Sequence =
		LAMBDA (i : Index) :
			IF i = max OR seq(i+1) = xb THEN xb
			ELSE seq(i) ENDIF;

%% Reverse a sequence.  Swaps over the elements about a pivot index, which
%% is computed using the length of the sequence.

	reverse (seq : Sequence) : Sequence =
		LET s : Size = size?(seq) IN
			LAMBDA (i : Index) :
				IF i > s THEN xb
				ELSE seq(s - i + 1)
				ENDIF;

%% Squash takes an invalid sequence containing medial undefined values and
%% compacts the sequence by shifting up all defined values to the low end
%% of the sequence.  This recursive algorithm iterates max-1 times, and
%% allows undefined values to bubble up to the high end.

	squashAux (seq : Sequence, j : Index) : Sequence =
		IF j = max THEN seq ELSE
			squashAux( LAMBDA (i : Index) :
				IF seq(i) = xb AND i < max THEN seq(i+1)
				ELSIF i > 1 AND seq(i-1) = xb THEN xb
				ELSE seq(i) ENDIF,
			j + 1)
		ENDIF;

	squash (seq : Sequence) : Sequence =
		squashAux(seq, 1);

%% Extract preserves in the sequence only those elements found at the given
%% set of indices, compacting the resulting sequence.  A special optimised
%% version removeAt(seq, j) is given, for use when Z extracts every index
%% but j in the range.

	extract (set : Domain, seq : Sequence) : Sequence =
		squash( LAMBDA (i : Index) :
				IF set(i) THEN seq(i) ELSE xb ENDIF );

	removeAt (seq : Sequence, j : Index) : Sequence =
		LAMBDA (i : Index) :
			IF i = max THEN xb
			ELSIF i < j THEN seq(i)
			ELSE seq(i+1)
			ENDIF;

%% Filter preserves in the sequence only those elements found in the given
%% set of elements, compacting the resulting sequence.  Special optimised
%% versions remove(seq, val) and removeOne(seq, val) are given, for use when
%% Z filters every element but one in a set.  Whereas remove strikes out all
%% repeated occurrences of an element, removeOne is designed for use with an 
%% ISEQ and strikes out a single element, more efficiently.

	filter (seq : Sequence, set : Range) : Sequence =
		squash( LAMBDA (i : Index) :
				IF set(seq(i)) THEN seq(i) ELSE xb ENDIF );

	remove (seq : Sequence, val : X) : Sequence =
		squash( LAMBDA (i : Index) :
			IF seq(i) = val THEN xb ELSE seq(i) ENDIF );

	removeOne (seq : Sequence, val : X) : Sequence =
		LAMBDA (i : Index) :
			IF (EXISTS (j : Index) : seq(j) = val AND j <= i)
			THEN IF i = max THEN xb ELSE seq(i+1) ENDIF
			ELSE seq(i) ENDIF;

%% Prefix, suffix and infix segment relations.  The Z manual defines these
%% relations using non-constuctive equivalences with concatenation.  These
%% SAL versions are constructive and much more efficient.  If prefix? or
%% suffix? holds, then infix? also holds as the more general subsequence
%% relationship.

	prefix? (sub, seq : Sequence) : BOOLEAN = 
		FORALL (i : Index) : sub(i) /= xb => (seq(i) = sub(i));

	suffix? (sub, seq : Sequence) : BOOLEAN =
		LET d : Size = size?(seq) - size?(sub) IN
			FORALL (i : Index) : sub(i) /= xb =>
				(seq(i+d) = sub(i));

	infix? (sub, seq : Sequence) : BOOLEAN =
		EXISTS (d : Size) : FORALL (i : Index) : 
			sub(i) /= xb => (seq(i+d) = sub(i));

%% Count occurrences of each element in a sequence.  The Z manual defines
%% items(seq) to return a bag containing the elements of the sequence.  The 
%% bag maps each element to a count of occurrences of that element in the 
%% original sequence.  A special optimised count?(seq, val) is given, for
%% use where Z only needs to count one element.

	countAux (seq : Sequence, val : X, s : Size, n : NATURAL) : NATURAL =
		IF s = 0 THEN n 
		    ELSE countAux(seq, val, s-1,
			IF seq(s) = val THEN n+1 ELSE n ENDIF)
		ENDIF;

	count? (seq : Sequence, val : X) : NATURAL = 
		countAux(seq, val, size?(seq), 0);

	items (seq : Sequence) : Bag =
		LET d : Size = size?(seq) IN
			LAMBDA (x : X) : countAux(seq, x, d, 0);

END