Filtering...

with-timeout

books/acl2s/cgen/with-timeout

Included Books

top
other
(in-package "ACL2")
include-book
(include-book "xdoc/top" :dir :system)
other
(defxdoc with-timeout
  :parents (cgen miscellaneous)
  :short "Evaluate form with a timeout (in seconds)"
  :long "<p>Evaluate form with a timeout in seconds. </p>

  <p>The general form is:
  @({with-timeout duration body timeout-form})
  </p>

  <p>
  @('duration') can be any rational value.  A duration of 0 seconds disables
  the timeout mechanism, i.e its a no-op. Suppose it is not, and @('duration')
  seconds elapse during evaluation of <tt>body</tt> then the evaluation is aborted
  and the value of @('timeout-form') is returned; in the normal case the value
  of <tt>body</tt> is returned.
  </p>
  <p> The signature of <tt>body</tt> and <tt>timeout-form</tt> should be the same.  </p>

  <h3>Advanced Notes:</h3>
  <p>
  This form should be called either at the top-level or in
  an environment where state is available and <tt>body</tt> has
  no free variables other than state.
  If the timeout-form is a long running computation,
  then the purpose of with-timeout is defeated.
  </p>

  <code>
    Usage:
    (with-timeout 5 (fibonacci 40) :timed-out)
    :doc with-timeout
  </code>
")
other
(defttag :acl2s-timeout)
other
(progn! (set-raw-mode t)
  (load (concatenate 'string (cbd) "with-timeout-raw.lsp")))
other
(defmacro-last with-timeout-aux)
with-time-limitmacro
(defmacro with-time-limit
  (time form)
  `(with-prover-time-limit (if (equal ,TIME 0)
      (expt 2 20)
      ,TIME)
    ,FORM))
with-timeoutmacro
(defmacro with-timeout
  (duration form timeout-form)
  "can only be called at top-level, that too only forms that are allowed
to be evaluated inside a function body. To eval defthm, use
with-timeout-ev instead"
  `(if (equal 0 ,DURATION)
    ,FORM
    (top-level (with-timeout1 ,DURATION ,FORM ,TIMEOUT-FORM))))
with-timeout1macro
(defmacro with-timeout1
  (duration form timeout-form)
  "can only be used inside a function body, and if form has
free variables other than state, then manually make a function
which takes those free variables as arguments and at the calling
context, pass the arguments, binding the free variables.
See top-level-test? macro for an example"
  `(if (equal 0 ,DURATION)
    ,FORM
    (with-timeout-aux '(,DURATION ,TIMEOUT-FORM) ,FORM)))
other
(defttag nil)