		Search-engine friendly clone of the ACL2 documentation.
Defbytelist-implementation
Defbytelist-fn

Events generated by defbytelist.
Signature
(defbytelist-fn type elt-type pred fix equiv parents short long wrld) → event
Arguments: wrld — Guard (plist-worldp wrld).
Returns: event — A ACL2::maybe-pseudo-event-formp.
For now we only perform partial validation of the inputs. Future implementations may perform a more thorough validation.
Definitions and Theorems

Function: defbytelist-fn
(defun defbytelist-fn (type elt-type
                            pred fix equiv parents short long wrld)
 (declare (xargs :guard (plist-worldp wrld)))
 (let ((__function__ 'defbytelist-fn))
  (declare (ignorable __function__))
  (b*
   (((unless (symbolp type))
     (raise
      "The TYPE input must be a symbol, ~
                but it is ~x0 instead."
      type))
    ((unless (symbolp elt-type))
     (raise
      "The :ELT-TYPE input must be a symbol,
                but it is ~x0 instead."
      elt-type))
    (defbyte-table (table-alist *defbyte-table-name* wrld))
    (defbyte-pair (assoc-eq elt-type defbyte-table))
    ((unless defbyte-pair)
     (raise
      "The :ELT-TYPE input ~x0 must name a type ~
                previously introduced via DEFBYTE, ~
                but this is not the case."
      elt-type))
    (defbyte-info (cdr defbyte-pair))
    (size (defbyte-info->size defbyte-info))
    (signed (defbyte-info->signed defbyte-info))
    (fty-table (get-fixtypes-alist wrld))
    (fty-info (find-fixtype elt-type fty-table))
    (bytep (fixtype->pred fty-info))
    (byte-fix (fixtype->fix fty-info))
    ((unless (symbolp pred))
     (raise
      "The :PRED input must be a symbol, ~
                but it is ~x0 instead."
      pred))
    ((unless (symbolp fix))
     (raise
      "The :FIX input must be a symbol, ~
                but it is ~x0 instead."
      fix))
    ((unless (symbolp equiv))
     (raise
      "The :EQUIV input must be a symbol, ~
                but it is ~x0 instead."
      equiv))
    (binpred (if signed 'acl2::signed-byte-listp
               'acl2::unsigned-byte-listp))
    (pkg (symbol-package-name type))
    (pkg (if (equal pkg *main-lisp-package-name*)
             "ACL2"
           pkg))
    (pkg-witness (pkg-witness pkg))
    (pred (or pred (add-suffix-to-fn type "-P")))
    (fix (or fix (add-suffix-to-fn type "-FIX")))
    (equiv (or equiv (add-suffix-to-fn type "-EQUIV")))
    (pred-forward-binpred
         (acl2::packn-pos (list pred '-forward- binpred)
                          pkg-witness))
    (pred-rewrite-binpred
         (acl2::packn-pos (list pred '-rewrite- binpred)
                          pkg-witness))
    (binpred-rewrite-pred
         (acl2::packn-pos (list binpred '-rewrite- pred)
                          pkg-witness))
    (true-listp-when-pred-rewrite
         (acl2::packn-pos (list 'true-listp-when- pred '-rewrite)
                          pkg-witness))
    (fix-of-take (acl2::packn-pos (list fix '-of-take)
                                  pkg-witness))
    (fix-of-rcons (acl2::packn-pos (list fix '-of-rcons)
                                   pkg-witness))
    (x (intern-in-package-of-symbol "X" pkg-witness))
    (a (intern-in-package-of-symbol "A" pkg-witness))
    (n (intern-in-package-of-symbol "N" pkg-witness))
    (type-theorems (add-suffix-to-fn type "-THEOREMS"))
    (deflist-event
     (cons
      'deflist
      (cons
       type
       (cons
        ':elt-type
        (cons
         elt-type
         (append
          (and parents (list :parents parents))
          (append
           (and short (list :short short))
           (append
            (and long (list :long long))
            (cons
             ':true-listp
             (cons
              't
              (cons
               ':elementp-of-nil
               (cons
                'nil
                (cons
                 ':pred
                 (cons
                  pred
                  (cons
                      ':fix
                      (cons fix
                            (cons ':equiv
                                  (cons equiv 'nil))))))))))))))))))
    (theorems-event
     (cons
      'defsection
      (cons
       type-theorems
       (cons
        ':extension
        (cons
         type
         (cons
          (cons
           'defrule
           (cons
            pred-forward-binpred
            (cons
             (cons
                'implies
                (cons (cons pred (cons x 'nil))
                      (cons (cons binpred (cons size (cons x 'nil)))
                            'nil)))
             (cons
              ':rule-classes
              (cons
               ':forward-chaining
               (cons
                ':in-theory
                (cons
                 (cons
                  'quote
                  (cons (cons pred (cons bytep (cons binpred 'nil)))
                        'nil))
                 'nil)))))))
          (cons
           (cons
            'defruled
            (cons
             pred-rewrite-binpred
             (cons
              (cons
                'equal
                (cons (cons pred (cons x 'nil))
                      (cons (cons binpred (cons size (cons x 'nil)))
                            'nil)))
              (cons
               ':in-theory
               (cons
                (cons
                  'quote
                  (cons (cons pred (cons bytep (cons binpred 'nil)))
                        'nil))
                'nil)))))
           (cons
            (cons
             'defruled
             (cons
              binpred-rewrite-pred
              (cons
               (cons 'equal
                     (cons (cons binpred (cons size (cons x 'nil)))
                           (cons (cons pred (cons x 'nil)) 'nil)))
               (cons
                  ':in-theory
                  (cons (cons 'quote
                              (cons (cons pred-rewrite-binpred 'nil)
                                    'nil))
                        'nil)))))
            (cons
             (cons
              'theory-invariant
              (cons
               (cons
                 'incompatible
                 (cons (cons ':rewrite
                             (cons pred-rewrite-binpred 'nil))
                       (cons (cons ':rewrite
                                   (cons binpred-rewrite-pred 'nil))
                             'nil)))
               'nil))
             (cons
              (cons
               'defruled
               (cons
                true-listp-when-pred-rewrite
                (cons
                 (cons 'implies
                       (cons (cons pred (cons x 'nil))
                             (cons (cons 'true-listp (cons x 'nil))
                                   'nil)))
                 (cons
                  ':in-theory
                  (cons (cons 'quote
                              (cons (cons pred '(true-listp)) 'nil))
                        'nil)))))
              (cons
               (cons
                'defrule
                (cons
                 fix-of-take
                 (cons
                  (cons
                   'implies
                   (cons
                    (cons
                       '<=
                       (cons (cons 'nfix (cons n 'nil))
                             (cons (cons 'len (cons x 'nil)) 'nil)))
                    (cons
                     (cons
                      'equal
                      (cons
                       (cons
                           fix
                           (cons (cons 'take (cons n (cons x 'nil)))
                                 'nil))
                       (cons
                        (cons
                         'take
                         (cons
                            n (cons (cons fix (cons x 'nil)) 'nil)))
                        'nil)))
                     'nil)))
                  (cons
                   ':in-theory
                   (cons
                    (cons
                     'quote
                     (cons
                      (cons
                       fix
                       (cons
                            (add-suffix-to-fn fix "-OF-CONS")
                            '(nfix zp len take acl2::take-of-cons)))
                      'nil))
                    'nil)))))
               (cons
                (cons
                 'defrule
                 (cons
                  fix-of-rcons
                  (cons
                   (cons
                    'equal
                    (cons
                     (cons
                          fix
                          (cons (cons 'rcons (cons a (cons x 'nil)))
                                'nil))
                     (cons
                      (cons
                        'rcons
                        (cons (cons byte-fix (cons a 'nil))
                              (cons (cons fix (cons x 'nil)) 'nil)))
                      'nil)))
                   (cons
                    ':in-theory
                    (cons
                     (cons
                      'quote
                      (cons
                       (cons
                        fix
                        (cons
                           (add-suffix-to-fn fix "-OF-CONS")
                           (cons (add-suffix-to-fn fix "-OF-APPEND")
                                 '(acl2::binary-append-without-guard
                                       rcons))))
                       'nil))
                     'nil)))))
                'nil)))))))))))))
   (cons 'encapsulate
         (cons 'nil
               (cons '(logic)
                     (cons deflist-event
                           (cons '(acl2::evmac-prepare-proofs)
                                 (cons theorems-event 'nil)))))))))