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?