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-read-len <tokens-read-len>] [:tokens-unread <tokens-unread>] [:checkpoints <checkpoints>] [:gcc <gcc>] [:size <size>])
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-read-len) (:tokens-unread) (:checkpoints) (:gcc) (:size)) 'make-parstate nil))
Function:
(defun parstate (bytes position chars-read chars-unread tokens-read tokens-read-len tokens-unread checkpoints gcc size) (declare (xargs :guard (and (byte-listp bytes) (positionp position) (char+position-listp chars-read) (char+position-listp chars-unread) (token+span-listp tokens-read) (natp tokens-read-len) (token+span-listp tokens-unread) (nat-listp checkpoints) (booleanp gcc) (natp size)))) (declare (xargs :guard (and (equal size (+ (len bytes) (len chars-unread) (len tokens-unread))) (equal tokens-read-len (len tokens-read))))) (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-read-len (mbe :logic (nfix tokens-read-len) :exec tokens-read-len)) (tokens-unread (mbe :logic (token+span-list-fix tokens-unread) :exec tokens-unread)) (checkpoints (mbe :logic (acl2::nat-list-fix checkpoints) :exec checkpoints)) (gcc (mbe :logic (acl2::bool-fix gcc) :exec gcc)) (size (mbe :logic (nfix size) :exec size))) (let ((tokens-read-len (mbe :logic (len tokens-read) :exec tokens-read-len)) (size (mbe :logic (+ (len bytes) (len chars-unread) (len tokens-unread)) :exec size))) (list (cons 'bytes bytes) (cons 'position position) (cons 'chars-read chars-read) (cons 'chars-unread chars-unread) (cons 'tokens-read tokens-read) (cons 'tokens-read-len tokens-read-len) (cons 'tokens-unread tokens-unread) (cons 'checkpoints checkpoints) (cons 'gcc gcc) (cons 'size size))))))