No matching definitions.

tur/vec-existential

stdlib/vec-existential.tur

Vec[A] as a size-hiding existential for heterogeneous collections.

Since: Phase EX2

defmacro

vec-of-sized

(vec-of-sized [sv])

wrap a SizedVec into a Vec, hiding the size index.

sva SizedVec value whose size index will be sealed

A value of type (exists [n] (SizedVec n int)) -- representable uniformly regardless of the original size index.

(vec-of-sized (SVCons 1 (SVCons 2 (SVNil))))
    ; => packed Vec; opening it recovers a length-2 SizedVec.

Since: Phase EX2-4

defmacro

open-vec

(open-vec [vec-expr n-name sv-name & body])

bind the hidden size index and the underlying SizedVec.

vec-expra Vec value (typically produced by vec-of-sized)
n-namesymbol that names the fresh abstract size index
sv-namesymbol that names the underlying SizedVec
bodyone or more body forms evaluated in the binders' scope

The value of the last body form.

(open-vec (vec-of-sized (SVCons 1 (SVNil))) n sv
    (sized-vec-len sv))   ; => 1

Since: Phase EX2-4