hons-extra - ACL2 Book

Included Books

bstar

other

(in-package "ACL2")

include-book

(include-book "std/util/bstar" :dir :system)

other

(defxdoc with-fast-alists
  :parents (fast-alists)
  :short "Concisely call @(see with-fast-alist) on multiple alists."
  :long "<p>Example:</p>
@({
   (with-fast-alists (a b c) form)
})

<p>is just shorthand for:</p>

@({
   (with-fast-alist a
    (with-fast-alist b
     (with-fast-alist c
      form)))
})

@(def with-fast-alists)
@(def with-fast-alists-fn)")

with-fast-alists-fnfunction

(defun with-fast-alists-fn
  (alists form)
  (if (atom alists)
    form
    `(with-fast-alist ,(CAR ALISTS)
      ,(WITH-FAST-ALISTS-FN (CDR ALISTS) FORM))))

with-fast-alistsmacro

(defmacro with-fast-alists
  (alists form)
  (with-fast-alists-fn alists form))

other

(def-b*-binder with-fast
  :short "@(see b*) binder to make some alists fast for the remainder of the
          @('b*') form."
  :decls ((declare (xargs :guard (not forms))
     (ignorable forms)))
  :body `(with-fast-alists ,ARGS ,REST-EXPR))

alist-of-alistspfunction

(defun alist-of-alistsp
  (lst)
  (declare (xargs :guard t))
  (cond ((atom lst) (null lst))
    ((and (consp (car lst)) (alistp (cdar lst))) (alist-of-alistsp (cdr lst)))
    (t nil)))

make-fast-alist-of-alistsfunction

(defun make-fast-alist-of-alists
  (lst)
  (declare (xargs :guard (alist-of-alistsp lst) :mode :logic))
  (cond ((atom lst) lst)
    (t (let* ((current-entry (car lst)))
        (cond ((atom current-entry) (prog2$ (er hard
                'make-fast-alist-of-alists
                "Guard of alist-of-alistp not met.  ~x0 was an atom ~
                          when it needed to be an [inner] alist."
                current-entry)
              lst))
          (t (let* ((current-entry-key (car current-entry)) (current-entry-val (cdr current-entry))
                (new-current-entry-val (make-fast-alist current-entry-val)))
              (hons-acons current-entry-key
                new-current-entry-val
                (make-fast-alist-of-alists (cdr lst))))))))))

make-fast-alist-of-alists-identitytheorem

(defthm make-fast-alist-of-alists-identity
  (equal (make-fast-alist-of-alists lst) lst))

in-theory

(in-theory (disable make-fast-alist-of-alists))

other

(defxdoc with-stolen-alists
  :parents (fast-alists)
  :short "Concisely call @(see with-stolen-alist) on multiple alists."
  :long "<p>Example:</p>
@({
    (with-stolen-alists (a b c) form)
})

<p>is just shorthand for:</p>

@({
    (with-stolen-alist a
      (with-stolen-alist b
        (with-stolen-alist c
          form)))
})

@(def with-stolen-alists)
@(def with-stolen-alists-fn)")

with-stolen-alists-fnfunction

(defun with-stolen-alists-fn
  (alists form)
  (if (atom alists)
    form
    `(with-stolen-alist ,(CAR ALISTS)
      ,(WITH-STOLEN-ALISTS-FN (CDR ALISTS) FORM))))

with-stolen-alistsmacro

(defmacro with-stolen-alists
  (alists form)
  (with-stolen-alists-fn alists form))

other

(def-b*-binder with-stolen
  :short "@(see b*) binder for invoking @(see with-stolen-alists) for the
          remainder of a @(see b*) form."
  :decls ((declare (xargs :guard (not forms))
     (ignorable forms)))
  :body `(with-stolen-alists ,ARGS ,REST-EXPR))

other

(defxdoc fast-alists-free-on-exit
  :parents (fast-alists)
  :short "Concisely call @(tsee fast-alist-free-on-exit) for several alists."
  :long "<p>For example:</p>

@({
    (fast-alists-free-on-exit (a b c) form)
})

<p>is just shorthand for:</p>

@({
    (fast-alist-free-on-exit a
     (fast-alist-free-on-exit b
      (fast-alist-free-on-exit c
       form)))
})

@(def fast-alists-free-on-exit)
@(def fast-alists-free-on-exit-fn)")

fast-alists-free-on-exit-fnfunction

(defun fast-alists-free-on-exit-fn
  (alists form)
  (if (atom alists)
    form
    `(fast-alist-free-on-exit ,(CAR ALISTS)
      ,(FAST-ALISTS-FREE-ON-EXIT-FN (CDR ALISTS) FORM))))

fast-alists-free-on-exitmacro

(defmacro fast-alists-free-on-exit
  (alists form)
  (fast-alists-free-on-exit-fn alists form))

other

(def-b*-binder free-on-exit
  :short "@(see b*) binder for freeing fast alists when the @(see b*) exits."
  :decls ((declare (xargs :guard (not forms))
     (ignorable forms)))
  :body `(fast-alists-free-on-exit ,ARGS ,REST-EXPR))