|
|
|---|
|
|
|
|---|
Generate specialized versions of the operations to convert between natural numbers and digits, using specified existing recognizers and fixers for the digits.
The operations in the library to convert between natural numbers and digits are parameterized over the base. The recognizers and fixers for (lists of) digits are also parameterized; they are binary functions.
Given a specific base, and specific unary recognizers and fixers for lists of digits in that base, it is possible to generate systematically versions of the operations in the library, and accompanying theorems, that are specialized to the base (and thus are not parameterized over it) and that depend on those unary recognizers and fixers. This macro carries out this specialization.
These specialized operations, in combination with the unary recognizers and fixers, are easier to use and reason about than the general operations, when the base is known.
(defdigits name :base ... :digit-pred ... :digit-fix ... :digits-pred ... :digits-fix ... :bendian-to-nat ... :lendian-to-nat ... :nat-to-bendian ... :nat-to-lendian ... :digit-pred-hints ... :digit-fix-hints ... :digit-pred-guard-hints ... :digit-fix-guard-hints ... :digits-pred-hints ... :digits-fix-hints ... :digits-pred-guard-hints ... :digits-fix-guard-hints ... :digits-description ... :parents ... :short ... :long ... )
A symbol that names the ensemble of the generated specialized conversion functions. This is used as the XDOC topic under which the XDOC topics for the generated events are put.
A positive integer greater than 1 that specifies the base.
Symbols that name existing functions, or macros for inline functions, to be used as specializations of dab-digitp and dab-digit-fix.
These must be part of an existing fixtype.
Symbols that name existing functions, or macros for inline functions, to be used as specializations of dab-digit-listp and dab-digit-list-fix.
These must be part of an existing fixtype.
Symbols that specify the names to use for the generated functions (see details below).
Hints to prove that the specialized recognizers and fixers are equivalent to the general ones, when their base argument is
base . Besides the equalities of the functions, the guard of the recognizer must be equivalent tot , and the guard of the fixer must include the recognizer.
A string describing the values in
digits-pred , used in the generated documentation. It must start with a lowercase character (because it is inserted in the middle of generated senteces) and it must be plural (so that the generated sentences are grammatically correct).
These, if present, are added to the XDOC topic generated for the ensemble of the generated specialized conversion functions.
Two rewrite rules, disabled by default, that equate
digit-pred anddigit-fix with dab-digitp and dab-digit-fix applied to the specified base.
digit-fix-guard-correct Two theorems, without rule classes, asserting that the guard of
digit-pred is equivalent tot and that the guard ofdigit-fix includesdigit-pred .
Two rewrite rules, disabled by default, that equate
digits-pred anddigits-fix with dab-digit-listp and dab-digit-list-fix applied to the specified base.
digits-fix-guard-correct Two theorems, without rule classes, asserting that the guard of
digits-pred is equivalent tot and that the guard ofdigits-fix includesdigits-pred .
Specialized versions of bendian=>nat, lendian=>nat, nat=>bendian, nat=>lendian, nat=>bendian*, nat=>lendian*, nat=>bendian+, and nat=>lendian+, for the specified
base . The names of the first four are as specified by the respective inputs; the names for the second four are obtained by adding* or+ after the names of the third and fourth function. These new functions are accompanied by several theorems corresponding to ones that accompany the original functions, i.e. they are specialized versions of the general theorems; we also generate some theory invariants that prevent some of the generated rewrite rules from being simultaneously enabled. These theorems, and the guards, usedigit-pred ,digit-fix ,digits-pred , anddigits-fix instead of dab-digitp, dab-digit-fix, dab-digit-listp, and dab-digit-list-fix. The generated theorems can be seen in the implementation, which uses a readable backquote notation; they can also be seen in the generated XDOC.
The generated events include XDOC documentation.
They are all under an XDOC for the ensemble,
whose name is specified in the