0

我按照 Rosette 网站上的说明下载了 Rosette ( https://docs.racket-lang.org/rosette-guide/ch_getting-started.html )。看来我可以运行这个程序并且没有输出错误。

    #lang rosette/safe

; Compute the absolute value of `x`.
(define (absv x)
  (if (< x 0) (- x) x))

; Define a symbolic variable called y of type integer.
(define-symbolic y integer?)

; Solve a constraint saying |y| = 5.
(solve
  (assert (= (absv y) 5)))

但是,当我尝试使用比基本球拍关键字更多的内容运行此程序或任何类似程序时,我得到了不清楚(对我而言)的错误。

#lang rosette

(struct plus (left right) #:transparent)
(struct mul (left right) #:transparent)
(struct square (arg) #:transparent)

(define prog (plus (square 7) 3))

(define (interpret p)
  (destruct p
    [(plus a b)  (+ (interpret a) (interpret b))]
    [(mul a b)   (* (interpret a) (interpret b))]
    [(square a)  (expt (interpret a) 2)]
    [_ p]))

(interpret prog)

这给了我一个错误destruct: unbound identifier in: destruct。到底是怎么回事?这段代码不是我自己的,是从教程中复制粘贴的,所以我认为它应该可以工作。我还尝试了从 Rosette 网站粘贴的示例代码副本,并给出了类似的错误。我已遵循所有安装说明并更新了环境路径等。有帮助吗?

4

1 回答 1

1

destruct默认情况下不提供#lang rosette。您需要通过以下方式要求它:

 (require rosette/lib/destruct)

#lang rosette

顺便说一句,您在哪里找到此代码?

于 2021-10-21T23:22:41.167 回答