Parse an initializer declarator.
(parse-init-declarator pstate) → (mv erp initdeclor span new-pstate)
An initializer declarator consists of a declarator, optionally followed by an equal sign and an initializer.
Function:
(defun parse-init-declarator (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-init-declarator)) (declare (ignorable __function__)) (b* (((reterr) (irr-initdeclor) (irr-span) (irr-parstate)) ((erp declor span pstate) (parse-declarator pstate)) ((erp token & pstate) (read-token pstate))) (cond ((token-punctuatorp token "=") (b* (((erp initer last-span pstate) (parse-initializer pstate))) (retok (make-initdeclor :declor declor :init? initer) (span-join span last-span) pstate))) (t (b* ((pstate (if token (unread-token pstate) pstate))) (retok (make-initdeclor :declor declor :init? nil) span pstate)))))))
Theorem:
(defthm initdeclorp-of-parse-init-declarator.initdeclor (b* (((mv acl2::?erp ?initdeclor ?span ?new-pstate) (parse-init-declarator pstate))) (initdeclorp initdeclor)) :rule-classes :rewrite)
Theorem:
(defthm spanp-of-parse-init-declarator.span (b* (((mv acl2::?erp ?initdeclor ?span ?new-pstate) (parse-init-declarator pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-parse-init-declarator.new-pstate (b* (((mv acl2::?erp ?initdeclor ?span ?new-pstate) (parse-init-declarator pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-init-declarator-uncond (b* (((mv acl2::?erp ?initdeclor ?span ?new-pstate) (parse-init-declarator pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-init-declarator-cond (b* (((mv acl2::?erp ?initdeclor ?span ?new-pstate) (parse-init-declarator pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)