		Search-engine friendly clone of the ACL2 documentation.

Deffold-reduce-event-generation

Deffoldred-gen-option-fold

Generate the fold function for an option type.

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

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-reduce.

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

Definitions and Theorems

Function: deffoldred-gen-option-fold

(defun deffoldred-gen-option-fold
       (sum mutrecp suffix extra-args
            result default combine fty-table)
 (declare (xargs :guard (and (flexsum-p sum)
                             (booleanp mutrecp)
                             (symbolp suffix)
                             (true-listp extra-args)
                             (symbolp result)
                             (symbolp combine)
                             (alistp fty-table))))
 (declare (xargs :guard (eq (flexsum->typemacro sum)
                            'defoption)))
 (let ((__function__ 'deffoldred-gen-option-fold))
  (declare (ignorable __function__))
  (b*
   ((type (flexsum->name sum))
    ((unless (symbolp type))
     (raise "Internal error: malformed type name ~x0."
            type)
     (mv '(_) nil))
    (type-suffix (deffoldred-gen-fold-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-type-suffix (deffoldred-gen-fold-name base-type suffix))
    (extra-args-names (deffoldred-extra-args-to-names extra-args))
    (body
     (cons
      type-case
      (cons type
            (cons ':some
                  (cons (cons base-type-suffix
                              (cons (cons accessor (cons type 'nil))
                                    extra-args-names))
                        (cons ':none (cons default '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-base-type-suffix
         (acl2::packn-pos (list type-suffix '-when-
                                base-type-suffix)
                          suffix))
    (base-suffix-when-type-suffix-and-not-nil
         (acl2::packn-pos (list base-type-suffix '-when-
                                type-suffix '-and-not-nil)
                          suffix))
    (base-suffix-of-type-some->val
         (acl2::packn-pos (list base-type-suffix '-of-
                                type '-some->val)
                          suffix))
    (thm-events
     (and
      (eq combine 'and)
      (eq default t)
      (cons
       (cons
        'defruled
        (cons
         type-suffix-when-base-type-suffix
         (cons (cons 'implies
                     (cons (cons base-type-suffix
                                 (cons type extra-args-names))
                           (cons (cons type-suffix
                                       (cons type extra-args-names))
                                 'nil)))
               (cons ':expand
                     (cons (cons type-suffix
                                 (cons type extra-args-names))
                           (cons ':enable
                                 (cons accessor 'nil)))))))
       (cons
        (cons
         'defruled
         (cons
          base-suffix-when-type-suffix-and-not-nil
          (cons
           (cons
               'implies
               (cons (cons 'and
                           (cons (cons type-suffix
                                       (cons type extra-args-names))
                                 (cons type 'nil)))
                     (cons (cons base-type-suffix
                                 (cons type extra-args-names))
                           'nil)))
           (cons ':expand
                 (cons (cons type-suffix
                             (cons type extra-args-names))
                       (cons ':enable
                             (cons accessor 'nil)))))))
        (cons
         (cons
          'defruled
          (cons
           base-suffix-of-type-some->val
           (cons
            (cons
             'implies
             (cons
              (cons
                   'and
                   (cons (cons type-suffix
                               (cons type extra-args-names))
                         (cons (cons type-case (cons type '(:some)))
                               'nil)))
              (cons (cons base-type-suffix
                          (cons (cons accessor (cons type 'nil))
                                extra-args-names))
                    'nil)))
            (cons ':expand
                  (cons (cons type-suffix
                              (cons type extra-args-names))
                        'nil)))))
         (cons
          (cons
           'add-to-ruleset
           (cons
            (deffoldred-gen-ruleset-name suffix)
            (cons
             (cons
              'quote
              (cons
               (cons
                   type-suffix-when-base-type-suffix
                   (cons base-suffix-when-type-suffix-and-not-nil
                         (cons base-suffix-of-type-some->val 'nil)))
               'nil))
             'nil)))
          'nil)))))))
   (mv fn-event thm-events))))

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

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

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