		Search-engine friendly clone of the ACL2 documentation.

Event-macro-applicability-condition-utilities

Make-evmac-appcond?

Conditionally construct an applicability condition.

Event macros sometimes have applicability conditions that are present (i.e. that must be proved) only under certain conditions on the inputs. An example is the applicability conditions related to guards in APT transformations, which are present only if guards must be verified.

This function provides a convenient way for event macros to generate either nil or a singleton list of an applicability condition with given :name and :formula, based on whether the :when input is nil or not. We treat the latter input as a boolean, but do not require it to be, for greater flexibility (e.g. so that member can be used); its default is t, i.e. generate the applicability condition unless an explicit condition (which may hold or not) is given.

An event macro may generate all its applicability conditions by appending calls of this function.

Note that this macro expands into a non-strict and form, so that the name and formula arguments are not evaluated if the condition evaluates to nil. This is important if the evaluation of the name and formula (most likely the formula, as the name is often just a keyword constant) only makes sense (in particular, does not cause an error) under the condition.

Macro: make-evmac-appcond?

(defmacro make-evmac-appcond? (name formula &key (when 't))
 (cons
  'and
  (cons
   when
   (cons
    (cons
     'list
     (cons (cons 'make-evmac-appcond
                 (cons ':name
                       (cons name
                             (cons ':formula (cons formula 'nil)))))
           'nil))
    'nil))))