如何将表达式列表拆分为代码? [英] How can I unsplice a list of expression into code?

问题描述

我的项目有一个实验，基本上，我需要在代码中嵌入一些s表达式并让它运行，就像这样，

I have an experiment for my project, basically, I need to embedded some s-expression into the code and make it run, like this,

(define (test lst)
    (define num 1)
    (define l (list))
    `@lst) ; oh, this is not the right way to go.

  (define lst
    `( (define num2 (add1 num))
      (displayln num2)))

我希望 test 函数就像在球拍代码中的 test(lst) 之后一样:

I want the test function be like after test(lst) in racket code:

(define (test lst)
    (define num 1)
    (define l (list))
    (define num2 (add1 num)
    (displayln num2))

我怎样才能在球拍中做到这一点?

How can I do this in racket?

更新我想使用 eval 或前面的问题的原因是我使用的是 Z3 球拍绑定，我需要生成公式(使用球拍绑定 API)，然后我将在某些时候触发查询点，那是我需要评估这些代码的时候.在我的情况下，我还没有想出其他方法......一个超级简单的例子是，想象一下
(let ([arr (array-alloc 10)])
(array-set!arr 3 4))

Update The reason I would like to use eval or the previous questions is that I am using Z3 racket binding, I need to generate formulas (which uses racket binding APIs), and then I will fire the query at some point, that's when I need to evaluate those code. I have not figured out other ways to go in my case... One super simple example is, imagine
(let ([arr (array-alloc 10)])
(array-set! arr 3 4))

我有一些模型来分析构造(所以我没有直接使用racketZ3)，在每个分析点时，我都会将程序中的数据类型映射到Z3类型，并做出一些断言，

I have some model to analyze the constructs (so I am not using racketZ3 directly), during each analyzing point, I will map the data types in the program into the Z3 types, and made some assertions,

我将生成如下内容:

• 在分配站点，我需要制定以下公式:

• At allocation site, I will need to make the following formula:

(smt:declare-fun arr_z3() IntList)
(define len (make-length 10))

然后在数组集站点，我将有以下断言并检查 3 是否小于长度

Then at the array set site, I will have the following assertions and to check whether the 3 is less then the length

(smt:assert (</s 3 (len arr_z3)))
(smt:check-sat)

最后，我将收集如上生成的公式，并将它们包装在能够触发 Z3 绑定的表单中，以运行以下收集的信息作为代码:

Then finally, I will gather the formulas generated as above, and wrap them in the form which is able to fire Z3 binding to run the following gathered information as code:

(smt:with-context
(smt:新上下文)
(定义 len (make-length 10))
(smt:assert (</s 3 (len arr_z3)))(smt:check-sat))

这是我能想到的超级简单的例子……有意义吗?
附注.Z3 Racket 绑定在 5.3.1 版本上会因为某些原因崩溃，但它在 5.2.1 版本上基本可以工作

This is the super simple example I can think of... making sense?
side note. Z3 Racket binding will crash for some reason on version 5.3.1, but it mostly can work on version 5.2.1

推荐答案

在没有更好地了解问题的情况下，很难说出解决这个问题的正确方法是什么.一种蛮力方法，例如:

Without knowing the problem better, it's hard to say what the correct approach to this problem is. A brute force approach, such as the following:

#lang racket

(define (make-test-body lst)

  (define source `(define (test)
                    (define num 1)
                    (define l (list))
                    ,@lst))
  source)


(define lst
  `((define num2 (add1 num))
    (displayln num2)))

(define test-source
  (make-test-body lst))

(define test
  (parameterize ([current-namespace (make-base-namespace)])
    (eval `(let ()
             ,test-source
             test))))

(test)

可能是您想要的，但可能不是.

may be what you want, but probably not.

这篇关于如何将表达式列表拆分为代码?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！