		Search-engine friendly clone of the ACL2 documentation.

Deffold-reduce-event-generation

Deffoldred-gen-omap-fold

Generate a fold function for an omap type, with accompanying theorems.

Signature
(deffoldred-gen-omap-fold omap mutrecp suffix extra-args result default combine fty-table) → (mv fn-event thm-events)
Arguments: omap — Guard (flexomap-p omap).; 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 omap type is part of a mutually recursive clique.

Definitions and Theorems

Function: deffoldred-gen-omap-fold

(defun deffoldred-gen-omap-fold
       (omap mutrecp suffix extra-args
             result default combine fty-table)
 (declare (xargs :guard (and (flexomap-p omap)
                             (booleanp mutrecp)
                             (symbolp suffix)
                             (true-listp extra-args)
                             (symbolp result)
                             (symbolp combine)
                             (alistp fty-table))))
 (let ((__function__ 'deffoldred-gen-omap-fold))
  (declare (ignorable __function__))
  (b*
   ((type (flexomap->name omap))
    ((unless (symbolp type))
     (raise "Internal error: malformed type name ~x0."
            type)
     (mv '(_) nil))
    (type-suffix (deffoldred-gen-fold-name type suffix))
    (type-count (flexomap->count omap))
    (recog (flexomap->pred omap))
    (recp (flexomap->recp omap))
    (key-recog (flexomap->key-type omap))
    ((unless (symbolp key-recog))
     (raise "Internal error: malformed recognizer ~x0."
            key-recog)
     (mv '(_) nil))
    (key-info (flextype-with-recognizer key-recog fty-table))
    (key-type (or (and key-info (flextype->name key-info))
                  (case key-recog
                    (integerp 'acl2::int)
                    (t (raise "Not supported yet: key-recog.")))))
    (val-recog (flexomap->val-type omap))
    ((unless (symbolp val-recog))
     (raise "Internal error: malformed recognizer ~x0."
            val-recog)
     (mv '(_) nil))
    (val-info (flextype-with-recognizer val-recog fty-table))
    (val-type (flextype->name val-info))
    (val-type-suffix (deffoldred-gen-fold-name val-type suffix))
    (extra-args-names (deffoldred-extra-args-to-names extra-args))
    (body
     (cons
      'cond
      (cons
       (cons (cons 'not
                   (cons (cons 'mbt
                               (cons (cons recog (cons type 'nil))
                                     'nil))
                         'nil))
             (cons default 'nil))
       (cons
        (cons (cons 'omap::emptyp (cons type 'nil))
              (cons default 'nil))
        (cons
         (cons
          't
          (cons
           (cons
            combine
            (cons
               (cons val-type-suffix
                     (cons (cons 'omap::head-val (cons type 'nil))
                           extra-args-names))
               (cons (cons type-suffix
                           (cons (cons 'omap::tail (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))))))))))))))
    (type-suffix-when-emptyp
         (acl2::packn-pos (list type-suffix '-when-emptyp)
                          suffix))
    (type-suffix-of-tail
         (acl2::packn-pos (list type-suffix '-of-tail)
                          suffix))
    (type-suffix-of-update
         (acl2::packn-pos (list type-suffix '-of-update)
                          suffix))
    (val-type-suffix-of-head-when-type-suffix
         (acl2::packn-pos (list val-type-suffix '-of-head-when-
                                type-suffix)
                          suffix))
    (thm-events
     (append
      (cons
       (cons
        'defruled
        (cons
         type-suffix-when-emptyp
         (cons
          (cons
           'implies
           (cons
               (cons 'omap::emptyp (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
         'add-to-ruleset
         (cons (deffoldred-gen-ruleset-name suffix)
               (cons (cons 'quote
                           (cons (cons type-suffix-when-emptyp 'nil)
                                 'nil))
                     'nil)))
        'nil))
      (and
       (eq combine 'and)
       (eq default t)
       (cons
        (cons
         'defruled
         (cons
          type-suffix-of-tail
          (cons
           (cons
            'implies
            (cons
               (cons 'and
                     (cons (cons recog (cons type 'nil))
                           (cons (cons type-suffix
                                       (cons type extra-args-names))
                                 'nil)))
               (cons (cons type-suffix
                           (cons (cons 'omap::tail (cons type 'nil))
                                 extra-args-names))
                     'nil)))
           (cons ':enable
                 (cons type-suffix 'nil)))))
        (cons
         (cons
          'defruled
          (cons
           type-suffix-of-update
           (cons
            (cons
             'implies
             (cons
              (cons
               'and
               (cons (cons recog (cons type 'nil))
                     (cons (cons val-type-suffix
                                 (cons val-type extra-args-names))
                           (cons (cons type-suffix
                                       (cons type extra-args-names))
                                 'nil))))
              (cons
               (cons
                type-suffix
                (cons (cons 'omap::update
                            (cons key-type
                                  (cons val-type (cons type 'nil))))
                      extra-args-names))
               'nil)))
            (cons
             ':induct
             (cons
              't
              (cons
               ':enable
               (cons
                (cons
                 type-suffix
                 (cons
                  recog
                  '(omap::update omap::emptyp omap::mfix
                                 omap::mapp omap::head omap::tail)))
                'nil)))))))
         (cons
          (cons
           'defruled
           (cons
            val-type-suffix-of-head-when-type-suffix
            (cons
             (cons
              'implies
              (cons
               (cons
                'and
                (cons
                 (cons recog (cons type 'nil))
                 (cons
                  (cons type-suffix
                        (cons type extra-args-names))
                  (cons
                   (cons 'not
                         (cons (cons 'omap::emptyp (cons type 'nil))
                               'nil))
                   'nil))))
               (cons
                (cons
                 val-type-suffix
                 (cons
                  (cons
                     'mv-nth
                     (cons '1
                           (cons (cons 'omap::head (cons type 'nil))
                                 '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-tail
                 (cons
                      type-suffix-of-update
                      (cons val-type-suffix-of-head-when-type-suffix
                            'nil)))
                'nil))
              'nil)))
           'nil))))))))
   (mv fn-event thm-events))))

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

(defthm pseudo-event-formp-of-deffoldred-gen-omap-fold.fn-event
 (b* (((mv ?fn-event ?thm-events)
       (deffoldred-gen-omap-fold omap 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-omap-fold.thm-events

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