oracle-time

(in-package "ACL2")

(defxdoc oracle-time
  :parents (time$)
  :short "Carry out a computation, returning (not just printing!) how long it
took and (on supported Lisps) how many bytes were allocated."
  :long "<p>The @('oracle-time') macro allows you to run a form and get the
elapsed time and memory allocation back as real ACL2 values.</p>

<p>In most cases, you don't really need to do this.  Instead, see @(see time$),
which is built into ACL2 and allows you to print the runtime and allocation of
a form as a logically invisible side-effect.  Since @(see time$) doesn't return
the elapsed time or allocation, it is simpler and doesn't need access to @(see
state).  It also has some nice features for controlling when timing information
is printed.</p>

<p>On the other hand, if you want to do things like collect up tables that
describe how your functions perform on various inputs, then @(see time$) won't
do what you want: it just prints the timing information to the terminal,
leaving you with no way to collect and compare the times and allocations.  In
this case, @('oracle-time') may be able to do what you want.  The main
limitation is that it does need access to the state.</p>


<h5>Basic Example</h5>

@({
    (oracle-time (fib 35))   ; Simple since it returns a single value
      -->
    (mv time                 ; Rational, number of seconds
        bytes                ; Natural, bytes allocated
        ans                  ; Answer from (fib 35)
        state)               ; Updated state
})


<h5>Example with Multiple Return Values</h5>

@({
    (oracle-time (random$ 100 state)  ; Returns multiple values
       :ret (mv ans state))           ; Explains the return type
      -->
    (mv time                          ; Rational, number of seconds
        bytes                         ; Natural, bytes allocated
        ans                           ; The random number produced
        state)                        ; Updated state
})

<p>See also the community book @('tools/oracle-time-tests.lisp') for some
additional tests and working examples.</p>

<h5>General Form</h5>

@({
    (oracle-time form [:ret retspec])
})

<p>The @('form') can be any arbitrary ACL2 form that you want to execute.  If
the form returns an ordinary, single value, e.g., as in @('(fib 35)') then the
@(':ret') argument is not needed.  Otherwise, @(':ret') should explain the
return signature of @('form').</p>

<p>The return value of @('oracle-time') extends the return value of @('form')
with multiple values.  The basic idea is that @('oracle-time') is going to
macroexpand to something like this:</p>

@({
     (mv-let retspec
        form
        (b* (((mv & time state) (read-acl2-oracle state))
             ((mv & bytes state) (read-acl2-oracle state)))
          (mv time bytes retspec [state])))
})

<p>You can see here that the @('retspec') is used to explain how to bind the
results of executing the form.  It is also, essentially, spliced into the
return value of the whole @('oracle-time') call.  The only twist is that if
@('retspec') mentions @('state'), then we don't add an extra @('state') onto
the end of the form.</p>")

(defttag :oracle-time)

(include-raw "oracle-time-raw.lsp")

(defmacro-last oracle-time-exec)