		Search-engine friendly clone of the ACL2 documentation.

Atc-implementation

Atc-process-inputs-and-gen-everything

Process the inputs and generate the events and code.

Signature
(atc-process-inputs-and-gen-everything args call state) → (mv erp event state)
Arguments: args — Guard (true-listp args).; call — Guard (pseudo-event-formp call).
Returns: event — Type (pseudo-event-formp event).

Definitions and Theorems

Function: atc-process-inputs-and-gen-everything

(defun atc-process-inputs-and-gen-everything (args call state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (true-listp args)
                             (pseudo-event-formp call))))
 (let ((__function__ 'atc-process-inputs-and-gen-everything))
  (declare (ignorable __function__))
  (b* (((reterr) '(_) state)
       ((when (atc-table-lookup call (w state)))
        (retok '(value-triple :redundant)
               state))
       ((erp targets file-name path-wo-ext
             header pretty-printing proofs prog-const
             wf-thm fn-thms & & print state)
        (atc-process-inputs args state))
       ((erp event)
        (atc-gen-everything targets file-name path-wo-ext
                            header pretty-printing proofs prog-const
                            wf-thm fn-thms print call state)))
    (retok event state))))

Theorem: pseudo-event-formp-of-atc-process-inputs-and-gen-everything.event

(defthm
  pseudo-event-formp-of-atc-process-inputs-and-gen-everything.event
  (b* (((mv acl2::?erp acl2::?event acl2::?state)
        (atc-process-inputs-and-gen-everything args call state)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)