		Search-engine friendly clone of the ACL2 documentation.

Atc-tag-tables

Atc-type-to-recognizer

ACL2 recognizer corresponding to a C type.

Signature
(atc-type-to-recognizer type prec-tags) → recognizer
Arguments: type — Guard (typep type).; prec-tags — Guard (atc-string-taginfo-alistp prec-tags).
Returns: recognizer — Type (symbolp recognizer).

For a supported integer type, the predicate is the recognizer of values of that type. For a structure type, the predicate is the recognizer of structures of that type. For a pointer to integer type, the predicate is the recognizer of that referenced type. For a pointer to structure type, the predicate is the recognizer of structures of that type. For an array of integer type, the predicate is the recognizer of arrays of that element type.

This is based on our current ACL2 representation of C types, which may be extended in the future. Note that, in the current representation, the predicate corresponding to each type is never a recognizer of pointer values.

Definitions and Theorems

Function: atc-type-to-recognizer

(defun atc-type-to-recognizer (type prec-tags)
 (declare
      (xargs :guard (and (typep type)
                         (atc-string-taginfo-alistp prec-tags))))
 (let ((__function__ 'atc-type-to-recognizer))
  (declare (ignorable __function__))
  (type-case
   type
   :void (raise "Internal error: type ~x0." type)
   :char (raise "Internal error: type ~x0." type)
   :schar 'scharp
   :uchar 'ucharp
   :sshort 'sshortp
   :ushort 'ushortp
   :sint 'sintp
   :uint 'uintp
   :slong 'slongp
   :ulong 'ulongp
   :sllong 'sllongp
   :ullong 'ullongp
   :struct
   (defstruct-info->recognizer
    (atc-tag-info->defstruct (atc-get-tag-info type.tag prec-tags)))
   :pointer
   (type-case
        type.to
        :void (raise "Internal error: type ~x0." type)
        :char (raise "Internal error: type ~x0." type)
        :schar 'scharp
        :uchar 'ucharp
        :sshort 'sshortp
        :ushort 'ushortp
        :sint 'sintp
        :uint 'uintp
        :slong 'slongp
        :ulong 'ulongp
        :sllong 'sllongp
        :ullong 'ullongp
        :struct (defstruct-info->recognizer
                     (atc-tag-info->defstruct
                          (atc-get-tag-info type.to.tag prec-tags)))
        :pointer (raise "Internal error: type ~x0." type)
        :array (raise "Internal error: type ~x0." type))
   :array
   (type-case type.of
              :void (raise "Internal error: type ~x0." type)
              :char (raise "Internal error: type ~x0." type)
              :schar 'schar-arrayp
              :uchar 'uchar-arrayp
              :sshort 'sshort-arrayp
              :ushort 'ushort-arrayp
              :sint 'sint-arrayp
              :uint 'uint-arrayp
              :slong 'slong-arrayp
              :ulong 'ulong-arrayp
              :sllong 'sllong-arrayp
              :ullong 'ullong-arrayp
              :struct (raise "Internal error: type ~x0." type)
              :pointer (raise "Internal error: type ~x0." type)
              :array (raise "Internal error: type ~x0." type)))))

Theorem: symbolp-of-atc-type-to-recognizer

(defthm symbolp-of-atc-type-to-recognizer
  (b* ((recognizer (atc-type-to-recognizer type prec-tags)))
    (symbolp recognizer))
  :rule-classes :rewrite)