		Search-engine friendly clone of the ACL2 documentation.

Atc-event-and-code-generation

Atc-gen-ext-declon-lists

Generate two lists of C external declarations from the targets, including generating C loops from recursive ACL2 functions.

Signature
(atc-gen-ext-declon-lists targets prec-fns prec-tags prec-objs proofs prog-const init-fun-env-thm fn-thms fn-appconds appcond-thms header print names-to-avoid state) → (mv erp exts-h exts-c events updated-names-to-avoid)
Arguments: targets — Guard (symbol-listp targets).; prec-fns — Guard (atc-symbol-fninfo-alistp prec-fns).; prec-tags — Guard (atc-string-taginfo-alistp prec-tags).; prec-objs — Guard (atc-string-objinfo-alistp prec-objs).; proofs — Guard (booleanp proofs).; prog-const — Guard (symbolp prog-const).; init-fun-env-thm — Guard (symbolp init-fun-env-thm).; fn-thms — Guard (symbol-symbol-alistp fn-thms).; fn-appconds — Guard (symbol-symbol-alistp fn-appconds).; appcond-thms — Guard (keyword-symbol-alistp appcond-thms).; header — Guard (booleanp header).; print — Guard (evmac-input-print-p print).; names-to-avoid — Guard (symbol-listp names-to-avoid).
Returns: exts-h — Type (ext-declon-listp exts-h).; exts-c — Type (ext-declon-listp exts-c).; events — Type (pseudo-event-form-listp events).; updated-names-to-avoid — Type (symbol-listp updated-names-to-avoid), given (symbol-listp names-to-avoid).

The first list, exts-h, is for the generated header; the second list, exts-c, is for the generated source file. The flag header controls whether the header is generated or not: if the flag is nil, exts-h is empty, i.e. we only generate external declarations for the source file.

If the header is generated, all the structs and external objects go there, while only declarations for the functions go there; furthermore, the external objects have no initializers there. The function definitions go into the source file, together with the external objects that have initializers. If the header is not generated, everything goes into the source file.

Definitions and Theorems

Function: atc-gen-ext-declon-lists

