		Search-engine friendly clone of the ACL2 documentation.

Sparseint$-concat

Make-sparseint$-concat

Basic constructor macro for sparseint$-concat structures.

Syntax

(make-sparseint$-concat [:width <width>] 
                        [:lsbs-taller <lsbs-taller>] 
                        [:msbs-taller <msbs-taller>] 
                        [:lsbs <lsbs>] 
                        [:msbs <msbs>])

This is the usual way to construct sparseint$-concat structures. It simply conses together a structure with the specified fields.

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

Definition

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

Macro: make-sparseint$-concat

(defmacro make-sparseint$-concat (&rest args)
  (std::make-aggregate 'sparseint$-concat
                       args
                       '((:width)
                         (:lsbs-taller)
                         (:msbs-taller)
                         (:lsbs)
                         (:msbs))
                       'make-sparseint$-concat
                       nil))

Function: sparseint$-concat

(defun sparseint$-concat (width lsbs-taller msbs-taller lsbs msbs)
  (declare (xargs :guard (and (posp width)
                              (booleanp lsbs-taller)
                              (booleanp msbs-taller)
                              (sparseint$-p lsbs)
                              (sparseint$-p msbs))))
  (declare (xargs :guard t))
  (let ((__function__ 'sparseint$-concat))
    (declare (ignorable __function__))
    (b* ((width (mbe :logic (pos-fix width)
                     :exec width))
         (lsbs-taller (mbe :logic (acl2::bool-fix lsbs-taller)
                           :exec lsbs-taller))
         (msbs-taller (mbe :logic (acl2::bool-fix msbs-taller)
                           :exec msbs-taller))
         (lsbs (mbe :logic (sparseint$-fix lsbs)
                    :exec lsbs))
         (msbs (mbe :logic (sparseint$-fix msbs)
                    :exec msbs)))
      (cons (logcons (bool->bit lsbs-taller)
                     (logcons (bool->bit msbs-taller) width))
            (cons lsbs msbs)))))