		Search-engine friendly clone of the ACL2 documentation.

Term-checkers-atc

Atc-check-mv-let

Check if a term may be an mv-let statement term.

Signature
(atc-check-mv-let term) → (mv yes/no var? vars indices val body wrapper? mv-var)
Arguments: term — Guard (pseudo-termp term).
Returns: yes/no — Type (booleanp yes/no).; var? — Type (symbolp var?).; vars — Type (symbol-listp vars).; indices — Type (nat-listp indices).; val — Type (pseudo-termp val).; body — Type (pseudo-termp body).; wrapper? — Type (symbolp wrapper?).; mv-var — Type (symbolp mv-var).

The forms of these terms are described in the user documentation.

First, we check if the term is an mv-let, obtaining variables, indices, value term, and body term. Then we check whether the value term is a declar<n> or an assign<n>: in this case, we return the first variable separately from the other variables, and we also return the corresponding declar or assign wrapper. Otherwise, we return all the variables together, with nil as the var? and wrapper? results. We also return, in mv-var, the variable to which the term is let-bound (see ACL2::make-mv-let-call); this is used for reconstructing the transformed term.

Definitions and Theorems

Function: atc-check-mv-let

(defun atc-check-mv-let (term)
  (declare (xargs :guard (pseudo-termp term)))
  (let ((__function__ 'atc-check-mv-let))
    (declare (ignorable __function__))
    (b* (((mv okp mv-var vars indices & val body)
          (fty-check-mv-let-call term))
         ((when (not okp))
          (mv nil nil nil nil nil nil nil nil))
         ((mv okp wrapper & wrapped)
          (atc-check-declar/assign-n val))
         ((when (not okp))
          (mv t
              nil vars indices val body nil mv-var)))
      (mv t (car vars)
          (cdr vars)
          indices wrapped body wrapper mv-var))))

Theorem: booleanp-of-atc-check-mv-let.yes/no

(defthm booleanp-of-atc-check-mv-let.yes/no
  (b* (((mv ?yes/no ?var? ?vars
            ?indices ?val ?body ?wrapper? ?mv-var)
        (atc-check-mv-let term)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: symbolp-of-atc-check-mv-let.var?

(defthm symbolp-of-atc-check-mv-let.var?
  (b* (((mv ?yes/no ?var? ?vars
            ?indices ?val ?body ?wrapper? ?mv-var)
        (atc-check-mv-let term)))
    (symbolp var?))
  :rule-classes :rewrite)

Theorem: symbol-listp-of-atc-check-mv-let.vars

(defthm symbol-listp-of-atc-check-mv-let.vars
  (b* (((mv ?yes/no ?var? ?vars
            ?indices ?val ?body ?wrapper? ?mv-var)
        (atc-check-mv-let term)))
    (symbol-listp vars))
  :rule-classes :rewrite)

Theorem: nat-listp-of-atc-check-mv-let.indices

(defthm nat-listp-of-atc-check-mv-let.indices
  (b* (((mv ?yes/no ?var? ?vars
            ?indices ?val ?body ?wrapper? ?mv-var)
        (atc-check-mv-let term)))
    (nat-listp indices))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-atc-check-mv-let.val

(defthm pseudo-termp-of-atc-check-mv-let.val
  (b* (((mv ?yes/no ?var? ?vars
            ?indices ?val ?body ?wrapper? ?mv-var)
        (atc-check-mv-let term)))
    (pseudo-termp val))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-atc-check-mv-let.body

(defthm pseudo-termp-of-atc-check-mv-let.body
  (b* (((mv ?yes/no ?var? ?vars
            ?indices ?val ?body ?wrapper? ?mv-var)
        (atc-check-mv-let term)))
    (pseudo-termp body))
  :rule-classes :rewrite)

Theorem: symbolp-of-atc-check-mv-let.wrapper?

(defthm symbolp-of-atc-check-mv-let.wrapper?
  (b* (((mv ?yes/no ?var? ?vars
            ?indices ?val ?body ?wrapper? ?mv-var)
        (atc-check-mv-let term)))
    (symbolp wrapper?))
  :rule-classes :rewrite)

Theorem: symbolp-of-atc-check-mv-let.mv-var

(defthm symbolp-of-atc-check-mv-let.mv-var
  (b* (((mv ?yes/no ?var? ?vars
            ?indices ?val ?body ?wrapper? ?mv-var)
        (atc-check-mv-let term)))
    (symbolp mv-var))
  :rule-classes :rewrite)

Theorem: pseudo-term-count-of-atc-check-mv-let-val

(defthm pseudo-term-count-of-atc-check-mv-let-val
  (b* (((mv ?yes/no ?var? ?vars
            ?indices ?val ?body ?wrapper? ?mv-var)
        (atc-check-mv-let term)))
    (implies yes/no
             (< (pseudo-term-count val)
                (pseudo-term-count term))))
  :rule-classes :linear)

Theorem: pseudo-term-count-of-atc-check-mv-let-body

(defthm pseudo-term-count-of-atc-check-mv-let-body
  (b* (((mv ?yes/no ?var? ?vars
            ?indices ?val ?body ?wrapper? ?mv-var)
        (atc-check-mv-let term)))
    (implies yes/no
             (< (pseudo-term-count body)
                (pseudo-term-count term))))
  :rule-classes :linear)