		Search-engine friendly clone of the ACL2 documentation.

Schemalg-input-processing

Schemalg-check-allowed-input

Check whether an input is allowed for the current schema.

This macro produces a term, to be bound to (er &) in a b*, that checks whether, if an input is present, the keyword in the variable schema is among a list of allowed schemas. The input? argument must be the a variable that contains the boolean flag saying whether a certain input is present or not; the name of this variable must be the name of the input followed by a ?. The schemas-allowed arguments must be schemas for which the input is question may be present.

Macro: schemalg-check-allowed-input

(defmacro schemalg-check-allowed-input
          (input? &rest schemas-allowed)
 (declare (xargs :guard (and (symbolp input?)
                             (keyword-listp schemas-allowed))))
 (cons
  'if
  (cons
   (cons
    'and
    (cons
     input?
     (cons
          (cons 'not
                (cons (cons 'member-eq
                            (cons 'schema
                                  (cons (cons 'list schemas-allowed)
                                        'nil)))
                      'nil))
          'nil)))
   (cons
    (cons
     'er-soft+
     (cons
      'ctx
      (cons
       't
       (cons
        'nil
        (cons
         '"The ~x0 input can be present only if ~
                  the :SCHEMA input is ~v1, but that input is ~x2 instead."
         (cons
           (b*
             ((input?-string (symbol-name input?))
              (input-string (subseq input?-string
                                    0 (1- (length input?-string)))))
             (intern input-string "KEYWORD"))
           (cons (cons 'list schemas-allowed)
                 '(schema))))))))
    '((value nil))))))