Events generated by defbytelist.
(defbytelist-fn type elt-type pred fix equiv parents short long wrld) → event
For now we only perform partial validation of the inputs. Future implementations may perform a more thorough validation.
Function:
(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)))))))))