		Search-engine friendly clone of the ACL2 documentation.

Abnf-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 (abnf::treep tree).; chars — Guard (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 (abnf::treep tree)
                             (stringp chars))))
 (let ((__function__ 'check-tree-schars))
  (declare (ignorable __function__))
  (b* (((okf nats) (check-tree-leafterm tree)))
    (if
     (abnf::nats-match-sensitive-chars-p nats (acl2::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 (abnf::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 (abnf::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)