Parses zero or more occurrences of '"." identifier' and returns a list of identifier AST nodes.
(parse-*-.-identifier tokens) → (mv result-asts tokens-after-identifiers)
Function:
(defun parse-*-.-identifier (tokens) (declare (xargs :guard (abnf::tree-listp tokens))) (let ((__function__ 'parse-*-.-identifier)) (declare (ignorable __function__)) (b* ((tokens (abnf::tree-list-fix tokens)) ((when (endp tokens)) (mv nil tokens)) (tokens-after-dot-or-err (parse-symbol "." tokens)) ((when (reserrp tokens-after-dot-or-err)) (mv nil tokens)) ((mv first-id tokens-after-first-id) (parse-identifier tokens-after-dot-or-err)) ((when (null first-id)) (mv nil tokens)) ((when (reserrp tokens-after-first-id)) (mv nil tokens)) ((unless (identifierp first-id)) (mv nil tokens)) ((mv rest-ids tokens-after-rest-ids) (parse-*-.-identifier tokens-after-first-id))) (mv (cons first-id rest-ids) tokens-after-rest-ids))))
Theorem:
(defthm identifier-listp-of-parse-*-.-identifier.result-asts (b* (((mv ?result-asts ?tokens-after-identifiers) (parse-*-.-identifier tokens))) (identifier-listp result-asts)) :rule-classes :rewrite)
Theorem:
(defthm tree-listp-of-parse-*-.-identifier.tokens-after-identifiers (b* (((mv ?result-asts ?tokens-after-identifiers) (parse-*-.-identifier tokens))) (abnf::tree-listp tokens-after-identifiers)) :rule-classes :rewrite)
Theorem:
(defthm len-of-parse-*-.-identifier (b* (((mv ?result-asts ?tokens-after-identifiers) (parse-*-.-identifier tokens))) (<= (len tokens-after-identifiers) (len tokens))) :rule-classes :linear)