Recognize translated mv-lets after pre-translation.
(atj-check-marked-annotated-mv-let-call term) → (mv yes/no mv-var mv-term vars indices 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
This code recognizes terms of the form above,
returning some of the constituents if successful.
The
Function:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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)