• 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-map
          • Deffold-map-implementation
      • Fty-extensions
      • Defsubtype
      • Defset
      • Deftypes
      • Specific-types
      • Defflatsum
      • Deflist-of-len
      • Defbytelist
      • Defomap
      • Fty::basetypes
      • Defvisitors
      • Deffixtype-alias
      • Deffixequiv-sk
      • Defunit
      • Multicase
      • Deffixequiv-mutual
      • Fty::baselists
      • Def-enumcase
      • 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-map

Mapping folds for fixtypes.

Introduction

This macro automates the creation of the `mapping' class of folds on fixtypes described in fold. The user specifies any number of overrides of the boilerplate code for specific cases of the fixtypes in the same manner as deffold-reduce.

General Form

(deffold-map suffix
             :types      ...  ; no default
             :extra-args ...  ; default nil
             :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

Fixtypes for which map 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 recursive calls.

This must be a list of extended formals which deffold-map puts into the generated defines.

: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 map 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 fixed input.
  • If <type> has one or more components whose types are specified by the :types input, the function is defined to return the map over the product fields.
• 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 or more components whose types are specified by the :types input, the case is defined to return the map over the product fields.
• If <type> is a deflist:
  • If the list is empty, the function is defined to return nil.
  • If the list is not empty, the function is defined to return the cons of the mapped car to the recursively mapped cdr.
• If <type> is a defoption:
  • If the option value is nil, the function is defined to return nil.
  • If the option value is not nil, the function is defined to return the map function of the base type applied to the value.
• If <type> is a defomap:
  • If the map is empty, the function is defined to return nil.
  • If the map is not empty, the function is defined to return the omap::update of the head key and the mapped value to the recursively mapped omap::tail.

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>-type-prescription
• <type>-<suffix>-when-atom
• <type>-<suffix>-of-cons
• <type>-<suffix>-of-append
• consp-of-<type>-<suffix>
• len-of-<type>-<suffix>
• nth-of-<type>-<suffix>
• <type>-<suffix>-of-revappend
• <type>-<suffix>-of-reverse

These theorems are disabled, and added to the generated ruleset described below.

Accompanying option theorems.

For each defoption type specified by the :types input, we generate the following theorems, whose exact form can be inspected with pe or similar command:

• <type>-<suffix>-under-iff

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>-type-prescription
• <type>-<suffix>-when-emptyp
• emptyp-of-<type>-<suffix>
• keys-of-<type>-<suffix>
• assoc-of-<type>-<suffix>

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-map-implementation

Implementation of deffold-map.