with-waterfall-parallelism

Included Books

top

other

(in-package "ACL2")

include-book

(include-book "xdoc/top" :dir :system)

with-waterfall-parallelism-fnfunction

(defun with-waterfall-parallelism-fn
  (events state)
  (declare (xargs :mode :program :stobjs state))
  (let ((curr-waterfall-parallelism-val (f-get-global 'waterfall-parallelism state)))
    `(progn (local (make-event (er-progn (set-waterfall-parallelism t)
            (value '(value-triple nil)))
          :check-expansion t))
      ,@EVENTS
      (local (make-event (er-progn (set-waterfall-parallelism ',CURR-WATERFALL-PARALLELISM-VAL)
            (value '(value-triple t)))
          :check-expansion t)))))

with-waterfall-parallelismmacro

(defmacro with-waterfall-parallelism
  (&rest events)
  `(make-event (with-waterfall-parallelism-fn ',EVENTS state)))

other

(defxdoc with-waterfall-parallelism
  :parents (parallelism)
  :short "Enable waterfall parallelism for an enclosed event"
  :long "<p>Example usage:</p>
  @({
  (with-waterfall-parallelism
    (defthm assoc-append
     (equal (append x (append y z))
            (append (append x y) z))))
  })")