		Search-engine friendly clone of the ACL2 documentation.

Schemalg-event-generation

Schemalg-gen-spec-2

Generate the function spec-2[?h].

Signature
(schemalg-gen-spec-2 schema spec-2 spec-2-enable old x-x1...xn x-a1...am x y iorel ?h verify-guards wrld) → (mv local-event exported-event)
Arguments: schema — Guard (keywordp schema).; spec-2 — Guard (symbolp spec-2).; spec-2-enable — Guard (booleanp spec-2-enable).; old — Guard (symbolp old).; x-x1...xn — Guard (symbol-listp x-x1...xn).; x-a1...am — Guard (pseudo-term-listp x-a1...am).; x — Guard (symbolp x).; y — Guard (symbolp y).; iorel — Guard (pseudo-lambdap iorel).; ?h — Guard (symbolp ?h).; verify-guards — Guard (booleanp verify-guards).; wrld — Guard (plist-worldp wrld).
Returns: local-event — A pseudo-event-formp.; exported-event — A pseudo-event-formp.

Definitions and Theorems

Function: schemalg-gen-spec-2

(defun schemalg-gen-spec-2
       (schema spec-2
               spec-2-enable old x-x1...xn x-a1...am
               x y iorel ?h verify-guards wrld)
 (declare (xargs :guard (and (keywordp schema)
                             (symbolp spec-2)
                             (booleanp spec-2-enable)
                             (symbolp old)
                             (symbol-listp x-x1...xn)
                             (pseudo-term-listp x-a1...am)
                             (symbolp x)
                             (symbolp y)
                             (pseudo-lambdap iorel)
                             (symbolp ?h)
                             (booleanp verify-guards)
                             (plist-worldp wrld))))
 (let ((__function__ 'schemalg-gen-spec-2))
  (declare (ignorable __function__))
  (case schema
   (:divconq-list-0-1
        (prog2$ (raise "Internal error: schema is ~x0." schema)
                (mv '(irrelevant) '(irrelevant))))
   (:divconq-list-0-1-2
    (b*
     ((cdr-x-x1...xn (loop$ for var in x-x1...xn collect
                            (if (eq var x) (list 'cdr var) var)))
      (car-x-a1...am (loop$ for term in x-a1...am collect
                            (if (eq term x) (list 'car term) term)))
      (iorel-term1
           (apply-term iorel (append cdr-x-x1...xn (list y))))
      (??h-call (cons ?h
                      (append car-x-a1...am (cons y 'nil))))
      (iorel-term2 (apply-term iorel
                               (append x-x1...xn (list ?h-call))))
      (iorel-term1 (untranslate iorel-term1 t wrld))
      (iorel-term2 (untranslate iorel-term2 t wrld)))
     (evmac-generate-soft-defun-sk2
      spec-2
      :formals nil
      :guard t
      :body
      (cons
       'forall
       (cons
        (append x-x1...xn (cons y 'nil))
        (cons
         (cons
          'impliez
          (cons
           (cons
            'and
            (cons (cons 'consp (cons x 'nil))
                  (cons (cons 'consp
                              (cons (cons 'cdr (cons x 'nil)) 'nil))
                        (cons iorel-term1 'nil))))
           (cons iorel-term2 'nil)))
         'nil)))
      :verify-guards verify-guards
      :enable spec-2-enable
      :guard-hints
      (cons (cons '"Goal"
                  (cons ':use
                        (cons (cons ':guard-theorem (cons old 'nil))
                              'nil)))
            'nil))))
   (:divconq-oset-0-1
        (prog2$ (raise "Internal error: schema is ~x0." schema)
                (mv '(irrelevant) '(irrelevant))))
   (t (prog2$ (raise "Internal error: unknown schema ~x0."
                     schema)
              (mv '(irrelevant) '(irrelevant)))))))