• 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
              • Deffold-reduce-event-generation
              • Deffoldred-process-inputs-and-gen-everything
              • Deffoldred-fn
              • Deffold-reduce-input-processing
              • Deffoldred-macro-definition
          • Deffold-map
        • 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
  • Deffold-reduce

Deffold-reduce-implementation

Implementation of deffold-reduce.

The implementation functions have arguments and results consistently named as follows (unless otherwise stated, explicitly or implicitly, in the functions):

  • suffix is the homonymous input to the event macro.
  • types is the homonymous input to the event macro.
  • extra-args is the homonymous input to the event macro.
  • result is the homonymous input to the event macro.
  • default is the homonymous input to the event macro.
  • combine is the homonymous input to the event macro.
  • override is the homonymous input to the event macro.
  • parents is the homonymous input to the event macro.
  • short is the homonymous input to the event macro.
  • long is the homonymous input to the event macro.
  • overrides is an alist representation of the :override input. With reference to the documentation page of deffold-reduce: for each element <type> <term> in :override, this alist has an element (cons <type> <term>); for each element <type> <kind> <term> in :override, this alist has an element (cons (cons <type> <kind>) <term>).
  • fty-table is the alist of the table of all (fix)types (except some built-in ones, such as nat), i.e. the table flextypes-table. The format is defined in [books]/centaur/fty/database.lisp. It has one entry for each mutually recursive clique of types, with singly recursive or non-recursive types being in singleton cliques.
  • targets is a list (in no particular order) of all the type names for which fold functions are generated.
  • target is an element of targets explained above.

Implementation functions' arguments and results that are not listed above are described in, or clear from, those functions' documentation.

Subtopics

Deffold-reduce-event-generation
Event generation performed by deffold-reduce.
Deffoldred-process-inputs-and-gen-everything
Process the inputs and generate the events.
Deffoldred-fn
Event expansion of deffold-reduce.
Deffold-reduce-input-processing
Input processing performed by deffold-reduce.
Deffoldred-macro-definition
Definition of deffold-reduce.