		Search-engine friendly clone of the ACL2 documentation.

Pinst-special-term

Make-pinst-special-term

Basic constructor macro for pinst-special-term structures.

Syntax

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

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-pinst-special-term

(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: pinst-special-term

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