9.0
top
up

3.1Lifted Racket FormsπŸ”— i

Rosette lifts the following Racket forms:

Literals

quote , #%datum

Procedure Applications

#%app , #%plain-app

Procedure Expressions

lambda , λ , case-lambda , #%plain-lambda

Local Definitions

local

Conditionals

if , and , or , cond with [testbody...+] and [else body...+] clauses

Dispatch

case

Sequencing

begin , begin0 , begin-for-syntax

Guarded Evaluation

when , unless

Assignment

set! , set!-values

Quasiquoting

quasiquote , unquote

Syntax Quoting

quote-syntax

Lifted forms have the same meaning in Rosette programs as they do in Racket programs. For example, the Racket expression (if test-exprthen-exprelse-expr) evaluates test-expr first and then, depending on the outcome, it returns the result of evaluating either then-expr or else-expr. Rosette preserves this interpretation of if for concrete values, and also extends it to work with symbolic values:
> (let ([y0])
(if #t(void )(set! y3))
(printf "y unchanged: ~a\n"y)
(if #f(set! y3)(void ))
(printf "y unchanged: ~a\n"y)
(if x(void )(set! y3))
(printf "y symbolic: ~a\n"y))

y unchanged: 0

y unchanged: 0

y symbolic: (ite x 0 3)

top
up

AltStyle γ«γ‚ˆγ£γ¦ε€‰ζ›γ•γ‚ŒγŸγƒšγƒΌγ‚Έ (->γ‚ͺγƒͺγ‚ΈγƒŠγƒ«) /