0

ACL2 マクロ トランスフォーマーで、関数定義を最上位に持ち上げることは可能ですか?

関数を指定すると、以下のlet-mapような関数を定義できるマクロを設計しようとしています。map-doubledouble

最上位のみを気にする場合は、define-mapマクロを使用してこれを行うことができます。ただし、このマクロを別の式内にネストされたコンテキストで呼び出すことができるようにしたいと考えています。たとえば、次のようになります。

(defunc double (x)
  :input-contract (rationalp x)
  :output-contract (rationalp (double x))
  (* 2 x))

(let-map map-double double
  (map-double (list 1 2 3)))
;(LIST 2 4 6)

;; I would want nested calls to work as well:
(let-map double-all-1d double
  (let-map double-all-2d double-all-1d
    (double-all-2d (list (list 1 2 3) (list 4 5) (list 6)))))
;(LIST (LIST 2 4 6) (LIST 8 10) (LIST 12))

let-mapマクロで function を定義してから、本体の結果を返します。map-doubleこの場合は を呼び出し(map-double (list 1 2 3))ます。これを で定義しようとしましfletたが、私のmap-double関数は再帰的であるため、機能fletしません。

(defmacro let-map (map-f f body)
  `(flet ((,map-f (lst)
                  (cond ((endp lst) (list))
                        (t (cons (,f (first lst))
                                 ; doesn't work because
                                 ; `flet` doesn't support recursion
                                 (,map-f (rest lst)))))))
     ,body))

を使用しますlabelsが、ACL2 ではサポートされていません。

map-fしたがって、再帰を可能にするために、 (map-doubleこのマクロを使用している)の定義をトップレベルに上げたいと思います。これは ACL2 マクロ システムで可能ですか?

ラケットのようなシステムでは、このような機能を使用しますsyntax-local-lift-expression。では、ACL2 に類似の形式はありますか?

4

0 に答える 0