		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-queries

Check-fn-call

Check if a term is a (translated) call of a named function.

Signature
(check-fn-call term) → (mv yes/no fn args)
Arguments: term — Guard (pseudo-termp term).
Returns: yes/no — Type (booleanp yes/no).; fn — Type (symbolp fn), given the guard.; args — Type (pseudo-term-listp args), given the guard.

If it is, the first result is t and the other results are the function symbol and the arguments on which the function is called. Otherwise, all the results are nil.

Definitions and Theorems

Function: check-fn-call

(defun check-fn-call (term)
  (declare (xargs :guard (pseudo-termp term)))
  (let ((__function__ 'check-fn-call))
    (declare (ignorable __function__))
    (b* (((when (variablep term))
          (mv nil nil nil))
         ((when (fquotep term)) (mv nil nil nil))
         (fn (ffn-symb term))
         ((when (flambdap fn)) (mv nil nil nil)))
      (mv t fn (fargs term)))))

Theorem: booleanp-of-check-fn-call.yes/no

(defthm booleanp-of-check-fn-call.yes/no
  (b* (((mv ?yes/no ?fn ?args)
        (check-fn-call term)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: symbolp-of-check-fn-call.fn

(defthm symbolp-of-check-fn-call.fn
  (implies (and (pseudo-termp term))
           (b* (((mv ?yes/no ?fn ?args)
                 (check-fn-call term)))
             (symbolp fn)))
  :rule-classes :rewrite)

Theorem: pseudo-term-listp-of-check-fn-call.args

(defthm pseudo-term-listp-of-check-fn-call.args
  (implies (and (pseudo-termp term))
           (b* (((mv ?yes/no ?fn ?args)
                 (check-fn-call term)))
             (pseudo-term-listp args)))
  :rule-classes :rewrite)

Theorem: true-listp-of-check-fn-call.args

(defthm true-listp-of-check-fn-call.args
  (implies (and (pseudo-termp term))
           (b* (((mv ?yes/no ?fn ?args)
                 (check-fn-call term)))
             (true-listp args)))
  :rule-classes :type-prescription)

Theorem: check-fn-call-not-quote

(defthm check-fn-call-not-quote
  (b* (((mv ?yes/no ?fn ?args)
        (check-fn-call term)))
    (not (equal fn 'quote))))

Theorem: acl2-count-of-check-fn-call

(defthm acl2-count-of-check-fn-call
  (b* (((mv ?yes/no ?fn ?args)
        (check-fn-call term)))
    (implies yes/no
             (< (acl2-count args)
                (acl2-count term))))
  :rule-classes :linear)