Abstract a
(abs-declaration tree) → decl
Function:
(defun abs-declaration (tree) (declare (xargs :guard (abnf::treep tree))) (let ((__function__ 'abs-declaration)) (declare (ignorable __function__)) (b* (((okf tree) (abnf::check-tree-nonleaf-1-1 tree "declaration")) ((okf rulename?) (abnf::check-tree-nonleaf? tree))) (cond ((equal rulename? "function-declaration") (b* (((okf fun) (abs-function-declaration tree))) (topdecl-function fun))) ((equal rulename? "transition-declaration") (b* (((okf fun) (abs-transition-declaration tree))) (topdecl-function fun))) ((equal rulename? "struct-declaration") (b* (((okf sdecl) (abs-struct-declaration tree))) (topdecl-struct sdecl))) ((equal rulename? "record-declaration") (b* (((okf rdecl) (abs-record-declaration tree))) (topdecl-struct rdecl))) ((equal rulename? "mapping-declaration") (b* (((okf mdecl) (abs-mapping-declaration tree))) (topdecl-mapping mdecl))) (t (reserrf (list :found-subtree (abnf::tree-info-for-error tree))))))))
Theorem:
(defthm topdecl-resultp-of-abs-declaration (b* ((decl (abs-declaration tree))) (topdecl-resultp decl)) :rule-classes :rewrite)
Theorem:
(defthm abs-declaration-of-tree-fix-tree (equal (abs-declaration (abnf::tree-fix tree)) (abs-declaration tree)))
Theorem:
(defthm abs-declaration-tree-equiv-congruence-on-tree (implies (abnf::tree-equiv tree tree-equiv) (equal (abs-declaration tree) (abs-declaration tree-equiv))) :rule-classes :congruence)