		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-queries

All-non-gv-ffn-symbs

Non-guard-verified functions called by a term.

Signature
(all-non-gv-ffn-symbs term ans wrld) → final-ans
Arguments: term — Guard (pseudo-termp term).; ans — Guard (symbol-listp ans).; wrld — Guard (plist-worldp wrld).
Returns: final-ans — Type (symbol-listp final-ans), given the guard.

The name of this function is consistent with the name of all-ffn-symbs in the ACL2 source code.

Note that if any function inside the :logic component of an mbe or called via ec-call is not guard-verified, we return it. See all-non-gv-exec-ffn-symbs for a similar utility that does not return such functions.

Function: all-non-gv-ffn-symbs

(defun all-non-gv-ffn-symbs (term ans wrld)
  (declare (xargs :guard (and (pseudo-termp term)
                              (symbol-listp ans)
                              (plist-worldp wrld))))
  (let ((__function__ 'all-non-gv-ffn-symbs))
    (declare (ignorable __function__))
    (b* (((when (variablep term)) ans)
         ((when (fquotep term)) ans)
         (fn/lambda (ffn-symb term))
         (ans (if (flambdap fn/lambda)
                  (all-non-gv-ffn-symbs (lambda-body fn/lambda)
                                        ans wrld)
                (if (guard-verified-p fn/lambda wrld)
                    ans
                  (add-to-set-eq fn/lambda ans)))))
      (all-non-gv-ffn-symbs-lst (fargs term)
                                ans wrld))))

Function: all-non-gv-ffn-symbs-lst

(defun all-non-gv-ffn-symbs-lst (terms ans wrld)
  (declare (xargs :guard (and (pseudo-term-listp terms)
                              (symbol-listp ans)
                              (plist-worldp wrld))))
  (let ((__function__ 'all-non-gv-ffn-symbs-lst))
    (declare (ignorable __function__))
    (b* (((when (endp terms)) ans)
         (ans (all-non-gv-ffn-symbs (car terms)
                                    ans wrld)))
      (all-non-gv-ffn-symbs-lst (cdr terms)
                                ans wrld))))

Theorem: return-type-of-all-non-gv-ffn-symbs.final-ans

(defthm return-type-of-all-non-gv-ffn-symbs.final-ans
  (implies (and (pseudo-termp term)
                (symbol-listp ans)
                (plist-worldp wrld))
           (b* ((?final-ans (all-non-gv-ffn-symbs term ans wrld)))
             (symbol-listp final-ans)))
  :rule-classes :rewrite)

Theorem: return-type-of-all-non-gv-ffn-symbs-lst.final-ans

(defthm return-type-of-all-non-gv-ffn-symbs-lst.final-ans
  (implies
       (and (pseudo-term-listp terms)
            (symbol-listp ans)
            (plist-worldp wrld))
       (b* ((?final-ans (all-non-gv-ffn-symbs-lst terms ans wrld)))
         (symbol-listp final-ans)))
  :rule-classes :rewrite)

Subtopics

All-non-gv-ffn-symbs-lst