/usr/share/acl2-4.3/books/misc/symbol-btree.lisp is in acl2-books-source 4.3-3.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 | ;; Original author: ???
;; Updated June 29, 2008 by Jared Davis to bring everything into logic mode.
;; A symbol-btree is a data structure of the form (symbol value left . right)
;; where left and right are symbol-btrees.
;; Example use:
#|
ACL2 !>(assign btree (symbol-alist-to-btree '((c . 3) (a . 1) (b . 2) (d . 4))))
(C 3 (B 2 (A 1 NIL)) D 4)
ACL2 !>(symbol-btree-lookup 'd (@ btree))
4
ACL2 !>(symbol-btree-lookup 'e (@ btree))
NIL
ACL2 !>(symbol-btree-lookup 'c (@ btree))
3
ACL2 !>
|#
;; This book is not very complete. There are tons of obvious theorems to prove,
;; like lookup of update, etc., and the equivalence of lookups after
;; rebalancing. But I (Jared) am too lazy to do this, and only wanted to bring
;; these functions into :logic mode. Also, I tried to maintain total
;; compatibility with the previous version, except for local events and the new
;; :logic mode functions.
(in-package "ACL2")
(local (include-book "ihs/quotient-remainder-lemmas" :dir :system))
(local (in-theory (disable floor)))
(local (defthm len-evens-<
(implies (consp (cdr x))
(< (len (evens x))
(len x)))
:hints (("Goal" :induct (evens x)))
:rule-classes :linear))
(local (defthm len-evens-<=
(<= (len (evens x))
(len x))
:hints (("Goal" :induct (evens x)))
:rule-classes :linear))
(local (defthm alistp-of-cdr
(implies (alistp x)
(alistp (cdr x)))))
(local (defthm true-listp-when-alistp
(implies (alistp x)
(true-listp x))))
(local (defthmd consp-under-iff-when-true-listp
(implies (true-listp x)
(iff (consp x)
x))))
(local (defthm consp-of-car-when-alistp
(implies (alistp x)
(equal (consp (car x))
(consp x)))))
(local (defthm symbol-alistp-of-append
(implies (and (symbol-alistp x)
(symbol-alistp y))
(symbol-alistp (append x y)))))
(local (defthm alistp-when-symbol-alistp
(implies (symbol-alistp x)
(alistp x))))
(defun symbol-btreep (x)
(declare (xargs :guard t))
(or (not x)
(and (true-listp x)
(symbolp (car x))
(or (null (caddr x))
(and (symbol-btreep (caddr x))
(symbol-< (car (caddr x))
(car x))))
(or (null (cdddr x))
(and (symbol-btreep (cdddr x))
(symbol-< (car x)
(car (cdddr x))))))))
(defun symbol-btree-lookup (key btree)
(declare (xargs :guard (and (symbolp key)
(symbol-btreep btree))))
(cond ((atom btree)
nil)
((eq key (car btree))
(cadr btree))
((symbol-< key (car btree))
(symbol-btree-lookup key (caddr btree)))
(t
(symbol-btree-lookup key (cdddr btree)))))
(defun merge-symbol-alist-< (l1 l2 acc)
(declare (xargs :guard (and (symbol-alistp l1)
(symbol-alistp l2)
(true-listp acc))
:measure (+ (len l1) (len l2))))
(cond ((endp l1) (revappend acc l2))
((endp l2) (revappend acc l1))
((symbol-< (caar l1) (caar l2))
(merge-symbol-alist-< (cdr l1) l2 (cons (car l1) acc)))
(t (merge-symbol-alist-< l1 (cdr l2) (cons (car l2) acc)))))
(defun merge-sort-symbol-alist-< (l)
(declare (xargs :guard (symbol-alistp l)
:verify-guards nil
:measure (len l)))
(cond ((endp (cdr l)) l)
(t (merge-symbol-alist-< (merge-sort-symbol-alist-< (evens l))
(merge-sort-symbol-alist-< (odds l))
nil))))
(defthm symbol-alistp-merge-symbol-alist-<
(implies (and (symbol-alistp x)
(symbol-alistp y)
(symbol-alistp acc))
(symbol-alistp (merge-symbol-alist-< x y acc))))
(defthm symbol-alistp-evens
(implies (symbol-alistp x)
(symbol-alistp (evens x)))
:hints (("Goal" :induct (evens x))))
(defthm symbol-alistp-merge-sort-symbol-alist-<
(implies (symbol-alistp x)
(symbol-alistp (merge-sort-symbol-alist-< x))))
(verify-guards merge-sort-symbol-alist-<)
(defun sorted-symbol-alist-to-symbol-btree (x n)
;; Return 2 values:
;; (1) the symbol-btree corresponding to first n entries of x; and
;; (2) the rest of x.
(declare (xargs :guard (and (natp n)
(alistp x))
:verify-guards nil))
(cond ((zp n)
(mv nil x))
((endp (cdr x))
(mv (list (caar x) (cdar x))
(cdr x)))
(t
(let ((n2 (floor n 2)))
(mv-let (left restx)
(sorted-symbol-alist-to-symbol-btree x n2)
(mv-let (right restx2)
(sorted-symbol-alist-to-symbol-btree (cdr restx) (- n (1+ n2)))
(mv (list* (caar restx)
(cdar restx)
left
right)
restx2)))))))
(local (defthm alistp-of-mv-nth-1-of-sorted-symbol-alist-to-symbol-btree
(implies (alistp x)
(equal (alistp (mv-nth 1 (sorted-symbol-alist-to-symbol-btree x n)))
t))))
(local (defthm consp-of-mv-nth-1-of-sorted-symbol-alist-to-symbol-btree
(implies (alistp x)
(equal (consp (mv-nth 1 (sorted-symbol-alist-to-symbol-btree x n)))
(if (mv-nth 1 (sorted-symbol-alist-to-symbol-btree x n))
t
nil)))))
(verify-guards sorted-symbol-alist-to-symbol-btree
:hints(("Goal"
:do-not '(generalize fertilize eliminate-destructors)
:in-theory (disable alistp)
)))
(defun symbol-alist-to-btree (alist)
(declare (xargs :guard (symbol-alistp alist)
:verify-guards nil))
(let ((n (length alist))
(sorted-alist (merge-sort-symbol-alist-< alist)))
(mv-let (ans empty)
(sorted-symbol-alist-to-symbol-btree sorted-alist n)
(declare (ignore empty))
ans)))
(verify-guards symbol-alist-to-btree)
(defun symbol-btree-update (key val btree)
(declare (xargs :guard (and (symbolp key)
(symbol-btreep btree))))
(cond
((endp btree)
(list* key val nil nil))
((eq key (car btree))
(list* key val (caddr btree) (cdddr btree)))
((symbol-< key (car btree))
(list* (car btree) (cadr btree)
(symbol-btree-update key val (caddr btree))
(cdddr btree)))
(t
(list* (car btree) (cadr btree)
(caddr btree)
(symbol-btree-update key val (cdddr btree))))))
(defun symbol-btree-to-alist (x)
(declare (xargs :guard (symbol-btreep x)
:verify-guards nil))
(if (consp x)
(cons (cons (car x) (cadr x))
(append (symbol-btree-to-alist (caddr x))
(symbol-btree-to-alist (cdddr x))))
nil))
(defthm true-listp-symbol-btree-to-alist
(true-listp (symbol-btree-to-alist btree))
:rule-classes :type-prescription)
(verify-guards symbol-btree-to-alist)
(defun rebalance-symbol-btree (btree)
(declare (xargs :guard (symbol-btreep btree)))
(symbol-alist-to-btree
(symbol-btree-to-alist btree)))
|