(abs-primary-expression-alt tree) → expr-or-err
Function:
(defun abs-primary-expression-alt (tree) (declare (xargs :guard (abnf::treep tree))) (let ((__function__ 'abs-primary-expression-alt)) (declare (ignorable __function__)) (b* (((unless (cst-matchp tree "primary-expression")) (reserrf (list :expecting-primary-expression (tree-info-for-error tree)))) (alternate-index (cst-primary-expression-conc? tree)) (subtree (case alternate-index (1 (cst-primary-expression-conc1-rep-elem tree)) (2 (cst-primary-expression-conc2-rep-elem tree)) (otherwise (reserrf (list :malformed-primary-express-tree (tree-info-for-error tree)))))) ((when (reserrp subtree)) subtree)) (case alternate-index (1 (let ((id-or-err (abs-identifier subtree))) (if (stringp id-or-err) (make-expression-var :name id-or-err) id-or-err))) (2 (let ((int-or-err (abs-integer subtree))) (if (integerp int-or-err) (make-expression-const :value int-or-err) int-or-err)))))))
Theorem:
(defthm expression-resultp-of-abs-primary-expression-alt (b* ((expr-or-err (abs-primary-expression-alt tree))) (expression-resultp expr-or-err)) :rule-classes :rewrite)
Theorem:
(defthm abs-primary-expression-alt-of-tree-fix-tree (equal (abs-primary-expression-alt (abnf::tree-fix tree)) (abs-primary-expression-alt tree)))
Theorem:
(defthm abs-primary-expression-alt-tree-equiv-congruence-on-tree (implies (abnf::tree-equiv tree tree-equiv) (equal (abs-primary-expression-alt tree) (abs-primary-expression-alt tree-equiv))) :rule-classes :congruence)