Check that the parameters in a function are sufficiently simple to handle.
(vl-fun-paramdecllist-types-okp x warnings function) → (mv okp warnings)
We make sure that all of the parameters in the function are plain parameters with no ranges or weird types. This restriction might not be necessary, but we are not sure whether other kinds of parameters would require some special handling.
Function:
(defun vl-fun-paramdecllist-types-okp (x warnings function) (declare (xargs :guard (and (vl-paramdecllist-p x) (vl-warninglist-p warnings) (vl-fundecl-p function)))) (let ((__function__ 'vl-fun-paramdecllist-types-okp)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv t (ok))) ((vl-paramdecl x1) (car x)) ((unless (and (eq (vl-paramtype-kind x1.type) :vl-implicitvalueparam) (not (vl-implicitvalueparam->sign x1.type)) (not (vl-implicitvalueparam->range x1.type)))) (mv nil (fatal :type :vl-bad-function-paramdecl :msg "In ~a0, parameter ~s1 has unsupported type ~x2." :args (list function x1.name x1.type)))) ((unless (vl-implicitvalueparam->default x1.type)) (mv nil (fatal :type :vl-bad-function-paramdecl :msg "In ~a0, parameter ~s1 has no value, which is not supported." :args (list function x1.name))))) (vl-fun-paramdecllist-types-okp (cdr x) warnings function))))
Theorem:
(defthm booleanp-of-vl-fun-paramdecllist-types-okp.okp (b* (((mv ?okp ?warnings) (vl-fun-paramdecllist-types-okp x warnings function))) (booleanp okp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-warninglist-p-of-vl-fun-paramdecllist-types-okp.warnings (b* (((mv ?okp ?warnings) (vl-fun-paramdecllist-types-okp x warnings function))) (vl-warninglist-p warnings)) :rule-classes :rewrite)