		Search-engine friendly clone of the ACL2 documentation.

Function-recursion

File-function-recursion-okp

Check if a Leo file has no function recursion.

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

We build the call graph of the file, by going through all the top-level 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 function recursion. If that fails, there is a recursion.

Definitions and Theorems

Function: file-function-recursion-okp

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

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

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

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

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

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

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