6.3 Utility Libraries

On this page:

6.3.1Value Destructuring Library

destruct

destruct*

destruct-lambda

6.3.2Value Browser Library

render-value/snip

render-value/window

6.3.2.1Layout

6.3.2.2Examples

9.0

top ← prev up next →

6.3Utility Libraries🔗 i

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

6.3.1Value Destructuring Library🔗 i

(require rosette/lib/destruct ) package: rosette

syntax
( destruct val-expr[patbody...+]...)

Finds the first pat that matches the result of val-expr, and evaluates the corresponding bodys with bindings introduced by pat (if any). In other words, it provides a lifted pattern matching similar to match with limited capabilities:

A sub-pattern is restricted to an identifier, a wildcard (_), or an ellipsis (e.g., ...). That is, destruct allows value destructuring only at the outermost level (nested destructuring is disallowed).
All binding identifiers in a clause must be unique (no duplicate binding identifiers).
Only patterns with lifted semantics are supported. See the grammar below for full details.
Side-conditioning via #:when and the failure procedure are not supported.

Examples:

> (struct add(xy))
> (struct mul(xy))

> (define (interpv)
(destruct v
[(addxy)(+ xy)]
[(mulxy)(* xy)]
[_ (assert #f"infeasible")]))
> (interp(add34))

7
> (interp(mul56))

30
> (define-symbolic bboolean? )
> (interp(if b(add34)(mul56)))

(ite b 7 30)

The grammar of pat is as follows, where non-italicized identifiers are recognized literally (i.e., not by binding).

pat

::=

match anything; see details below

(listlvp...)

match a list

(list-restlvp...sp)

match a list with tail

(list*lvp...sp)

match a list with tail

(vectorlvp...)

match a vector

(consspsp)

match a pair

(boxsp)

match a box

(struct-idsp...)

match a struct-id instance

::=

match anything, bind identifier

match anything, ignore the result

lvp

::=

spooo

greedily match anything

match anything

ooo

::=

...

zero or more; ... is literal

___

zero or more

..k

k or more

__k

k or more

See match for the semantics of each pattern.

syntax
( destruct* (val-expr...)[(pat...)body...+]...)

Similar to match* but with the restrictions of destruct .

Examples:

> (define x(if b(list 1)(list 12)))
> (define y(if b(list 10)(list 1020)))

> (destruct* (xy)
[((list p)(list q))(+ pq)]
[((list pp*)(list qq*))(+ pp*qq*)])

(ite b 11 33)

syntax
( destruct-lambda [(pat...)body...+]...)

Similar to match-lambda but with the restrictions of destruct .

Example:

> (map (destruct-lambda [(addxy)(+ xy)])
(list (if b(add12)(add34))
(add56)
(if (not b)(add78)(add910))))

(list (ite b 3 7) 11 (ite b 19 15))

6.3.2Value Browser Library🔗 i

(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[#:handlerhandler])→(is-a?/c snip% )
val:any/c

handler : (-> any/c (-> any/c (is-a?/c snip% ))layout )
= (λ (valuerec)#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[#:handlerhandler])→(is-a?/c snip% )
val:any/c

handler : (-> any/c (-> any/c (is-a?/c snip% ))layout )
= (λ (valuerec)#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.2.1Layout🔗 i

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 ‹row›s

‹row›

::=

'#:gap|a list of ‹col›s

‹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.2.2Examples🔗 i

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

>(define-symbolic ninteger? )
>(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 (+ n1)
(if (= n0)12)
(f1)))
[画像:image]
>(struct foo[ab])
>(render-value/snip (list (list 12)
(foo12)
(vector 12)
(box 1)
(if (= n1)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 1234)
(set 123)))
[画像: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 abcd) 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 1234)
(set 123))
#:handler(λ (valuerec)
(cond
[(hash? value)
(append*
'([(emph"Kind: ")"hash"])
(for/list ([(kv)(in-hash value)])
`(#:gap
[,(reck)]
[,(recv)])))]
[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).

top ← prev up next →