Filtering...

alist-defuns

books/std/alists/alist-defuns

Included Books

define bstar list-defuns alist-equiv append-alist-keys append-alist-vals
other
(in-package "ACL2")
include-book
(include-book "std/util/define" :dir :system)
include-book
(include-book "std/util/bstar" :dir :system)
include-book
(include-book "../lists/list-defuns")
local
(local (include-book "alist-equiv"))
local
(local (include-book "append-alist-keys"))
local
(local (include-book "append-alist-vals"))
alist-keysfunction
(defund alist-keys
  (x)
  (declare (xargs :guard t))
  (cond ((atom x) nil)
    ((atom (car x)) (alist-keys (cdr x)))
    (t (cons (caar x) (alist-keys (cdr x))))))
alist-valsfunction
(defund alist-vals
  (x)
  (declare (xargs :guard t))
  (cond ((atom x) nil)
    ((atom (car x)) (alist-vals (cdr x)))
    (t (cons (cdar x) (alist-vals (cdr x))))))
hons-rassoc-equalfunction
(defund hons-rassoc-equal
  (val alist)
  (declare (xargs :guard t))
  (cond ((atom alist) nil)
    ((and (consp (car alist)) (equal val (cdar alist))) (car alist))
    (t (hons-rassoc-equal val (cdr alist)))))
alists-agreefunction
(defund alists-agree
  (keys al1 al2)
  "Do AL1 and AL2 agree on the value of every KEY in KEYS?"
  (declare (xargs :guard t))
  (or (atom keys)
    (and (equal (hons-get (car keys) al1) (hons-get (car keys) al2))
      (alists-agree (cdr keys) al1 al2))))
sub-alistpfunction
(defund sub-alistp
  (a b)
  "Is every key bound in A also bound to the same value in B?"
  (declare (xargs :guard t))
  (mbe :logic (alists-agree (alist-keys a) a b)
    :exec (with-fast-alist a
      (with-fast-alist b (alists-agree (alist-keys a) a b)))))
alist-equivfunction
(defund alist-equiv
  (a b)
  "Do A and B agree on the values of every key?"
  (declare (xargs :guard t))
  (mbe :logic (and (sub-alistp a b) (sub-alistp b a))
    :exec (with-fast-alist a
      (with-fast-alist b (and (sub-alistp a b) (sub-alistp b a))))))
other
(defequiv alist-equiv)
fal-extract1function
(defund fal-extract1
  (keys al)
  "Assumes AL is fast"
  (declare (xargs :guard t))
  (b* (((when (atom keys)) nil) (look (hons-get (car keys) al))
      ((when look) (cons look (fal-extract1 (cdr keys) al))))
    (fal-extract1 (cdr keys) al)))
fal-extractfunction
(defund fal-extract
  (keys al)
  "Makes AL fast if necessary"
  (declare (xargs :guard t
      :guard-hints (("Goal" :in-theory (enable fal-extract fal-extract1)))))
  (mbe :logic (b* (((when (atom keys)) nil) (look (hons-get (car keys) al))
        ((when look) (cons look (fal-extract (cdr keys) al))))
      (fal-extract (cdr keys) al))
    :exec (with-fast-alist al (fal-extract1 keys al))))
fal-extract-vals1function
(defund fal-extract-vals1
  (keys al)
  "Assumes AL is fast"
  (declare (xargs :guard t))
  (if (atom keys)
    nil
    (cons (cdr (hons-get (car keys) al))
      (fal-extract-vals1 (cdr keys) al))))
fal-extract-valsfunction
(defund fal-extract-vals
  (keys al)
  "Makes AL fast if necessary"
  (declare (xargs :guard t
      :guard-hints (("Goal" :in-theory (enable fal-extract-vals fal-extract-vals1)))))
  (mbe :logic (if (atom keys)
      nil
      (cons (cdr (hons-get (car keys) al))
        (fal-extract-vals (cdr keys) al)))
    :exec (with-fast-alist al (fal-extract-vals1 keys al))))
