Defun-sk-queries
Utilities to query defun-sk functions.
defun-sk mimics functions with (top-level) quantifiers
in the quantifier-free logic of ACL2, by conservatively axiomatizing an associated witness function
and by defining the defun-sk function
in terms of the witness function
(either via an actual definition,
or via a definition rule if :constrain is not nil).
It also generates a rewrite rule to support reasoning
about the function with the quantifier.
These defun-sk query utilities provide facilities
to check whether a function has been introduced via defun-sk,
and, if so, to retrieve its defun-sk-specific constituents.
Constituents of the function that are not defun-sk-specific
(formal arguments, guard, etc.)
can be retrieved with more general utilities. Since defun-sk extends the pe-table
with the defun-sk form,
these utilities consult the pe-table to determine whether
a function has been introduced by defun-sk,
and if that is the case, the defun-sk-specific components
are retrieved based on the expected structure of
the defun-sk form and of the forms it generates
(encapsulate, defchoose, etc.).
Thus, if the pe-table is extended
with a form starting with defun-sk
without using defun-sk
(by directly calling extend-pe-table),
these utilities, as currently implemented,
can be fooled and return meaningless results.
(These utilities could be extended to defensively check
that the form and its expansion have the right structure,
if that becomes important.)
Subtopics
- Defun-sk-matrix
- Retrieve the matrix of a function introduced via defun-sk,
in untranslated form.
- Defun-sk-p
- Check if a named function has been introduced via defun-sk,
returning the function's defun-sk form if the check succeeds.
- Defun-sk-namep
- Recognize symbols
that name functions introduced via defun-sk.
- Defun-sk-body
- Retrieve the body of a function introduced via defun-sk.
- Defun-sk-imatrix
- Retrieve the matrix of a function introduced via defun-sk,
in untranslated form.
- Defun-sk-definition-name
- Retrieve the name of the definition rule of
a function introduced via defun-sk.
- Defun-sk-witness
- Retrieve the name of the witness of
a function introduced via defun-sk.
- Defun-sk-classicalp
- Retrieve the value of the :classicalp option of
a function introduced via defun-sk.
- Defun-sk-rewrite-kind
- Retrieve the kind of the rewrite rule of
a function introduced via defun-sk.
- Defun-sk-rewrite-name
- Retrieve the name of the rewrite rule of
a function introduced via defun-sk.
- Defun-sk-rewrite-kind-p
- Kinds of rewrite rules associated to
defun-sk functions with the universal quantifier.
- Defun-sk-quantifier
- Retrieve the quantifier of
a function introduced via defun-sk.
- Defun-sk-options
- Retrieve the keyed options of
a function introduced via defun-sk.
- Defun-sk-bound-vars
- Retrieve the bound variables of
a function introduced via defun-sk.
- Defun-sk-strengthen
- Retrieve the value of the :strengthen option of
a function introduced via defun-sk.
- Defun-sk-quantifier-p
- Existential and universal quantifiers.
