		Search-engine friendly clone of the ACL2 documentation.

Atj-pre-translation-type-annotation

Atj-check-annotated-mv-let-call

Recognize and decompose type-annotated mv-lets.

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

The type annotation pre-translation step recognizes mv-lets and transforms them as explained in atj-type-annotate-term. So the resulting term should have the form

([reqinf>reqinf]
 ((lambda ([types]mv)
          ([reqinf>reqinf]
           ((lambda ([type1]var1 ... [typen]varn)
                    ([...>reqinf] body-term))
            ([AV>type1] (mv-nth ([AI>AI] '0)
                                ([types>types] [types]mv)))
            ...
            ([AV>typen] (mv-nth ([AI>AI] 'n-1)
                                ([types>types] [types]mv))))))
  ([types>types] mv-term)))

where mv may not be the symbol `mv' but some other symbol. Because of the pre-translation step that removes unused variables, the formals and arguments of the inner lambda may be fewer than the elements of types; i.e. some mv-nth indices may be skipped.

This code recognizes terms of the form above, returning some of the constituents if successful. The mv-var result is [types]mv, i.e. the annotated multi-value variable. The mv-term result is ([types>types] mv-term), i.e. the wrapped multi-value term. The vars result is ([type1]var1 ... [typen]varn) (possibly skipping some indices), i.e. the list of formals of the inner lambda expression, all annotated. The indices result is the ordered list of mv-nth indices actually present; these are 0-based. The body-term result is ([...>reqinf] body-term), i.e. the wrapped body of the inner lambda expression..

Definitions and Theorems

Function: atj-check-annotated-mv-let-call-aux

(defun atj-check-annotated-mv-let-call-aux (args vars types mv-var)
 (declare (xargs :guard (and (pseudo-term-listp args)
                             (symbol-listp vars)
                             (atj-type-listp types)
                             (symbolp mv-var))))
 (declare (xargs :guard (and (= (len vars) (len args))
                             (consp types))))
 (let ((__function__ 'atj-check-annotated-mv-let-call-aux))
   (declare (ignorable __function__))
   (b*
    (((when (endp args)) nil)
     ((mv arg arg-src arg-dst)
      (atj-type-unwrap-term (car args)))
     ((unless (and (not (variablep arg))
                   (not (fquotep arg))
                   (eq (ffn-symb arg) 'mv-nth)
                   (= (len (fargs arg)) 2)
                   (equal (fargn arg 2)
                          (atj-type-wrap-term mv-var types types))))
      (raise "Internal error: malformed term ~x0."
             (car args))
      (repeat (len args) 0))
     ((mv index index-src index-dst)
      (atj-type-unwrap-term (fargn arg 1)))
     ((unless
           (and (quotep index)
                (equal index-src
                       (list (atj-type-acl2 (atj-atype-integer))))
                (equal index-dst
                       (list (atj-type-acl2 (atj-atype-integer))))))
      (raise "Internal error: malformed term ~x0."
             (car args))
      (repeat (len args) 0))
     (index (unquote-term index))
     ((unless (integer-range-p 0 (len types) index))
      (raise "Internal error: malformed term ~x0."
             (car args))
      (repeat (len args) 0))
     ((unless (and (equal arg-src
                          (list (atj-type-acl2 (atj-atype-value))))
                   (equal arg-dst (list (nth index types)))))
      (raise "Internal error: malformed term ~x0."
             (car args))
      (repeat (len args) 0))
     (var (car vars))
     ((mv & var-types)
      (atj-type-unannotate-var var))
     ((unless (equal var-types (list (nth index types))))
      (raise "Internal error: malformed term ~x0."
             (car args))
      (repeat (len args) 0)))
    (cons index
          (atj-check-annotated-mv-let-call-aux (cdr args)
                                               (cdr vars)
                                               types mv-var)))))

Theorem: nat-listp-of-atj-check-annotated-mv-let-call-aux

(defthm nat-listp-of-atj-check-annotated-mv-let-call-aux
 (b*
  ((indices
      (atj-check-annotated-mv-let-call-aux args vars types mv-var)))
  (nat-listp indices))
 :rule-classes :rewrite)

Theorem: len-of-atj-check-annotated-mv-let-call-aux

(defthm len-of-atj-check-annotated-mv-let-call-aux
 (b*
  ((?indices
      (atj-check-annotated-mv-let-call-aux args vars types mv-var)))
  (equal (len indices) (len args))))

Function: atj-check-annotated-mv-let-call

(defun atj-check-annotated-mv-let-call (term)
 (declare (xargs :guard (pseudo-termp term)))
 (let ((__function__ 'atj-check-annotated-mv-let-call))
  (declare (ignorable __function__))
  (b*
   (((mv outer-lambda-call reqinf reqinf2)
     (atj-type-unwrap-term term))
    ((unless (equal reqinf reqinf2))
     (mv nil nil nil nil nil nil))
    ((mv okp mv-var
         wrapped-inner-lambda-call mv-term)
     (check-unary-lambda-call outer-lambda-call))
    ((unless okp)
     (mv nil nil nil nil nil nil))
    ((mv & types)
     (atj-type-unannotate-var mv-var))
    ((unless (> (len types) 1))
     (mv nil nil nil nil nil nil))
    ((mv & src-types dst-types)
     (atj-type-unwrap-term mv-term))
    ((unless (and (equal src-types types)
                  (equal dst-types types)))
     (raise "Internal error: malformed term ~x0."
            term)
     (mv nil nil nil nil nil nil))
    ((mv inner-lambda-call src-types dst-types)
     (atj-type-unwrap-term wrapped-inner-lambda-call))
    ((unless (and (equal src-types reqinf)
                  (equal dst-types reqinf)))
     (mv nil nil nil nil nil nil))
    ((mv okp vars body-term args)
     (check-lambda-call inner-lambda-call))
    ((unless okp)
     (raise "Internal error: malformed term ~x0."
            term)
     (mv nil nil nil nil nil nil))
    ((mv & & dst-types)
     (atj-type-unwrap-term body-term))
    ((unless (equal dst-types reqinf))
     (raise "Internal error: malformed term ~x0."
            term)
     (mv nil nil nil nil nil nil))
    (indices
      (atj-check-annotated-mv-let-call-aux args vars types mv-var)))
   (mv t mv-var
       mv-term vars indices body-term))))

Theorem: booleanp-of-atj-check-annotated-mv-let-call.yes/no

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

Theorem: symbolp-of-atj-check-annotated-mv-let-call.mv-var

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

Theorem: pseudo-termp-of-atj-check-annotated-mv-let-call.mv-term

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

Theorem: symbol-listp-of-atj-check-annotated-mv-let-call.vars

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

Theorem: nat-listp-of-atj-check-annotated-mv-let-call.indices

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

Theorem: pseudo-termp-of-atj-check-annotated-mv-let-call.body-term

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

Theorem: len-of-atj-check-annotated-mv-let.vars/indices

(defthm len-of-atj-check-annotated-mv-let.vars/indices
  (b* (((mv ?yes/no ?mv-var
            ?mv-term ?vars ?indices ?body-term)
        (atj-check-annotated-mv-let-call term)))
    (equal (len indices) (len vars))))

Theorem: atj-check-annotated-mv-let-mv-term-smaller

(defthm atj-check-annotated-mv-let-mv-term-smaller
  (b* (((mv ?yes/no ?mv-var
            ?mv-term ?vars ?indices ?body-term)
        (atj-check-annotated-mv-let-call term)))
    (implies yes/no
             (< (acl2-count mv-term)
                (acl2-count term))))
  :rule-classes :linear)

Theorem: atj-check-annotated-mv-let-body-term-smaller

(defthm atj-check-annotated-mv-let-body-term-smaller
  (b* (((mv ?yes/no ?mv-var
            ?mv-term ?vars ?indices ?body-term)
        (atj-check-annotated-mv-let-call term)))
    (implies yes/no
             (< (acl2-count body-term)
                (acl2-count term))))
  :rule-classes :linear)