Events generated by defsubtype.
(defsubtype-fn subtype supertype restriction fix-value 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 defsubtype-fn (subtype supertype restriction fix-value pred fix equiv parents short long wrld) (declare (xargs :guard (plist-worldp wrld))) (let ((__function__ 'defsubtype-fn)) (declare (ignorable __function__)) (b* (((unless (symbolp subtype)) (raise "The SUBTYPE input must be a symbol, ~ but it is ~x0 instead." subtype)) ((unless (symbolp supertype)) (raise "The :SUPERTYPE input must be a symbol, ~ but it is ~x0 instead." supertype)) ((unless (possible-predicate-p restriction)) (raise "The :RESTRICTION input must be either the name of a predicate, ~ or a lambda expression predicate, but it is ~x0 instead." restriction)) (fty-table (get-fixtypes-alist wrld)) (fty-info (find-fixtype supertype fty-table)) ((unless fty-info) (raise "The :SUPERTYPE input ~x0 must name a fixtype, ~ but it does not." supertype)) (super-pred (fixtype->pred 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)) (pkg (symbol-package-name subtype)) (pkg (if (equal pkg *main-lisp-package-name*) "ACL2" pkg)) (pkg-witness (pkg-witness pkg)) (pred (or pred (add-suffix-to-fn subtype "-P"))) (fix (or fix (add-suffix-to-fn subtype "-FIX"))) (equiv (or equiv (add-suffix-to-fn subtype "-EQUIV"))) (booleanp-of-pred (acl2::packn-pos (list 'booleanp-of- pred) pkg-witness)) (super-pred-when-pred-rewrite (acl2::packn-pos (list super-pred '-when- pred '-rewrite) pkg-witness)) (super-pred-when-pred-forward (acl2::packn-pos (list super-pred '-when- pred '-forward) 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 subtype)) "::" (common-lisp::string-downcase (symbol-name subtype)) ")")) (pred-event (cons 'define (cons pred (cons (cons x 'nil) (cons ':parents (cons (cons subtype 'nil) (cons ':short (cons (concatenate 'string "Recognizer for " type-ref ".") (cons (cons 'and (cons (cons super-pred (cons x 'nil)) (cons (cons restriction (cons x '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 super-pred-when-pred-rewrite (cons (cons 'implies (cons (cons pred (cons x 'nil)) (cons (cons super-pred (cons x 'nil)) 'nil))) 'nil))) (cons (cons 'defrule (cons super-pred-when-pred-forward (cons (cons 'implies (cons (cons pred (cons x 'nil)) (cons (cons super-pred (cons x 'nil)) 'nil))) '(:rule-classes :forward-chaining)))) 'nil))))))))))))))) (fix-event (cons 'define (cons fix (cons (cons (cons x (cons pred 'nil)) 'nil) (cons ':parents (cons (cons subtype '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 fix-value '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)) 'nil))) (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 subtype (append (and parents (list :parents parents)) (append (and short (list :short short)) (append (and long (list :long long)) (cons (cons 'deffixtype (cons subtype (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)))))))))