		Search-engine friendly clone of the ACL2 documentation.

Numbered-names

Check-numbered-name

Check if a symbol is a numbered name.

Signature
(check-numbered-name name wrld) → (mv yes/no base index)
Arguments: name — Guard (symbolp name).; wrld — Guard (plist-worldp wrld).
Returns: yes/no — t iff name is a numbered name.
Type (booleanp yes/no).; base — Base symbol of name, or nil if yes/no is nil.
Type (symbolp base).; index — Numeric index of name, or 0 if it is the wildcard, or nil if yes/no is nil.
Type (maybe-natp index).

If successful, return its base symbol and index (or wildcard).

Definitions and Theorems

Function: check-numbered-name

(defun check-numbered-name (name wrld)
 (declare (xargs :guard (and (symbolp name)
                             (plist-worldp wrld))))
 (let ((__function__ 'check-numbered-name))
  (declare (ignorable __function__))
  (b*
    ((name-chars (explode (symbol-name name)))
     (index-start-chars
          (explode (get-numbered-name-index-start wrld)))
     (index-end-chars (explode (get-numbered-name-index-end wrld)))
     (wildcard-chars
          (explode (get-numbered-name-index-wildcard wrld)))
     (len-of-name-without-end-marker (- (len name-chars)
                                        (len index-end-chars)))
     ((unless (and (> len-of-name-without-end-marker 0)
                   (equal (subseq name-chars
                                  len-of-name-without-end-marker
                                  (len name-chars))
                          index-end-chars)))
      (mv nil nil nil))
     (name-chars-without-end-marker
          (take len-of-name-without-end-marker
                name-chars))
     (digits-of-index
          (reverse (str::take-leading-dec-digit-chars
                        (reverse name-chars-without-end-marker)))))
   (if digits-of-index
    (b*
     (((when (eql (car digits-of-index) #\0))
       (mv nil nil nil))
      (index (str::dec-digit-chars-value digits-of-index))
      (name-chars-without-index-and-end-marker
           (take (- (len name-chars-without-end-marker)
                    (len digits-of-index))
                 name-chars-without-end-marker))
      (len-of-base-of-name
           (- (len name-chars-without-index-and-end-marker)
              (len index-start-chars)))
      ((unless
        (and
         (> len-of-base-of-name 0)
         (equal
              (subseq name-chars-without-index-and-end-marker
                      len-of-base-of-name
                      (len name-chars-without-index-and-end-marker))
              index-start-chars)))
       (mv nil nil nil))
      (base-chars (take len-of-base-of-name
                        name-chars-without-index-and-end-marker))
      ((unless base-chars) (mv nil nil nil)))
     (mv t
         (intern-in-package-of-symbol (implode base-chars)
                                      name)
         index))
    (b*
     ((len-of-name-without-wildcard-and-end-marker
           (- (len name-chars-without-end-marker)
              (len wildcard-chars)))
      ((unless
        (and
          (> len-of-name-without-wildcard-and-end-marker
             0)
          (equal (subseq name-chars-without-end-marker
                         len-of-name-without-wildcard-and-end-marker
                         (len name-chars-without-end-marker))
                 wildcard-chars)))
       (mv nil nil nil))
      (name-chars-without-wildcard-and-end-marker
           (take len-of-name-without-wildcard-and-end-marker
                 name-chars-without-end-marker))
      (len-of-base-of-name
           (- (len name-chars-without-wildcard-and-end-marker)
              (len index-start-chars)))
      ((unless
        (and
         (> len-of-base-of-name 0)
         (equal
           (subseq name-chars-without-wildcard-and-end-marker
                   len-of-base-of-name
                   (len name-chars-without-wildcard-and-end-marker))
           index-start-chars)))
       (mv nil nil nil))
      (base-chars (take len-of-base-of-name
                        name-chars-without-wildcard-and-end-marker))
      ((unless base-chars) (mv nil nil nil)))
     (mv t
         (intern-in-package-of-symbol (implode base-chars)
                                      name)
         0))))))

Theorem: booleanp-of-check-numbered-name.yes/no

(defthm booleanp-of-check-numbered-name.yes/no
  (b* (((mv ?yes/no ?base ?index)
        (check-numbered-name name wrld)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: symbolp-of-check-numbered-name.base

(defthm symbolp-of-check-numbered-name.base
  (b* (((mv ?yes/no ?base ?index)
        (check-numbered-name name wrld)))
    (symbolp base))
  :rule-classes :rewrite)

Theorem: maybe-natp-of-check-numbered-name.index

(defthm maybe-natp-of-check-numbered-name.index
  (b* (((mv ?yes/no ?base ?index)
        (check-numbered-name name wrld)))
    (maybe-natp index))
  :rule-classes :rewrite)