• 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-omap-map

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

Signature

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

Arguments

omap — Guard (flexomap-p omap).

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 omap type is part of a mutually recursive clique.

Definitions and Theorems

Function: deffold-map-gen-omap-map

(defun deffold-map-gen-omap-map
       (omap mutrecp suffix extra-args fty-table)
 (declare (xargs :guard (and (flexomap-p omap)
                             (booleanp mutrecp)
                             (symbolp suffix)
                             (true-listp extra-args)
                             (alistp fty-table))))
 (let ((__function__ 'deffold-map-gen-omap-map))
  (declare (ignorable __function__))
  (b*
   ((type (flexomap->name omap))
    ((unless (symbolp type))
     (raise "Internal error: malformed type name ~x0."
            type)
     '(_))
    (type-suffix (deffold-map-gen-map-name type suffix))
    (type-fix (flexomap->fix omap))
    (type-count (flexomap->count omap))
    (recog (flexomap->pred omap))
    (recp (flexomap->recp omap))
    (val-recog (flexomap->val-type omap))
    ((unless (symbolp val-recog))
     (raise "Internal error: malformed recognizer ~x0."
            val-recog)
     '(_))
    (val-info (flextype-with-recognizer val-recog fty-table))
    (val-type (flextype->name val-info))
    (val-type-suffix (deffold-map-gen-map-name val-type suffix))
    (extra-args-names (deffold-map-extra-args-to-names extra-args))
    (body
     (cons
      'if
      (cons
       (cons
         'or
         (cons (cons 'not
                     (cons (cons 'mbt
                                 (cons (cons recog (cons type 'nil))
                                       'nil))
                           'nil))
               (cons (cons 'omap::emptyp (cons type 'nil))
                     'nil)))
       (cons
        'nil
        (cons
         (cons
          'omap::update
          (cons
           (cons 'omap::head-key (cons type 'nil))
           (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)))))
    (type-suffix-type-prescription
         (acl2::packn-pos (list type-suffix '-type-prescription)
                          suffix))
    (type-suffix-when-emptyp
         (acl2::packn-pos (list type-suffix '-when-emptyp)
                          suffix))
    (emptyp-of-type-suffix
         (acl2::packn-pos (list 'emptyp-of- type-suffix)
                          suffix))
    (keys-of-type-suffix
         (acl2::packn-pos (list 'keys-of- type-suffix)
                          suffix))
    (assoc-of-type-suffix
         (acl2::packn-pos (list 'assoc-of- type-suffix)
                          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 omap::update
                               omap::update-type-prescription)
                 (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-emptyp
         (cons
          (cons
           'implies
           (cons
               (cons 'omap::emptyp (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 '(omap::emptyp))
                                  'nil))
                      'nil)))
             'nil)
            'nil)))))
       (cons
        (cons
         'defruled
         (cons
          emptyp-of-type-suffix
          (cons
           (cons
            'equal
            (cons (cons 'omap::emptyp
                        (cons (cons type-suffix
                                    (cons type extra-args-names))
                              'nil))
                  (cons (cons 'omap::emptyp
                              (cons (cons type-fix (cons type 'nil))
                                    'nil))
                        'nil)))
           (cons ':expand
                 (cons (cons (cons type-suffix
                                   (cons type extra-args-names))
                             'nil)
                       'nil)))))
        (cons
         (cons
          'defruled
          (cons
           keys-of-type-suffix
           (cons
            (cons
             'equal
             (cons
                  (cons 'omap::keys
                        (cons (cons type-suffix
                                    (cons type extra-args-names))
                              'nil))
                  (cons (cons 'omap::keys
                              (cons (cons type-fix (cons type 'nil))
                                    'nil))
                        'nil)))
            (cons
             ':enable
             (cons
              '((:i omap::keys))
              (cons
               ':expand
               (cons (cons (cons type-suffix
                                 (cons type extra-args-names))
                           'nil)
                     (cons ':induct
                           (cons (cons 'omap::keys (cons type 'nil))
                                 'nil)))))))))
         (cons
          (cons
           'defruled
           (cons
            assoc-of-type-suffix
            (cons
             (cons
              'equal
              (cons
               (cons 'omap::assoc
                     (cons 'key
                           (cons (cons type-suffix
                                       (cons type extra-args-names))
                                 'nil)))
               (cons
                (cons
                 'if
                 (cons
                  (cons 'omap::assoc
                        (cons 'key
                              (cons (cons type-fix (cons type 'nil))
                                    'nil)))
                  (cons
                   (cons
                    'cons
                    (cons
                     'key
                     (cons
                      (cons
                       val-type-suffix
                       (cons
                        (cons
                         'cdr
                         (cons
                          (cons
                           'omap::assoc
                           (cons
                              'key
                              (cons (cons type-fix (cons type 'nil))
                                    'nil)))
                          'nil))
                        extra-args-names))
                      'nil)))
                   '(nil))))
                'nil)))
             (cons
              ':enable
              (cons
               '((:i omap::assoc))
               (cons
                ':expand
                (cons
                     (cons (cons type-suffix
                                 (cons type extra-args-names))
                           'nil)
                     (cons ':induct
                           (cons (cons 'omap::assoc
                                       (cons 'key (cons type '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-emptyp
                    (cons emptyp-of-type-suffix
                          (cons keys-of-type-suffix
                                (cons assoc-of-type-suffix '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-omap-map

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