		Search-engine friendly clone of the ACL2 documentation.

Function-recursion

Topdecl-list-call-graph

Call graph induced by a list of top-level declarations.

Signature
(topdecl-list-call-graph decls) → graph
Arguments: decls — Guard (topdecl-listp decls).
Returns: graph — Type (alistp graph).

This lifts topdecl-call-graph to lists. We return the union of the graphs for each element of the list. Note that type checking ensures the absence of different declarations of the same function, ensuring that the unioned alists have disjoint keys.

Definitions and Theorems

Function: topdecl-list-call-graph

(defun topdecl-list-call-graph (decls)
  (declare (xargs :guard (topdecl-listp decls)))
  (let ((__function__ 'topdecl-list-call-graph))
    (declare (ignorable __function__))
    (cond ((endp decls) nil)
          (t (append (topdecl-call-graph (car decls))
                     (topdecl-list-call-graph (cdr decls)))))))

Theorem: alistp-of-topdecl-list-call-graph

(defthm alistp-of-topdecl-list-call-graph
  (b* ((graph (topdecl-list-call-graph decls)))
    (alistp graph))
  :rule-classes :rewrite)

Theorem: topdecl-list-call-graph-of-topdecl-list-fix-decls

(defthm topdecl-list-call-graph-of-topdecl-list-fix-decls
  (equal (topdecl-list-call-graph (topdecl-list-fix decls))
         (topdecl-list-call-graph decls)))

Theorem: topdecl-list-call-graph-topdecl-list-equiv-congruence-on-decls

(defthm
     topdecl-list-call-graph-topdecl-list-equiv-congruence-on-decls
  (implies (topdecl-list-equiv decls decls-equiv)
           (equal (topdecl-list-call-graph decls)
                  (topdecl-list-call-graph decls-equiv)))
  :rule-classes :congruence)