		Search-engine friendly clone of the ACL2 documentation.

Kestrel-utilities

Typed-tuplep

Recognize typed tuples, i.e. true lists whose elements satisfy specified predicates.

The macro is called as

(typed-tuplep type1 ... typeN object)

where object is a form and each typeI is a function name or macro name or lambda expression.

The macro call expands to

(let ((x object))
  (and (true-listp x)
       (equal (len x) N)
       (type1 (nth 0 x))
       ...
       (typeN (nth N-1 x))))

When N is 0, typed-tuplep recognizes just nil.

When called with no arguments, i.e. (typed-tuplep), the macro (arbitrarily) expands to t.

Macro: typed-tuplep

(defmacro
 typed-tuplep (&rest args)
 (or
  (null args)
  (let
   ((component-types (butlast args 1))
    (object (car (last args)))
    (variable 'x))
   (cons
    'let
    (cons
     (cons (cons variable (cons object 'nil))
           'nil)
     (cons
      (cons
       'and
       (cons
        (cons 'true-listp (cons variable 'nil))
        (cons
          (cons 'equal
                (cons (cons 'len (cons variable 'nil))
                      (cons (len component-types) 'nil)))
          (typed-tuplep-conjuncts component-types 0 variable nil))))
      'nil))))))

Definitions and Theorems

Function: typed-tuplep-conjuncts

(defun
 typed-tuplep-conjuncts
 (component-types i variable rev-conjuncts)
 (declare (xargs :guard (and (true-listp component-types)
                             (natp i)
                             (symbolp variable)
                             (true-listp rev-conjuncts))))
 (let
  ((__function__ 'typed-tuplep-conjuncts))
  (declare (ignorable __function__))
  (cond
      ((endp component-types)
       (reverse rev-conjuncts))
      (t (typed-tuplep-conjuncts
              (cdr component-types)
              (1+ i)
              variable
              (cons (cons (car component-types)
                          (cons (cons 'nth
                                      (cons i (cons variable 'nil)))
                                'nil))
                    rev-conjuncts))))))

Theorem: true-listp-of-typed-tuplep-conjuncts

(defthm
 true-listp-of-typed-tuplep-conjuncts
 (implies
  (true-listp rev-conjuncts)
  (b*
     ((conjuncts (typed-tuplep-conjuncts component-types
                                         i variable rev-conjuncts)))
     (true-listp conjuncts)))
 :rule-classes :rewrite)