without-waterfall-parallelism

Included Books

top

other

(in-package "ACL2")

include-book

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

without-waterfall-parallelism-fnfunction

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

without-waterfall-parallelismmacro

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

other

(defxdoc without-waterfall-parallelism
  :parents (parallelism)
  :short "Disable waterfall parallelism for an enclosed event"
  :long "<p>Example usage:</p>
  @({
  (without-waterfall-parallelism
    (defun foo (x) (* x 3)))
  })")