(in-package "ACL2")
 
(defstruct bg-obj
  (ready)    ;; semaphore to say if ready
  (result)   ;; result when finished
  )

(defmacro bg-push (val bg-stobj)
  ;; The process is to carry out our computation, then signal obj that it is ready.
  `(let* ((__bg_obj   (make-bg-obj :ready (ccl::make-semaphore)
                                   :result nil))
          (__bg_proc  (ccl::make-process 'bg)))
     (format t "BG-PUSH ~a.~%" ',val)
     (ccl::process-preset __bg_proc
                          (lambda ()
                            (setf (bg-obj-result __bg_obj) ,val)
                            (ccl::signal-semaphore (bg-obj-ready __bg_obj))))
     (ccl::process-enable __bg_proc)
     (bg-push-fn __bg_obj ,bg-stobj)))

(defund bg-pop (bg)
  (let* ((acc (bg-accum bg))
         (car (if (consp acc) (car acc) nil))
         (cdr (if (consp acc) (cdr acc) nil))
         (bg  (update-bg-accum cdr bg))
         (car (if (bg-obj-p car)
                  (progn
                    (ccl::wait-on-semaphore (bg-obj-ready car))
                    (bg-obj-result car))
                car)))
    (mv car bg)))