General-purpose, depth-first topological sort for dependency graphs.

- Signature
(toposort graph) → (mv successp result)

- Arguments
`graph`— Alist that binds nodes to the lists of nodes they (directly) depend on. See below.- Returns
`successp`— True when the graph is loop-free and hence can be topologically sorted, ornil when there is a loop.

Type (booleanp successp) .`result`— On success: a list of nodes in topological order, guaranteed equivalent to(alist-keys graph) and in dependency order. On failure: a list of nodes that have a dependency loop.

Type (true-listp result) .

We implement a depth-first topological sort of the graph. If the
graph is loop-free, this produces

The graph is as described in depgraph, but note:

graph is expected to be complete, i.e., every node that is ever listed as a dependent should be bound ingraph ; we will**cause a hard error**if this is not the case.graph should (typically) not contain nodes that depend on themselves; any such nodes form trivial self-loops and will cause topological ordering to fail.

In rare cases you may actually be able to directly use this to sort some structures in a dependency order. But most of the time, we imagine that you will need to:

- Extract a dependency graph in the expected "toposort format",
- Run toposort to get a topological ordering (or find a loop), and finally
- Reorder your data according to the ordering that has been produced.

It might sometimes be more efficient to write custom topological sorts for various data structures. But that's a lot of work. We think that the translation steps are usually cheap enough that in most cases, the above strategy is the easiest way to topologically sort your data.

**Function: **

(defun toposort (graph) (declare (xargs :guard t)) (let ((__function__ 'toposort)) (declare (ignorable __function__)) (b* (((with-fast graph)) (keys (alist-keys graph)) ((mv successp seen) (toposort-aux keys (len keys) graph)) ((unless successp) (b* ((loop (extract-topological-loop (cdr seen) (caar seen) (list (caar seen)) seen))) (fast-alist-free seen) (or (dependency-chain-p loop graph) (er hard? 'toposort "failed to produce a valid dependency chain!")) (or (hons-equal (car loop) (car (last loop))) (er hard? 'toposort "failed to produce a loop!")) (mv nil loop))) (nodes (extract-topological-order seen nil))) (fast-alist-free seen) (or (topologically-ordered-p nodes graph) (er hard? 'toposort "failed to produce a topological ordering!")) (mv t nodes))))

**Theorem: **

(defthm booleanp-of-toposort.successp (b* (((mv ?successp ?result) (toposort graph))) (booleanp successp)) :rule-classes :type-prescription)

**Theorem: **

(defthm true-listp-of-toposort.result (b* (((mv ?successp ?result) (toposort graph))) (true-listp result)) :rule-classes :type-prescription)

We always know, regardless of success, that the nodes we return in our ordering or in our loop must be members of the graph:

**Theorem: **

(defthm subsetp-equal-of-toposort (subsetp-equal (mv-nth 1 (toposort graph)) (alist-keys graph)))

On success, we know something even better, namely that our ordering
contains *all* of the nodes of the graph:

**Theorem: **

(defthm toposort-set-equiv (implies (mv-nth 0 (toposort graph)) (set-equiv (mv-nth 1 (toposort graph)) (alist-keys graph))))

And incidentally, on success, our ordering contains no duplicates:

**Theorem: **

(defthm no-duplicatesp-equal-of-toposort (implies (mv-nth 0 (toposort graph)) (no-duplicatesp-equal (mv-nth 1 (toposort graph)))))

- Toposort-aux
- Main depth-first topological sorting routine.
- Extract-topological-loop
- Extract the topological loop from failed applications of toposort-aux.
- Extract-topological-order
- Extract the topological order from successful applications of toposort-aux.