Generate a shallowly embedded ACL2 call of mv.
(atj-gen-shallow-mv-call arg-blocks arg-exprs src-types dst-types guards$) → (mv block expr)
Calls of mv are introduced by a pre-translation step: see herefor details.
These calls are treated specially for code generation. We generate a call of the factory method of the mv class corresponding to the destination types of the arguments, converting each argument from the source types as needed.
Function:
(defun atj-gen-shallow-mv-call (arg-blocks arg-exprs src-types dst-types guards$) (declare (xargs :guard (and (jblock-listp arg-blocks) (jexpr-listp arg-exprs) (atj-type-listp src-types) (atj-type-listp dst-types) (booleanp guards$)))) (declare (xargs :guard (and (consp src-types) (consp dst-types)))) (let ((__function__ 'atj-gen-shallow-mv-call)) (declare (ignorable __function__)) (b* ((block (flatten (jblock-list-fix arg-blocks))) ((unless (>= (len src-types) 2)) (raise "Internal error: ~ MV has arguments ~x0, which are fewer than two." arg-exprs) (mv nil (jexpr-name "irrelevant"))) ((unless (= (len src-types) (len dst-types))) (raise "Internal error: ~ the source types ~x0 and destination types ~x1 ~ differ in number." src-types dst-types) (mv nil (jexpr-name "irrelevant"))) ((unless (= (len arg-exprs) (len dst-types))) (raise "Internal error: ~ the arguments ~x0 and ~ source and destination types ~x1 and ~x2 ~ differ in number." arg-exprs src-types dst-types) (mv nil (jexpr-name "irrelevant"))) (exprs (atj-adapt-exprs-to-types arg-exprs src-types dst-types guards$)) (expr (jexpr-smethod (jtype-class (atj-gen-shallow-mv-class-name dst-types)) *atj-mv-factory-method-name* exprs))) (mv block expr))))
Theorem:
(defthm jblockp-of-atj-gen-shallow-mv-call.block (b* (((mv common-lisp::?block ?expr) (atj-gen-shallow-mv-call arg-blocks arg-exprs src-types dst-types guards$))) (jblockp block)) :rule-classes :rewrite)
Theorem:
(defthm jexprp-of-atj-gen-shallow-mv-call.expr (b* (((mv common-lisp::?block ?expr) (atj-gen-shallow-mv-call arg-blocks arg-exprs src-types dst-types guards$))) (jexprp expr)) :rule-classes :rewrite)