		Search-engine friendly clone of the ACL2 documentation.

Tree-utilities

Tree-info-for-error

Information about a tree for an error result.

Signature
(tree-info-for-error tree) → info
Arguments: tree — Guard (treep tree).

When an ABNF tree does not satisfy certain conditions, it is useful to return some information about the tree in the error result. Since ABNF trees may be large, in general we do not want to put the whole tree into the error result. Instead, we want to put some summary information. This function calculates that information.

Definitions and Theorems

Function: tree-info-for-error

(defun tree-info-for-error (tree)
  (declare (xargs :guard (treep tree)))
  (let ((__function__ 'tree-info-for-error))
    (declare (ignorable __function__))
    (tree-case tree
               :leafterm (list :leafterm tree.get)
               :leafrule (list :leafrule tree.get)
               :nonleaf (list :nonleaf
                              tree.rulename? (len tree.branches)))))

Theorem: tree-info-for-error-of-tree-fix-tree

(defthm tree-info-for-error-of-tree-fix-tree
  (equal (tree-info-for-error (tree-fix tree))
         (tree-info-for-error tree)))

Theorem: tree-info-for-error-tree-equiv-congruence-on-tree

(defthm tree-info-for-error-tree-equiv-congruence-on-tree
  (implies (tree-equiv tree tree-equiv)
           (equal (tree-info-for-error tree)
                  (tree-info-for-error tree-equiv)))
  :rule-classes :congruence)