		Search-engine friendly clone of the ACL2 documentation.

Atc-event-and-code-generation

Atc-gen-everything

Generate the file and the events.

Signature
(atc-gen-everything targets file-name path-wo-ext header pretty-printing proofs prog-const wf-thm fn-thms print call state) → (mv erp event)
Arguments: targets — Guard (symbol-listp targets).; file-name — Guard (stringp file-name).; path-wo-ext — Guard (stringp path-wo-ext).; header — Guard (booleanp header).; pretty-printing — Guard (pprint-options-p pretty-printing).; proofs — Guard (booleanp proofs).; prog-const — Guard (symbolp prog-const).; wf-thm — Guard (symbolp wf-thm).; fn-thms — Guard (symbol-symbol-alistp fn-thms).; print — Guard (evmac-input-print-p print).; call — Guard (pseudo-event-formp call).
Returns: event — Type (pseudo-event-formp event).

We locally install the ``trivial ancestor check'' from the library. We found at least a case in which ACL2's default heuristic ancestor check prevented a valid functional correctness theorem from being proved. Since by construction the symbolic execution should always terminate, it does not seem like ACL2's heuristic ancestor check would ever be helpful (if this turns out to be wrong, we will re-evaluate). Thus, we locally install the simpler ancestor check.

We also (locally, implicitly) allow variables to be ignored. Ignored variables may arise in the correctness theorems for loop bodies: atc-loop-body-term-subst replaces recursive calls, which include all the formals of the loop function, with just the affected variables, which may be a subset of the formals; if the call is the body of a let, the formals that are not affected then become ignored.

Definitions and Theorems

Function: atc-gen-everything

(defun atc-gen-everything
       (targets file-name path-wo-ext
                header pretty-printing proofs prog-const
                wf-thm fn-thms print call state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbol-listp targets)
                             (stringp file-name)
                             (stringp path-wo-ext)
                             (booleanp header)
                             (pprint-options-p pretty-printing)
                             (booleanp proofs)
                             (symbolp prog-const)
                             (symbolp wf-thm)
                             (symbol-symbol-alistp fn-thms)
                             (evmac-input-print-p print)
                             (pseudo-event-formp call))))
 (let ((__function__ 'atc-gen-everything))
  (declare (ignorable __function__))
  (b*
   (((reterr) '(_))
    (names-to-avoid (list* prog-const wf-thm (strip-cdrs fn-thms)))
    ((erp fileset events &)
     (atc-gen-fileset targets path-wo-ext
                      proofs prog-const wf-thm fn-thms
                      header print names-to-avoid state))
    (fileset-gen-event
         (atc-gen-fileset-event fileset
                                file-name pretty-printing print))
    (assert-events
         (atc-gen-thm-assert-events wf-thm fn-thms proofs))
    (encapsulate
     (cons
      'encapsulate
      (cons
       'nil
       (cons
        '(evmac-prepare-proofs)
        (cons
         '(local (acl2::use-trivial-ancestors-check))
         (cons '(set-ignore-ok t)
               (append events
                       (append assert-events
                               (cons fileset-gen-event 'nil))))))))
)
    (encapsulate+ (restore-output? (eq print :all)
                                   encapsulate))
    (info (make-atc-call-info :encapsulate encapsulate))
    (table-event (atc-table-record-event call info)))
   (retok (cons 'progn
                (cons encapsulate+
                      (cons table-event
                            '((value-triple :invisible)))))))))

Theorem: pseudo-event-formp-of-atc-gen-everything.event

(defthm pseudo-event-formp-of-atc-gen-everything.event
  (b* (((mv acl2::?erp acl2::?event)
        (atc-gen-everything targets file-name path-wo-ext
                            header pretty-printing proofs prog-const
                            wf-thm fn-thms print call state)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)