		Search-engine friendly clone of the ACL2 documentation.

Returns-specifiers

Tuple

A way to use mv-like return specifiers for tuples.

Return specifiers support individual names and types (and hypothes, etc.) for components of mv results. However, when a function returns an error triple whose value (i.e. middle component) consists of multiple results, given that the error triple already consists of multiple results (three: the error, the value, and the state), it is not possible to use the mv return specifier notation for the value of the error triple.

So here we provide a macro, called tuple, to mimic the mv return specifier notation for a single value, such as the middle component of an error triple.

The macro call

(tuple (var1 type1)
       ...
       (varn typen)
       x)

where each vari is a variable symbol, each typei is a predicate symbol or a term over vari, and x is a variable symbol, expands to

(and (tuplep n x)
     (b* (((list var1 ... varn) x))
       (and (type1 var1)
            ...
            (typen varn))))

where each (typei vari) is as shown if typei is a symbol, otherwise we use the term typei instead.

This lets us write return specifiers of the form

:returns (mv erp
             (val (tuple (var1 type1) ... (varn typen) val))
             state)

where we can use the call (tuple ...) as the type of val, so that the expansion will express that val is an n-tuple whose components have the specified types.

We may extend this macro with support for :hyp and other features of return specifiers.

The macro is in the STD package, but we also add a synonym in the ACL2 package.

Macro: tuple

(defmacro tuple (&rest args)
 (b* ((var (car (last args)))
      (comps (butlast args 1))
      ((mv vars conjuncts) (tuple-fn comps)))
  (cons
   'and
   (cons
    (cons 'tuplep
          (cons (len comps) (cons var 'nil)))
    (cons (cons 'b*
                (cons (cons (cons (cons 'list vars) (cons var 'nil))
                            'nil)
                      (cons (cons 'and conjuncts) 'nil)))
          'nil)))))

Macro: tuple

(defmacro acl2::tuple (&rest args)
  (cons 'tuple args))

Definitions and Theorems

Function: tuple-fn

(defun tuple-fn (args)
  (declare (xargs :guard (true-listp args)))
  (let ((__function__ 'tuple-fn))
    (declare (ignorable __function__))
    (b* (((when (endp args)) (mv nil nil))
         (arg (car args))
         ((unless (tuplep 2 arg)) (mv nil nil))
         (var (first arg))
         (type (second arg))
         (conjunct (if (symbolp type)
                       (list type var)
                     type))
         ((mv vars conjuncts)
          (tuple-fn (cdr args))))
      (mv (cons var vars)
          (cons conjunct conjuncts)))))