• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
      • Deftagsum
      • Defprod
      • Defflexsum
      • Defbitstruct
      • Deflist
      • Defalist
      • Defbyte
      • Deffixequiv
      • Defresult
      • Deffixtype
      • Defoption
      • Fty-discipline
      • Fold
        • Deffold-reduce
          • Deffold-reduce-implementation
      • Fty-extensions
      • Defsubtype
      • Defset
      • Deftypes
      • Specific-types
      • Defflatsum
      • Deflist-of-len
      • Defbytelist
      • Fty::basetypes
      • Defomap
      • Defvisitors
      • Deffixtype-alias
      • Deffixequiv-sk
      • Defunit
      • Deffixequiv-mutual
      • Fty::baselists
      • Defmap
    • Apt
    • Std/util
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
    • Defthm-domain
    • Event-macros
    • Def-universal-equiv
    • Def-saved-obligs
    • With-supporters-after
    • Definec
    • Sig
    • Outer-local
    • Data-structures
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 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.

<type>-<suffix>

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 a singleton, the function is defined to return the result of calling the fold function for the element type on the element of the list.
  • If the list has two or more elements, 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 elements, nested to the right (i.e. (combine val1 ... (combine valN-1 valN))).
• 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 a singleton, the function is defined to return the result of applying the fold function for the value type to the value of the map.
  • If the map has two or more elements, the function is defined to return the result of combining, via the function specified by the :combine input, the results of applying the fold function for the value type to the values of the map, nested to the right (i.e. (combine val1 ... (combine valN-1 valN))).

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.