Parse attribute parameters.
(parse-attribute-parameters pstate) → (mv erp attrparams span new-pstate)
This is only used if GCC extensions are supported.
See the ABNF grammar rule for
If parsing is successful, we return a list of zero or more expressions, which are the parameters. We re-use parse-argument-expressions to parse the zero or more comma-separated expressions. This parsing function does exactly what is needed here.
Function:
(defun parse-attribute-parameters (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-attribute-parameters)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) (irr-parstate)) ((erp open-span pstate) (read-punctuator "(" pstate)) ((erp exprs & pstate) (parse-argument-expressions pstate)) ((erp close-span pstate) (read-punctuator ")" pstate))) (retok exprs (span-join open-span close-span) pstate))))
Theorem:
(defthm expr-listp-of-parse-attribute-parameters.attrparams (b* (((mv acl2::?erp ?attrparams ?span ?new-pstate) (parse-attribute-parameters pstate))) (expr-listp attrparams)) :rule-classes :rewrite)
Theorem:
(defthm spanp-of-parse-attribute-parameters.span (b* (((mv acl2::?erp ?attrparams ?span ?new-pstate) (parse-attribute-parameters pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-parse-attribute-parameters.new-pstate (b* (((mv acl2::?erp ?attrparams ?span ?new-pstate) (parse-attribute-parameters pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-attribute-parameters-uncond (b* (((mv acl2::?erp ?attrparams ?span ?new-pstate) (parse-attribute-parameters pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-attribute-parameters-cond (b* (((mv acl2::?erp ?attrparams ?span ?new-pstate) (parse-attribute-parameters pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)