• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
      • Deftagsum
      • Defprod
      • Defflexsum
      • Defbitstruct
      • Deflist
      • Defalist
      • Defbyte
      • Defresult
      • Deffixequiv
      • Deffixtype
      • Defoption
      • Fty-discipline
      • Fold
        • Deffold-reduce
          • Deffold-reduce-implementation
            • Deffold-reduce-event-generation
              • Deffoldred-gen-prod-combination
              • Deffoldred-gen-list-fold
              • Deffoldred-gen-prod-combination+theorem
              • Deffoldred-gen-omap-fold
              • Deffoldred-gen-clique-fold/folds
              • Deffoldred-gen-option-fold
              • Deffoldred-gen-prod-fold
              • Deffoldred-gen-sum-fold
              • Deffoldred-gen-sum-cases
              • Deffoldred-gen-everything
              • Deffoldred-gen-prod/sum/option-fold
              • Deffoldred-gen-types-folds
              • Deffoldred-gen-type-fold
              • Deffoldred-gen-cliques-folds
              • Deffoldred-extra-args-to-names
              • Deffoldred-gen-fold-name
              • Deffoldred-gen-topic-name
              • Deffoldred-gen-ruleset-name
            • Deffoldred-process-inputs-and-gen-everything
            • Deffoldred-fn
            • Deffold-reduce-input-processing
            • Deffoldred-macro-definition
        • Deffold-map
        • Defmake-self
      • Specific-types
      • Fty-extensions
      • Defsubtype
      • Deftypes
      • Defset
      • Defflatsum
      • Deflist-of-len
      • Defomap
      • Defbytelist
      • 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-event-generation

Deffoldred-gen-prod/sum/option-fold

Generate the fold function for a product, sum, or option type.

Signature

(deffoldred-gen-prod/sum/option-fold 
     sum 
     mutrecp suffix targets extra-args result 
     default combine overrides fty-table) 
 
  → 
(mv fn-event thm-events)

Arguments

sum — Guard (flexsum-p sum).

mutrecp — Guard (booleanp mutrecp).

suffix — Guard (symbolp suffix).

targets — Guard (symbol-listp targets).

extra-args — Guard (true-listp extra-args).

result — Guard (symbolp result).

combine — Guard (symbolp combine).

overrides — Guard (alistp overrides).

fty-table — Guard (alistp fty-table).

Returns

fn-event — Type (acl2::pseudo-event-formp fn-event).

thm-events — Type (acl2::pseudo-event-form-listp thm-events).

In the FTY table, these are all stored as sum types, but with a discriminator as the type macro.

Definitions and Theorems

Function: deffoldred-gen-prod/sum/option-fold

(defun deffoldred-gen-prod/sum/option-fold
       (sum mutrecp suffix targets extra-args result
            default combine overrides fty-table)
 (declare (xargs :guard (and (flexsum-p sum)
                             (booleanp mutrecp)
                             (symbolp suffix)
                             (symbol-listp targets)
                             (true-listp extra-args)
                             (symbolp result)
                             (symbolp combine)
                             (alistp overrides)
                             (alistp fty-table))))
 (let ((__function__ 'deffoldred-gen-prod/sum/option-fold))
  (declare (ignorable __function__))
  (b* ((typemacro (flexsum->typemacro sum)))
   (cond
     ((eq typemacro 'defprod)
      (deffoldred-gen-prod-fold
           sum
           mutrecp suffix targets extra-args result
           default combine overrides fty-table))
     ((eq typemacro 'deftagsum)
      (deffoldred-gen-sum-fold
           sum
           mutrecp suffix targets extra-args result
           default combine overrides fty-table))
     ((eq typemacro 'defoption)
      (deffoldred-gen-option-fold sum mutrecp suffix extra-args
                                  result default combine fty-table))
     (t (prog2$ (raise "Internal error: unsupported sum type ~x0."
                       sum)
                (mv '(_) nil)))))))

Theorem: pseudo-event-formp-of-deffoldred-gen-prod/sum/option-fold.fn-event

(defthm
 pseudo-event-formp-of-deffoldred-gen-prod/sum/option-fold.fn-event
 (b* (((mv ?fn-event ?thm-events)
       (deffoldred-gen-prod/sum/option-fold
            sum
            mutrecp suffix targets extra-args result
            default combine overrides fty-table)))
   (acl2::pseudo-event-formp fn-event))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deffoldred-gen-prod/sum/option-fold.thm-events

(defthm
 pseudo-event-form-listp-of-deffoldred-gen-prod/sum/option-fold.thm-events
 (b* (((mv ?fn-event ?thm-events)
       (deffoldred-gen-prod/sum/option-fold
            sum
            mutrecp suffix targets extra-args result
            default combine overrides fty-table)))
   (acl2::pseudo-event-form-listp thm-events))
 :rule-classes :rewrite)