hons-help

(in-package "ACL2")

(set-state-ok t)

(defsection make-fal
  :parents (fast-alists)
  :short "Make a fast alist out of an alist."
  :long "<p>Note: it is usually better to use @(see make-fast-alist).</p>

<p>@('(make-fal al name)') copies the alist AL with @(see hons-acons) to make a
fast alist that ends with NAME.</p>

<p>Typically @('name') is an atom, and it becomes the final @(see cdr) of the
new fast alist.  Some atoms have special meanings, e.g., they act as size
hints; see @(see hons-acons) for details.</p>

<p>However, @('name') can also be an existing fast alist.  In this case, this
fast alist is extended with the new pairs from @('al'), using @(see
hons-acons).  Note that @('name') will no longer be fast after the call of
@('make-fal').</p>

<p>There's nothing under-the-hood about @('make-fal'); it just repeatedly calls
@('hons-acons').  The built-in function @(see make-fast-alist) is generally
more efficient and can be nicer to reason about because logically it is just
the identity.  On the other hand, @('make-fast-alist') can't be used to extend
an existing fast alist like @('make-fal').</p>"
  (defn make-fal
    (al name)
    (cond ((atom al) name)
      ((atom (car al)) (make-fal (cdr al) name))
      (t (hons-acons (caar al) (cdar al) (make-fal (cdr al) name))))))

(defsection ansfl
  :parents (fast-alists)
  :short "@('(ANSFL X Y)') returns the single value @('X') after first flushing
          the fast hash table backing for @('Y'), if @('Y') is a fast alist."
  :long "<p>Thus</p>
         @({(ANSFL X Y) = X})
         <p>@('X') must be a form that returns a single value.</p>"
  (defmacro ansfl
    (x y)
    `((lambda (ansfl-do-not-use-elsewhere1 ansfl-do-not-use-elsewhere2)
       (declare (ignore ansfl-do-not-use-elsewhere2))
       ansfl-do-not-use-elsewhere1) ,X
      (flush-hons-get-hash-table-link ,Y))))

(defn ansfl-last-list
  (r bindings)
  (if (atom bindings)
    r
    `(ansfl ,(ANSFL-LAST-LIST R (GENTLE-CDR BINDINGS))
      ,(GENTLE-CAAR BINDINGS))))

(defn hons-put-list
  (keys values l)
  (if (atom keys)
    l
    (let* ((cp (consp values)) (val (if cp
            (car values)
            values))
        (next-values (if cp
            (cdr values)
            values))
        (old-pair (hons-get (car keys) l))
        (redundant (and old-pair (hons-equal val (cdr old-pair))))
        (next-l (if redundant
            l
            (hons-acons (car keys) val l))))
      (hons-put-list (cdr keys) next-values next-l))))

(defn hons-binary-append
  (x y)
  (mbe :logic (append x y)
    :exec (if (atom x)
      y
      (hons (car x) (hons-binary-append (cdr x) y)))))

