Defwellformed
Defwellformed is a macro for introducing well-formedness
checking functions.
Motivation
Throughout VL, there are many functions that check to see whether some
module element is well-formed. When we introduce these well-formedness checks,
we often want to have two versions of the check:
- A vanilla Boolean-valued predicate, foo-okp, that causes no
side effects and is easy to reason about, and
- A debugging function, foo-okp-warn that generates useful warnings that explain precisely why the object is malformed. In particular,
foo-okp-warn takes a warnings accumulator as an extra argument, and
returns (mv okp warnings').
The value of the debugging function is probably obvious: it allows us to
provide a better explanation for why some module is not being translated. But
the debugging function is not well-suited for reasoning. In particular,
in theorems we generally do not care about which warnings have been
accumulated; we only want to know whether some structure is well-formed. If we
try to use the debugging function directly for this purpose, we might write
theorems such as:
(implies (and (foo-p x)
(car (foo-okp-warn x warnings)))
(consequence x))
The problem with such a theorem is that warnings is a free variable,
which can cause problems for ACL2 when it tries to apply the rule.
So, our approach is to introduce both versions of the well-formedness
check, and then add a theorem that shows the first value returned by
foo-okp-warn is exactly the value returned by foo-okp. Accordingly,
we can run foo-okp-warn in our code and get useful warning messages, but
we can always reason about the simpler function foo-okp.
Unfortunately, writing two versions of a function comes at its own cost; we
have to duplicate the code, keep both versions in sync, and write these
boilerplate theorems. The macro defwellformed allows us to automate
this process.
Using defwellformed
The defwellformed macro is similar to defun. The general form
is:
(defwellformed foo-okp (x other-args ...)
:guard (and (foop x) ...)
:body [...]
:extra-decls ((xargs ...))
:parents ...
:short ...
:long ...)
Here, foo-okp is the name of the new vanilla function, and (x
other-args ...) are the formals. The :guard and :body are used in
the defun form we generate, as are any :extra-decls that you need.
Finally, the parents, short, and long fields are as in defxdoc.
The debugging function is always named by appending -warn to the name
of the vanilla function. Having such a convention is necessary for our
implementation of (@wf-call ...).
Meta-macros
The tricky part to using defwellformed is to write a :body that serves
both as the vanilla definition and as the debugging definition. To accomplish
this, we make use of certain "meta-macros", which can be identifier with the
prefix @wf-.
In particular, the bodies of our well-formedness checks generally look
something like this:
(let ((bar ...)
(baz ...))
(@wf-progn
(@wf-assert condition1 [type msg args])
(@wf-assert condition2 [type msg args])
(@wf-note condition type msg args)
(@wf-call other-wf-check ...)
...))
These @wf- expressions are only valid in the body of the
defwellformed command, and are given different expansions depending
upon whether we are in the vanilla or debugging version of the function.
In the vanilla function,
- (@wf-progn ...) becomes (and ...)
- (@wf-and ...) becomes (and ...)
- (@wf-assert condition ...) becomes (if condition t nil)
- (@wf-note condition ...) becomes t
- (@wf-call other-wf-check ...) becomes (other-wf-check ...)
But in the debugging function, a more complex expansion is used.
- (@wf-progn ...)
- This becomes an appropriate mv-let strucutre to handle the return
values from @wf-assert and @ commands. Note that in the debugging
version execution continues after a violation is discovered so that we
uncover as many problems as possible. This behavior can cause problems for
guard verification: you cannot rely upon the earlier assertions having
"passed" in the guards of your later assertions. Hence the introduction of
@wf-and.
- (@wf-and ...)
- This becomes an mv-let structure as in @wf-progn, but
execution stops when any assertion is violated.
- (@wf-assert condition type msg args)
- If the condition is violated, okp becomes nil and we add
a (non-fatal) warning of the indicated type, message, and arguments.
- (@wf-note condition type msg args)
- We add a warning of the indicated type, message, and args, to the list of
warnings, but we do not set okp to nil. That is, this is just a way
to note suspicious things that aren't necessarily outright problems.
- (@wf-call other-wf-check ...)
- Becomes (other-wf-check-warn ...). In other words, this allows you to
call the vanilla version of some subsidiary well-formedness check from the
vanilla version of your function, and the debugging version from your debugging
function.
Note also that defwellformed-list allows you to call a
well-formedness predicate on every element in a list, and that mutual-defwellformed is a replacement for mutual-recursion that allows
for the mutually-recursive use of defwellformed.
