Binder
Form that can bind a free variable to the result of some (possibly
nondeterministic) computation.
- Signature
(binder val) → *
Logically, (binder val) just returns val. However, in
FGL, the intended use is to bind a free variable in a rewrite rule to the
result of some computation with some particular properties. The val
argument must be a function--say bindingfn--whose first argument is a
variable var and which has either a binder rule of the following form:
(implies (and ... hyps ...
(equiv2 var (binding-impl-term ...)))
(equiv1 (bindingfn var arg1 ... argn) var))
or else a binder metafunction associated with it. In the first case (and assuming we
are in an
equiv1 equiv context),
(binder (bindingfn var val1 ... valn))
results in
var being bound to the result of symbolically interpreting
(binding-impl-term ...) under the substitution binding
argi to
vali and in the
equiv2 context. In the second case, the binder
metafunction is applied to the symbolic values
val1 ... valn, resulting in
a term, bindings, and equivalence context;
var is bound to the result of
symbolically interpreting the term under the bindings in the equivalence
context.
An example application is to check whether the symbolic value of some term
is syntactically an integer. We define (check-integerp var x) to be
(and (integerp x) var) and associate this with a binding metafunction that
returns T if x is syntactically an integer. Another application is to
perform a SAT check and return the result (:unsat, :sat, or
:failed).
Definitions and Theorems
Function: binder
(defun binder (val)
(declare (xargs :guard t))
(let ((__function__ 'binder))
(declare (ignorable __function__))
val))
