		Search-engine friendly clone of the ACL2 documentation.

Backtraces

Function-rules-to-backtrace-spec

Get a set of FGL backtrace specifiers for all FGL rules targeting a function symbol

Signature
(function-rules-to-backtrace-spec fn vars interp-st state) → *
Arguments: fn — Guard (pseudo-fnsym-p fn).; vars — Guard (pseudo-var-list-p vars).

Definitions and Theorems

Function: function-rules-to-backtrace-spec

(defun function-rules-to-backtrace-spec (fn vars interp-st state)
  (declare (xargs :stobjs (interp-st state)))
  (declare (xargs :guard (and (pseudo-fnsym-p fn)
                              (pseudo-var-list-p vars))))
  (let ((__function__ 'function-rules-to-backtrace-spec))
    (declare (ignorable __function__))
    (b* ((wrld (w state))
         (table (interp-st->rewrite-rules interp-st)
)
         ((mv ?err rules)
          (fgl-function-rules fn table wrld))
         (formals (getpropc fn 'formals t wrld))
         ((unless (pseudo-var-list-p formals))
          (raise "Bad formals for ~x0: ~x1" fn formals)
          nil))
      (function-rules-to-backtrace-spec-aux rules formals vars))))