append-alist-vals-execfunction
(defund append-alist-vals-exec
  (x acc)
  (declare (xargs :guard t))
  (mbe :logic (if (atom x)
      acc
      (append-alist-vals-exec (cdr x) (revappend (cdar x) acc)))
    :exec (cond ((atom x) acc)
      ((atom (car x)) (append-alist-vals-exec (cdr x) acc))
      (t (append-alist-vals-exec (cdr x)
          (revappend-without-guard (cdar x) acc))))))
append-alist-valsfunction
(defund append-alist-vals
  (x)
  (declare (xargs :guard t))
  (mbe :logic (if (atom x)
      nil
      (append (cdar x) (append-alist-vals (cdr x))))
    :exec (reverse (append-alist-vals-exec x nil))))
append-alist-keys-execfunction
(defund append-alist-keys-exec
  (x acc)
  (declare (xargs :guard t))
  (mbe :logic (if (atom x)
      acc
      (append-alist-keys-exec (cdr x) (revappend (caar x) acc)))
    :exec (cond ((atom x) acc)
      ((atom (car x)) (append-alist-keys-exec (cdr x) acc))
      (t (append-alist-keys-exec (cdr x)
          (revappend-without-guard (caar x) acc))))))
append-alist-keysfunction
(defund append-alist-keys
  (x)
  (declare (xargs :guard t))
  (mbe :logic (if (atom x)
      nil
      (append (caar x) (append-alist-keys (cdr x))))
    :exec (reverse (append-alist-keys-exec x nil))))
other
(define worth-hashing1
  (x n)
  (declare (type (unsigned-byte 8) n)
    (xargs :guard t))
  (mbe :logic (>= (len x) n)
    :exec (cond ((eql n 0) t)
      ((atom x) nil)
      (t (worth-hashing1 (cdr x) (the (unsigned-byte 8) (1- n)))))))
local
(local (in-theory (enable worth-hashing1)))
other
(define worth-hashing
  (x)
  :returns bool
  :inline t
  (mbe :logic (>= (len x) 18)
    :exec (and (consp x) (worth-hashing1 (cdr x) 17))))
other
(define fal-all-boundp-fast
  (keys alist)
  (if (atom keys)
    t
    (and (hons-get (car keys) alist)
      (fal-all-boundp-fast (cdr keys) alist))))
other
(define fal-all-boundp-slow
  (keys alist)
  (if (atom keys)
    t
    (and (hons-assoc-equal (car keys) alist)
      (fal-all-boundp-slow (cdr keys) alist))))
other
(define fal-all-boundp
  (keys alist)
  (declare (xargs :guard t :verify-guards nil))
  (mbe :logic (if (atom keys)
      t
      (and (hons-assoc-equal (car keys) alist)
        (fal-all-boundp (cdr keys) alist)))
    :exec (if (atom keys)
      t
      (if (and (worth-hashing keys) (worth-hashing alist))
        (with-fast-alist alist (fal-all-boundp-fast keys alist))
        (fal-all-boundp-slow keys alist)))))
fal-all-boundp-fast-removalencapsulate
(encapsulate nil
  (local (in-theory (enable fal-all-boundp)))
  (defthm fal-all-boundp-fast-removal
    (equal (fal-all-boundp-fast keys alist)
      (fal-all-boundp keys alist))
    :hints (("Goal" :in-theory (enable fal-all-boundp-fast))))
  (defthm fal-all-boundp-slow-removal
    (equal (fal-all-boundp-slow keys alist)
      (fal-all-boundp keys alist))
    :hints (("Goal" :in-theory (enable fal-all-boundp-slow))))
  (verify-guards fal-all-boundp))
other
(define hons-put-assoc
  (key val x)
  (cond ((atom x) (cons (cons key val) x))
    ((atom (car x)) (cons (car x) (hons-put-assoc key val (cdr x))))
    ((equal key (caar x)) (cons (cons key val) (cdr x)))
    (t (cons (car x) (hons-put-assoc key val (cdr x))))))