-- Copyright 1993-1998, by the Cecil Project
-- Department of Computer Science and Engineering, University of Washington
-- See the LICENSE file for license information.

(--DOC
  A `stream' is like a collection of values, but the values are accessed
  in sequence. Streams have an implicit position within the stream of
  values, pointing between two values (or before the first value or
  after the last value), and operations on streams are relative to
  this implicit position.
--)

----------
-- stream[T] is the most general stream type.
-- It supports the read-only stream interface.
----------

(--DOC
  The basic `stream' data type supports forward reading of a stream of
  values. The `at_end' and `before_end' testers check whether the current
  position is after the last value in the stream. The `forward'
  operation advances the position past the next value in the
  stream. The `next' operation reads and returns the next value in the
  stream, advancing the position as a side-effect; the `next_N'
  operation reads and returns the next N elements of the stream. The
  `peek_next' operation reads and returns the next element of the stream
  but does not advance the position; a subsequent `next' or `peek_next'
  operation will return the same value.
--)
abstract object stream[T];

--DOCSKIP keep predicates out of manual
predicate stream_at_end[T] isa stream[T] when stream.is_at_end;
predicate stream_before_end[T] isa stream[T] when stream.before_end;
divide stream[T] into stream_at_end[T], stream_before_end[T];
--DOCENDSKIP

-- test whether current position is after last element of the stream
signature is_at_end(stream[`T]):bool;
method before_end(s@:stream[`T]):bool { s.is_at_end.not }

-- children must override either forward or next!!

-- move forward through stream, ignoring the element
-- (useful for e.g. write-only file streams)
method forward(s@:stream[`T]):void {
    forward(s, { error("at end of stream") });
}
signature forward(stream[`T], at_end:&():void):void;
implementation forward(s@:stream_before_end[`T], at_end:&():void):void {
    s.next;
    void }
implementation forward(s@:stream_at_end[`T], at_end:&():void):void {
    eval(at_end);
}

-- move forward through stream, returning element that was moved over
signature next(stream[`T], at_end:&():T):T;
implementation next(s@:stream_before_end[`T], at_end:&():T):T {
    let x:T := s.peek_next;
    s.forward;
    x }
implementation next(s@:stream_at_end[`T], at_end:&():void):void {
    eval(at_end);
}
method next(s@:stream[`T]):T {
    next(s, { error("at end of stream") }) }

method next_N(s@:stream[`T], n:int):sequence[T] {
    new_i_vector_init[T](n, &(i:int){ s.next }) }

-- get the element of the stream after the current position, but don't consume
signature peek_next(stream[`T], at_end:&():T):T;
implementation peek_next(s@:stream_at_end[`T], at_end:&():T):T { eval(at_end) }
method peek_next(s@:stream[`T]):T {
    peek_next(s, { error("at end of stream") }) }

method as_collection(s@:stream[`T]):sequence[T] {
    let c:array[T] := new_array[T]();
    loop_exit(&(done:&():none){
	c.add_last(s.next(done));
    });
    c }

-- may also want some sort of buffered exploration operation
--   (like saveExcursion)


----------
-- m_stream: a mutable stream interface.
----------

--DOC A mutable stream supports changing the value after current
--DOC position in the stream, and optionally advancing the position past
--DOC that value. A `flush' operation makes updates to stream values visible
--DOC externally, for those implementations of streams such as files that
--DOC have separate external views.

abstract object m_stream[T] isa stream[T];

--DOCSKIP keep predicates out of manual
predicate m_stream_at_end[T] isa m_stream[T], stream_at_end[T];
predicate m_stream_before_end[T] isa m_stream[T], stream_before_end[T];
--DOCENDSKIP

-- change the element of the stream right after the current position
signature set_peek_next(m_stream[`T], :T):void;
implementation set_peek_next(@:m_stream_at_end[`T], :T):void {
    error("writing off end of stream");
}

-- change the element of the stream right after the current position,
-- and advance over changed element
method set_next(s@:m_stream[`T], x:T):void {
    s.peek_next := x;
    s.forward;
}

-- by default, flushes are not needed
method flush(@:m_stream[`T]):void {}


----------
-- removable_stream allows removing an element from the stream.
----------

--DOC A `removable_stream' supports the `remove_next' operation, which
--DOC removes the next element from the stream.

abstract object removable_stream[T] isa stream[T];

--DOCSKIP
predicate removable_stream_at_end[T] isa removable_stream[T], stream_at_end[T];
predicate removable_stream_before_end[T] isa removable_stream[T],
					     stream_before_end[T];
--DOCENDSKIP

-- delete the element of the stream after the current position from the stream
-- (may need a version with a closure for the case when the stream is empty)
signature remove_next(removable_stream[`T]):void;
implementation remove_next(@:removable_stream_at_end[`T]):void {
    error("removing from the end of the stream");
}


----------
-- insertable_stream allows inserting an element into the stream
----------

--DOC An `insertable_stream' allows an item (or a collection of items)
--DOC to be inserted immediately behind the current position of the
--DOC stream, i.e., the position in the stream is right after the inserted
--DOC value(s).

abstract object insertable_stream[T] isa stream[T];

-- insert an element into the stream at the current position, advance the
-- current position to just after the inserted element
signature insert(insertable_stream[`T], :T):void;

