		Search-engine friendly clone of the ACL2 documentation.

Skip-detection

Sd-keygen

(sd-keygen x acc) derives a list of sd-key-ps from x, a wire name, and accumulates them into acc.

Definitions and Theorems

Function: sd-keygen-aux

(defun sd-keygen-aux (n x xl acc)
  (declare (xargs :guard (and (natp n)
                              (natp xl)
                              (stringp x)
                              (= xl (length x))
                              (sd-keylist-p acc))))
  (b* ((n (lnfix n))
       (x (mbe :logic (string-fix x) :exec x))
       (xl (mbe :logic (length x) :exec xl))
       ((when (>= n xl))
        (let* ((x-honsed (hons-copy x))
               (key (make-sd-key :pat x-honsed
                                 :index nil
                                 :orig x-honsed)))
          (cons key acc)))
       (char (char x n))
       ((unless (str::dec-digit-char-p char))
        (sd-keygen-aux (+ 1 n) x xl acc))
       ((mv val len)
        (str::parse-nat-from-string x 0 0 n xl))
       (prefix (subseq x 0 n))
       (suffix (subseq x (min xl (+ n len)) nil))
       (pat (cat prefix "*" suffix))
       (key (make-sd-key :pat (hons-copy pat)
                         :index val
                         :orig x)))
    (sd-keygen-aux (+ len n)
                   x xl (cons key acc))))

Function: sd-keygen

(defun sd-keygen (x acc)
  (declare (xargs :guard (and (stringp x) (sd-keylist-p acc))))
  (sd-keygen-aux 0 x (length x) acc))

Theorem: sd-keylist-p-of-sd-keygen

(defthm sd-keylist-p-of-sd-keygen
  (implies (force (sd-keylist-p acc))
           (sd-keylist-p (sd-keygen x acc))))

Function: sd-keygen-list

(defun sd-keygen-list (x acc)
  (declare (xargs :guard (and (string-listp x)
                              (sd-keylist-p acc))))
  (if (atom x)
      acc
    (let ((acc (sd-keygen (car x) acc)))
      (sd-keygen-list (cdr x) acc))))

Theorem: sd-keylist-p-of-sd-keygen-list

(defthm sd-keylist-p-of-sd-keygen-list
  (implies (force (sd-keylist-p acc))
           (sd-keylist-p (sd-keygen-list x acc))))