		Search-engine friendly clone of the ACL2 documentation.

Deffold-map-event-generation

Deffold-map-gen-option-map

Generate the map function for an option type.

Signature
(deffold-map-gen-option-map sum mutrecp suffix extra-args fty-table) → event
Arguments: sum — Guard (flexsum-p sum).; 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).

In the FTY table, option types are stored as sum types, but with an indication of defoption as the type macro.

This function is as described in deffold-map.

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

Definitions and Theorems

Function: deffold-map-gen-option-map

(defun deffold-map-gen-option-map
       (sum mutrecp suffix extra-args fty-table)
 (declare (xargs :guard (and (flexsum-p sum)
                             (booleanp mutrecp)
                             (symbolp suffix)
                             (true-listp extra-args)
                             (alistp fty-table))))
 (declare (xargs :guard (eq (flexsum->typemacro sum)
                            'defoption)))
 (let ((__function__ 'deffold-map-gen-option-map))
  (declare (ignorable __function__))
  (b*
   ((type (flexsum->name sum))
    ((unless (symbolp type))
     (raise "Internal error: malformed type name ~x0."
            type)
     '(_))
    (type-suffix (deffold-map-gen-map-name type suffix))
    (type-count (flexsum->count sum))
    (recog (flexsum->pred sum))
    (recp (flexsum->recp sum))
    (type-case (flexsum->case sum))
    ((mv base-type accessor)
     (components-of-flexoption-with-name type fty-table))
    (base-flextype (flextype-with-name base-type fty-table))
    ((unless base-flextype)
     (raise "Internal error: malformed type ~x0."
            base-type)
     '(_))
    (base-type-fix (flextype->fix base-flextype))
    (base-type-suffix (deffold-map-gen-map-name base-type suffix))
    (extra-args-names (deffold-map-extra-args-to-names extra-args))
    (body
     (cons
      type-case
      (cons
       type
       (cons
        ':some
        (cons
            (cons base-type-fix
                  (cons (cons base-type-suffix
                              (cons (cons accessor (cons type 'nil))
                                    extra-args-names))
                        'nil))
            '(:none nil))))))
    (type-suffix-under-iff
         (acl2::packn-pos (list type-suffix '-under-iff)
                          suffix))
    (thm-events
     (cons
      (cons
       'defruled
       (cons
        type-suffix-under-iff
        (cons
         (cons 'iff
               (cons (cons type-suffix
                           (cons type extra-args-names))
                     (cons type 'nil)))
         (cons
            ':expand
            (cons (cons (cons type-suffix
                              (cons type extra-args-names))
                        'nil)
                  (cons ':cases
                        (cons (cons (cons 'equal (cons type '(nil)))
                                    'nil)
                              'nil)))))))
      'nil))
    (ruleset-event
     (cons 'add-to-ruleset
           (cons (deffold-map-gen-ruleset-name suffix)
                 (cons (cons 'quote
                             (cons (cons type-suffix-under-iff '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-option-map

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