Deffixtype
Define a new type for use with the fty-discipline.
In its most basic form, deffixtype just associates a new type
name with the corresponding predicate, fixing function, and equivalence
relation. It stores this association in a table, fty::fixtypes.
The type then becomes ``known'' to other fty macros such as deffixequiv, defprod, and so on.
Basic Example
You could use the following to define the nat
type with the recognizer natp, the fixing function nfix, the
equivalence relation nat-equiv, and natp as the preferred xdoc topic when linking to this type.
(fty::deffixtype nat
:pred natp
:fix nfix
:equiv nat-equiv
:topic natp)
For this to be sensible, the recognizer, fixing function, and equivalence
relation should satisfy the constraints described in fty-discipline, and
the equivalence relation must have already be admitted by defequiv.
In practice, you shouldn't really need to introduce deffixtype forms
for basic ACL2 types like natp by yourself. Instead, see the basetypes book.
More Typical Example
Very often, the equivalence relation for a new type is ``induced'' by the
fixing function in a completely standard way. Once you have introduced your
recognizer and fixing function, you can just have deffixtype introduce the
equivalence relation for you. For example:
(defun foop (x)
(declare (xargs :guard t))
(and (consp x)
(equal (car x) 'foo)))
(defun-inline foo-fix (x)
(declare (xargs :guard (foop x)))
(mbe :logic (if (foop x) x '(foo . nil))
:exec x))
(deffixtype foo
:pred foop
:fix foo-fix
:equiv foo-equiv
:define t ;; define foo-equiv for me
:forward t ;; prove some useful theorems about foo-equiv
)
Besides registering the foo type with FTY, this
will introduce foo-equiv essentially as if you had written:
(defun-inline foo-equiv (x y)
(declare (xargs :guard (and (foop x)
(foop y))))
(equal (foo-fix x) (foo-fix y)))
It will then prove foo-equiv is an equivalence relation and prove some
minor boilerplate theorems.
General Form
(deffixtype widget ;; name of the new type for fty
:pred widget-p
:fix widget-fix
:equiv widget-equiv
;; optional arguments ;; default
:executablep bool ;; t
:define bool ;; nil
:inline bool ;; t
:equal {eq,eql,equal,...} ;; equal
:forward bool ;; nil
:hints (("Goal"...)) ;; nil
:verbosep bool ;; nil
:topic symbol
)
Optional arguments
:verbosep
:verbosep can be set to T to avoid suppressing theorem prover output
during the resulting forms. This can be useful if the macro causes an error
and you need to debug it.
:define
:define is NIL by default; if set to T, then the equivalence relation
is assumed not to exist yet, and is defined as equality of fix, with
appropriate rules to rewrite the fix away under the equivalence and to
propagate the congruence into the fix.
:forward
Only matters when define is T. When :forward is T, four
additional lemmas will be proved about the new equivalence relation and stored
as ACL2::forward-chaining rules. In particular, the following will all
forward-chain to (widget-equiv x y):
- (equal (widget-fix x) y)
- (equal x (widget-fix y))
- (widget-equiv (widget-fix x) y), and
- (widget-equiv x (widget-fix y))
:hints
Only matters when define is NIL. This allows you to give hints for the theorem that shows the new equivalence relation holds
between x and y exactly when (equal (widget-fix x) (widget-fix
y)).
(When define is T we don't need to prove this, because it's exactly the
definition of the equivalence relation we introduce.)
:inline
Minor efficiency option, only matters when :define is T. When
:inline is T (which is the default), the new equivalence relation's
function will be introduced using defun-inline instead of defun.
:equal
Minor efficiency option, only matters when define is T. By default,
the new equivalence relation will compute the equal of the fixes. In some
cases, your type may be so restrictive that a more efficient equality check
like eq or eql can be used instead. For instance, if you are
defining character equivalence, you might use :equal eql so that your new
equivalence relation will compute the eql of the fixes instead of the
equal of the fixes.
:executablep
:executablep should be set to NIL if either the fixing function or
predicate are ACL2::non-executable or especially expensive. This mainly
affects, in deffixequiv and deffixequiv-mutual, whether a theorem is
introduced that normalizes constants by applying the fixing function to
them.
:topic
Set up a preferred xdoc documentation topic name for this type.
When other documentation topics want to refer to this type, they should link to
the preferred :topic. This may be useful when your type is embedded
within some larger defprod or similar.
Usually you don't need to provide a :topic explicitly. The :topic
will default to the name of the new type name being defined, e.g., widget.
We usually use the type name as the ``main'' topic. For instance, widget
would typically be the parent topic for widget-p, widget-fix,
widget-equiv, and related functions. This convention is followed
throughout the deftypes family of macros.
However, this convention is sometimes inappropriate, especially for built-in
ACL2 types such as natp and booleanp. In these cases, we'd
prefer to link to existing documentation such as the recognizers.
Subtopics
- Deffixtype-alias
- Introduce an alias of an existing fixtype.