method insert_all(s@:insertable_stream[`T], c@:ordered_collection[T]):void {
    do(c, &(e:T){ insert(s,e); });
}


----------
-- extensible_stream allows adding elements to the end of the stream.
----------

--DOC An `extensible_stream' allows an item (or a collection of items)
--DOC to be added to the end of the stream; the position of the stream is
--DOC moved to the end of the stream after the added items.

abstract object extensible_stream[T] isa stream[T];

-- append to stream, leaving current position at end of stream
signature add_last(extensible_stream[`T], x:T):void;

method add_all_last(s@:extensible_stream[`T], c@:ordered_collection[T]):void {
    do(c, &(e:T){ add_last(s,e); });
}


----------
-- reversible_stream allows moving backwards in the stream.
----------

--DOC A `reversible_stream' allows backward motion through the
--DOC stream. It supports backward-looking functions analogous to the
--DOC forward-looking operations of the generic stream. Similarly,
--DOC `m_reversible_stream' supports backwards-looking mutation operations.
abstract object reversible_stream[T] isa stream[T];

--DOCSKIP
predicate reversible_stream_at_start[T] isa reversible_stream[T]
			when reversible_stream.is_at_start;
predicate reversible_stream_after_start[T] isa reversible_stream[T]
			when reversible_stream.after_start;
divide reversible_stream[T] into reversible_stream_at_start[T],
				 reversible_stream_after_start[T];
--DOCENDSKIP

-- test whether current position is before the first element of the stream
signature is_at_start(reversible_stream[`T]):bool;
method after_start(s@:reversible_stream[`T]):bool { s.is_at_start.not }

-- children must override either backward or prev!!

-- move backward in the stream, ignoring the element
-- (useful for e.g. write-only file streams)
signature backward(reversible_stream[`T], at_start:&():void):void;
implementation backward(s@:reversible_stream_after_start[`T],
			at_start:&():void):void {
    s.prev;
    void }
implementation backward(s@:reversible_stream_at_start[`T],
			at_start:&():void):void {
    eval(at_start);
}
method backward(s@:reversible_stream[`T]):void {
    backward(s, { error("already at start of stream") });
}

-- move backward in the stream, returning the element that was moved over
signature prev(reversible_stream[`T], at_start:&():T):T;
implementation prev(s@:reversible_stream_after_start[`T], at_start:&():T):T {
    let x:T := s.peek_prev;
    s.backward;
    x }
implementation prev(s@:reversible_stream_at_start[`T], at_start:&():T):T {
    eval(at_start) }
method prev(s@:reversible_stream[`T]):T {
    prev(s, { error("already at start of stream") }) }

-- get the element of the stream before the current position, but don't move
signature peek_prev(reversible_stream[`T], at_start:&():T):T;
implementation peek_prev(@:reversible_stream_at_start[`T], at_start:&():T):T {
    eval(at_start) }
method peek_prev(s@:reversible_stream[`T]):T {
    peek_prev(s, { error("at start of stream") }) }


----------
-- m_reversible_stream supports mutable stream interface in the
-- reverse direction
----------

abstract object m_reversible_stream[T] isa reversible_stream[T], m_stream[T];

--DOCSKIP
predicate m_reversible_stream_at_start[T]
	isa m_reversible_stream[T], reversible_stream_at_start[T];
predicate m_reversible_stream_after_start[T]
	isa m_reversible_stream[T], reversible_stream_after_start[T];
--DOCENDSKIP

-- change the element of the stream just before the current position
signature set_peek_prev(m_reversible_stream[`T], :T):void;
implementation set_peek_prev(@:m_reversible_stream_at_start[`T], :T):void {
    error("writing off end of stream");
}

-- change the element of the stream just before the current position
method set_prev(s@:m_reversible_stream[`T], x:T):void {
    s.peek_prev := x;
    s.backward;
}


----------
-- positionable_stream allows arbitrary movement in the stream.
----------

--DOC A `positionable_stream' supports querying and setting the position
--DOC in the stream explicitly. The length of the stream can be determined
--DOC also. Finally, a positionable stream can be viewed as an indexed
--DOC collection using the view_indexed operation. (view_indexed may not
--DOC be implemented yet.)

abstract object positionable_stream[T] isa reversible_stream[T];

signature position(positionable_stream[`T]):int;
signature set_position(positionable_stream[`T], :int, off_end:&():void):void;
method set_position(s@:positionable_stream[`T], p:int):void {
    set_position(s, p, { error("positioning off end of stream") });
}

method forward(s@:positionable_stream[`T], at_end:&():void):void {
    set_position(s, s.position.succ, at_end);
}
method backward(s@:positionable_stream[`T], at_start:&():void):void {
    set_position(s, s.position.pred, at_start);
}

method to_start(s@:positionable_stream[`T]):void { s.position := 0; }
method to_end(s@:positionable_stream[`T]):void { s.position := s.length; }

method is_at_start(s@:positionable_stream[`T]):bool { s.position = 0 }
method is_at_end(s@:positionable_stream[`T]):bool { s.position = s.length }

signature length(positionable_stream[`T]):int;
method is_empty(s@:positionable_stream[`T]):bool { s.length = 0 }
method non_empty(s@:positionable_stream[`T]):bool { s.is_empty.not }

method view_indexed(@:positionable_stream[`T]):indexed[T] {
    error("not implemented yet")
}


----------
-- m_positionable_stream supports the mutable stream interface for a
-- positionable stream
----------

abstract object m_positionable_stream[T] isa positionable_stream[T],
					   m_reversible_stream[T];