		Search-engine friendly clone of the ACL2 documentation.

Defresult

Reserrf-push

Push the current function onto the stack of an error result, optionally with additional information.

This is useful when receiving an error result from a called function, to add the caller to the stack, and possibly more information, before propagating the error. This addition is handled automatically when using patbind-okf, actually using nil as extra information; when that binder cannot be used for some reason, or when additional information must be pushed, then this reserrf-push macro may come handy.

This assumes that __function__ is bound to the current function name, which is automatically the case when using define.

Macro: reserrf-push

(defmacro reserrf-push (error &optional info)
 (cons
  'b*
  (cons
   (cons (cons 'stack
               (cons (cons 'reserr->info (cons error 'nil))
                     'nil))
         'nil)
   (cons
    (cons
      'reserr
      (cons (cons 'cons
                  (cons (cons 'list
                              (cons '__function__ (cons info 'nil)))
                        '(stack)))
            'nil))
    'nil))))