Process the
(defobject-process-type type) → (mv erp type)
If successful, we return the C type specified by the input.
Function:
(defun defobject-process-type (type) (declare (xargs :guard t)) (let ((__function__ 'defobject-process-type)) (declare (ignorable __function__)) (b* (((reterr) (irr-type)) (msg (msg "The :TYPE input ~x0 must be ~ either an element of ~x1 ~ or a list of two elements ~ where the first is an element of ~x1 ~ and the second is a positive integer ~ not exceeding ~x2." type *nonchar-integer-fixtypes* (ullong-max)))) (if (atom type) (b* (((unless (symbolp type)) (reterr msg)) (ctype (fixtype-to-integer-type type)) ((unless ctype) (reterr msg))) (retok ctype)) (b* (((unless (std::tuplep 2 type)) (reterr msg)) ((list elemfixtype size) type) ((unless (symbolp elemfixtype)) (reterr msg)) (elemtype (fixtype-to-integer-type elemfixtype)) ((unless elemtype) (reterr msg)) ((unless (posp size)) (reterr msg)) ((unless (<= size (ullong-max))) (reterr msg))) (retok (make-type-array :of elemtype :size size)))))))
Theorem:
(defthm typep-of-defobject-process-type.type (b* (((mv acl2::?erp ?type) (defobject-process-type type))) (typep type)) :rule-classes :rewrite)