• 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-map
          • Deffold-map-implementation
            • Deffold-map-event-generation
              • Deffold-map-gen-list-map
              • Deffold-map-gen-omap-map
              • Deffold-map-gen-clique-map/maps
              • Deffold-map-gen-prod-map
              • Deffold-map-gen-sum-case
              • Deffold-map-gen-sum-map
              • Deffold-map-gen-option-map
              • Deffold-map-gen-sum-cases
              • Deffold-map-gen-everything
              • Deffold-map-gen-sum-case-loop
              • Deffold-map-gen-prod/sum/option-map
              • Deffold-map-gen-cliques-maps
              • Deffold-map-gen-types-maps
              • Deffold-map-gen-type-map
              • Deffold-map-extra-args-to-names
              • Deffold-map-gen-map-name
              • Deffold-map-gen-topic-name
              • Deffold-map-gen-ruleset-name
            • Deffold-map-process-inputs-and-gen-everything
            • Deffold-map-fn
            • Deffold-map-input-processing
            • Deffold-map-macro-definition
        • 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-map-event-generation

Deffold-map-gen-list-map

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

Signature

(deffold-map-gen-list-map list mutrecp suffix extra-args fty-table) 
  → 
event

Arguments

list — Guard (flexlist-p list).

mutrecp — Guard (booleanp mutrecp).

suffix — Guard (symbolp suffix).

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

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

Returns

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

This is as described in deffold-map.

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

Definitions and Theorems

Function: deffold-map-gen-list-map

