		Search-engine friendly clone of the ACL2 documentation.

Types

Tyspecseq-to-type

Turn a type specifier sequence into a type.

Signature
(tyspecseq-to-type tyspec) → type
Arguments: tyspec — Guard (tyspecseqp tyspec).
Returns: type — Type (typep type).

This is a subroutine of tyname-to-type, in a sense. A type specifier sequence already denotes a type (of certain kinds); but in general it is type names that denote types (of all kinds).

Definitions and Theorems

Function: tyspecseq-to-type

(defun tyspecseq-to-type (tyspec)
 (declare (xargs :guard (tyspecseqp tyspec)))
 (let ((__function__ 'tyspecseq-to-type))
  (declare (ignorable __function__))
  (tyspecseq-case
   tyspec
   :void (type-void)
   :char (type-char)
   :schar (type-schar)
   :uchar (type-uchar)
   :sshort (type-sshort)
   :ushort (type-ushort)
   :sint (type-sint)
   :uint (type-uint)
   :slong (type-slong)
   :ulong (type-ulong)
   :sllong (type-sllong)
   :ullong (type-ullong)
   :bool
   (prog2$
    (raise
     "Internal error: ~
                                 _Bool not supported yet.")
    (ec-call (type-fix :irrelevant)))
   :float
   (prog2$
    (raise
     "Internal error: ~
                                  float not supported yet.")
    (ec-call (type-fix :irrelevant)))
   :double
   (prog2$
    (raise
     "Internal error: ~
                                   double not supported yet.")
    (ec-call (type-fix :irrelevant)))
   :ldouble
   (prog2$
    (raise
     "Internal error: ~
                                    long double not supported yet.")
    (ec-call (type-fix :irrelevant)))
   :struct (type-struct tyspec.tag)
   :union
   (prog2$
    (raise
     "Internal error: ~
                                  union ~x0 not supported yet."
     tyspec.tag)
    (ec-call (type-fix :irrelevant)))
   :enum
   (prog2$
    (raise
     "Internal error: ~
                                 enum ~x0 not supported yet."
     tyspec.tag)
    (ec-call (type-fix :irrelevant)))
   :typedef
   (prog2$
    (raise
     "Internal error: ~
                                    typedef ~x0 not supported yet."
     tyspec.name)
    (ec-call (type-fix :irrelevant))))))

Theorem: typep-of-tyspecseq-to-type

(defthm typep-of-tyspecseq-to-type
  (b* ((type (tyspecseq-to-type tyspec)))
    (typep type))
  :rule-classes :rewrite)

Theorem: tyspecseq-to-type-of-tyspecseq-fix-tyspec

(defthm tyspecseq-to-type-of-tyspecseq-fix-tyspec
  (equal (tyspecseq-to-type (tyspecseq-fix tyspec))
         (tyspecseq-to-type tyspec)))

Theorem: tyspecseq-to-type-tyspecseq-equiv-congruence-on-tyspec

(defthm tyspecseq-to-type-tyspecseq-equiv-congruence-on-tyspec
  (implies (tyspecseq-equiv tyspec tyspec-equiv)
           (equal (tyspecseq-to-type tyspec)
                  (tyspecseq-to-type tyspec-equiv)))
  :rule-classes :congruence)