		Search-engine friendly clone of the ACL2 documentation.

Schemalg-input-processing

Schemalg-process-inputs

Process all the inputs.

Signature
(schemalg-process-inputs old schema schema? list-input list-input? oset-input oset-input? cdr-output cdr-output? tail-output tail-output? fvar-0-name fvar-0-name? fvar-1-name fvar-1-name? fvar-2-name fvar-2-name? algo-name algo-enable spec-0-name spec-0-name? spec-0-enable spec-0-enable? spec-1-name spec-1-name? spec-1-enable spec-1-enable? spec-2-name spec-2-name? spec-2-enable spec-2-enable? equal-algo-name equal-algo-enable new-name new-enable old-if-new-name old-if-new-name? old-if-new-enable old-if-new-enable? verify-guards print show-only ctx state) → (mv erp result state)
Arguments: schema? — Guard (booleanp schema?).; list-input? — Guard (booleanp list-input?).; oset-input? — Guard (booleanp oset-input?).; cdr-output? — Guard (booleanp cdr-output?).; tail-output? — Guard (booleanp tail-output?).; fvar-0-name? — Guard (booleanp fvar-0-name?).; fvar-1-name? — Guard (booleanp fvar-1-name?).; fvar-2-name? — Guard (booleanp fvar-2-name?).; spec-0-name? — Guard (booleanp spec-0-name?).; spec-0-enable? — Guard (booleanp spec-0-enable?).; spec-1-name? — Guard (booleanp spec-1-name?).; spec-1-enable? — Guard (booleanp spec-1-enable?).; spec-2-name? — Guard (booleanp spec-2-name?).; spec-2-enable? — Guard (booleanp spec-2-enable?).; old-if-new-name? — Guard (booleanp old-if-new-name?).; old-if-new-enable? — Guard (booleanp old-if-new-enable?).
Returns: result — A (tuple (old symbolp) (?f symbolp) (x-x1...xn symbolp) (x-a1...am symbolp) (out symbolp) (iorel pseudo-lambdap) (x symbolp) (y symbolp) (?g symbolp) (?g0 symbolp) (?g1 symbolp) (?h symbolp) (?f1...?fp symbol-listp) (algo symbolp) (spec-0 symbolp) (spec-1 symbolp) (spec-2 symbolp) (equal-algo symbolp) (new symbolp) (new-enable booleanp) (old-if-new symbolp) (old-if-new-enable booleanp) (verify-guards booleanp) (updated-names-to-avoid symbol-listp) result).

Definitions and Theorems

Function: schemalg-process-inputs

(defun schemalg-process-inputs
       (old schema schema? list-input
            list-input? oset-input oset-input?
            cdr-output cdr-output? tail-output
            tail-output? fvar-0-name fvar-0-name?
            fvar-1-name fvar-1-name? fvar-2-name
            fvar-2-name? algo-name algo-enable
            spec-0-name spec-0-name? spec-0-enable
            spec-0-enable? spec-1-name spec-1-name?
            spec-1-enable spec-1-enable?
            spec-2-name spec-2-name? spec-2-enable
            spec-2-enable? equal-algo-name
            equal-algo-enable new-name new-enable
            old-if-new-name old-if-new-name?
            old-if-new-enable old-if-new-enable?
            verify-guards print show-only ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (booleanp schema?)
                             (booleanp list-input?)
                             (booleanp oset-input?)
                             (booleanp cdr-output?)
                             (booleanp tail-output?)
                             (booleanp fvar-0-name?)
                             (booleanp fvar-1-name?)
                             (booleanp fvar-2-name?)
                             (booleanp spec-0-name?)
                             (booleanp spec-0-enable?)
                             (booleanp spec-1-name?)
                             (booleanp spec-1-enable?)
                             (booleanp spec-2-name?)
                             (booleanp spec-2-enable?)
                             (booleanp old-if-new-name?)
                             (booleanp old-if-new-enable?))))
 (let ((__function__ 'schemalg-process-inputs))
  (declare (ignorable __function__))
  (b*
   ((names-to-avoid nil)
    ((er (list old ??f x-x1...xn x-a1...am out iorel))
     (process-input-old-soft-io-sel-mod
          old verify-guards ctx state))
    ((er &)
     (schemalg-process-schema schema schema? ctx state))
    ((er (list x y ??g ??g0 ??g1 ??h ??f1...?fp
               spec-0 spec-1 spec-2 names-to-avoid))
     (schemalg-process-schema-inputs
          schema list-input list-input?
          oset-input oset-input? cdr-output
          cdr-output? tail-output tail-output?
          fvar-0-name fvar-0-name? fvar-1-name
          fvar-1-name? fvar-2-name fvar-2-name?
          spec-0-name spec-0-name? spec-0-enable
          spec-0-enable? spec-1-name spec-1-name?
          spec-1-enable spec-1-enable?
          spec-2-name spec-2-name? spec-2-enable
          spec-2-enable? old ?f x-x1...xn
          x-a1...am names-to-avoid ctx state))
    ((er (list algo names-to-avoid))
     (schemalg-process-algo-name
          algo-name
          ?f ?f1...?fp names-to-avoid ctx state))
    ((er &)
     (ensure-value-is-boolean$ algo-enable
                               "The :ALGO-ENABLE input" t nil))
    ((er (list equal-algo names-to-avoid))
     (schemalg-process-equal-algo-name
          equal-algo-name
          ?f algo names-to-avoid ctx state))
    ((er &)
     (ensure-value-is-boolean$
          equal-algo-enable
          "The :EQUAL-ALGO-ENABLE input" t nil))
    ((er (list new names-to-avoid))
     (process-input-new-name new-name old names-to-avoid ctx state))
    ((er new-enable)
     (process-input-new-enable new-enable old ctx state))
    ((er (list old-if-new names-to-avoid))
     (process-input-old-if-new-name
          old-if-new-name old-if-new-name?
          old new names-to-avoid ctx state))
    ((er old-if-new-enable)
     (process-input-old-if-new-enable old-if-new-enable
                                      old-if-new-enable? ctx state))
    ((er verify-guards)
     (process-input-verify-guards verify-guards old ctx state))
    ((er &)
     (evmac-process-input-print print ctx state))
    ((er &)
     (evmac-process-input-show-only show-only ctx state)))
   (value (list old ?f x-x1...xn x-a1...am
                out iorel x y ?g ?g0 ?g1 ?h ?f1...?fp
                algo spec-0 spec-1 spec-2 equal-algo new
                new-enable old-if-new old-if-new-enable
                verify-guards names-to-avoid)))))