		Search-engine friendly clone of the ACL2 documentation.

Parstate$

Make-parstate$

Basic constructor macro for parstate$ structures.

Syntax

(make-parstate$ [:bytes <bytes>] 
                [:position <position>] 
                [:chars-read <chars-read>] 
                [:chars-unread <chars-unread>] 
                [:tokens-read <tokens-read>] 
                [:tokens-unread <tokens-unread>] 
                [:version <version>])

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

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

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-parstate$

(defmacro make-parstate$ (&rest args)
  (std::make-aggregate 'parstate$
                       args
                       '((:bytes)
                         (:position)
                         (:chars-read)
                         (:chars-unread)
                         (:tokens-read)
                         (:tokens-unread)
                         (:version))
                       'make-parstate$
                       nil))

Function: parstate$

(defun parstate$ (bytes position chars-read chars-unread
                        tokens-read tokens-unread version)
  (declare (xargs :guard (and (byte-listp bytes)
                              (positionp position)
                              (char+position-listp chars-read)
                              (char+position-listp chars-unread)
                              (token+span-listp tokens-read)
                              (token+span-listp tokens-unread)
                              (c::versionp version))))
  (declare (xargs :guard t))
  (b*
    ((bytes (mbe :logic (byte-list-fix bytes)
                 :exec bytes))
     (position (mbe :logic (position-fix position)
                    :exec position))
     (chars-read (mbe :logic (char+position-list-fix chars-read)
                      :exec chars-read))
     (chars-unread (mbe :logic (char+position-list-fix chars-unread)
                        :exec chars-unread))
     (tokens-read (mbe :logic (token+span-list-fix tokens-read)
                       :exec tokens-read))
     (tokens-unread (mbe :logic (token+span-list-fix tokens-unread)
                         :exec tokens-unread))
     (version (mbe :logic (c::version-fix version)
                   :exec version)))
    (cons (cons bytes (cons position chars-read))
          (cons (cons chars-unread tokens-read)
                (cons tokens-unread version)))))