		Search-engine friendly clone of the ACL2 documentation.

Schemalg-event-generation

Schemalg-gen-algo

Generate the function algo[?f1]...[?fp].

Signature
(schemalg-gen-algo schema algo algo-enable x-z1...zm x ?g ?g0 ?g1 ?h verify-guards) → (mv local-event exported-event)
Arguments: schema — Guard (keywordp schema).; algo — Guard (symbolp algo).; algo-enable — Guard (booleanp algo-enable).; x-z1...zm — Guard (symbol-listp x-z1...zm).; x — Guard (symbolp x).; ?g — Guard (symbolp ?g).; ?g0 — Guard (symbolp ?g0).; ?g1 — Guard (symbolp ?g1).; ?h — Guard (symbolp ?h).; verify-guards — Guard (booleanp verify-guards).
Returns: local-event — Type (pseudo-event-formp local-event).; exported-event — Type (pseudo-event-formp exported-event).

Definitions and Theorems

Function: schemalg-gen-algo

(defun schemalg-gen-algo
       (schema algo algo-enable
               x-z1...zm x ?g ?g0 ?g1 ?h verify-guards)
 (declare (xargs :guard (and (keywordp schema)
                             (symbolp algo)
                             (booleanp algo-enable)
                             (symbol-listp x-z1...zm)
                             (symbolp x)
                             (symbolp ?g)
                             (symbolp ?g0)
                             (symbolp ?g1)
                             (symbolp ?h)
                             (booleanp verify-guards))))
 (let ((__function__ 'schemalg-gen-algo))
  (declare (ignorable __function__))
  (case schema
    (:divconq-list-0-1 (schemalg-gen-algo-divconq-list-0-1
                            algo algo-enable
                            x-z1...zm x ?g ?h verify-guards))
    (:divconq-list-0-1-2 (schemalg-gen-algo-divconq-list-0-1-2
                              algo algo-enable
                              x-z1...zm x ?g0 ?g1 ?h verify-guards))
    (:divconq-oset-0-1 (schemalg-gen-algo-divconq-oset-0-1
                            algo algo-enable
                            x-z1...zm x ?g ?h verify-guards))
    (t (prog2$ (raise "Internal error: unknown schema ~x0."
                      schema)
               (mv '(irrelevant) '(irrelevant)))))))

Theorem: pseudo-event-formp-of-schemalg-gen-algo.local-event

(defthm pseudo-event-formp-of-schemalg-gen-algo.local-event
  (b* (((mv ?local-event ?exported-event)
        (schemalg-gen-algo schema algo algo-enable x-z1...zm
                           x ?g ?g0 ?g1 ?h verify-guards)))
    (pseudo-event-formp local-event))
  :rule-classes :rewrite)

Theorem: pseudo-event-formp-of-schemalg-gen-algo.exported-event

(defthm pseudo-event-formp-of-schemalg-gen-algo.exported-event
  (b* (((mv ?local-event ?exported-event)
        (schemalg-gen-algo schema algo algo-enable x-z1...zm
                           x ?g ?g0 ?g1 ?h verify-guards)))
    (pseudo-event-formp exported-event))
  :rule-classes :rewrite)