Check if a type is statically well-formed.
The primitive types are always well-formed. The collection types and the option type are well-formed iff their argument types are. A defined type is well-formed iff it references a defined type in the existing top-level constructs, or one of the types being currently defined.
Function:
(defun check-type (type ctxt) (declare (xargs :guard (and (typep type) (contextp ctxt)))) (let ((__function__ 'check-type)) (declare (ignorable __function__)) (type-case type :boolean t :character t :string t :integer t :set (check-type type.element ctxt) :sequence (check-type type.element ctxt) :map (and (check-type type.domain ctxt) (check-type type.range ctxt)) :option (check-type type.base ctxt) :defined (bool-fix (or (get-type-definition type.name (context->tops ctxt)) (member-equal type.name (context->types ctxt)))))))
Theorem:
(defthm booleanp-of-check-type (b* ((yes/no (check-type type ctxt))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm check-type-of-type-fix-type (equal (check-type (type-fix type) ctxt) (check-type type ctxt)))
Theorem:
(defthm check-type-type-equiv-congruence-on-type (implies (type-equiv type type-equiv) (equal (check-type type ctxt) (check-type type-equiv ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-type-of-context-fix-ctxt (equal (check-type type (context-fix ctxt)) (check-type type ctxt)))
Theorem:
(defthm check-type-context-equiv-congruence-on-ctxt (implies (context-equiv ctxt ctxt-equiv) (equal (check-type type ctxt) (check-type type ctxt-equiv))) :rule-classes :congruence)