		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-queries

Check-list-call

Check if a term is a (translated) call of list.

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

In translated form, the term must have the form (cons ... (cons ... (cons ... (... 'nil)...))), i.e. be a nest of conses that ends in a quoted nil. The nest may be empty, i.e. the term may be just a quoted nil. If the term has this form, we return the list of its element terms, i.e. all the cars of the nest, in the same order.

Definitions and Theorems

Function: check-list-call

(defun check-list-call (term)
  (declare (xargs :guard (pseudo-termp term)))
  (let ((__function__ 'check-list-call))
    (declare (ignorable __function__))
    (b* (((when (variablep term)) (mv nil nil))
         ((when (fquotep term))
          (if (equal term *nil*)
              (mv t nil)
            (mv nil nil)))
         (fn (ffn-symb term))
         ((unless (eq fn 'cons)) (mv nil nil))
         (args (fargs term))
         ((unless (= (len args) 2))
          (raise "Internal error: found CONS with ~x0 arguments."
                 (len args))
          (mv nil nil))
         (car (first args))
         (cdr (second args))
         ((mv yes/no-rest elements-rest)
          (check-list-call cdr))
         ((unless yes/no-rest) (mv nil nil)))
      (mv t (cons car elements-rest)))))

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

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

Theorem: pseudo-term-listp-of-check-list-call.elements

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