Basic constructor macro for parstate structures.
(make-parstate [:bytes <bytes>] [:position <position>] [:chars-read <chars-read>] [:chars-unread <chars-unread>] [:tokens-read <tokens-read>] [:tokens-unread <tokens-unread>] [:checkpoints <checkpoints>])
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.
This is an ordinary
Macro:
(defmacro make-parstate (&rest args) (std::make-aggregate 'parstate args '((:bytes) (:position) (:chars-read) (:chars-unread) (:tokens-read) (:tokens-unread) (:checkpoints)) 'make-parstate nil))
Function:
(defun parstate (bytes position chars-read chars-unread tokens-read tokens-unread checkpoints) (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) (nat-listp checkpoints)))) (declare (xargs :guard t)) (let ((__function__ 'parstate)) (declare (ignorable __function__)) (b* ((bytes (mbe :logic (acl2::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)) (checkpoints (mbe :logic (acl2::nat-list-fix checkpoints) :exec checkpoints))) (list (cons 'bytes bytes) (cons 'position position) (cons 'chars-read chars-read) (cons 'chars-unread chars-unread) (cons 'tokens-read tokens-read) (cons 'tokens-unread tokens-unread) (cons 'checkpoints checkpoints)))))