		Search-engine friendly clone of the ACL2 documentation.

Struct-recursion

Structdecl-struct-graph

Struct graph induced by a struct definition.

Signature
(structdecl-struct-graph decl) → graph
Arguments: decl — Guard (structdeclp decl).
Returns: graph — Type (alistp graph).

We return a dependency graph expressing that the circui type defined by the struct type declaration depends on the type identifiers in the components' types. This dependency relation is the direct containment relation of struct types. The format is that of an alist for the dependency graph library.

Definitions and Theorems

Function: structdecl-struct-graph

(defun structdecl-struct-graph (decl)
  (declare (xargs :guard (structdeclp decl)))
  (let ((__function__ 'structdecl-struct-graph))
    (declare (ignorable __function__))
    (b* ((subs (compdecl-list-type-identifiers
                    (structdecl->components decl))))
      (list (cons (structdecl->name decl) subs)))))

Theorem: alistp-of-structdecl-struct-graph

(defthm alistp-of-structdecl-struct-graph
  (b* ((graph (structdecl-struct-graph decl)))
    (alistp graph))
  :rule-classes :rewrite)

Theorem: structdecl-struct-graph-of-structdecl-fix-decl

(defthm structdecl-struct-graph-of-structdecl-fix-decl
  (equal (structdecl-struct-graph (structdecl-fix decl))
         (structdecl-struct-graph decl)))

Theorem: structdecl-struct-graph-structdecl-equiv-congruence-on-decl

(defthm structdecl-struct-graph-structdecl-equiv-congruence-on-decl
  (implies (structdecl-equiv decl decl-equiv)
           (equal (structdecl-struct-graph decl)
                  (structdecl-struct-graph decl-equiv)))
  :rule-classes :congruence)