Read a specific punctuator token.
This is called when we expect a specific punctuator. We pass the string for the punctuator, and we read the next token, ensuring it exists and it is that punctuator.
Function:
(defun read-punctuator (punct pstate) (declare (xargs :guard (and (stringp punct) (parstatep pstate)))) (let ((__function__ 'read-punctuator)) (declare (ignorable __function__)) (b* (((reterr) (irr-span) (irr-parstate)) ((erp token span pstate) (read-token pstate)) ((unless (token-punctuatorp token punct)) (reterr-msg :where (position-to-msg (span->start span)) :expected (msg "the punctuator ~x0" punct) :found (token-to-msg token)))) (retok span pstate))))
Theorem:
(defthm spanp-of-read-punctuator.span (b* (((mv acl2::?erp ?span ?new-pstate) (read-punctuator punct pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-read-punctuator.new-pstate (b* (((mv acl2::?erp ?span ?new-pstate) (read-punctuator punct pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-read-punctuator-uncond (b* (((mv acl2::?erp ?span ?new-pstate) (read-punctuator punct pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-read-punctuator-cond (b* (((mv acl2::?erp ?span ?new-pstate) (read-punctuator punct pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)