[Home] [prev] [up] [next]     ((src/stream.as))

13 Infinite Lists

If random access to elements is not needed then an infinite list would be advantageous.

ToDo ⊲ 65 ⊳
rhx ⊲ 53 ⊳ 03-Oct-2006: The following code is not (yet) used.

Type Constructor

ListStream

Usage

T == Integer
s: ListStream T := stream 0;
s := stream(generator [1, 3]);
g: Generator T == generate for i in 2.. repeat yield i;
s := stream g;

Description

Implements an infinite list.

The domain ListStream can be abstractly seen as an infinite list. However, to make this data structure finite, it is more appropriate to view it as a pair (t,g) of an element of T and a Generator(T).

424⟨dom: ListStream 424⟩≡
ListStream(T: Type): with {
        ⟨exports: ListStream 426⟩
} == add {
        ⟨representation: ListStream 425⟩
        import from Rep, I, T;
        macro X == rep x;
        ⟨implementation: ListStream 427b⟩
}

Defines:
ListStream, never used.

Uses I 47.

Exports of ListStream

stream: Generator T -> %

first: % -> T

rest: % -> %

425⟨representation: ListStream 425⟩≡   (424)
Rep == Record(
    elt: T,
    next: Union(gen: Generator T, listStream: %)
);

Uses Generator 617.

Export of ListStream

stream: Generator T -> %

426⟨exports: ListStream 426⟩≡   (424)  427a ⊳
stream: Generator T -> %;

Uses Generator 617.

Export of ListStream

first: % -> T

427a⟨exports: ListStream 426⟩+≡   (424)  ⊲426  428a ⊳
first: % -> T;
427b⟨implementation: ListStream 427b⟩≡   (424)  428b ⊳
first(x: %): T == X.elt;

Export of ListStream

rest: % -> %

428a⟨exports: ListStream 426⟩+≡   (424)  ⊲427a
rest: % -> %;
428b⟨implementation: ListStream 427b⟩+≡   (424)  ⊲427b
rest(x: %): % == {
        import from Partial T;
        X.next case listStream => X.next.listStream;
        g := X.next.gen;
        e := partialNext! g;
        failed? e => x;
        per [retract e, union g];
}

Uses Partial 614.

[Home] [prev] [up] [next]     ((src/stream.as))