Basic constructor macro for pinst-special-term structures.
(make-pinst-special-term [:width <width>] [:first <first>] [:init-args-indent <init-args-indent>] [:init-args <init-args>] [:body-args-indent <body-args-indent>] [:body-args <body-args>])
This is the usual way to construct pinst-special-term structures. It simply conses together a structure with the specified fields.
This macro generates a new pinst-special-term structure from scratch. See also change-pinst-special-term, which can "change" an existing structure, instead.
This is an ordinary
Macro:
(defmacro make-pinst-special-term (&rest args) (std::make-aggregate 'pinst-special-term args '((:width) (:first) (:init-args-indent) (:init-args) (:body-args-indent) (:body-args)) 'make-pinst-special-term nil))
Function:
(defun pinst-special-term (width first init-args-indent init-args body-args-indent body-args) (declare (xargs :guard (and (posp width) (pinst-p first) (integerp init-args-indent) (pinstlist-p init-args) (natp body-args-indent) (pinstlist-p body-args)))) (declare (xargs :guard t)) (let ((acl2::__function__ 'pinst-special-term)) (declare (ignorable acl2::__function__)) (b* ((width (mbe :logic (acl2::pos-fix width) :exec width)) (first (mbe :logic (pinst-fix first) :exec first)) (init-args-indent (mbe :logic (ifix init-args-indent) :exec init-args-indent)) (init-args (mbe :logic (pinstlist-fix init-args) :exec init-args)) (body-args-indent (mbe :logic (nfix body-args-indent) :exec body-args-indent)) (body-args (mbe :logic (pinstlist-fix body-args) :exec body-args))) (cons :special-term (std::prod-cons (std::prod-cons width (std::prod-cons first init-args-indent)) (std::prod-cons init-args (std::prod-cons body-args-indent body-args)))))))