		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-code-generation

Atj-check-marked-annotated-mv-let-call

Recognize translated mv-lets after pre-translation.

Signature
(atj-check-marked-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. the variable reuse pre-translation step additionally marks the variables, and the variable renaming pre-translation step may change their (unmarked, unannotated) names. So the resulting term should have the form

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

where [m], [m1], ..., [mn] are new/old markings, and where mv may not be the symbol `mv' but some other symbol. Because of the pre-translation steps 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 [m][types]mv, i.e. the marked and annotated multi-value variable. The mv-term result is ([types>types] mv-term), i.e. the wrapped multi-value term. The vars result is ([m1][type1]var1 ... [mn][typen]varn) (possibly skipping some indices), i.e. the list of formals of the inner lambda expression, all marked and 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. The term and variable results are marked/annotated/wrapped so that they can be treated uniformly by the code generation functions.

Definitions and Theorems

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

(defun atj-check-marked-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-marked-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))
    ((mv var &) (atj-unmark-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-marked-annotated-mv-let-call-aux (cdr args)
                                                   (cdr vars)
                                                   types mv-var)))))

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

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

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

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

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

(defun atj-check-marked-annotated-mv-let-call (term)
  (declare (xargs :guard (pseudo-termp term)))
  (let ((__function__ 'atj-check-marked-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 mv-var-unmarked &)
          (atj-unmark-var mv-var))
         ((mv & types)
          (atj-type-unannotate-var mv-var-unmarked))
         ((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-marked-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-marked-annotated-mv-let-call.yes/no

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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