		Search-engine friendly clone of the ACL2 documentation.

Svar

Make-svar

Basic constructor macro for svar structures.

Syntax

(make-svar [:name <name>] 
           [:delay <delay>] 
           [:bits <bits>] 
           [:props <props>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-svar

(defmacro make-svar (&rest args)
  (std::make-aggregate 'svar
                       args
                       '((:name)
                         (:delay . 0)
                         (:bits . 0)
                         (:props))
                       'make-svar
                       nil))

Function: svar

(defun svar (name delay bits props)
 (declare (xargs :guard (and (natp delay)
                             (integerp bits)
                             (svar-proplist-p props))))
 (declare (xargs :guard t))
 (let ((__function__ 'svar))
  (declare (ignorable __function__))
  (b* ((delay (mbe :logic (nfix delay) :exec delay))
       (bits (mbe :logic (ifix bits) :exec bits))
       (props (mbe :logic (svar-proplist-fix props)
                   :exec props)))
   (cond
    (props (hons :var (hons name
                            (hons (hons :delay delay)
                                  (hons (hons :bits bits) props)))))
    ((>= delay 16)
     (hons :var (hons name (hons delay bits))))
    ((and (or (stringp name)
              (and (symbolp name)
                   (not (booleanp name))))
          (eql delay 0)
          (eql bits 0))
     name)
    (t (hons :var (hons name (logapp 4 delay bits))))))))