Attempts to eat an identifier and a following open parenthesis, and build an identifier AST node.
(parse-identifier-and-open-paren tokens) → (mv result-ast tokens-after-id-and-open-paren)
Function:
(defun parse-identifier-and-open-paren (tokens) (declare (xargs :guard (abnf::tree-listp tokens))) (let ((__function__ 'parse-identifier-and-open-paren)) (declare (ignorable __function__)) (b* (((when (endp tokens)) (mv (reserrf "no id here") nil)) ((mv id-ast? tokens-after-identifier-or-error) (parse-identifier tokens)) ((when (or (null id-ast?) (reserrp tokens-after-identifier-or-error))) (mv (reserrf "no id here 2") nil)) (tokens-after-paren-or-error (parse-symbol "(" tokens-after-identifier-or-error)) ((when (reserrp tokens-after-paren-or-error)) (mv (reserrf "no start of funcall here") nil))) (mv id-ast? tokens-after-paren-or-error))))
Theorem:
(defthm identifier-resultp-of-parse-identifier-and-open-paren.result-ast (b* (((mv ?result-ast ?tokens-after-id-and-open-paren) (parse-identifier-and-open-paren tokens))) (identifier-resultp result-ast)) :rule-classes :rewrite)
Theorem:
(defthm tree-listp-of-parse-identifier-and-open-paren.tokens-after-id-and-open-paren (b* (((mv ?result-ast ?tokens-after-id-and-open-paren) (parse-identifier-and-open-paren tokens))) (abnf::tree-listp tokens-after-id-and-open-paren)) :rule-classes :rewrite)
Theorem:
(defthm len-of-parse-identifier-and-open-paren-< (b* (((mv ?result-ast ?tokens-after-id-and-open-paren) (parse-identifier-and-open-paren tokens))) (implies (not (reserrp result-ast)) (< (len tokens-after-id-and-open-paren) (len tokens)))) :rule-classes :linear)