		Search-engine friendly clone of the ACL2 documentation.

Segment-driver

Make-segment-driver

Basic constructor macro for segment-driver structures.

Syntax

(make-segment-driver [:lsb <lsb>] 
                     [:width <width>] 
                     [:value <value>] 
                     [:strength <strength>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-segment-driver

(defmacro make-segment-driver (&rest args)
  (std::make-aggregate 'segment-driver
                       args
                       '((:lsb)
                         (:width)
                         (:value)
                         (:strength . 6))
                       'make-segment-driver
                       nil))

Function: segment-driver

(defun segment-driver (lsb width value strength)
  (declare (xargs :guard (and (natp lsb)
                              (posp width)
                              (svex-p value)
                              (natp strength))))
  (declare (xargs :guard t))
  (let ((__function__ 'segment-driver))
    (declare (ignorable __function__))
    (b* ((lsb (mbe :logic (nfix lsb) :exec lsb))
         (width (mbe :logic (pos-fix width)
                     :exec width))
         (value (mbe :logic (svex-fix value)
                     :exec value))
         (strength (mbe :logic (nfix strength)
                        :exec strength)))
      (std::prod-cons (std::prod-cons lsb width)
                      (std::prod-cons value strength)))))