The following utility libraries facilitate the development of solver-aided programs.
|(require rosette/lib/destruct)||package: rosette|
(destruct val-expr [pat body ...+] ...)
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.
The grammar of pat is as follows, where non-italicized identifiers are recognized literally (i.e., not by binding).
match anything; see details below
(list lvp ...)
match a list
(list-rest lvp ... sp)
match a list with tail
(list* lvp ... sp)
match a list with tail
(vector lvp ...)
match a vector
(cons sp sp)
match a pair
match a box
(struct-id sp ...)
match a struct-id instance
match anything, bind identifier
match anything, ignore the result
greedily match anything
zero or more; ... is literal
zero or more
k or more
k or more
See match for the semantics of each pattern.
(destruct* (val-expr ...) [(pat ...) body ...+] ...)
(destruct-lambda [(pat ...) body ...+] ...)
|(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.
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.
#f | a list of ‹row›s
'#:gap | a list of ‹col›s
a snip% | ‹string› | '(emph ‹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.
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: > (define-symbolic f (~> integer? integer?)) > (render-value/snip (list (+ n 1) (if (= n 0) 1 2) (f 1))) > (struct foo [a b]) > (render-value/snip (list (list 1 2) (foo 1 2) (vector 1 2) (box 1) (if (= n 1) 2 "a")))
> (render-value/snip (list (hash 1 2 3 4) (set 1 2 3)))
`([(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])))
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).