(defsection hons-append
  :parents (fast-alists append)
  :short "APPEND using HONS instead of CONS"
  (defmacro hons-append
    (x y &rest rst)
    (xxxjoin 'hons-binary-append (cons x (cons y rst)))))

(defsection hons-revappend
  :parents (fast-alists revappend)
  :short "REVAPPEND using HONS instead of CONS"
  (defn hons-revappend
    (x y)
    (mbe :logic (revappend x y)
      :exec (if (atom x)
        y
        (hons-revappend (cdr x) (hons (car x) y))))))

(defsection hons-reverse
  :parents (fast-alists reverse)
  :short "REVERSE using HONS instead of CONS"
  (defn hons-reverse
    (x)
    (mbe :logic (reverse x)
      :exec (if (stringp x)
        (reverse x)
        (hons-revappend x nil)))))

(defsection hons-list
  :parents (fast-alists list)
  :short "(LIST ...) using HONS instead of CONS"
  (defmacro hons-list
    (&rest x)
    (if (atom x)
      nil
      (list 'hons (car x) (cons 'hons-list (cdr x))))))

(defsection hons-list*
  :parents (fast-alists list*)
  :short "(LIST* ...) using HONS instead of CONS"
  (defmacro hons-list*
    (&rest x)
    (cond ((atom x) x)
      ((atom (cdr x)) (car x))
      (t (list 'hons (car x) (cons 'hons-list* (cdr x)))))))

(defsection hons-make-list
  :parents (fast-alists make-list)
  :short "Like @(see make-list), but produces honses."
  (defn hons-make-list-acc
    (n val ac)
    (mbe :logic (make-list-ac n val ac)
      :exec (if (not (posp n))
        ac
        (hons-make-list-acc (1- n) val (hons val ac)))))
  (defmacro hons-make-list
    (size &key initial-element)
    `(hons-make-list-acc ,SIZE ,INITIAL-ELEMENT nil)))

(defsection hons-member-equal
  :parents (fast-alists member-equal)
  :short "MEMBER-EQUAL using HONS-EQUAL for each equality check"
  (defn hons-member-equal
    (x y)
    (mbe :logic (member-equal x y)
      :exec (cond ((atom y) nil)
        ((hons-equal x (car y)) y)
        (t (hons-member-equal x (cdr y)))))))

(defsection hons-dups-p1
  :parents (fast-alists)
  :short "Basic duplicates check; table is a fast alist that associates
          already-seen elements with t."
  (defn hons-dups-p1
    (l tab)
    (cond ((atom l) (ansfl nil tab))
      ((hons-get (car l) tab) (ansfl l tab))
      (t (hons-dups-p1 (cdr l) (hons-acons (car l) t tab))))))

(defn hons-dups-p (l) (hons-dups-p1 l '*hons-dups-p*))

(defn hons-duplicates1
  (l tab)
  (cond ((atom l) (ansfl nil tab))
    ((hons-get (car l) tab) (cons (car l) (hons-duplicates1 (cdr l) tab)))
    (t (hons-duplicates1 (cdr l) (hons-acons (car l) t tab)))))

(defn hons-duplicates (l) (hons-duplicates1 l nil))

(defsection hons-sublis-aux
  :parents (hons-sublis)
  :short "Memoized core of @(see hons-sublis)."
  (defun hons-sublis-aux
    (fal x)
    (declare (xargs :guard t))
    (if (atom x)
      (let ((pair (hons-get x fal)))
        (if pair
          (cdr pair)
          x))
      (cons (hons-sublis-aux fal (car x))
        (hons-sublis-aux fal (cdr x)))))
  (encapsulate nil
    (local (defthm lemma
        (implies (alistp x)
          (equal (hons-assoc-equal a x) (assoc a x)))
        :hints (("Goal" :induct (len x)))))
    (defthm hons-sublis-aux-removal
      (implies (alistp fal)
        (equal (hons-sublis-aux fal x) (sublis fal x)))))
  (memoize 'hons-sublis-aux :condition '(consp x)))

(defsection hons-sublis
  :parents (hons sublis)
  :short "@(tsee memoize)d version of SUBLIS which uses @(see fast-alists)."
  :long "<p>@('(hons-sublis fal x)') is like @(see sublis), but may be faster
in two ways.</p>

<ol>

<li>It uses @(see hons-get) instead of @(see assoc), which may provide a
speedup when the alist in question is very long.  Note that for good
performance, the fast-alist argument, @('fal'), must be a valid
fast-alist.</li>

<li>It uses a memoized auxiliary function, which may provide a speedup when the
tree argument, @('x'), contains large, shared structures.</li>

</ol>"
  (defun hons-sublis
    (fal x)
    (declare (xargs :guard t))
    (let ((ret (hons-sublis-aux fal x)))
      (prog2$ (clear-memoize-table 'hons-sublis-aux) ret)))
  (defthm hons-sublis-removal
    (implies (alistp fal)
      (equal (hons-sublis fal x) (sublis fal x)))))

(defn hons-int1
  (l1 al2)
  (cond ((atom l1) nil)
    ((hons-get (car l1) al2) (cons (car l1) (hons-int1 (cdr l1) al2)))
    (t (hons-int1 (cdr l1) al2))))

(defn hons-intersection2
  (l1 l2)
  (cond ((atom l1) nil)
    ((hons-member-equal (car l1) l2) (cons (car l1) (hons-intersection2 (cdr l1) l2)))
    (t (hons-intersection2 (cdr l1) l2))))

(defn hons-intersection
  (l1 l2)
  (cond ((worth-hashing l2) (with-fast-list fl2
        l2
        '*hons-intersection-alist*
        (hons-int1 l1 fl2)))
    (t (hons-intersection2 l1 l2))))

(defn hons-intersect-p1
  (l1 al2)
  (cond ((atom l1) nil)
    ((hons-get (car l1) al2) t)
    (t (hons-intersect-p1 (cdr l1) al2))))

(defn hons-intersect-p2
  (l1 l2)
  (cond ((atom l1) nil)
    ((hons-member-equal (car l1) l2) t)
    (t (hons-intersect-p2 (cdr l1) l2))))

(defn hons-intersect-p
  (l1 l2)
  (cond ((and (worth-hashing l1) (worth-hashing l2)) (with-fast-list fl2
        l2
        '*hons-intersect-p-alist*
        (hons-intersect-p1 l1 fl2)))
    (t (hons-intersect-p2 l1 l2))))

(defn hons-sd1
  (l1 al2)
  (cond ((atom l1) nil)
    ((hons-get (car l1) al2) (hons-sd1 (cdr l1) al2))
    (t (cons (car l1) (hons-sd1 (cdr l1) al2)))))

(defn hons-set-diff2
  (l1 l2)
  (cond ((atom l1) nil)
    ((hons-member-equal (car l1) l2) (hons-set-diff2 (cdr l1) l2))
    (t (cons (car l1) (hons-set-diff2 (cdr l1) l2)))))

(defn hons-set-diff
  (l1 l2)
  (cond ((worth-hashing l2) (with-fast-list fl2
        l2
        '*hons-set-diff-alist*
        (hons-sd1 l1 fl2)))
    (t (hons-set-diff2 l1 l2))))

(defn hons-union1
  (l1 al2 acc)
  (cond ((atom l1) acc)
    ((hons-get (car l1) al2) (hons-union1 (cdr l1) al2 acc))
    (t (hons-union1 (cdr l1) al2 (cons (car l1) acc)))))

(defn hons-union2
  (l1 l2 acc)
  (cond ((atom l1) acc)
    ((hons-member-equal (car l1) l2) (hons-union2 (cdr l1) l2 acc))
    (t (hons-union2 (cdr l1) l2 (cons (car l1) acc)))))

(defn hons-un1
  (l1 fl2)
  (cond ((atom l1) fl2)
    ((hons-get (car l1) fl2) (hons-un1 (cdr l1) fl2))
    (t (hons-un1 (cdr l1) (hons-acons (car l1) t fl2)))))

(defn hons-union
  (l1 l2)
  (cond ((atom l1) l2)
    ((atom l2) l1)
    ((atom (cdr l1)) (if (hons-member-equal (car l1) l2)
        l2
        (cons (car l1) l2)))
    ((atom (cdr l2)) (if (hons-member-equal (car l2) l1)
        l1
        (cons (car l2) l1)))
    (t (let ((len1 (len l1)) (len2 (len l2)))
        (cond ((and (>= len2 len1) (>= len1 *magic-number-for-hashing*)) (with-fast-list fl2
              l2
              '*hons-union*
              (hons-union1 l1 fl2 l2)))
          ((and (>= len1 len2) (>= len2 *magic-number-for-hashing*)) (with-fast-list fl1
              l1
              '*hons-union*
              (hons-union1 l2 fl1 l1)))
          (t (hons-union2 l1 l2 l2)))))))

(defn hons-union-list
  (l)
  (if (atom l)
    nil
    (hons-union (car l) (hons-union-list (cdr l)))))

(defn hons-subset1
  (l al)
  (or (atom l)
    (and (hons-get (car l) al) (hons-subset1 (cdr l) al))))

(defn hons-subset2
  (l1 l2)
  (cond ((atom l1) t)
    ((hons-member-equal (car l1) l2) (hons-subset2 (cdr l1) l2))))

(defn hons-subset
  (l1 l2)
  (cond ((worth-hashing l2) (with-fast-list fl2
        l2
        '*hons-subset-alist*
        (hons-subset1 l1 fl2)))
    (t (hons-subset2 l1 l2))))

(defn hons-set-equal
  (l1 l2)
  (and (hons-subset l1 l2) (hons-subset l2 l1)))

(defstub fail (x y) t)