ATSLIB/prelude/stream
Synopsis
typedef
stream (a:t0p) = lazy (stream_con(a))
Synopsis
datatype
stream_con
(a:t@ype+) =
| stream_nil of ()
| stream_cons of (a, stream(a))
where stream (a:t@ype) = lazy (stream_con(a))
Synopsis
exception StreamSubscriptExn of ()
Synopsis
fun{a:t0p}
stream2list
(xs: stream(INV(a))):<!laz> List0_vt(a)
Description
This function turns a given stream into a linear list.
Synopsis
fun{a:t0p}
stream_take_exn{n:nat}
(xs: stream(INV(a)), n: int n):<!laz> list_vt(a, n)
Synopsis
fun{a:t0p}
stream_drop_exn
(xs: stream(INV(a)), n: intGte(0)):<!laz> stream(a)
Synopsis
fun{a:t0p}
stream_nth_exn
(xs: stream(INV(a)), n: intGte(0)):<!laz> (a)
Description
Given a stream xs and a natural number n, this
function returns xs[n], that is, element n in xs if
xs contains at least n elements. Otherwise,
a run-time exception (StreamSubscriptExn) is raised.
Synopsis
fun{a:t0p}
stream_nth_opt
(xs: stream(INV(a)), n: intGte(0)):<!laz> Option_vt(a)
Description
This function is the optional version of stream_nth_exn.
Synopsis
fun{a:t0p}
stream_append
(xs: stream(INV(a)), ys: stream(a)):<!laz> stream(a)
Synopsis
fun{a:t0p}
stream_concat(xss: stream(stream(INV(a)))):<!laz> stream(a)
Synopsis
fun{a:t0p}
stream_filter
(xs: stream(INV(a))):<!laz> stream(a)
Synopsis
fun{a:t0p} stream_filter$pred (x: a):<> bool
Synopsis
fun{a:t0p}
stream_filter_fun
(
xs: stream(INV(a)), pred: (a) -<fun> bool
) :<!laz> stream(a)
Synopsis
fun{a:t0p}
stream_filter_cloref
(
xs: stream(INV(a)), pred: (a) -<cloref> bool
) :<!laz> stream(a)
Synopsis
fun{
a:t0p}{b:t0p
} stream_map
(xs: stream(INV(a))):<!laz> stream(b)
Synopsis
fun{
a:t0p}{b:t0p
} stream_map$fopr (x: a):<> (b)
Synopsis
fun{
a:t0p}{b:t0p
} stream_map_fun
(xs: stream(INV(a)), fopr: (a) -<fun> b):<!laz> stream(b)
Synopsis
fun{
a:t0p}{b:t0p
} stream_map_cloref
(xs: stream(INV(a)), fopr: (a) -<cloref> b):<!laz> stream(b)
Synopsis
fun{
a:t0p}{b:t0p
} stream_imap
(xs: stream(INV(a))):<!laz> stream(b)
Synopsis
fun{
a:t0p}{b:t0p
} stream_imap$fopr (i: intGte(0), x: a):<> (b)
Synopsis
fun{
a:t0p}{b:t0p
} stream_imap_fun
(
xs: stream(INV(a)), fopr: (intGte(0), a) -<fun> b
) :<!laz> stream(b)
Synopsis
fun{
a:t0p}{b:t0p
} stream_imap_cloref
(
xs: stream(INV(a)), fopr: (intGte(0), a) -<cloref> b
) :<!laz> stream(b)
Synopsis
fun{
a1,a2:t0p}{b:t0p
} stream_map2
(
xs1: stream(INV(a1))
, xs2: stream(INV(a2))
) :<!laz> stream(b)
Synopsis
fun{
a1,a2:t0p}{b:t0p
} stream_map2$fopr (x1: a1, x2: a2):<> b
Synopsis
fun{
a1,a2:t0p}{b:t0p
} stream_map2_fun
(
xs1: stream(INV(a1))
, xs2: stream(INV(a2)), fopr: (a1, a2) -<fun> b
) :<!laz> stream(b)
Synopsis
fun{
a1,a2:t0p}{b:t0p
} stream_map2_cloref
(
xs1: stream(INV(a1))
, xs2: stream(INV(a2)), fopr: (a1, a2) -<cloref> b
) :<!laz> stream(b)
Synopsis
fun
{a:t0p}
stream_merge
(
xs1: stream(INV(a)), xs2: stream(a)
) :<!laz> stream(a)
Synopsis
fun{a:t0p}
stream_merge$cmp (x1: a, x2: a):<> int
Synopsis
fun
{a:t0p}
stream_merge_fun
(
xs1: stream(INV(a))
, xs2: stream(a), cmp: (a, a) -<fun> int
) :<!laz> stream(a)
Synopsis
fun
{a:t0p}
stream_merge_cloref
(
xs1: stream(INV(a))
, xs2: stream(a), cmp: (a, a) -<cloref> int
) :<!laz> stream(a)
Synopsis
fun{a:t0p}
stream_mergeq
(
xs1: stream(INV(a)), xs2: stream(a)
) :<!laz> stream(a)
Synopsis
fun{a:t0p}
stream_mergeq$cmp(x1: a, x2: a):<> int
Synopsis
fun{a:t0p}
stream_mergeq_fun
(
xs1: stream(INV(a))
, xs2: stream(a), cmp: (a, a) -<fun> int
) :<!laz> stream(a)
Synopsis
fun{a:t0p}
stream_mergeq_cloref
(
xs1: stream(INV(a))
, xs2: stream(a), cmp: (a, a) -<cloref> int
) :<!laz> stream(a)
Synopsis
fun
{a:t0p}
stream_foreach(xs: stream(a)): void
Synopsis
fun
{a:t0p}
{env:vt0p}
stream_foreach_env(xs: stream(a), &env >> _): void
Synopsis
fun
{a:t0p}
{env:vt0p}
stream_foreach$cont(x: a, env: &env): bool
Synopsis
fun
{a:t0p}
{env:vt0p}
stream_foreach$fwork(x: a, env: &env): void