		Search-engine friendly clone of the ACL2 documentation.

Vl-genif

Make-vl-genif

Basic constructor macro for vl-genif structures.

Syntax

(make-vl-genif [:test <test>] 
               [:then <then>] 
               [:else <else>] 
               [:loc <loc>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-genif

(defmacro make-vl-genif (&rest args)
  (std::make-aggregate 'vl-genif
                       args '((:test) (:then) (:else) (:loc))
                       'make-vl-genif
                       nil))

Function: vl-genif

(defun vl-genif (test then else loc)
  (declare (xargs :guard (and (vl-expr-p test)
                              (vl-genelement-p then)
                              (vl-genelement-p else)
                              (vl-location-p loc))))
  (declare (xargs :guard t))
  (let ((__function__ 'vl-genif))
    (declare (ignorable __function__))
    (b* ((test (mbe :logic (vl-expr-fix test)
                    :exec test))
         (then (mbe :logic (vl-genelement-fix then)
                    :exec then))
         (else (mbe :logic (vl-genelement-fix else)
                    :exec else))
         (loc (mbe :logic (vl-location-fix loc)
                   :exec loc)))
      (cons :vl-genif (std::prod-cons (std::prod-cons test then)
                                      (std::prod-cons else loc))))))