4.8 Boxes

9.0

4.8Boxes🔗 i

A box is a single (im)mutable storage cell, which behaves like a one-element (im)mutable vector. Like vectors, immutable boxes are treated as transparent immutable values: they are eq? when their contents are eq? . Mutable boxes are references rather than values, so they are eq? only when they point to the same box object. Boxes can be concrete or symbolic, and they can contain both symbolic and concrete values.

Examples:

> (define v1(box 1))
> (define v2(box 1))
> (eq? v1v2)

#f
> (equal? v1v2)

#t
> (define v3(box-immutable 1))
> (define v4(box-immutable 1))
> (eq? v3v4)

#t
> (equal? v1v3)

#t

Examples:

> (define-symbolic xinteger? )
> (define-symbolic bboolean? )
> (define v1(box x));v1 is a box with symbolic contents.
> (define v2(if bv1(box 3)));v2 is a symbolic box.
> (define sol(solve (assert (= 4(unbox v2)))))
> sol

(model

[x 4]

[b #t])
> (evaluate v1sol)

'#&4
> (evaluate v2sol)

'#&4
> (evaluate (eq? v1v2)sol)

#t

Lifted box operations are shown below.

box? , box , box-immutable , unbox , set-box!

top ← prev up next →