		Search-engine friendly clone of the ACL2 documentation.

Svstate

Make-svstate

Basic constructor macro for svstate structures.

Syntax

(make-svstate [:blkst <blkst>] 
              [:nonblkst <nonblkst>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-svstate

(defmacro make-svstate (&rest args)
  (std::make-aggregate 'svstate
                       args '((:blkst quote (nil)) (:nonblkst))
                       'make-svstate
                       nil))

Function: svstate

(defun svstate (blkst nonblkst)
  (declare (xargs :guard (and (svstack-p blkst)
                              (svex-alist-p nonblkst))))
  (declare (xargs :guard (consp blkst)))
  (let ((__function__ 'svstate))
    (declare (ignorable __function__))
    (b* ((blkst (mbe :logic (svstack-fix blkst)
                     :exec blkst))
         (nonblkst (mbe :logic (svex-alist-fix nonblkst)
                        :exec nonblkst)))
      (let ((blkst (mbe :logic (svstack-nonempty-fix blkst)
                        :exec blkst)))
        (std::prod-cons blkst nonblkst)))))