		Search-engine friendly clone of the ACL2 documentation.

Dependencies

Topo-dependencies

A topological ordering of type (clique) based on type dependencies.

Signature
(topo-dependencies name fty-table) → dependencies
Arguments: name — Guard (symbolp name).; fty-table — Guard (alistp fty-table).
Returns: dependencies — Type (symbol-listp dependencies).

This is the topological ordering of depgraph, obtained via depgraph::toposort.

Definitions and Theorems

Function: topo-dependencies

(defun topo-dependencies (name fty-table)
  (declare (xargs :guard (and (symbolp name)
                              (alistp fty-table))))
  (let ((__function__ 'topo-dependencies))
    (declare (ignorable __function__))
    (b* ((depgraph (depgraph name fty-table))
         ((mv successp result)
          (depgraph::toposort depgraph))
         ((unless successp)
          (raise "Internal error: assembled graph is not a DAG ~x0"
                 depgraph))
         ((unless (symbol-listp result))
          (raise "Internal error: result is not a symbol-list ~x0"
                 result)))
      result)))

Theorem: symbol-listp-of-topo-dependencies

(defthm symbol-listp-of-topo-dependencies
  (b* ((dependencies (topo-dependencies name fty-table)))
    (symbol-listp dependencies))
  :rule-classes :rewrite)