Parse a pointer.
(parse-pointer parstate) → (mv erp tyqualss span new-parstate)
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 (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-pointer)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) parstate) ((erp span parstate) (read-punctuator "*" parstate)) ((erp token & parstate) (read-token parstate))) (cond ((token-type-qualifier-p token) (b* ((parstate (unread-token parstate)) ((erp tyquals span2 parstate) (parse-type-qualifier-list parstate)) ((erp token & parstate) (read-token parstate))) (cond ((token-punctuatorp token "*") (b* ((parstate (unread-token parstate)) ((erp tyqualss last-span parstate) (parse-pointer parstate))) (retok (cons tyquals tyqualss) (span-join span last-span) parstate))) (t (b* ((parstate (if token (unread-token parstate) parstate))) (retok (list tyquals) (span-join span span2) parstate)))))) ((token-punctuatorp token "*") (b* ((parstate (unread-token parstate)) ((erp tyqualss last-span parstate) (parse-pointer parstate))) (retok (cons nil tyqualss) (span-join span last-span) parstate))) (t (b* ((parstate (if token (unread-token parstate) parstate))) (retok (list nil) span parstate)))))))
Theorem:
(defthm type-qual-list-listp-of-parse-pointer.tyqualss (b* (((mv acl2::?erp ?tyqualss ?span ?new-parstate) (parse-pointer parstate))) (type-qual-list-listp tyqualss)) :rule-classes :rewrite)
Theorem:
(defthm spanp-of-parse-pointer.span (b* (((mv acl2::?erp ?tyqualss ?span ?new-parstate) (parse-pointer parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-parse-pointer.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?tyqualss ?span ?new-parstate) (parse-pointer parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-pointer-uncond (b* (((mv acl2::?erp ?tyqualss ?span ?new-parstate) (parse-pointer parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-pointer-cond (b* (((mv acl2::?erp ?tyqualss ?span ?new-parstate) (parse-pointer parstate))) (implies (and (not erp) token?) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)