Generate two lists of C external declarations from the targets, including generating C loops from recursive ACL2 functions.
(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)
The first list,
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.
Function:
(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:
(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:
(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:
(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:
(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)