(defun atc-gen-ext-declon-lists
       (targets prec-fns prec-tags prec-objs
                proofs prog-const init-fun-env-thm
                fn-thms fn-appconds appcond-thms
                header print names-to-avoid state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbol-listp targets)
                             (atc-symbol-fninfo-alistp prec-fns)
                             (atc-string-taginfo-alistp prec-tags)
                             (atc-string-objinfo-alistp prec-objs)
                             (booleanp proofs)
                             (symbolp prog-const)
                             (symbolp init-fun-env-thm)
                             (symbol-symbol-alistp fn-thms)
                             (symbol-symbol-alistp fn-appconds)
                             (keyword-symbol-alistp appcond-thms)
                             (booleanp header)
                             (evmac-input-print-p print)
                             (symbol-listp names-to-avoid))))
 (let ((__function__ 'atc-gen-ext-declon-lists))
  (declare (ignorable __function__))
  (b*
   (((reterr) nil nil nil nil)
    (wrld (w state))
    ((when (endp targets))
     (retok nil nil nil names-to-avoid))
    (target (car targets))
    ((erp exts-h exts-c prec-fns prec-tags
          prec-objs events names-to-avoid)
     (b*
      (((reterr) nil nil nil nil nil nil nil)
       ((when (function-symbolp target wrld))
        (b*
         ((fn target)
          ((when (eq fn 'quote))
           (reterr
                (raise "Internal error: QUOTE target function.")))
          ((unless (logicp fn wrld))
           (reterr (raise "Internal error: ~x0 not in logic mode."
                          fn)))
          ((erp exts-h
                exts-c prec-fns events names-to-avoid)
           (if
            (irecursivep+ fn wrld)
            (b*
              (((reterr) nil nil nil nil nil)
               ((erp events prec-fns names-to-avoid)
                (atc-gen-loop fn prec-fns
                              prec-tags prec-objs proofs prog-const
                              fn-thms fn-appconds appcond-thms
                              print names-to-avoid state)))
              (retok nil nil prec-fns events names-to-avoid))
            (b*
             (((reterr) nil nil nil nil nil)
              ((erp fundef events prec-fns names-to-avoid)
               (atc-gen-fundef fn prec-fns prec-tags prec-objs
                               proofs prog-const init-fun-env-thm
                               fn-thms print names-to-avoid state))
              (ext (ext-declon-fundef fundef)))
             (if header
                 (retok (list (ext-declon-fun-declon
                                   (fundef-to-fun-declon fundef)))
                        (list ext)
                        prec-fns events names-to-avoid)
               (retok nil (list ext)
                      prec-fns events names-to-avoid))))))
         (retok exts-h exts-c prec-fns prec-tags
                prec-objs events names-to-avoid)))
       (name (symbol-name target))
       (info (defstruct-table-lookup name wrld))
       ((when info)
        (b* (((mv tag-declon
                  tag-thms prec-tags names-to-avoid)
              (atc-gen-tag-declon name info prec-tags
                                  proofs names-to-avoid (w state)))
             (ext (ext-declon-tag-declon tag-declon)))
          (if header (retok (list ext)
                            nil prec-fns prec-tags
                            prec-objs tag-thms names-to-avoid)
            (retok nil (list ext)
                   prec-fns prec-tags
                   prec-objs tag-thms names-to-avoid))))
       (info (defobject-table-lookup name (w state)))
       ((when info)
        (b* (((mv obj-declon-h obj-declon-c prec-objs)
              (atc-gen-obj-declon name info prec-objs header)))
          (if header
              (retok (list (ext-declon-obj-declon obj-declon-h))
                     (list (ext-declon-obj-declon obj-declon-c))
                     prec-fns
                     prec-tags prec-objs nil names-to-avoid)
            (retok nil
                   (list (ext-declon-obj-declon obj-declon-c))
                   prec-fns prec-tags
                   prec-objs nil names-to-avoid)))))
      (reterr
       (raise
        "Internal error: ~
                          target ~x0 is not ~
                          a function or DEFSTRUCT or DEFOBJECT."
        target))))
    ((erp more-exts-h
          more-exts-c more-events names-to-avoid)
     (atc-gen-ext-declon-lists (cdr targets)
                               prec-fns prec-tags prec-objs
                               proofs prog-const init-fun-env-thm
                               fn-thms fn-appconds appcond-thms
                               header print names-to-avoid state)))
   (retok (append exts-h more-exts-h)
          (append exts-c more-exts-c)
          (append events more-events)
          names-to-avoid))))

Theorem: ext-declon-listp-of-atc-gen-ext-declon-lists.exts-h

(defthm ext-declon-listp-of-atc-gen-ext-declon-lists.exts-h
  (b*
    (((mv acl2::?erp ?exts-h
          ?exts-c ?events ?updated-names-to-avoid)
      (atc-gen-ext-declon-lists targets prec-fns prec-tags prec-objs
                                proofs prog-const init-fun-env-thm
                                fn-thms fn-appconds appcond-thms
                                header print names-to-avoid state)))
    (ext-declon-listp exts-h))
  :rule-classes :rewrite)

Theorem: ext-declon-listp-of-atc-gen-ext-declon-lists.exts-c

(defthm ext-declon-listp-of-atc-gen-ext-declon-lists.exts-c
  (b*
    (((mv acl2::?erp ?exts-h
          ?exts-c ?events ?updated-names-to-avoid)
      (atc-gen-ext-declon-lists targets prec-fns prec-tags prec-objs
                                proofs prog-const init-fun-env-thm
                                fn-thms fn-appconds appcond-thms
                                header print names-to-avoid state)))
    (ext-declon-listp exts-c))
  :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-atc-gen-ext-declon-lists.events

(defthm pseudo-event-form-listp-of-atc-gen-ext-declon-lists.events
  (b*
    (((mv acl2::?erp ?exts-h
          ?exts-c ?events ?updated-names-to-avoid)
      (atc-gen-ext-declon-lists targets prec-fns prec-tags prec-objs
                                proofs prog-const init-fun-env-thm
                                fn-thms fn-appconds appcond-thms
                                header print names-to-avoid state)))
    (pseudo-event-form-listp events))
  :rule-classes :rewrite)

Theorem: symbol-listp-of-atc-gen-ext-declon-lists.updated-names-to-avoid

(defthm
    symbol-listp-of-atc-gen-ext-declon-lists.updated-names-to-avoid
 (implies
   (symbol-listp names-to-avoid)
   (b*
    (((mv acl2::?erp ?exts-h
          ?exts-c ?events ?updated-names-to-avoid)
      (atc-gen-ext-declon-lists targets prec-fns prec-tags prec-objs
                                proofs prog-const init-fun-env-thm
                                fn-thms fn-appconds appcond-thms
                                header print names-to-avoid state)))
    (symbol-listp updated-names-to-avoid)))
 :rule-classes :rewrite)