|
|
|---|
|
|
|
|---|
Generators of template ACL2 events.
These utilities generate ``schematic'' ACL2 events, i.e. events built out of constrained functions that are meant to represent classes of events of a certain form. An example is a function definition
(defun f (x) (if (a x) (b x) (c x (f (d x)))))
where
These utilities provide macros to generate templates of various forms. More macros may be added to the current initial selection. Existing macros may be renamed to maintain rational and uniform naming as more macros are added.
A use for the templates generated by these macros is in testing tools that manipulate ACL2 events, e.g. APT transformations. Assuming that the tools operate somewhat ``uniformly'' (in a suitably sense) on ACL2 events, testing the tools on a template can be regarded as somewhat equivalent to testing the tools on all the instances of the template. This uniformity assumption may not be quite true, e.g. due to prover heuristics, but a template may still ``cover'' a large class of its instances.