module streams.
getcell (fcell V) V.
getcell (dcell P) V :- P V.
snil empty.
scons X P (stream X (dcell P)).
head (stream V S) V.
tail (stream V S) T :- getcell S T.
map F empty empty.
map F (stream V S) T :-
scons (F V) (X\ (sigma Y\ tail (stream V S) Y, map F Y X)) T.
% A sequence with I increment.
inc X I T :- Y is X + I, scons X (S\ inc Y I S) T.
nat S :- inc 0 1 S.
even S :- inc 0 2 S.
odd S :- inc 1 2 S.
% Fibonacci sequence.
fb X Y S :-
Z is X + Y, scons Z (T\ fb Y Z T) S.
fib X Y (stream X (fcell (stream Y (fcell T)))) :-
fb X Y T.
% The take predicate takes n first elements of a stream.
take 0 S nil.
take N S (V :: L) :-
N > 0, M is N - 1, head S V, tail S T, take M T L.
% Take two streams, merge them by taking the elements of
% both streams alternately.
merge empty S S.
merge S empty S.
merge (stream A S) (stream B T) (stream A (fcell W)) :-
tail (stream A S) S',
tail (stream B T) T',
scons B (Z\ merge S' T' Z) W.
% now prove that merge of even and odd is nat...
%
list2stream nil empty.
list2stream (X::L) (stream X (fcell S)) :-
list2stream L S.