Generate a C external object declaration.
(atc-gen-obj-declon name info prec-objs header) → (mv declon-h declon-c updated-prec-objs)
If the
Function:
(defun atc-gen-obj-declon (name info prec-objs header) (declare (xargs :guard (and (stringp name) (defobject-infop info) (atc-string-objinfo-alistp prec-objs) (booleanp header)))) (let ((__function__ 'atc-gen-obj-declon)) (declare (ignorable __function__)) (b* ((id (defobject-info->name-ident info)) (type (defobject-info->type info)) (initer? (defobject-info->init info)) ((mv tyspec declor) (ident+type-to-tyspec+declor id type)) (declon-h (and header (make-obj-declon :scspec (scspecseq-extern) :tyspec tyspec :declor declor :init? nil))) (declon-c (make-obj-declon :scspec (scspecseq-none) :tyspec tyspec :declor declor :init? initer?)) (info (atc-obj-info info)) (prec-objs (acons (str-fix name) info (atc-string-objinfo-alist-fix prec-objs)))) (mv declon-h declon-c prec-objs))))
Theorem:
(defthm obj-declon-optionp-of-atc-gen-obj-declon.declon-h (b* (((mv ?declon-h ?declon-c ?updated-prec-objs) (atc-gen-obj-declon name info prec-objs header))) (obj-declon-optionp declon-h)) :rule-classes :rewrite)
Theorem:
(defthm obj-declonp-of-atc-gen-obj-declon.declon-c (b* (((mv ?declon-h ?declon-c ?updated-prec-objs) (atc-gen-obj-declon name info prec-objs header))) (obj-declonp declon-c)) :rule-classes :rewrite)
Theorem:
(defthm atc-string-objinfo-alistp-of-atc-gen-obj-declon.updated-prec-objs (b* (((mv ?declon-h ?declon-c ?updated-prec-objs) (atc-gen-obj-declon name info prec-objs header))) (atc-string-objinfo-alistp updated-prec-objs)) :rule-classes :rewrite)
Theorem:
(defthm atc-gen-obj-declon-h-iff-header (b* (((mv ?declon-h ?declon-c ?updated-prec-objs) (atc-gen-obj-declon name info prec-objs header))) (iff declon-h header)))