		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abs-declaration

Abstract a declaration to a top-level declaration.

Signature
(abs-declaration tree) → decl
Arguments: tree — Guard (abnf::treep tree).
Returns: decl — Type (topdecl-resultp decl).

Definitions and Theorems

Function: abs-declaration

(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: topdecl-resultp-of-abs-declaration

(defthm topdecl-resultp-of-abs-declaration
  (b* ((decl (abs-declaration tree)))
    (topdecl-resultp decl))
  :rule-classes :rewrite)

Theorem: abs-declaration-of-tree-fix-tree

(defthm abs-declaration-of-tree-fix-tree
  (equal (abs-declaration (abnf::tree-fix tree))
         (abs-declaration tree)))

Theorem: abs-declaration-tree-equiv-congruence-on-tree

(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)