		Search-engine friendly clone of the ACL2 documentation.

Vl-operandinfo

Make-vl-operandinfo

Basic constructor macro for vl-operandinfo structures.

Syntax

(make-vl-operandinfo [:orig-expr <orig-expr>] 
                     [:context <context>] 
                     [:prefixname <prefixname>] 
                     [:declname <declname>] 
                     [:hidtrace <hidtrace>] 
                     [:hidtype <hidtype>] 
                     [:seltrace <seltrace>] 
                     [:part <part>] 
                     [:type <type>])

This is the usual way to construct vl-operandinfo structures. It simply conses together a structure with the specified fields.

This macro generates a new vl-operandinfo structure from scratch. See also change-vl-operandinfo, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-operandinfo

(defmacro make-vl-operandinfo (&rest args)
  (std::make-aggregate 'vl-operandinfo
                       args
                       '((:orig-expr)
                         (:context)
                         (:prefixname)
                         (:declname)
                         (:hidtrace)
                         (:hidtype)
                         (:seltrace)
                         (:part)
                         (:type))
                       'make-vl-operandinfo
                       nil))

Function: vl-operandinfo

(defun vl-operandinfo
       (orig-expr context prefixname declname
                  hidtrace hidtype seltrace part type)
 (declare (xargs :guard (and (vl-expr-p orig-expr)
                             (vl-scopecontext-p context)
                             (vl-scopeexpr-p prefixname)
                             (stringp declname)
                             (vl-hidtrace-p hidtrace)
                             (vl-datatype-p hidtype)
                             (vl-seltrace-p seltrace)
                             (vl-partselect-p part)
                             (vl-datatype-p type))))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-operandinfo))
  (declare (ignorable __function__))
  (b* ((orig-expr (mbe :logic (vl-expr-fix orig-expr)
                       :exec orig-expr))
       (context (mbe :logic (vl-scopecontext-fix context)
                     :exec context))
       (prefixname (mbe :logic (vl-scopeexpr-fix prefixname)
                        :exec prefixname))
       (declname (mbe :logic (str-fix declname)
                      :exec declname))
       (hidtrace (mbe :logic (vl-hidtrace-fix hidtrace)
                      :exec hidtrace))
       (hidtype (mbe :logic (vl-datatype-fix hidtype)
                     :exec hidtype))
       (seltrace (mbe :logic (vl-seltrace-fix seltrace)
                      :exec seltrace))
       (part (mbe :logic (vl-partselect-fix part)
                  :exec part))
       (type (mbe :logic (vl-datatype-fix type)
                  :exec type)))
   (std::prod-cons
    (std::prod-cons (std::prod-cons orig-expr context)
                    (std::prod-cons prefixname declname))
    (std::prod-cons (std::prod-cons hidtrace hidtype)
                    (std::prod-cons seltrace
                                    (std::prod-cons part type)))))))