ACL2 recognizer corresponding to a C type.
(atc-type-to-recognizer type prec-tags) → 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.
Function:
(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:
(defthm symbolp-of-atc-type-to-recognizer (b* ((recognizer (atc-type-to-recognizer type prec-tags))) (symbolp recognizer)) :rule-classes :rewrite)