		Search-engine friendly clone of the ACL2 documentation.
Tyspecseq
Tyspecseqp

Recognizer for tyspecseq structures.
Signature
(tyspecseqp x) → *
Definitions and Theorems

Function: tyspecseqp
(defun tyspecseqp (x)
  (declare (xargs :guard t))
  (let ((__function__ 'tyspecseqp))
    (declare (ignorable __function__))
    (and (consp x)
         (cond ((or (atom x) (eq (car x) :void))
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 0)
                     (b* nil t)))
               ((eq (car x) :char)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 0)
                     (b* nil t)))
               ((eq (car x) :schar)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 0)
                     (b* nil t)))
               ((eq (car x) :uchar)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 0)
                     (b* nil t)))
               ((eq (car x) :sshort)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 2)
                     (b* ((signed (std::da-nth 0 (cdr x)))
                          (int (std::da-nth 1 (cdr x))))
                       (and (booleanp signed)
                            (booleanp int)))))
               ((eq (car x) :ushort)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 1)
                     (b* ((int (std::da-nth 0 (cdr x))))
                       (booleanp int))))
               ((eq (car x) :sint)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 2)
                     (b* ((signed (std::da-nth 0 (cdr x)))
                          (int (std::da-nth 1 (cdr x))))
                       (and (booleanp signed)
                            (booleanp int)
                            (or signed int)))))
               ((eq (car x) :uint)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 1)
                     (b* ((int (std::da-nth 0 (cdr x))))
                       (booleanp int))))
               ((eq (car x) :slong)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 2)
                     (b* ((signed (std::da-nth 0 (cdr x)))
                          (int (std::da-nth 1 (cdr x))))
                       (and (booleanp signed)
                            (booleanp int)))))
               ((eq (car x) :ulong)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 1)
                     (b* ((int (std::da-nth 0 (cdr x))))
                       (booleanp int))))
               ((eq (car x) :sllong)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 2)
                     (b* ((signed (std::da-nth 0 (cdr x)))
                          (int (std::da-nth 1 (cdr x))))
                       (and (booleanp signed)
                            (booleanp int)))))
               ((eq (car x) :ullong)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 1)
                     (b* ((int (std::da-nth 0 (cdr x))))
                       (booleanp int))))
               ((eq (car x) :bool)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 0)
                     (b* nil t)))
               ((eq (car x) :float)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 1)
                     (b* ((complex (std::da-nth 0 (cdr x))))
                       (booleanp complex))))
               ((eq (car x) :double)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 1)
                     (b* ((complex (std::da-nth 0 (cdr x))))
                       (booleanp complex))))
               ((eq (car x) :ldouble)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 1)
                     (b* ((complex (std::da-nth 0 (cdr x))))
                       (booleanp complex))))
               ((eq (car x) :struct)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 1)
                     (b* ((tag (std::da-nth 0 (cdr x))))
                       (identp tag))))
               ((eq (car x) :union)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 1)
                     (b* ((tag (std::da-nth 0 (cdr x))))
                       (identp tag))))
               ((eq (car x) :enum)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 1)
                     (b* ((tag (std::da-nth 0 (cdr x))))
                       (identp tag))))
               (t (and (eq (car x) :typedef)
                       (and (true-listp (cdr x))
                            (eql (len (cdr x)) 1))
                       (b* ((name (std::da-nth 0 (cdr x))))
                         (identp name))))))))