		Search-engine friendly clone of the ACL2 documentation.

Tree-utilities

Check-tree-schars

Check if an ABNF tree is a leaf tree whose natural numbers case-sensitively match a string of ACL2 characters.

Signature
(check-tree-schars tree chars) → pass
Arguments: tree — Guard (treep tree).; chars — Guard (common-lisp::stringp chars).
Returns: pass — Type (pass-resultp pass).

Definitions and Theorems

Function: check-tree-schars

(defun check-tree-schars (tree chars)
  (declare (xargs :guard (and (treep tree)
                              (common-lisp::stringp chars))))
  (let ((__function__ 'check-tree-schars))
    (declare (ignorable __function__))
    (b* (((okf nats) (check-tree-leafterm tree)))
      (if (nats-match-sensitive-chars-p nats (explode chars))
          :pass
        (reserrf (list :required
                       :schars (str-fix chars)
                       :found (tree-info-for-error tree)))))))

Theorem: pass-resultp-of-check-tree-schars

(defthm pass-resultp-of-check-tree-schars
  (b* ((pass (check-tree-schars tree chars)))
    (pass-resultp pass))
  :rule-classes :rewrite)

Theorem: check-tree-schars-of-tree-fix-tree

(defthm check-tree-schars-of-tree-fix-tree
  (equal (check-tree-schars (tree-fix tree)
                            chars)
         (check-tree-schars tree chars)))

Theorem: check-tree-schars-tree-equiv-congruence-on-tree

(defthm check-tree-schars-tree-equiv-congruence-on-tree
  (implies (tree-equiv tree tree-equiv)
           (equal (check-tree-schars tree chars)
                  (check-tree-schars tree-equiv chars)))
  :rule-classes :congruence)

Theorem: check-tree-schars-of-str-fix-chars

(defthm check-tree-schars-of-str-fix-chars
  (equal (check-tree-schars tree (str-fix chars))
         (check-tree-schars tree chars)))

Theorem: check-tree-schars-streqv-congruence-on-chars

(defthm check-tree-schars-streqv-congruence-on-chars
  (implies (acl2::streqv chars chars-equiv)
           (equal (check-tree-schars tree chars)
                  (check-tree-schars tree chars-equiv)))
  :rule-classes :congruence)