		Search-engine friendly clone of the ACL2 documentation.

Svtv-spec

Make-svtv-spec

Basic constructor macro for svtv-spec structures.

Syntax

(make-svtv-spec [:fsm <fsm>] 
                [:cycle-phases <cycle-phases>] 
                [:namemap <namemap>] 
                [:probes <probes>] 
                [:in-alists <in-alists>] 
                [:override-test-alists <override-test-alists>] 
                [:override-val-alists <override-val-alists>] 
                [:initst-alist <initst-alist>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-svtv-spec

(defmacro make-svtv-spec (&rest args)
  (std::make-aggregate 'svtv-spec
                       args
                       '((:fsm)
                         (:cycle-phases)
                         (:namemap)
                         (:probes)
                         (:in-alists)
                         (:override-test-alists)
                         (:override-val-alists)
                         (:initst-alist))
                       'make-svtv-spec
                       nil))

Function: svtv-spec

(defun svtv-spec (fsm cycle-phases namemap
                      probes in-alists override-test-alists
                      override-val-alists initst-alist)
 (declare (xargs :guard (and (fsm-p fsm)
                             (svtv-cyclephaselist-p cycle-phases)
                             (svtv-name-lhs-map-p namemap)
                             (svtv-probealist-p probes)
                             (svex-alistlist-p in-alists)
                             (svex-alistlist-p override-test-alists)
                             (svex-alistlist-p override-val-alists)
                             (svex-alist-p initst-alist))))
 (declare (xargs :guard t))
 (let ((__function__ 'svtv-spec))
  (declare (ignorable __function__))
  (b*
   ((fsm (mbe :logic (fsm-fix fsm) :exec fsm))
    (cycle-phases (mbe :logic (svtv-cyclephaselist-fix cycle-phases)
                       :exec cycle-phases))
    (namemap (mbe :logic (svtv-name-lhs-map-fix namemap)
                  :exec namemap))
    (probes (mbe :logic (svtv-probealist-fix probes)
                 :exec probes))
    (in-alists (mbe :logic (svex-alistlist-fix in-alists)
                    :exec in-alists))
    (override-test-alists
         (mbe :logic (svex-alistlist-fix override-test-alists)
              :exec override-test-alists))
    (override-val-alists
         (mbe :logic (svex-alistlist-fix override-val-alists)
              :exec override-val-alists))
    (initst-alist (mbe :logic (svex-alist-fix initst-alist)
                       :exec initst-alist)))
   (list (cons 'fsm fsm)
         (cons 'cycle-phases cycle-phases)
         (cons 'namemap namemap)
         (cons 'probes probes)
         (cons 'in-alists in-alists)
         (cons 'override-test-alists
               override-test-alists)
         (cons 'override-val-alists
               override-val-alists)
         (cons 'initst-alist initst-alist)))))