		Search-engine friendly clone of the ACL2 documentation.

Term-checkers-atc

Atc-check-declar/assign-n

Check if a term is a call of declar<n> or assign<n>.

Signature
(atc-check-declar/assign-n term) → (mv yes/no wrapper n wrapped)
Arguments: term — Guard (pseudo-termp term).
Returns: yes/no — Type (booleanp yes/no).; wrapper — Type (symbolp wrapper).; n — Type (natp n).; wrapped — Type (pseudo-termp wrapped).

These are the macros described in atc-let-designations. These macros expand to

(mv-let (*0 *1 *2 ... *<n>)
  <wrapped>
  (mv (<wrapper> *0) *1 *2 ... *<n>))

which in translated terms looks like

((lambda (mv)
         ((lambda (*0 *1 *2 ... *<n>)
                  (cons ((<wrapper> *0) (cons *1 ... (cons *<n> 'nil)))))
          (mv-nth '0 mv)
          (mv-nth '1 mv)
          ...
          (mv-nth '<n> mv)))
 <wrapped>)

So here we attempt to recognize this for of translated terms. If successful, we return <wrapper>, <n>, and <wrapped>.

Definitions and Theorems

Function: atc-check-declar/assign-n

(defun atc-check-declar/assign-n (term)
 (declare (xargs :guard (pseudo-termp term)))
 (let ((__function__ 'atc-check-declar/assign-n))
   (declare (ignorable __function__))
   (b*
    (((mv okp
          mv-var vars indices hides wrapped body)
      (fty-check-mv-let-call term))
     ((unless okp) (mv nil nil 0 nil))
     ((unless (eq mv-var 'mv))
      (mv nil nil 0 nil))
     (n+1 (len vars))
     ((unless (>= n+1 2)) (mv nil nil 0 nil))
     (n (1- n+1))
     ((unless (equal vars
                     (loop$ for i of-type integer
                            from 0 to n collect (pack '* i))))
      (mv nil nil 0 nil))
     ((unless (equal indices
                     (loop$ for i
                            of-type integer from 0 to n collect i)))
      (mv nil nil 0 nil))
     ((unless (equal hides (repeat n+1 nil)))
      (mv nil nil 0 nil))
     ((mv okp terms)
      (fty-check-list-call body))
     ((unless okp) (mv nil nil 0 nil))
     ((unless (equal (len terms) n+1))
      (mv nil nil 0 nil))
     ((cons term terms) terms)
     ((unless (pseudo-term-case term :fncall))
      (mv nil nil 0 nil))
     (wrapper (pseudo-term-fncall->fn term))
     ((unless (member-eq wrapper '(declar assign)))
      (mv nil nil 0 nil))
     ((unless (equal (pseudo-term-fncall->args term)
                     (list '*0)))
      (mv nil nil 0 nil))
     ((unless (equal terms
                     (loop$ for i of-type integer
                            from 1 to n collect (pack '* i))))
      (mv nil nil 0 nil)))
    (mv t wrapper n wrapped))))

Theorem: booleanp-of-atc-check-declar/assign-n.yes/no

(defthm booleanp-of-atc-check-declar/assign-n.yes/no
  (b* (((mv ?yes/no ?wrapper ?n ?wrapped)
        (atc-check-declar/assign-n term)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: symbolp-of-atc-check-declar/assign-n.wrapper

(defthm symbolp-of-atc-check-declar/assign-n.wrapper
  (b* (((mv ?yes/no ?wrapper ?n ?wrapped)
        (atc-check-declar/assign-n term)))
    (symbolp wrapper))
  :rule-classes :rewrite)

Theorem: natp-of-atc-check-declar/assign-n.n

(defthm natp-of-atc-check-declar/assign-n.n
  (b* (((mv ?yes/no ?wrapper ?n ?wrapped)
        (atc-check-declar/assign-n term)))
    (natp n))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-atc-check-declar/assign-n.wrapped

(defthm pseudo-termp-of-atc-check-declar/assign-n.wrapped
  (b* (((mv ?yes/no ?wrapper ?n ?wrapped)
        (atc-check-declar/assign-n term)))
    (pseudo-termp wrapped))
  :rule-classes :rewrite)

Theorem: pseudo-term-count-of-atc-check-declar/assign-n-wrapped

(defthm pseudo-term-count-of-atc-check-declar/assign-n-wrapped
  (b* (((mv ?yes/no ?wrapper ?n ?wrapped)
        (atc-check-declar/assign-n term)))
    (implies yes/no
             (< (pseudo-term-count wrapped)
                (pseudo-term-count term))))
  :rule-classes :linear)