In a macro transformer, is it possible to lift a definition to the top level?

101 Views Asked by At

In an ACL2 macro transformer, is it possible to lift a function definition to the top level?

I'm trying to design a macro let-map that can define functions like map-double below when given a double function.

If I only cared about the top level, I could do this with a define-map macro. However, I want this macro to be able to be able to called in a context nested within another expression. So for example:

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

I want the let-map macro to define a function map-double, and then return the result of the body, in this case calling (map-double (list 1 2 3)). I tried defining this in terms of flet, but my map-double function is recursive, so flet doesn't work.

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

I would use labels, but it's not supported in ACL2.

So to allow recursion, I want to lift the definition of map-f (which is map-double in my use of this macro) to the top level. Is this possible in the ACL2 macro system?

In a system like racket, I would use a function like syntax-local-lift-expression to do this. So is there an analogous form in ACL2?

0

There are 0 best solutions below