{"size": 1634, "ext": "scrbl", "max_stars_repo_path": "rosette/guide/scribble/datatypes/boxes.scrbl", "max_stars_repo_name": "remysucre/rosette", "max_stars_repo_stars_event_min_datetime": null, "max_stars_repo_stars_event_max_datetime": null, "max_issues_repo_path": "rosette/guide/scribble/datatypes/boxes.scrbl", "max_issues_repo_name": "remysucre/rosette", "max_issues_repo_issues_event_min_datetime": null, "max_issues_repo_issues_event_max_datetime": null, "max_forks_repo_path": "rosette/guide/scribble/datatypes/boxes.scrbl", "max_forks_repo_name": "remysucre/rosette", "max_forks_repo_forks_event_min_datetime": "2016-01-27T20:39:05.000Z", "max_forks_repo_forks_event_max_datetime": "2016-01-27T20:39:05.000Z"}
{"max_stars_count": null, "max_issues_count": null, "max_forks_count": 1, "avg_line_length": 36.3111111111, "max_line_length": 126, "alphanum_fraction": 0.7013463892}
#lang scribble/manual

@(require (for-label rosette/base/form/define racket)
          scribble/core scribble/html-properties scribble/eval racket/sandbox racket/runtime-path
          "../util/lifted.rkt")

@(define box-ops (select '(box? box box-immutable unbox set-box! box-cas!)))

@(define-runtime-path root ".")
@(define rosette-eval (rosette-log-evaluator (logfile root "boxes-log")))

@title[#:tag "sec:box"]{Boxes}

A box is a single (im)mutable storage cell, which behaves like a one-element (im)mutable @seclink["sec:vec"]{vector}.
Like vectors, immutable boxes are treated as transparent immutable values:  they are @racket[eq?] when their
contents are @racket[eq?].  Mutable boxes are references rather than values, so they are @racket[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[#:eval rosette-eval
(define v1 (box 1))
(define v2 (box 1))
(eq? v1 v2)
(equal? v1 v2)
(define v3 (box-immutable 1))
(define v4 (box-immutable 1))
(eq? v3 v4)
(equal? v1 v3)
]

@examples[#:eval rosette-eval
(define-symbolic x integer?)
(define-symbolic b boolean?)
(code:line (define v1 (box x))           (code:comment "v1 is a box with symbolic contents"))
(code:line (define v2 (if b v1 (box 3))) (code:comment "v2 is a symbolic box"))
(define sol (solve (assert (= 4 (unbox v2)))))
(evaluate v1 sol)
(evaluate v2 sol)
(evaluate (eq? v1 v2) sol)]

Lifted box operations are shown below.  
@tabular[#:style (style #f (list (attributes '((id . "lifted")(class . "boxed")))))
(list (list @box-ops))]

@(kill-evaluator rosette-eval)
