On this page:
6.3.1 Value Browser Library
render-value/  snip
render-value/  window
6.3.1.1 Layout
6.3.1.2 Examples
7.7

6.3 Utility Libraries

The following utility libraries facilitate the development of solver-aided programs.

6.3.1 Value Browser Library

 (require rosette/lib/value-browser) package: rosette

Rosette programs often generate complex symbolic values that can be difficult to read and debug. One common problem is that the printer truncates their representation when it exceeds the threshold set by (error-print-width). This library provides an interactive value browser to help programmers navigate and read complex symbolic values.

procedure

(render-value/snip val [#:handler handler])  (is-a?/c snip%)

  val : any/c
  handler : (-> any/c (-> any/c (is-a?/c snip%)) layout)
   = (λ (value rec) #f)
Constructs a snip% object that displays a value browser. In DrRacket, either evaluating the snip object at the top-level or calling print on the snip object will display the value browser in the REPL.

The value browser supports displaying and navigating values of lifted datatypes. Values of other types (e.g., string or hash) are displayed as leaves in the navigation tree, labeled with the kind other. The optional argument handler can be supplied to customize the display of other values and recover the ability to navigate their structure. See layout and the examples below for more details.

procedure

(render-value/window val [#:handler handler])  (is-a?/c snip%)

  val : any/c
  handler : (-> any/c (-> any/c (is-a?/c snip%)) layout)
   = (λ (value rec) #f)
Similar to render-value/snip, but displays the snip object in a new window frame instead of the REPL. This is useful when executing programs from the command line.

6.3.1.1 Layout

A layout is an embedded DSL describing the tabular layout to display a value of an unlifted datatype in the value browser. It has the following grammar:

 

layout

 ::= 

#f  |  a list of rows

 

row

 ::= 

'#:gap  |  a list of cols

 

col

 ::= 

a snip%  |  string  |  '(emph string )

 

string

 ::= 

a string

Here, #f means the value is atomic (and will be categorized under the kind other), '#:gap means a vertical gap, and emph means emphasis.

6.3.1.2 Examples

The value browser helps navigate values of lifted datatypes as shown below.

> (define-symbolic n integer?)
> (render-value/snip (list 1
                           1.2
                           #t
                           n
                           (bv 1 (bitvector 2))
                           +))
; After expanding the snip:
image
> (define-symbolic f (~> integer? integer?))
> (render-value/snip (list (+ n 1)
                           (if (= n 0) 1 2)
                           (f 1)))
image
> (struct foo [a b])
> (render-value/snip (list (list 1 2)
                           (foo 1 2)
                           (vector 1 2)
                           (box 1)
                           (if (= n 1) 2 "a")))
image

But when we try to display an unlifted value like a hash or a set, the browser categorizes it with the kind other, with navigation disabled.

> (render-value/snip (list (hash 1 2 3 4)
                           (set 1 2 3)))
image

To allow hash navigation, supply a handler that returns a desired layout when a hash is passed in (as the first argument). For instance, we might want (hash a b c d) to have the following layout:

`([(emph "Kind: ") "hash"]
  #:gap
  [,snip-a]
  [,snip-b]
  #:gap
  [,snip-c]
  [,snip-d])

In this layout, snip-a, snip-b, snip-c, and snip-d can be obtained by applying the recursive renderer to a, b, c, and d respectively.

Using the above layout, we enable hash navigation as follows:

> (render-value/snip (list (hash 1 2 3 4)
                           (set 1 2 3))
                     #:handler (λ (value rec)
                                 (cond
                                   [(hash? value)
                                    (append*
                                     '([(emph "Kind: ") "hash"])
                                     (for/list ([(k v) (in-hash value)])
                                       `(#:gap
                                         [,(rec k)]
                                         [,(rec v)])))]
                                   [else #f])))
image

Note that you should use the recursive renderer (provided as the second argument) rather than calling render-value/snip directly so that the correct handler is used when rendering sub-value (e.g., a hash of hashes).