Events generated by deflist-of-len.
(deflist-of-len-fn type list-type length 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 deflist-of-len-fn (type list-type length pred fix equiv parents short long wrld) (declare (xargs :guard (plist-worldp wrld))) (let ((__function__ 'deflist-of-len-fn)) (declare (ignorable __function__)) (b* (((unless (symbolp type)) (raise "The TYPE input must be a symbol, ~ but it is ~x0 instead." type)) ((unless (symbolp list-type)) (raise "The :LIST-TYPE input must be a symbol, ~ but it is ~x0 instead." list-type)) (fty-table (get-fixtypes-alist wrld)) (fty-info (find-fixtype list-type fty-table)) ((unless fty-info) (raise "The :LIST-TYPE input ~x0 must name a fixtype, ~ but it does not." list-type)) (list-pred (fixtype->pred fty-info)) (list-fix (fixtype->fix fty-info)) ((unless (natp length)) (raise "The :LENGTH input must be a non-negative integer, ~ but it is ~x0 instead." length)) ((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)) (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"))) (booleanp-of-pred (acl2::packn-pos (list 'booleanp-of- pred) pkg-witness)) (list-pred-when-pred-rewrite (acl2::packn-pos (list list-pred '-when- pred '-rewrite) pkg-witness)) (list-pred-when-pred-forward (acl2::packn-pos (list list-pred '-when- pred '-forward) pkg-witness)) (len-when-pred-tau (acl2::packn-pos (list 'len-when- pred '-tau) pkg-witness)) (pred-of-fix (acl2::packn-pos (list pred '-of- fix) pkg-witness)) (fix-when-pred (acl2::packn-pos (list fix '-when- pred) pkg-witness)) (x (intern-in-package-of-symbol "X" pkg-witness)) (type-ref (concatenate 'string "@(tsee " (common-lisp::string-downcase (symbol-package-name type)) "::" (common-lisp::string-downcase (symbol-name type)) ")")) (pred-event (cons 'define (cons pred (cons (cons x 'nil) (cons ':parents (cons (cons type 'nil) (cons ':short (cons (concatenate 'string "Recognizer for " type-ref ".") (cons (cons 'and (cons (cons list-pred (cons x 'nil)) (cons (cons 'equal (cons (cons 'len (cons x 'nil)) (cons length 'nil))) 'nil))) (cons ':no-function (cons 't (cons '/// (cons (cons 'defrule (cons booleanp-of-pred (cons (cons 'booleanp (cons (cons pred (cons x 'nil)) 'nil)) 'nil))) (cons (cons 'defrule (cons list-pred-when-pred-rewrite (cons (cons 'implies (cons (cons pred (cons x 'nil)) (cons (cons list-pred (cons x 'nil)) 'nil))) 'nil))) (cons (cons 'defrule (cons list-pred-when-pred-forward (cons (cons 'implies (cons (cons pred (cons x 'nil)) (cons (cons list-pred (cons x 'nil)) 'nil))) '(:rule-classes :forward-chaining)))) (cons (cons 'defrule (cons len-when-pred-tau (cons (cons 'implies (cons (cons pred (cons x 'nil)) (cons (cons 'equal (cons (cons 'len (cons x 'nil)) (cons length 'nil))) 'nil))) '(:rule-classes :tau-system)))) 'nil)))))))))))))))) (fix-event (cons 'define (cons fix (cons (cons (cons x (cons pred 'nil)) 'nil) (cons ':parents (cons (cons type 'nil) (cons ':short (cons (concatenate 'string "Fixer for " type-ref ".") (cons (cons 'mbe (cons ':logic (cons (cons 'if (cons (cons pred (cons x 'nil)) (cons x (cons (cons list-fix (cons (cons 'take (cons length (cons x 'nil))) 'nil)) 'nil)))) (cons ':exec (cons x 'nil))))) (cons ':no-function (cons 't (cons '/// (cons (cons 'defrule (cons pred-of-fix (cons (cons pred (cons (cons fix (cons x 'nil)) 'nil)) (cons ':enable (cons (cons pred '(deflist-of-len-support-lemma)) '(:disable take)))))) (cons (cons 'defrule (cons fix-when-pred (cons (cons 'implies (cons (cons pred (cons x 'nil)) (cons (cons 'equal (cons (cons fix (cons x 'nil)) (cons x 'nil))) 'nil))) 'nil))) 'nil)))))))))))))) (type-event (cons 'defsection (cons type (append (and parents (list :parents parents)) (append (and short (list :short short)) (append (and long (list :long long)) (cons (cons 'deffixtype (cons type (cons ':pred (cons pred (cons ':fix (cons fix (cons ':equiv (cons equiv '(:define t :forward t))))))))) 'nil)))))))) (cons 'encapsulate (cons 'nil (cons '(logic) (cons pred-event (cons fix-event (cons type-event 'nil)))))))))