		Search-engine friendly clone of the ACL2 documentation.

Svtv

Make-svtv

Basic constructor macro for svtv structures.

Syntax

(make-svtv [:name <name>] 
           [:outexprs <outexprs>] 
           [:nextstate <nextstate>] 
           [:states <states>] 
           [:inmasks <inmasks>] 
           [:outmasks <outmasks>] 
           [:inmap <inmap>] 
           [:orig-ins <orig-ins>] 
           [:orig-overrides <orig-overrides>] 
           [:orig-outs <orig-outs>] 
           [:orig-internals <orig-internals>] 
           [:expanded-ins <expanded-ins>] 
           [:expanded-overrides <expanded-overrides>] 
           [:nphases <nphases>] 
           [:labels <labels>] 
           [:form <form>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-svtv

(defmacro make-svtv (&rest args)
  (std::make-aggregate 'svtv
                       args
                       '((:name)
                         (:outexprs)
                         (:nextstate)
                         (:states)
                         (:inmasks)
                         (:outmasks)
                         (:inmap)
                         (:orig-ins)
                         (:orig-overrides)
                         (:orig-outs)
                         (:orig-internals)
                         (:expanded-ins)
                         (:expanded-overrides)
                         (:nphases)
                         (:labels)
                         (:form))
                       'make-svtv
                       nil))

Function: svtv

(defun svtv (name outexprs nextstate states inmasks
                  outmasks inmap orig-ins orig-overrides
                  orig-outs orig-internals expanded-ins
                  expanded-overrides nphases labels form)
 (declare (xargs :guard (and (symbolp name)
                             (svex-alist-p outexprs)
                             (svex-alist-p nextstate)
                             (svex-alistlist-p states)
                             (svar-boolmasks-p inmasks)
                             (svar-boolmasks-p outmasks)
                             (svtv-inputmap-p inmap)
                             (true-list-listp orig-ins)
                             (true-list-listp orig-overrides)
                             (true-list-listp orig-outs)
                             (true-list-listp orig-internals)
                             (svtv-lines-p expanded-ins)
                             (svtv-lines-p expanded-overrides)
                             (natp nphases)
                             (symbol-listp labels))))
 (declare (xargs :guard t))
 (let ((__function__ 'svtv))
   (declare (ignorable __function__))
   (b*
    ((name (mbe :logic (acl2::symbol-fix name)
                :exec name))
     (outexprs (mbe :logic (svex-alist-fix outexprs)
                    :exec outexprs))
     (nextstate (mbe :logic (svex-alist-fix nextstate)
                     :exec nextstate))
     (states (mbe :logic (svex-alistlist-fix states)
                  :exec states))
     (inmasks (mbe :logic (svar-boolmasks-fix inmasks)
                   :exec inmasks))
     (outmasks (mbe :logic (svar-boolmasks-fix outmasks)
                    :exec outmasks))
     (inmap (mbe :logic (svtv-inputmap-fix inmap)
                 :exec inmap))
     (orig-ins (mbe :logic (true-list-list-fix orig-ins)
                    :exec orig-ins))
     (orig-overrides (mbe :logic (true-list-list-fix orig-overrides)
                          :exec orig-overrides))
     (orig-outs (mbe :logic (true-list-list-fix orig-outs)
                     :exec orig-outs))
     (orig-internals (mbe :logic (true-list-list-fix orig-internals)
                          :exec orig-internals))
     (expanded-ins (mbe :logic (svtv-lines-fix expanded-ins)
                        :exec expanded-ins))
     (expanded-overrides
          (mbe :logic (svtv-lines-fix expanded-overrides)
               :exec expanded-overrides))
     (nphases (mbe :logic (nfix nphases)
                   :exec nphases))
     (labels (mbe :logic (acl2::symbol-list-fix labels)
                  :exec labels)))
    (list name outexprs nextstate
          states inmasks outmasks inmap orig-ins
          orig-overrides orig-outs orig-internals
          expanded-ins expanded-overrides
          nphases labels form))))