callers-and-ancestors

other

(in-package "ACL2")

other

(set-state-ok t)

other

(program)

immediate-ancestors-wfunction

(defun immediate-ancestors-w
  (fn wrld)
  (remove1-eq fn
    (all-fnnames (getprop fn 'unnormalized-body *t* 'current-acl2-world wrld))))

all-ancestors1mutual-recursion

(mutual-recursion (defun all-ancestors1
    (fn acc wrld)
    (let ((imm (immediate-ancestors-w fn wrld)))
      (cond ((subsetp-eq imm acc) acc)
        (t (all-ancestors1-lst imm (union-eq imm acc) wrld)))))
  (defun all-ancestors1-lst
    (x acc wrld)
    (cond ((endp x) acc)
      (t (all-ancestors1-lst (cdr x)
          (all-ancestors1 (car x) acc wrld)
          wrld)))))

all-ancestors-wfunction

(defun all-ancestors-w
  (fn wrld)
  (let ((imm (immediate-ancestors-w fn wrld)))
    (all-ancestors1-lst imm imm wrld)))

immediate-ancestorsfunction

(defun immediate-ancestors
  (fn state)
  (immediate-ancestors-w fn (w state)))

all-ancestorsfunction

(defun all-ancestors
  (fn state)
  (all-ancestors-w fn (w state)))

extend-immediate-callers-table1function

(defun extend-immediate-callers-table1
  (fn imm-ancs acc)
  (cond ((endp imm-ancs) acc)
    (t (extend-immediate-callers-table1 fn
        (cdr imm-ancs)
        (let* ((anc (car imm-ancs)) (old (cdr (hons-get anc acc))))
          (cond ((member-eq fn old) acc)
            (t (hons-acons anc (cons fn old) acc))))))))

extend-immediate-callers-tablefunction

(defun extend-immediate-callers-table
  (fns wrld acc)
  (cond ((endp fns) acc)
    (t (extend-immediate-callers-table (cdr fns)
        wrld
        (extend-immediate-callers-table1 (car fns)
          (immediate-ancestors-w (car fns) wrld)
          acc)))))

all-defined-fnsfunction

(defun all-defined-fns
  (wrld acc)
  (cond ((endp wrld) acc)
    ((and (eq (cadar wrld) 'formals)
       (not (eq (cddar wrld) *acl2-property-unbound*))) (all-defined-fns (cdr wrld) (cons (caar wrld) acc)))
    (t (all-defined-fns (cdr wrld) acc))))

build-immediate-callers-tablefunction

(defun build-immediate-callers-table
  (state)
  (let ((wrld (w state)))
    (if (boundp-global 'immediate-callers-table state)
      state
      (f-put-global 'immediate-callers-table
        (extend-immediate-callers-table (all-defined-fns wrld nil)
          wrld
          'immediate-callers-table)
        state))))

chk-immediate-callers-tablefunction

(defun chk-immediate-callers-table
  (state)
  (or (boundp-global 'immediate-callers-table state)
    (er hard
      'immediate-callers
      "Please evaluate ~x0 first."
      '(build-immediate-callers-table state))))

immediate-callersfunction

(defun immediate-callers
  (fn state)
  (prog2$ (chk-immediate-callers-table state)
    (cdr (hons-get fn (f-get-global 'immediate-callers-table state)))))

all-callers1mutual-recursion

(mutual-recursion (defun all-callers1
    (fn acc table)
    (let ((imm (cdr (hons-get fn table))))
      (cond ((subsetp-eq imm acc) acc)
        (t (all-callers1-lst imm (union-eq imm acc) table)))))
  (defun all-callers1-lst
    (x acc table)
    (cond ((endp x) acc)
      (t (all-callers1-lst (cdr x)
          (all-callers1 (car x) acc table)
          table)))))

all-callersfunction

(defun all-callers
  (fn state)
  (prog2$ (chk-immediate-callers-table state)
    (all-callers1 fn
      nil
      (f-get-global 'immediate-callers-table state))))