		Search-engine friendly clone of the ACL2 documentation.

Dependencies

Depgraph

Build a directed acyclic graph of type (clique) dependencies.

Signature
(depgraph name fty-table) → depgraph
Arguments: name — Guard (symbolp name).; fty-table — Guard (alistp fty-table).
Returns: depgraph — Type (alistp depgraph).

The graph is represented as an alist from symbols to lists of symbols. Each symbol is the name of a standalone type or of a type clique.

Definitions and Theorems

Function: depgraph-loop

(defun depgraph-loop (names depgraph fty-table count)
 (declare
   (xargs :guard (and (symbol-listp names)
                      (alistp depgraph)
                      (alistp fty-table)
                      (unsigned-byte-p acl2::*fixnat-bits* count))))
 (declare (xargs :split-types t)
          (type (unsigned-byte 60) count))
 (let ((__function__ 'depgraph-loop))
  (declare (ignorable __function__))
  (b*
   (((when (or (endp names)
               (= (mbe :logic (nfix count)
                       :exec (the (unsigned-byte 60) count))
                  0)))
     (mbe :logic (if (alistp depgraph) depgraph nil)
          :exec depgraph))
    (name (first names))
    ((when (assoc-eq name depgraph))
     (depgraph-loop (rest names)
                    depgraph fty-table (1- count)))
    (flextypes (flextypes-with-name name fty-table))
    ((unless (flextypes-p flextypes))
     (raise
      "Internal error: type does not have a corresponding flextypes
                   entry ~x0."
      name))
    (dependencies
         (flextypes-direct-dependencies flextypes fty-table))
    (depgraph (acons name dependencies depgraph)))
   (depgraph-loop (append dependencies (rest names))
                  depgraph fty-table (1- count)))))

Theorem: alistp-of-depgraph-loop

(defthm alistp-of-depgraph-loop
 (b* ((new-depgraph (depgraph-loop names depgraph fty-table count)))
   (alistp new-depgraph))
 :rule-classes :rewrite)

Function: depgraph

(defun depgraph (name fty-table)
  (declare (xargs :guard (and (symbolp name)
                              (alistp fty-table))))
  (let ((__function__ 'depgraph))
    (declare (ignorable __function__))
    (depgraph-loop (list name)
                   nil fty-table
                   (1- (expt 2 acl2::*fixnat-bits*)))))

Theorem: alistp-of-depgraph

(defthm alistp-of-depgraph
  (b* ((depgraph (depgraph name fty-table)))
    (alistp depgraph))
  :rule-classes :rewrite)