入力ストリームは、readメソッドに与えられたバッファに要素を格納可能な型です。 実行時には、次のような特徴を満たさなければいけません。
+ stream.emptyは、そのストリームからノンブロッキングで一要素でも取り出せる場合にはfalseとなる。 + stream.frontは、そのストリームからノンブロッキングで一要素取り出す。 + stream.popFrontは、そのストリームをノンブロッキングでひとつ進める。 + stream.lengthが有効である場合、この値はノンブロッキングで読み出すことができる要素数となる。 + stream.read(buf)は、ノンブロッキングで処理しなければいけない。 + stream.read(buf)は、bufのうち先頭から読み込みに成功した要素数だけのスライスを返す。 - stream.length >= buf.lengthのとき、常に、buf.length == stream.read(buf).lengthとなる。 //+ stream.closedは、いくら待ってもそれ以上要素が取り出せない状況でtrueとなる。 // - stream.closedが真の場合、stream.emptyであり、lenghtが有効であればstream.length == 0を満たす。 + stream.fetch()は、stream.emptyが偽になるまで、 もしくはそのストリームからは今後一切データを取り出せないと判断した時点で処理を返す。 stream.fetch()は、待機後のstream.empty()を返す。 + streamが無限レンジの場合、stream.read(buf)は常にbufの全要素に読み込む。
See Implementation
入力ストリームは、readメソッドに与えられたバッファに要素を格納可能な型です。 実行時には、次のような特徴を満たさなければいけません。
+ stream.emptyは、そのストリームからノンブロッキングで一要素でも取り出せる場合にはfalseとなる。 + stream.frontは、そのストリームからノンブロッキングで一要素取り出す。 + stream.popFrontは、そのストリームをノンブロッキングでひとつ進める。 + stream.lengthが有効である場合、この値はノンブロッキングで読み出すことができる要素数となる。 + stream.read(buf)は、ノンブロッキングで処理しなければいけない。 + stream.read(buf)は、bufのうち先頭から読み込みに成功した要素数だけのスライスを返す。 - stream.length >= buf.lengthのとき、常に、buf.length == stream.read(buf).lengthとなる。 //+ stream.closedは、いくら待ってもそれ以上要素が取り出せない状況でtrueとなる。 // - stream.closedが真の場合、stream.emptyであり、lenghtが有効であればstream.length == 0を満たす。 + stream.fetch()は、stream.emptyが偽になるまで、 もしくはそのストリームからは今後一切データを取り出せないと判断した時点で処理を返す。 stream.fetch()は、待機後のstream.empty()を返す。 + streamが無限レンジの場合、stream.read(buf)は常にbufの全要素に読み込む。