|
|
|---|
|
|
|
|---|
Input processing in event macros.
Event macros normally take inputs from the user. Thus, it is generally necessary to validate these inputs, and often transform them slightly (e.g. supply a default value, or translate a term), derive additional information from them (e.g. retrieve the formals and guard of a function symbol), etc. We call all of this `input processing'.
Input processing is normally the first thing that an event macro implementation does, before using the result of input processing to generate event, possibly files, etc.
Event macro applicability conditions are a form of input validation, but we do not consider them part of input processing, for the purpose of this event macro library. Applicability conditions are ``deep'', undecidable checks, while the input validation that is part of input processing is normally decidable, and often relatively simple. There are also cases in which the inputs cannot completely validated until they are subjected to the more core processing performed by the event macro, e.g. if the event macro is a code generator for ACL2, it may be more natural to perform certain validation checks on ACL2 terms while they are being translated to constructs of the target language. These examples show that input processing does not necessarily perform a complete validation of the inputs of the event macro; it only makes those that can be conveniently done as a first phase in the macro, before the phase(s) to generate events, files, etc.
An event macros should throw soft errors when some input validation fails. This allows the soft errors to be potentially caught programmatically, when an event macro is used that way. Hard errors should be used only for internal implementation errors, e.g. some expected condition that fails to hold.