defmacroq - ACL2 Book

Included Books

top

other

(in-package "ACL2")

include-book

(include-book "xdoc/top" :dir :system)

other

(defxdoc defmacroq
  :parents (macros defmacro kestrel-utilities)
  :short "Define a macro that quotes arguments not wrapped in @(':eval')"
  :long "<p>@('Defmacroq') has the same general form as @('defmacro') (see
 @(see defmacro)), that is:</p>

 @({
 (defmacro name macro-args doc-string dcl ... dcl body)
 })

 <p>However, for any subsequent call of @('name'), and for each variable
 @('var') introduced by @(tsee macro-args) that is bound to a corresponding
 value @('val') from the call, @('var') is instead bound to @('(quote val)')
 with one exception: if @('val') is of the form @('(:eval x)'), then @('var')
 is bound to the expression @('x').  The following example shows how this
 works.</p>

 @({
 ACL2 !>(defmacroq mac2 (x y)
          `(list ,x ,y))

 Summary
 Form:  ( DEFMACRO MAC2 ...)
 Rules: NIL
 Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
  MAC2
 ACL2 !>:trans1 (mac2 (a b) (:eval (append '(c d) '(e f))))
  (LIST '(A B) (APPEND '(C D) '(E F)))
 ACL2 !>(mac2 (a b) (:eval (append '(c d) '(e f))))
 ((A B) (C D E F))
 ACL2 !>
 })

 <p>Thus, if we ignore the role of @(':eval'), the macro definition above is
 equivalent to the following.</p>

 @({
 (defmacro mac2 (x y)
   `(list ',x ',y))
 })")

defmacroq-bindingfunction

(defun defmacroq-binding
  (arg)
  (declare (xargs :guard (symbolp arg)))
  `(,ARG (if (and (consp ,ARG)
        (consp (cdr ,ARG))
        (null (cddr ,ARG))
        (eq (car ,ARG) :eval))
      (cadr ,ARG)
      (list 'quote ,ARG))))

defmacroq-bindingsfunction

(defun defmacroq-bindings
  (args)
  (declare (xargs :guard (symbol-listp args)))
  (cond ((endp args) nil)
    (t (cons (defmacroq-binding (car args))
        (defmacroq-bindings (cdr args))))))

defmacroqmacro

(defmacro defmacroq
  (fn args &rest rest)
  (let* ((vars (macro-vars args)) (bindings (defmacroq-bindings vars))
      (dcls (butlast rest 1))
      (body (car (last rest))))
    (cond ((member-eq 'state vars) (er hard
          'defmacroq
          "It is illegal to supply STATE as an argument of DEFMACROQ."))
      (t `(defmacro ,FN
          ,ARGS
          ,@DCLS
          (let ,BINDINGS
            ,BODY))))))

local

(local (progn (defmacroq mac4
      (x y z w)
      `(list ,X ,Y ,Z ,W (f-boundp-global 'boot-strap-flg state)))
    (defun f
      (a state b)
      (declare (xargs :stobjs state))
      (cons 17 (mac4 c (:eval (cons a b)) b (:eval (expt 2 3)))))
    (assert-event (equal (f (expt 4 1) state (reverse '(i j k)))
        '(17 c (4 k j i) b 8 t)))))