		Search-engine friendly clone of the ACL2 documentation.

Atc-event-and-code-generation

Atc-gen-obj-declon

Generate a C external object declaration.

Signature
(atc-gen-obj-declon name info prec-objs header) → (mv declon-h declon-c updated-prec-objs)
Arguments: name — Guard (stringp name).; info — Guard (defobject-infop info).; prec-objs — Guard (atc-string-objinfo-alistp prec-objs).; header — Guard (booleanp header).
Returns: declon-h — Type (obj-declon-optionp declon-h).; declon-c — Type (obj-declonp declon-c).; updated-prec-objs — Type (atc-string-objinfo-alistp updated-prec-objs).

If the :header input is t, we generate two declarations: one for the header, with extern and without initializer (whether the defobject has an initializer or not); and one for the source file, without extern, and with or without the intiializer depending of whether the defobject has it or not. If instead the :header input is nil, we generate one declaration, for the source file, without extern, and with or without the intiializer depending of whether the defobject has it or not. In other words, we always generate a declaration for the source file, the same regardless of :header, and we optionally generate an extern one for the header, always without initializer. The extern serves so that the declaration does not count like a tentative definition, and the only definition (tentative if it has no initializer) is in the source file.

Definitions and Theorems

Function: atc-gen-obj-declon

(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: obj-declon-optionp-of-atc-gen-obj-declon.declon-h

(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: obj-declonp-of-atc-gen-obj-declon.declon-c

(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: atc-string-objinfo-alistp-of-atc-gen-obj-declon.updated-prec-objs

(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: atc-gen-obj-declon-h-iff-header

(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)))