		Search-engine friendly clone of the ACL2 documentation.

Vl-oddinfo

Make-vl-oddinfo

Basic constructor macro for vl-oddinfo structures.

Syntax

(make-vl-oddinfo [:type <type>] 
                 [:subexpr <subexpr>] 
                 [:simple <simple>] 
                 [:complex <complex>] 
                 [:swidth <swidth>] 
                 [:cwidth <cwidth>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-oddinfo

(defmacro make-vl-oddinfo (&rest args)
  (std::make-aggregate 'vl-oddinfo
                       args
                       '((:type)
                         (:subexpr)
                         (:simple)
                         (:complex)
                         (:swidth)
                         (:cwidth))
                       'make-vl-oddinfo
                       nil))

Function: vl-oddinfo

(defun vl-oddinfo (type subexpr simple complex swidth cwidth)
  (declare (xargs :guard (and (symbolp type)
                              (vl-expr-p subexpr)
                              (vl-expr-p simple)
                              (vl-expr-p complex)
                              (maybe-natp swidth)
                              (maybe-natp cwidth))))
  (declare (xargs :guard t))
  (let ((__function__ 'vl-oddinfo))
    (declare (ignorable __function__))
    (b* ((type (mbe :logic (acl2::symbol-fix type)
                    :exec type))
         (subexpr (mbe :logic (vl-expr-fix subexpr)
                       :exec subexpr))
         (simple (mbe :logic (vl-expr-fix simple)
                      :exec simple))
         (complex (mbe :logic (vl-expr-fix complex)
                       :exec complex))
         (swidth (mbe :logic (maybe-natp-fix swidth)
                      :exec swidth))
         (cwidth (mbe :logic (maybe-natp-fix cwidth)
                      :exec cwidth)))
      (list (cons 'type type)
            (cons 'subexpr subexpr)
            (cons 'simple simple)
            (cons 'complex complex)
            (cons 'swidth swidth)
            (cons 'cwidth cwidth)))))