		Search-engine friendly clone of the ACL2 documentation.

Skip-detection

Make-sd-patalist

(make-sd-patalist x) separates a sd-keylist-p by their patterns, producing a sd-patalist-p.

We return a fast alist which has no shadowed pairs.

Definitions and Theorems

Function: make-sd-patalist-aux

(defun make-sd-patalist-aux (x acc)
  (declare (xargs :guard (and (sd-keylist-p x)
                              (sd-patalist-p acc))))
  (if (atom x)
      acc
    (let* ((key (car x))
           (pat (sd-key->pat key))
           (entry (cdr (hons-get pat acc)))
           (acc (hons-acons pat (cons key entry) acc)))
      (make-sd-patalist-aux (cdr x) acc))))

Theorem: alistp-of-make-sd-patalist-aux

(defthm alistp-of-make-sd-patalist-aux
  (implies (alistp acc)
           (alistp (make-sd-patalist-aux x acc))))

Theorem: sd-patalist-p-of-make-sd-patalist-aux

(defthm sd-patalist-p-of-make-sd-patalist-aux
  (implies (and (force (sd-keylist-p x))
                (force (sd-patalist-p acc)))
           (sd-patalist-p (make-sd-patalist-aux x acc))))

Function: make-sd-patalist

(defun make-sd-patalist (x)
  (declare (xargs :guard (sd-keylist-p x)))
  (b* ((unclean (make-sd-patalist-aux x nil))
       (clean (hons-shrink-alist unclean nil))
       (- (flush-hons-get-hash-table-link unclean)))
    clean))

Theorem: sd-patalist-p-of-make-sd-patalist

(defthm sd-patalist-p-of-make-sd-patalist
  (implies (force (sd-keylist-p x))
           (sd-patalist-p (make-sd-patalist x))))

Theorem: alistp-of-make-sd-patalist

(defthm alistp-of-make-sd-patalist
  (alistp (make-sd-patalist x)))