1

私は自分のプロジェクトの実験を行っています。基本的には、コードにいくつかの s 式を埋め込んで実行する必要があります。次のように、

(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)

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

ラケットでこれを行うにはどうすればよいですか？

更新または前の質問 を使用したい理由evalは、Z3 ラケット バインディングを使用しているためです。(ラケット バインディング API を使用する) 数式を生成する必要があり、その後、ある時点でクエリを起動します。それらのコードを評価します。私の場合、他の方法を考え出していません...非常に単純な例の1つは、想像してみてください
(let ([arr (array-alloc 10)])
(array-set! arr 3 4))

コンストラクトを分析するためのモデルがいくつかあります (そのため、racketZ3 を直接使用していません)。各分析ポイントで、プログラム内のデータ型を Z3 型にマップし、いくつかのアサーションを作成します。

次のようなものを生成します。

  • 割り当てサイトでは、次の式を作成する必要があります。

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

  • 次に、配列セットのサイトで、次のアサーションを行い、3 が長さよりも小さいかどうかを確認します

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

  • 最後に、上記のように生成された式を収集し、Z3 バインディングを起動して次の収集された情報をコードとして実行できる形式でそれらをラップします。

    (smt:with-context
    (smt:new-context)
    (define len (make-length 10))
    (smt:assert (</s 3 (len arr_z3))) (smt:check-sat))

これは私が考えることができる非常に単純な例です...理にかなっていますか?
サイドノート。バージョン 5.3.1 で Z3 Racket バインディングが何らかの理由でクラッシュしますが、バージョン 5.2.1 ではほとんど動作します。

4

3 に答える 3

1

警告：Schemeでの関数の動作に慣れていない場合は、答えを無視してください。マクロは高度な技術であり、最初に関数を理解する必要があります。

マクロについて質問しているようです。test以下を出力する関数として定義するコードを次に示します2。

 (define-syntax-rule (show-one-more-than num)
   (begin 
     (define num2 (add1 num))   
     (displayln num2)))

 (define (test) 
   (define num1 1)
   (show-one-more-than num1))

今、私はshow-one-more-thanマクロの代わりに関数として書くことができました（そしてそうすべきです！）が、マクロは実際には呼び出しサイトでコードを生成することによって動作しますdefine-syntax-rule。defineしたがって、上記のコードは次のように展開されます。

 (define (test)
   (define num1 1)
   (begin 
     (define num2 (add1 num1))
     (displayln num2)))
于 2012-11-17T12:06:43.020 に答える
1

問題をよりよく知ることなしに、この問題への正しいアプローチが何であるかを言うのは難しいです。次のようなブルー​​トフォースアプローチ：

#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)

あなたが望むものかもしれませんが、おそらくそうではありません。

于 2012-11-17T16:55:37.097 に答える
1

正直なところ、あなたが何を達成したいのか正確にはわかりません。N. Holm、Sketchy Scheme、第 4.5 版、p を引用します。108: »準引用符の主な目的は、数個の変数部分のみを含む固定リスト構造の構築です«. あなたが目指しているような文脈で準引用が使用されるとは思いません。

準引用符の典型的なコンテキストについては、次の例を検討してください。

(define (square x)
  (* x x))

(define sentence
  '(The square of))

(define (quasiquotes-unquotes-splicing x)
  `(,@sentence ,x is ,(square x)))

(quasiquotes-unquotes-splicing 2)
===> (The square of 2 is 4)
于 2012-11-17T09:37:39.220 に答える