		Search-engine friendly clone of the ACL2 documentation.

Svtv-precompose-data

Make-svtv-precompose-data

Basic constructor macro for svtv-precompose-data structures.

Syntax

(make-svtv-precompose-data [:simp <simp>] 
                           [:nextstate <nextstate>] 
                           [:input-substs <input-substs>] 
                           [:initst <initst>] 
                           [:pre-compose-inputs <pre-compose-inputs>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-svtv-precompose-data

(defmacro make-svtv-precompose-data (&rest args)
  (std::make-aggregate 'svtv-precompose-data
                       args
                       '((:simp)
                         (:nextstate)
                         (:input-substs)
                         (:initst)
                         (:pre-compose-inputs))
                       'make-svtv-precompose-data
                       nil))

Function: svtv-precompose-data

(defun svtv-precompose-data
       (simp nextstate
             input-substs initst pre-compose-inputs)
 (declare (xargs :guard (and (svex-simpconfig-p simp)
                             (svex-alist-p nextstate)
                             (svex-alistlist-p input-substs)
                             (svex-alist-p initst)
                             (svarlist-p pre-compose-inputs))))
 (declare (xargs :guard t))
 (let ((__function__ 'svtv-precompose-data))
  (declare (ignorable __function__))
  (b* ((simp (mbe :logic (svex-simpconfig-fix simp)
                  :exec simp))
       (nextstate (mbe :logic (svex-alist-fix nextstate)
                       :exec nextstate))
       (input-substs (mbe :logic (svex-alistlist-fix input-substs)
                          :exec input-substs))
       (initst (mbe :logic (svex-alist-fix initst)
                    :exec initst))
       (pre-compose-inputs
            (mbe :logic (svarlist-fix pre-compose-inputs)
                 :exec pre-compose-inputs)))
   (std::prod-cons
     (std::prod-cons simp nextstate)
     (std::prod-cons input-substs
                     (std::prod-cons initst pre-compose-inputs))))))