Initial parser state.
(init-parstate data gcc) → pstate
Given (the data of) a file to parse, and a flag saying whether GCC extensions should be accepted or not, the initial parsing state consists of the data to parse, no unread characters or tokens, no read characters or tokens, the initial file position, and no checkpoints.
Function:
(defun init-parstate (data gcc) (declare (xargs :guard (and (byte-listp data) (booleanp gcc)))) (let ((__function__ 'init-parstate)) (declare (ignorable __function__)) (make-parstate :bytes data :position (position-init) :chars-read nil :chars-unread nil :tokens-read nil :tokens-read-len 0 :tokens-unread nil :checkpoints nil :gcc gcc :size (len data))))
Theorem:
(defthm parstatep-of-init-parstate (b* ((pstate (init-parstate data gcc))) (parstatep pstate)) :rule-classes :rewrite)