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宏定义一个函数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