		Search-engine friendly clone of the ACL2 documentation.

Expdata-event-generation

Expdata-gen-result-vars

Generate variables for bounding results of old or new when they return multiple results.

Signature
(expdata-gen-result-vars old$ m) → vars
Arguments: old$ — Guard (symbolp old$).; m — Guard (posp m).
Returns: vars — Type (symbol-listp vars).

When old returns multiple results (and so new does too), sometimes we need to generate mv-let calls that bind the multiple results to variables. This function generates these variables, which are always the symbols result1, result2, etc. It turns out that these symbols are always adequate: they are the only variables in the body of generated mv-lets, and they are distinct from the symbol mv bound by the outer lambda expression in a translated mv-let (see make-mv-let-call

Definitions and Theorems

Function: expdata-gen-result-vars-aux

(defun expdata-gen-result-vars-aux (old$ j m)
  (declare (xargs :guard (and (symbolp old$) (posp j) (posp m))))
  (let ((__function__ 'expdata-gen-result-vars-aux))
    (declare (ignorable __function__))
    (b* (((unless (mbt (posp j))) nil)
         ((unless (mbt (posp m))) nil)
         ((when (> j m)) nil)
         (name (str::cat "RESULT" (str::nat-to-dec-string j)))
         (var (intern-in-package-of-symbol name old$))
         (vars (expdata-gen-result-vars-aux old$ (1+ j)
                                            m)))
      (cons var vars))))

Theorem: symbol-listp-of-expdata-gen-result-vars-aux

(defthm symbol-listp-of-expdata-gen-result-vars-aux
  (b* ((vars (expdata-gen-result-vars-aux old$ j m)))
    (symbol-listp vars))
  :rule-classes :rewrite)

Function: expdata-gen-result-vars

(defun expdata-gen-result-vars (old$ m)
  (declare (xargs :guard (and (symbolp old$) (posp m))))
  (declare (xargs :guard (> m 1)))
  (let ((__function__ 'expdata-gen-result-vars))
    (declare (ignorable __function__))
    (expdata-gen-result-vars-aux old$ 1 m)))

Theorem: symbol-listp-of-expdata-gen-result-vars

(defthm symbol-listp-of-expdata-gen-result-vars
  (b* ((vars (expdata-gen-result-vars old$ m)))
    (symbol-listp vars))
  :rule-classes :rewrite)