Initial parser state.
(init-parstate data) → pstate
Given (the data of) a file to parse, 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) (declare (xargs :guard (byte-listp data))) (let ((__function__ 'init-parstate)) (declare (ignorable __function__)) (make-parstate :bytes data :position (position-init) :chars-read nil :chars-unread nil :tokens-read nil :tokens-unread nil :checkpoints nil)))
Theorem:
(defthm parstatep-of-init-parstate (b* ((pstate (init-parstate data))) (parstatep pstate)) :rule-classes :rewrite)