		Search-engine friendly clone of the ACL2 documentation.

Deffold-reduce-event-generation

Deffoldred-gen-list-fold

Generate the fold function for a list type, with accompanying theorems.

Signature
(deffoldred-gen-list-fold list mutrecp suffix extra-args result default combine fty-table) → (mv fn-event thm-events)
Arguments: list — Guard (flexlist-p list).; mutrecp — Guard (booleanp mutrecp).; suffix — Guard (symbolp suffix).; extra-args — Guard (true-listp extra-args).; result — Guard (symbolp result).; combine — Guard (symbolp combine).; 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).

This is as described in deffold-reduce.

The mutrecp flag says whether this list type is part of a mutually recursive clique.

Definitions and Theorems

Function: deffoldred-gen-list-fold

(defun deffoldred-gen-list-fold
       (list mutrecp suffix extra-args
             result default combine fty-table)
 (declare (xargs :guard (and (flexlist-p list)
                             (booleanp mutrecp)
                             (symbolp suffix)
                             (true-listp extra-args)
                             (symbolp result)
                             (symbolp combine)
                             (alistp fty-table))))
 (let ((__function__ 'deffoldred-gen-list-fold))
  (declare (ignorable __function__))
  (b*
   ((type (flexlist->name list))
    ((unless (symbolp type))
     (raise "Internal error: malformed type name ~x0."
            type)
     (mv '(_) nil))
    (type-suffix (deffoldred-gen-fold-name type suffix))
    (type-count (flexlist->count list))
    (recog (flexlist->pred list))
    (elt-recog (flexlist->elt-type list))
    ((unless (symbolp elt-recog))
     (raise "Internal error: malformed recognizer ~x0."
            elt-recog)
     (mv '(_) nil))
    (elt-info (flextype-with-recognizer elt-recog fty-table))
    (elt-type (flextype->name elt-info))
    (recp (flexlist->recp list))
    ((unless (symbolp elt-type))
     (raise "Internal error: malformed type name ~x0."
            elt-type)
     (mv '(_) nil))
    (elt-type-suffix (deffoldred-gen-fold-name elt-type suffix))
    (extra-args-names (deffoldred-extra-args-to-names extra-args))
    (body
     (cons
      'cond
      (cons
       (cons (cons (if (flexlist->true-listp list)
                       'endp
                     'atom)
                   (cons type 'nil))
             (cons default 'nil))
       (cons
        (cons
         't
         (cons
          (cons combine
                (cons (cons elt-type-suffix
                            (cons (cons 'car (cons type 'nil))
                                  extra-args-names))
                      (cons (cons type-suffix
                                  (cons (cons 'cdr (cons type 'nil))
                                        extra-args-names))
                            'nil)))
          'nil))
        'nil))))
    (fn-event
     (cons
      'define
      (cons
       type-suffix
       (cons
        (cons (cons type (cons recog 'nil))
              extra-args)
        (cons
         ':returns
         (cons
          (cons 'result (cons result 'nil))
          (cons
           ':parents
           (cons
            (cons (deffoldred-gen-topic-name suffix)
                  'nil)
            (cons
             body
             (append
                 (and (or mutrecp recp)
                      (cons ':measure
                            (cons (cons type-count (cons type 'nil))
                                  'nil)))
                 (append (and (not mutrecp)
                              '(:verify-guards :after-returns))
                         (and (not mutrecp)
                              '(:hooks (:fix))))))))))))))
    (elt-type-suffix (deffoldred-gen-fold-name elt-type suffix))
    (type-suffix-when-atom
         (acl2::packn-pos (list type-suffix '-when-atom)
                          suffix))
    (type-suffix-of-cons
         (acl2::packn-pos (list type-suffix '-of-cons)
                          suffix))
    (type-suffix-of-append
         (acl2::packn-pos (list type-suffix '-of-append)
                          suffix))
    (type-suffix-of-rcons
         (acl2::packn-pos (list type-suffix '-of-rcons)
                          suffix))
    (elt-type-suffix-of-car-when-type-suffix
         (acl2::packn-pos (list elt-type-suffix '-of-car-when-
                                type-suffix)
                          suffix))
    (type-suffix-of-cdr-when-type-suffix
         (acl2::packn-pos (list type-suffix '-of-cdr-when-
                                type-suffix)
                          suffix))
    (type1 (add-suffix-to-fn type "1"))
    (type-elem (add-suffix-to-fn type "-ELEM"))
    (thm-events
     (append
      (cons
       (cons
        'defruled
        (cons
         type-suffix-when-atom
         (cons
          (cons
           'implies
           (cons
               (cons 'atom (cons type 'nil))
               (cons (cons 'equal
                           (cons (cons type-suffix
                                       (cons type extra-args-names))
                                 (cons default 'nil)))
                     'nil)))
          (cons ':enable
                (cons type-suffix 'nil)))))
       (cons
        (cons
         'defruled
         (cons
          type-suffix-of-cons
          (cons
           (cons
            'equal
            (cons
             (cons type-suffix
                   (cons (cons 'cons
                               (cons elt-type (cons type 'nil)))
                         extra-args-names))
             (cons
               (cons combine
                     (cons (cons elt-type-suffix
                                 (cons elt-type extra-args-names))
                           (cons (cons type-suffix
                                       (cons type extra-args-names))
                                 'nil)))
               'nil)))
           (cons
            ':expand
            (cons
                 (cons type-suffix
                       (cons (cons 'cons
                                   (cons elt-type (cons type 'nil)))
                             extra-args-names))
                 'nil)))))
        (cons
         (cons
          'add-to-ruleset
          (cons
            (deffoldred-gen-ruleset-name suffix)
            (cons (cons 'quote
                        (cons (cons type-suffix-when-atom
                                    (cons type-suffix-of-cons 'nil))
                              'nil))
                  'nil)))
         'nil)))
      (and
       (eq combine 'and)
       (eq default t)
       (cons
        (cons
         'defruled
         (cons
          type-suffix-of-append
          (cons
           (cons
            'equal
            (cons
             (cons type-suffix
                   (cons (cons 'append
                               (cons type (cons type1 'nil)))
                         extra-args-names))
             (cons
              (cons 'and
                    (cons (cons type-suffix
                                (cons type extra-args-names))
                          (cons (cons type-suffix
                                      (cons type1 extra-args-names))
                                'nil)))
              'nil)))
           (cons
            ':induct
            (cons
             't
             (cons
                 ':enable
                 (cons (cons 'append
                             (cons type-suffix
                                   (cons type-suffix-of-cons 'nil)))
                       'nil)))))))
        (cons
         (cons
          'defruled
          (cons
           type-suffix-of-rcons
           (cons
            (cons
             'equal
             (cons
              (cons type-suffix
                    (cons (cons 'rcons
                                (cons type-elem (cons type 'nil)))
                          extra-args-names))
              (cons
               (cons
                'and
                (cons (cons type-suffix
                            (cons type extra-args-names))
                      (cons (cons elt-type-suffix
                                  (cons type-elem extra-args-names))
                            'nil)))
               'nil)))
            (cons
                 ':enable
                 (cons (cons 'rcons
                             (cons type-suffix-of-append
                                   (cons type-suffix-of-cons 'nil)))
                       'nil)))))
         (cons
          (cons
           'defruled
           (cons
            elt-type-suffix-of-car-when-type-suffix
            (cons
             (cons
              'implies
              (cons (cons 'and
                          (cons (cons type-suffix
                                      (cons type extra-args-names))
                                (cons (cons 'consp (cons type 'nil))
                                      'nil)))
                    (cons (cons elt-type-suffix
                                (cons (cons 'car (cons type 'nil))
                                      extra-args-names))
                          'nil)))
             (cons ':enable
                   (cons type-suffix 'nil)))))
          (cons
           (cons
            'defruled
            (cons
             type-suffix-of-cdr-when-type-suffix
             (cons
              (cons
                'implies
                (cons (cons type-suffix
                            (cons type extra-args-names))
                      (cons (cons type-suffix
                                  (cons (cons 'cdr (cons type 'nil))
                                        extra-args-names))
                            'nil)))
              (cons ':enable
                    (cons type-suffix 'nil)))))
           (cons
            (cons
             'add-to-ruleset
             (cons
              (deffoldred-gen-ruleset-name suffix)
              (cons
               (cons
                'quote
                (cons
                 (cons
                  type-suffix-of-append
                  (cons
                     type-suffix-of-rcons
                     (cons elt-type-suffix-of-car-when-type-suffix
                           (cons type-suffix-of-cdr-when-type-suffix
                                 'nil))))
                 'nil))
               'nil)))
            'nil)))))))))
   (mv fn-event thm-events))))

Theorem: pseudo-event-formp-of-deffoldred-gen-list-fold.fn-event

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

Theorem: pseudo-event-form-listp-of-deffoldred-gen-list-fold.thm-events

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