		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-tyspecseq

Check a type specifier sequence.

Signature
(check-tyspecseq tyspec tagenv) → type
Arguments: tyspec — Guard (tyspecseqp tyspec).; tagenv — Guard (tag-envp tagenv).
Returns: type — Type (type-resultp type).

If successful, return the type denoted by the type specifier sequence.

We only accept certain type specifier sequences for now, namely the ones that have corresponding types in our model. The tag of a structure type specifier sequence must be in the tag environment. All the other (supported) type specifier sequences are always well-formed.

Definitions and Theorems

Function: check-tyspecseq

(defun check-tyspecseq (tyspec tagenv)
 (declare (xargs :guard (and (tyspecseqp tyspec)
                             (tag-envp tagenv))))
 (let ((__function__ 'check-tyspecseq))
  (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
     (reserrf (list :not-supported-bool))
     :float
     (reserrf (list :not-supported-float))
     :double
     (reserrf (list :not-supported-double))
     :ldouble
     (reserrf (list :not-supported-ldouble))
     :struct
     (b* ((info (tag-env-lookup tyspec.tag tagenv)))
       (tag-info-option-case
            info :some
            (if (tag-info-case info.val :struct)
                (type-struct tyspec.tag)
              (reserrf (list :struct-tag-mismatch
                             tyspec.tag info.val)))
            :none (reserrf (list :no-tag-found tyspec.tag))))
     :union (reserrf (list :not-supported-union tyspec.tag))
     :enum (reserrf (list :not-supported-enum tyspec.tag))
     :typedef (reserrf (list :not-supported-typedef tyspec.name)))))

Theorem: type-resultp-of-check-tyspecseq

(defthm type-resultp-of-check-tyspecseq
  (b* ((type (check-tyspecseq tyspec tagenv)))
    (type-resultp type))
  :rule-classes :rewrite)

Theorem: check-tyspecseq-of-tyspecseq-fix-tyspec

(defthm check-tyspecseq-of-tyspecseq-fix-tyspec
  (equal (check-tyspecseq (tyspecseq-fix tyspec)
                          tagenv)
         (check-tyspecseq tyspec tagenv)))

Theorem: check-tyspecseq-tyspecseq-equiv-congruence-on-tyspec

(defthm check-tyspecseq-tyspecseq-equiv-congruence-on-tyspec
  (implies (tyspecseq-equiv tyspec tyspec-equiv)
           (equal (check-tyspecseq tyspec tagenv)
                  (check-tyspecseq tyspec-equiv tagenv)))
  :rule-classes :congruence)

Theorem: check-tyspecseq-of-tag-env-fix-tagenv

(defthm check-tyspecseq-of-tag-env-fix-tagenv
  (equal (check-tyspecseq tyspec (tag-env-fix tagenv))
         (check-tyspecseq tyspec tagenv)))

Theorem: check-tyspecseq-tag-env-equiv-congruence-on-tagenv

(defthm check-tyspecseq-tag-env-equiv-congruence-on-tagenv
  (implies (tag-env-equiv tagenv tagenv-equiv)
           (equal (check-tyspecseq tyspec tagenv)
                  (check-tyspecseq tyspec tagenv-equiv)))
  :rule-classes :congruence)