hons

(in-package "ACL2")

(defmacro defn
  (f a &rest r)
  `(defun ,F ,A (declare (xargs :guard t)) ,@R))

(defmacro defnd
  (f a &rest r)
  `(defund ,F ,A (declare (xargs :guard t)) ,@R))

(defn hons-equal
  (x y)
  (declare (xargs :mode :logic))
  (equal x y))

(defn hons-assoc-equal
  (key alist)
  (declare (xargs :mode :logic))
  (cond ((atom alist) nil)
    ((and (consp (car alist)) (hons-equal key (caar alist))) (car alist))
    (t (hons-assoc-equal key (cdr alist)))))

(defn hons-get
  (key alist)
  (declare (xargs :mode :logic))
  (hons-assoc-equal key alist))

(defn hons-acons
  (key val alist)
  (declare (xargs :mode :logic))
  (cons (cons key val) alist))

(defmacro fast-alist-free-on-exit-raw
  (alist form)
  (declare (ignore alist))
  form)

(defn fast-alist-free
  (alist)
  (declare (xargs :mode :logic))
  alist)

(defmacro fast-alist-free-on-exit
  (alist form)
  `(return-last 'fast-alist-free-on-exit-raw ,ALIST ,FORM))

(defn hons-copy (x) (declare (xargs :mode :logic)) x)

(defn hons-copy-persistent (x) x)

(defn hons (x y) (cons x y))

(defn hons-equal-lite (x y) (equal x y))

(defn hons-clear (gc) (declare (ignore gc)) nil)

(defn hons-clear! (gc) (declare (ignore gc)) nil)

(defn hons-wash nil nil)

(defn hons-wash! nil nil)

(defn hons-summary nil nil)

(defmacro hons-resize
  (&key str-ht
    nil-ht
    cdr-ht
    cdr-ht-eql
    addr-ht
    other-ht
    sbits
    fal-ht
    persist-ht)
  `(hons-resize-fn ,STR-HT
    ,NIL-HT
    ,CDR-HT
    ,CDR-HT-EQL
    ,ADDR-HT
    ,OTHER-HT
    ,SBITS
    ,FAL-HT
    ,PERSIST-HT))

(defn hons-resize-fn
  (str-ht nil-ht
    cdr-ht
    cdr-ht-eql
    addr-ht
    other-ht
    sbits
    fal-ht
    persist-ht)
  (declare (ignore str-ht
      nil-ht
      cdr-ht
      cdr-ht-eql
      addr-ht
      other-ht
      sbits
      fal-ht
      persist-ht))
  nil)

(table hons 'slow-alist-warning :break)

(defmacro set-slow-alist-action
  (action)
  (declare (xargs :guard (or (eq action :warning) (eq action :break) (not action))))
  `(table hons 'slow-alist-warning ,ACTION))

(defn hons-acons!
  (key val alist)
  (cons (cons key val) alist))

(defn make-fast-alist (alist) alist)

(defn fast-alist-fork
  (alist ans)
  (cond ((atom alist) ans)
    ((atom (car alist)) (fast-alist-fork (cdr alist) ans))
    ((hons-assoc-equal (car (car alist)) ans) (fast-alist-fork (cdr alist) ans))
    (t (fast-alist-fork (cdr alist) (cons (car alist) ans)))))

(defn fast-alist-fork!
  (alist ans)
  (fast-alist-fork alist ans))

(defmacro hons-shrink-alist
  (alist ans)
  `(fast-alist-fork ,ALIST ,ANS))

(defmacro hons-shrink-alist!
  (alist ans)
  `(fast-alist-fork! ,ALIST ,ANS))

(add-macro-alias hons-shrink-alist fast-alist-fork)

(add-macro-alias hons-shrink-alist! fast-alist-fork!)

(defn fast-alist-clean
  (alist)
  (fast-alist-fork alist
    (if (consp alist)
      (cdr (last alist))
      alist)))

(defn fast-alist-clean! (alist) (fast-alist-clean alist))

(defn fast-alist-len
  (alist)
  (len (fast-alist-fork alist nil)))

(defn fast-alist-summary nil nil)

(defmacro with-fast-alist-raw
  (alist form)
  (declare (ignore alist))
  form)

(defmacro with-fast-alist
  (alist form)
  `(return-last 'with-fast-alist-raw ,ALIST ,FORM))

(defmacro with-stolen-alist-raw
  (alist form)
  (declare (ignore alist))
  form)

(defmacro with-stolen-alist
  (alist form)
  `(return-last 'with-stolen-alist-raw ,ALIST ,FORM))

(defn cons-subtrees
  (x al)
  (cond ((atom x) al)
    ((hons-get x al) al)
    (t (cons-subtrees (car x)
        (cons-subtrees (cdr x) (hons-acons x t al))))))

(defn number-subtrees
  (x)
  (len (cons-subtrees x 'number-subtrees)))

(defn flush-hons-get-hash-table-link
  (alist)
  (fast-alist-free alist))

(in-theory (disable (:executable-counterpart hons)
    (:executable-counterpart hons-copy)
    (:executable-counterpart hons-copy-persistent)
    (:executable-counterpart hons-summary)
    (:executable-counterpart fast-alist-summary)
    (:executable-counterpart hons-clear)
    (:executable-counterpart hons-clear!)
    (:executable-counterpart hons-wash)
    (:executable-counterpart hons-wash!)
    (:executable-counterpart hons-resize-fn)
    (:executable-counterpart hons-get)
    (:executable-counterpart hons-acons)
    (:executable-counterpart hons-acons!)
    (:executable-counterpart fast-alist-fork)
    (:executable-counterpart fast-alist-fork!)
    (:executable-counterpart fast-alist-clean)
    (:executable-counterpart fast-alist-clean!)
    (:executable-counterpart fast-alist-len)
    (:executable-counterpart fast-alist-free)
    (:executable-counterpart flush-hons-get-hash-table-link)))

(defun remove-keyword
  (word l)
  (declare (xargs :guard (and (keywordp word) (keyword-value-listp l))))
  (cond ((endp l) nil)
    ((eq word (car l)) (remove-keyword word (cddr l)))
    (t (list* (car l) (cadr l) (remove-keyword word (cddr l))))))