Fgl-rewrite-rules
Differences between FGL and ACL2 rewrite rules
FGL rewrite rules are essentially just ACL2 rewrite rules. More
specifically, they are derived from formulas that have basically the same form
as ACL2 rewrite rules; they need not be stored with
:rule-classes :rewrite. FGL uses a different set of rules than the ones
that are enabled for use in ACL2, because not all good ACL2 rewrite rules are
good FGL rewrite rules, and
vice versa. A particularly important difference is that syntaxp and
bind-free forms receive FGL symbolic
objects as their inputs, rather than ACL2 terms. FGL rewrite rules also
allow special constructs bind-var, binder, and syntax-bind
which allow free variables to be bound as with bind-free, but in the RHS
of the rewrite rule rather than in the hyps. They additionally support a form
abort-rewrite which causes the application of the rule to be aborted
when encountered in the RHS, similarly to if a hypothesis was not relieved.
Creating and Removing FGL Rewrite Rules
An FGL rewrite rule is an ACL2 rewrite rule. You can register an existing
ACL2 theorem for use as an FGL rewrite rule using:
(fgl::add-fgl-rewrite my-rule)
And you can disable that rule for use by FGL using:
(fgl::remove-fgl-rewrite my-rule)
To create a new rewrite rule and enable it for FGL, you may use:
(fgl::def-fgl-rewrite my-rule
body
:hints ...)
This just expands to:
(defthmd my-rule ...)
(fgl::add-fgl-rewrite my-rule)
FGL also supports rewrite rules that are triggered not on the leading
function symbol of the LHS, but on the leading function symbol of an
if-then-else branch. These rules can be added using
(fgl::add-fgl-branch-merge my-rule) and they can be created using:
(fgl::def-fgl-branch-merge my-rule
body
...)
A suitable branch merge rule has a left-hand side of the form (if test
then else) where then is a function call. Generally, test and
else should be free variables, but this isn't a hard and fast rule.
Advanced Features
FGL rewrite rules support ACL2's syntaxp and bind-free
hypothesis forms. However, it generally won't work to use the same rewrite
rule in both the ACL2 and FGL rewriters if it has syntaxp or bind-free
hypotheses, because in FGL the variables in the syntaxp/bind-free forms will be
bound to symbolic objects, whereas in ACL2 they will be bound to
terms. Therefore to use syntaxp, bind-free, and bind-var (discussed below),
one needs to be familiar with FGL symbolic objects -- see fgl-object.
Two additional features support a new style of programming rewrite rules.
Bind-var and syntax-bind allow functionality similar to bind-free,
but available within the right-hand side of a rewrite rule. Abort-rewrite
allows the rewrite operation to be cancelled partway through interpreting the
right-hand side.
Here is an example that uses both syntax-bind and abort-rewrite, from
"bitops.lisp":
(def-fgl-rewrite logtail-to-logtail-helper
(implies (syntaxp (not (fgl-object-case n :g-concrete)))
(equal (logtail n x)
(b* ((x (int x))
(n (nfix (int n)))
((when (syntax-bind n-concrete (fgl-object-case n :g-concrete)))
(logtail n x))
(n-width (syntax-bind n-width (fgl-object-case n
:g-integer (max 0 (1- (len n.bits)))
:otherwise nil)))
((unless (and n-width
(check-unsigned-byte-p n-width n)))
(abort-rewrite (logtail n x)))
(n-rev (int-revapp n-width n 0)))
(logtail-helper n-rev n-width x)))))
When attempting to apply this rewrite rule, the FGL rewriter starts in much
the same way as the ACL2 rewriter. As a precondition for attempting to apply
this rule, the term we are rewriting must be a call of logtail, and that call
must unify with the LHS of this rule -- in this case any call of logtail will
do so.
Next, we relieve the hyps. This rule only has one hyp, which is a
syntaxp call; we check that n is not a :g-concrete object.
Then we proceed by interpreting the RHS. We bind x to the result of
rewriting (int x) (where int is an alias for ifix and rebind
n to the result of rewriting (nfix (int n)), and then we encounter
our first syntax-bind form. The syntax-bind form has the free variable
n-concrete, which is here to logically represent the result we get from
evaluating the syntax-bind form. A syntax-bind form is logically equivalent to
its first argument, so when we prove logtail-to-logtail-helper correct we
prove it with the free variable n-concrete in place of the syntax-bind.
That means we are logically justified in returning anything we want from the
syntax-bind form -- since n-concrete is a free variable not previously bound,
the rule is applicable for any value of n-concrete. In this case we evaluate
(fgl-object-case n :g-concrete). (Note: syntax-bind is a macro that
uses the primitive forms bind-var and syntax-interp to implement
this behavior; see their documentation for more general usage.) This will
produce a Boolean value, which is a concrete FGL object representing itself. If
true, then n is concrete and we will produce the result of again rewriting
(logtail n x) -- note that we haven't created a loop here because the
syntaxp hyp required that the original n was not concrete. Otherwise, we
proceed with the next syntax-bind form.
This next syntax-bind form (note it must use a different free variable than
the other form!) returns either some natural number value or else NIL. Again,
either way it is a concrete object representing itself. We bind this to
n-width. We then require that n-width is nonnil and that we can show
n satisfies (unsigned-byte-p n-width n) (note: check-unsigned-byte-p
is an alias for unsigned-byte-p which has rules that try to prove it cheaply).
If not, then we come to an abort-rewrite form. When FGL arrives at an
abort-rewrite form, it aborts the current rewrite rule attempt, ignoring the
form inside the abort-rewrite. (In this case the form (logtail n x)
inside the abort-rewrite was selected to make it easy to prove
logtail-to-logtail-helper correct.) Otherwise, we go on with our rewrite.
Note we needed to know (unsigned-byte-p n-width n) in order to prove
logtail-to-logtail-helper. The syntax-bind form produces the correct
number, but while proving logtail-to-logtail-helper we don't know that.
Fortunately, it's fairly efficient to verify that after the fact using
check-unsigned-byte-p.
Examining the Interpreter State
FGL's implementation of syntaxp, bind-free, and syntax-bind interpret the
syntactic term using a custom evaluator, fancy-ev, that can be
instrumented to call functions that examine the ACL2 state and the FGL
interpreter state, and even make limited modifications to them. See the
documentation for fancy-ev for how to use it, and see fgl-interpreter-state for documentation of the contents of the interpreter state. One
main use of this is to examine counterexamples produced from incremental SAT
calls. By default, after loading fgl/top, the rewrite rule
show-counterexample-rw rewrites the constant-nil function
(show-counterexample msg) such that a syntax-bind form fetches the latest
incremental SAT counterexample and prints it.
Subtopics
- Fgl-syntactic-checker-binders
- Functions for checking syntactic properties of objects, and inferring
the logical properties that they imply
- Binder
- Form that can bind a free variable to the result of some (possibly
nondeterministic) computation.
- Fancy-ev
- Term evaluator used by FGL for syntaxp, bind-free, and syntax-bind interpretation.
- Def-fgl-program
- Define a function that is logically just NIL but has special extralogical behavior in FGL.
- Bind-var
- Form that can bind a free variable to the result of an arbitrary computation.
- Add-fgl-brewrites
- Enable some binder rewrite rules for use in FGL
- Def-fgl-rewrite
- Define a rewrite rule for FGL to use on term-level objects
- Narrow-equiv
- FGL testbench function to interpret a term under a narrower (stricter) equivalence context.
- Def-fgl-branch-merge
- Define a rule for FGL to use in merging IF branches
- Add-fgl-rewrites
- Enable some rewrite rules for use in FGL
- Fgl-interp-obj
- FGL testbench function to interpret a term that is the result of evaluating some form.
- Collect-cmr-rewrites-for-formula-name
- Syntax-bind
- Form that can bind a free variable to a value computed from examining
the syntax of other bound variables in the RHS of an FGL rewrite rule.
- Fgl-time
- FGL alternative to time$ that does not get elided by rewrite rule storage.
- Fgl-prog2
- In the FGL interpreter, run the first form for side effects and
return the result from the second form.
- Assume
- FGL testbench function to assume some condition while interpreting a term.
- Add-fgl-binder-meta
- Register a metafunction for use in rewriting binder invocations of a
trigger function in FGL.
- Add-fgl-primitive
- Register a primitive function for use in rewriting calls of a trigger
function in FGL.
- Add-fgl-meta
- Register a metafunction for use in rewriting calls of a trigger function
in FGL.
- Add-fgl-branch-merges
- Enable some rewrite rules's use for branch merging in FGL.
- Cmr::rewritelist->lhses
- Remove-fgl-brewrites
- Disable some binder rewrite rules' use in FGL.
- Remove-fgl-branch-merges
- Disable some rewrite rules' use for branch merging in FGL.
- Lhses->branch-function-syms
- Enable-execution
- Enable the use of concrete execution of a function in FGL rewriting.
- Abort-rewrite
- Form that aborts the application of an FGL rewrite rule when encountered
while processing the RHS of the rule.
- Syntax-interp
- Interpret a form on the syntactic representations of variables.
- Remove-fgl-rewrites
- Disable some rewrite rules' use in FGL.
- Lhses->leading-function-syms
- Remove-fgl-primitive
- Deregister a primitive function for use in FGL.
- Remove-fgl-binder-meta
- Deregister a binder metafunction for use in FGL.
- If!
- Function implementing IF that under FGL interpretation makes a
:g-ite object instead of doing the usual merging process.
- Disable-execution
- Disable the use of concrete execution of a function in FGL rewriting.
- Remove-fgl-meta
- Deregister a metafunction for use in FGL.
- Fgl-time-fn
- Disable-definition
- Disable the use of the given formula in FGL rewriting.
- Def-fgl-brewrite
- Define a binder rewrite rule for FGL to use on term-level objects
