tur/sized-handle-existential

stdlib/sized-handle-existential.tur

defmacro

pack-sized

(pack-sized [value-expr binder type-expr])

generic existential lift for phantom-indexed handles.

Parameters

value-expr		a sized-handle value to seal
binder		the existential binder vector, e.g. [n]
type-expr		the body type mentioning the binder, e.g. (SizedBuf n)

Returns

A packed value of type (exists ~binder ~type-expr).

Example

(pack-sized (sized-buf-new-zeroed 5) [n] (SizedBuf n))
    ; => packed SizedBuf; opening it recovers a fresh abstract n.

Since: Phase SZ8/P4

defmacro

(open-sized [packed-expr n-name handle-name & body])

bind the hidden size index and the underlying handle.

Parameters

packed-expr		a packed value (typically produced by pack-sized)
n-name		symbol that names the fresh abstract size index
handle-name		symbol that names the underlying sized handle
body		one or more body forms evaluated in the binders' scope

Returns

The value of the last body form.

Example

(open-sized packed n buf
    (println (sized-buf-len buf))
    (sized-buf-free buf))

Since: Phase SZ8/P4