		Search-engine friendly clone of the ACL2 documentation.

Fold

Deffold-reduce

Reducing folds for fixtypes.

Introduction

This macro automates the creation of the `reducing' class of folds on fixtypes described in fold. The user specifies R, a default for the constant arguments, the binary operation on R, and any number of overrides of the boilerplate code for specific cases of the fixtypes.

General Form

(deffold-reduce suffix
                :types      ...  ; no default
                :extra-args ...  ; default nil
                :result     ...  ; no default
                :default    ...  ; no default
                :combine    ...  ; no default
                :override   ...  ; default nil
                :parents    ...  ; no default
                :short      ...  ; no default
                :long       ...  ; no default
  )

Inputs

suffix

Suffix for the generated function names. The name of each generated function is <type>-<suffix>, where <type> is the type that the function operates on, and <suffix> is the value of this input, which must be a symbol. The function name is interned in the same package as <suffix>.

:types — no default

Fixtype for which fold functions must be generated.
This must be a list of symbols, which is not evaluated by the macro, where each symbols must be one of the following:
The name of an existing fixtype, if the fixtype is not recursive or singly recursive: this specifies the fixtype itself.
The name of an existing clique of two or more mutually recursive fixtypes: this specifies the fixtypes in the clique.
These symbols must be listed in bottom-up order, i.e. according to the order in which they are defined.
The following fixtypes can be specified (i.e. are currently supported by this tool):
defprod fixtypes.
deftagsum fixtypes.
deflist fixtypes. In this case, the element fixtype must be specified by the :types input too.
defoption fixtypes. In this case, the base fixtype must be specified by the :types input too.
defomap fixtypes. In this case, the value fixtype must be specified by the :types input too, while the key fixtype must not.

:extra-args — default nil

Extra arguments of the functions, which are passed unchanged to the recursively calls.
This must be a list of extended formals which deffold-reduce puts into the generated defines.

:result — no default

Recognizer of the R type of results.
It must be a symbol that names an existing unary predicate, which is used for the results of the generated functions.

:default — no default

Default result of the generated functions, used as described in the Section `Generated Events' below.
This must be a term.

:combine — no default

Binary operation to combine results.
It must be a symbol that names an existing binary function, which is used to combine the results of the recursive calls in the generated functions.

:override — default nil

Specifies which boilerplate results should be overridden. It is used as described in the Section `Generated Events' below.
This must be a parenthesized list (ovrd1 ... ovrd<n>), with <n> >= 0, where each ovrd<i> has one of two possible forms:
A pair (<type> <term>), where <type> is a defprod or deftagsum, and <term> is an (untranslated) term whose only free variables may be <type> and the formals specified in :extra-args.
A triple (<type> <kind> <term>), where <type> is a deftagsum, <kind> is a keyword identifying one of the summands of the type, and <term> is an (untranslated) term whose only free variables may be <type> and the formals specified in :extra-args.

:parents
:short
:long

These, if present, are added to the generated XDOC topic described in the Section `Generated Events' below.

Generated Events

abstract-syntax-<suffix>

An XDOC topic whose name is obtained by adding, at the end of the symbol abstract-syntax-, the symbol specified by the suffix input. If any of the :parents, :short, or :long inputs are provided, they are added to this XDOC topic. This XDOC topic is generated with ACL2::defxdoc+, with :order-topics t, so that the other generated events (described below), which all have this XDOC topic as parent, are listed in order as subtopics.

For each type <type> specified by the :types input, a fold function for that type, defined as follows:
If <type> is a defprod:
If the :override input includes an element (<type> <term>), the function is defined to return <term>.
If the :override input does not include an element of the form (<type> <term>), the function is defined to return the following:
If <type> has no components whose type is specified by the :types input, the function is defined to return the term specified by the :default input.
If <type> has exactly one component whose type is specified by the :types input, the function is defined to return the result of applying the fold function for that type to that component.
If <type> has two or more components whose types are specified by the :types input, the function is defined to return the result of combining, via the function specified by the :combine input, the results of applying the corresponding fold functions to the components, nested to the right (i.e. (combine val1 ... (combine valN-1 valN))).
If <type> is a deftagsum:
If the :override input includes an element (<type> <term>), the function is defined to return <term>.
Otherwise, the function is defined via <type>-case, and the case for each keyword <kind> is as follows:
If the :override input includes an element (<type> <kind> <term>), the case is defined to return <term>.
If the :override input does not include any element of the form (<type> <kind> <term>):
If the summand corresponding to <kind> has no components whose type is specified by the :types input, the case is defined to return the term specified by the :default input.
If the summand corresponding to <kind> has one component whose type is specified by the :types input, the case is defined to return the result of applying the fold function for that type to that component.
If the summand corresponding to <kind> has two or more components whose types are specified by the :types input, the case is defined to return the result of combining, via the function specified by the :combine input, the results of applying the corresponding fold functions to the components, nested to the right (i.e. (combine val1 ... (combine valN-1 valN))).
If <type> is a deflist:
If the list is empty, the function is defined to return the term specified by the :default input.
If the list is not empty, the function is defined to return the result of combining, via the function specified by the :combine input, the result of applying the element type's fold function to the car of the list with the result of applying to list type's fold function to the cdr of the list.
If <type> is a defoption:
If the option value is nil, the function is defined to return the term specified by the :default input.
If the option value is not nil, the function is defined to return the result of applying the fold for the base type on the value.
If <type> is a defomap:
If the map is empty, the function is defined to return the term specified by the :default input.
If the map is not empty, the function is defined to return the result of combining, via the function specified by the :combine input, the result of applying the map value type's fold function to the head value of the map with the result of applying to list type's fold function to the tail of the map.

Accompanying list theorems.

For each deflist type specified by the :types input, we generate the following theorems, whose exact form can be inspected with pe or similar command:
<type>-<suffix>-when-atom
<type>-<suffix>-of-cons
These theorems are disabled, and added to the generated ruleset described below.

Accompanying omap type theorems.

For each defomap type specified by the :types input, we generate the following theorems, whose exact form can be inspected with pe or similar command:
<type>-<suffix>-when-emptyp
These theorems are disabled, and added to the generated ruleset described below.

abstract-syntax-<suffix>-rules

A ruleset with the theorems that accompany the fold functions.

The theorems that accompany the predicates are generated as part of the define and defines that define the predicates, after the ///.

Subtopics

Deffold-reduce-implementation: Implementation of deffold-reduce.