(defun deffold-map-gen-list-map
       (list mutrecp suffix extra-args fty-table)
 (declare (xargs :guard (and (flexlist-p list)
                             (booleanp mutrecp)
                             (symbolp suffix)
                             (true-listp extra-args)
                             (alistp fty-table))))
 (let ((__function__ 'deffold-map-gen-list-map))
  (declare (ignorable __function__))
  (b*
   ((type (flexlist->name list))
    ((unless (symbolp type))
     (raise "Internal error: malformed type name ~x0."
            type)
     '(_))
    (type-suffix (deffold-map-gen-map-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)
     '(_))
    (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)
     '(_))
    (elt-type-suffix (deffold-map-gen-map-name elt-type suffix))
    (extra-args-names (deffold-map-extra-args-to-names extra-args))
    (body
     (cons
      'if
      (cons
       (cons (if (flexlist->true-listp list)
                 'endp
               'atom)
             (cons type 'nil))
       (cons
        'nil
        (cons
          (cons 'cons
                (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)))))
    (type-suffix-type-prescription
         (acl2::packn-pos (list type-suffix '-type-prescription)
                          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))
    (consp-of-type-suffix
         (acl2::packn-pos (list 'consp-of- type-suffix)
                          suffix))
    (len-of-type-suffix (acl2::packn-pos (list 'len-of- type-suffix)
                                         suffix))
    (nth-of-type-suffix (acl2::packn-pos (list 'nth-of- type-suffix)
                                         suffix))
    (type-suffix-of-revappend
         (acl2::packn-pos (list type-suffix '-of-revappend)
                          suffix))
    (type-suffix-of-reverse
         (acl2::packn-pos (list type-suffix '-of-reverse)
                          suffix))
    (thm-events
     (cons
      (cons
       'defruled
       (cons
        type-suffix-type-prescription
        (cons
         (cons 'true-listp
               (cons (cons type-suffix
                           (cons type extra-args-names))
                     'nil))
         (cons
          ':rule-classes
          (cons
           ':type-prescription
           (cons
            ':hints
            (cons
             (cons
              (cons
               '"Goal"
               (cons
                ':in-theory
                (cons
                 ''(true-listp)
                 (cons
                  ':expand
                  (cons
                     (cons (cons type-suffix
                                 (cons type extra-args-names))
                           'nil)
                     (cons ':induct
                           (cons (cons 'true-listp (cons type 'nil))
                                 'nil)))))))
              'nil)
             'nil)))))))
      (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))
                                 '(nil)))
                     'nil)))
          (cons
           ':hints
           (cons
            (cons
             (cons
              '"Goal"
              (cons ':in-theory
                    (cons (cons 'quote
                                (cons (cons type-suffix 'nil) 'nil))
                          'nil)))
             'nil)
            '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 'cons
                     (cons (cons elt-type-suffix
                                 (cons elt-type extra-args-names))
                           (cons (cons type-suffix
                                       (cons type extra-args-names))
                                 'nil)))
               'nil)))
           (cons
            ':hints
            (cons
             (cons
              (cons
               '"Goal"
               (cons
                ':in-theory
                (cons
                 (cons 'quote
                       (cons (cons type-suffix '(car-cons cdr-cons))
                             'nil))
                 'nil)))
              'nil)
             'nil)))))
        (cons
         (cons
          'defruled
          (cons
           type-suffix-of-append
           (cons
            (cons
             'equal
             (cons
              (cons type-suffix
                    (cons '(append x y) extra-args-names))
              (cons
               (cons
                'append
                (cons
                 (cons type-suffix (cons 'x extra-args-names))
                 (cons (cons type-suffix (cons 'y extra-args-names))
                       'nil)))
               'nil)))
            (cons
             ':hints
             (cons
              (cons
               (cons
                '"Goal"
                (cons
                 ':in-theory
                 (cons
                  (cons
                   'quote
                   (cons
                      (cons 'append
                            (cons type-suffix '(car-cons cdr-cons)))
                      'nil))
                  '(:induct (append x y)))))
               'nil)
              'nil)))))
         (cons
          (cons
           'defruled
           (cons
            consp-of-type-suffix
            (cons
             (cons
               'equal
               (cons (cons 'consp
                           (cons (cons type-suffix
                                       (cons type extra-args-names))
                                 'nil))
                     (cons (cons 'consp (cons type 'nil))
                           'nil)))
             (cons
              ':hints
              (cons
               (cons
                (cons
                 '"Goal"
                 (cons
                  ':in-theory
                  (cons
                   'nil
                   (cons
                     ':expand
                     (cons (cons (cons type-suffix
                                       (cons type extra-args-names))
                                 'nil)
                           'nil)))))
                'nil)
               'nil)))))
          (cons
           (cons
            'defruled
            (cons
             len-of-type-suffix
             (cons
              (cons
               'equal
               (cons (cons 'len
                           (cons (cons type-suffix
                                       (cons type extra-args-names))
                                 'nil))
                     (cons (cons 'len (cons type 'nil))
                           'nil)))
              (cons
               ':hints
               (cons
                (cons
                 (cons
                  '"Goal"
                  (cons
                   ':in-theory
                   (cons
                    ''(len cdr-cons)
                    (cons
                     ':expand
                     (cons (cons (cons type-suffix
                                       (cons type extra-args-names))
                                 'nil)
                           (cons ':induct
                                 (cons (cons 'len (cons type 'nil))
                                       'nil)))))))
                 'nil)
                'nil)))))
           (cons
            (cons
             'defruled
             (cons
              nth-of-type-suffix
              (cons
               (cons
                'equal
                (cons
                 (cons
                     'nth
                     (cons 'n
                           (cons (cons type-suffix
                                       (cons type extra-args-names))
                                 'nil)))
                 (cons
                  (cons
                   'if
                   (cons
                    (cons '<
                          (cons '(nfix n)
                                (cons (cons 'len (cons type 'nil))
                                      'nil)))
                    (cons
                     (cons
                        elt-type-suffix
                        (cons (cons 'nth (cons 'n (cons type 'nil)))
                              extra-args-names))
                     '(nil))))
                  'nil)))
               (cons
                ':hints
                (cons
                 (cons
                  (cons
                   '"Goal"
                   (cons
                    ':in-theory
                    (cons
                     (cons
                      'quote
                      (cons
                       (cons
                            'nth
                            (cons type-suffix
                                  '(len (:t len)
                                        nfix zp car-cons cdr-cons)))
                       'nil))
                     (cons
                      ':expand
                      (cons
                       (cons (cons type-suffix
                                   (cons type extra-args-names))
                             (cons (cons 'len (cons type 'nil))
                                   'nil))
                       (cons
                        ':induct
                        (cons (cons 'nth (cons 'n (cons type 'nil)))
                              'nil)))))))
                  'nil)
                 'nil)))))
            (cons
             (cons
              'defruled
              (cons
               type-suffix-of-revappend
               (cons
                (cons
                 'equal
                 (cons
                  (cons type-suffix
                        (cons '(revappend x y)
                              extra-args-names))
                  (cons
                   (cons
                    'revappend
                    (cons
                     (cons type-suffix (cons 'x extra-args-names))
                     (cons
                       (cons type-suffix (cons 'y extra-args-names))
                       'nil)))
                   'nil)))
                (cons
                 ':hints
                 (cons
                  (cons
                   (cons
                    '"Goal"
                    (cons
                     ':in-theory
                     (cons
                      (cons
                       'quote
                       (cons
                        (cons
                            'revappend
                            (cons type-suffix '(car-cons cdr-cons)))
                        'nil))
                      '(:induct (revappend x y)))))
                   'nil)
                  'nil)))))
             (cons
              (cons
               'defruled
               (cons
                type-suffix-of-reverse
                (cons
                 (cons
                  'equal
                  (cons
                   (cons type-suffix
                         (cons (cons 'reverse (cons type 'nil))
                               extra-args-names))
                   (cons
                     (cons 'reverse
                           (cons (cons type-suffix
                                       (cons type extra-args-names))
                                 'nil))
                     'nil)))
                 (cons
                  ':hints
                  (cons
                   (cons
                    (cons
                     '"Goal"
                     (cons
                      ':in-theory
                      (cons
                       (cons
                        'quote
                        (cons
                         (cons
                          'reverse
                          (cons
                           'revappend
                           (cons
                            type-suffix-type-prescription
                            (cons
                             type-suffix-when-atom
                             (cons
                                  type-suffix-of-revappend 'nil)))))
                         'nil))
                       'nil)))
                    'nil)
                   'nil)))))
              'nil))))))))))
    (ruleset-event
     (cons
      'add-to-ruleset
      (cons
       (deffold-map-gen-ruleset-name suffix)
       (cons
        (cons
         'quote
         (cons
          (cons
           type-suffix-type-prescription
           (cons
            type-suffix-when-atom
            (cons
             type-suffix-of-cons
             (cons
              type-suffix-of-append
              (cons
               consp-of-type-suffix
               (cons
                len-of-type-suffix
                (cons
                    nth-of-type-suffix
                    (cons type-suffix-of-revappend
                          (cons type-suffix-of-reverse 'nil)))))))))
          'nil))
        'nil)))))
   (cons
    'define
    (cons
     type-suffix
     (cons
      (cons (cons type (cons recog 'nil))
            extra-args)
      (cons
       ':returns
       (cons
        (cons 'result (cons recog 'nil))
        (cons
         ':parents
         (cons
          (cons (deffold-map-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))
             (append
              (and (not mutrecp) '(:hooks (:fix)))
              (cons
                   '///
                   (append thm-events
                           (cons ruleset-event 'nil)))))))))))))))))

Theorem: pseudo-event-formp-of-deffold-map-gen-list-map

(defthm pseudo-event-formp-of-deffold-map-gen-list-map
 (b*
  ((event
    (deffold-map-gen-list-map list
                              mutrecp suffix extra-args fty-table)))
  (acl2::pseudo-event-formp event))
 :rule-classes :rewrite)