Parse a pointer.
(parse-pointer pstate) → (mv erp tyqualss span new-pstate)
In the grammar, a `pointer' is a sequence of one or more stars, each followed by zero or more type qualifiers. In our abstract syntax, we model this notion as a list of lists of type qualifiers, one inner list for each star (implicit in our abstract syntax), with the outer list corresponding to the sequence of stars.
We read a star, which must be present: this function is called when we expect a pointer. If the next token is a type qualifier, we put it back and read a list of one or more type qualifiers; then we check the next token if there is another star, in which case we recursively call this function. If instead the initial star is followed by another star, we also call this function recursively. We stop when there is not a star.
Function:
(defun parse-pointer (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-pointer)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) (irr-parstate)) ((erp span pstate) (read-punctuator "*" pstate)) ((erp token & pstate) (read-token pstate))) (cond ((token-type-qualifier-p token) (b* ((pstate (unread-token pstate)) ((erp tyquals span2 pstate) (parse-type-qualifier-list pstate)) ((erp token & pstate) (read-token pstate))) (cond ((equal token (token-punctuator "*")) (b* ((pstate (unread-token pstate)) ((erp tyqualss last-span pstate) (parse-pointer pstate))) (retok (cons tyquals tyqualss) (span-join span last-span) pstate))) (t (b* ((pstate (if token (unread-token pstate) pstate))) (retok (list tyquals) (span-join span span2) pstate)))))) ((equal token (token-punctuator "*")) (b* ((pstate (unread-token pstate)) ((erp tyqualss last-span pstate) (parse-pointer pstate))) (retok (cons nil tyqualss) (span-join span last-span) pstate))) (t (b* ((pstate (if token (unread-token pstate) pstate))) (retok (list nil) span pstate)))))))
Theorem:
(defthm type-qual-list-listp-of-parse-pointer.tyqualss (b* (((mv acl2::?erp ?tyqualss ?span ?new-pstate) (parse-pointer pstate))) (type-qual-list-listp tyqualss)) :rule-classes :rewrite)
Theorem:
(defthm spanp-of-parse-pointer.span (b* (((mv acl2::?erp ?tyqualss ?span ?new-pstate) (parse-pointer pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-parse-pointer.new-pstate (b* (((mv acl2::?erp ?tyqualss ?span ?new-pstate) (parse-pointer pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-pointer-uncond (b* (((mv acl2::?erp ?tyqualss ?span ?new-pstate) (parse-pointer pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-pointer-cond (b* (((mv acl2::?erp ?tyqualss ?span ?new-pstate) (parse-pointer pstate))) (implies (and (not erp) token?) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)