		Search-engine friendly clone of the ACL2 documentation.

Struct-recursion

File-struct-recursion-okp

Check if a Leo file has no struct type recursion.

Signature
(file-struct-recursion-okp file) → yes/no
Arguments: file — Guard (filep file).
Returns: yes/no — Type (booleanp yes/no).

We build the dependency graph of the struct types in the file, by going through the declarations that form the file. Then we attempt to topologically sort the graph. If that succeeds, the graph has no circularities and therefore there is no struct type recursion. If that fails, there is a circularity.

Definitions and Theorems

Function: file-struct-recursion-okp

(defun file-struct-recursion-okp (file)
  (declare (xargs :guard (filep file)))
  (let ((__function__ 'file-struct-recursion-okp))
    (declare (ignorable __function__))
    (b* ((graph (topdecl-list-struct-graph
                     (programdecl->items (file->program file))))
         ((mv okp &) (depgraph::toposort graph)))
      okp)))

Theorem: booleanp-of-file-struct-recursion-okp

(defthm booleanp-of-file-struct-recursion-okp
  (b* ((yes/no (file-struct-recursion-okp file)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: file-struct-recursion-okp-of-file-fix-file

(defthm file-struct-recursion-okp-of-file-fix-file
  (equal (file-struct-recursion-okp (file-fix file))
         (file-struct-recursion-okp file)))

Theorem: file-struct-recursion-okp-file-equiv-congruence-on-file

(defthm file-struct-recursion-okp-file-equiv-congruence-on-file
  (implies (file-equiv file file-equiv)
           (equal (file-struct-recursion-okp file)
                  (file-struct-recursion-okp file-equiv)))
  :rule-classes :congruence)