Ensure that a function's variables are simple enough to convert into nets.
(vl-fun-vardecllist-types-okp x warnings function) → (mv okp warnings)
Function:
(defun vl-fun-vardecllist-types-okp (x warnings function) (declare (xargs :guard (and (vl-vardecllist-p x) (vl-warninglist-p warnings) (vl-fundecl-p function)))) (let ((__function__ 'vl-fun-vardecllist-types-okp)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv t (ok))) (x1 (vl-vardecl-fix (car x))) ((vl-vardecl x1) x1) ((unless (vl-simplereg-p x1)) (mv nil (fatal :type :vl-bad-function-vardecl :msg "In ~a0, variable ~s1 is not a simple register. ~ Other types of variables are not yet supported." :args (list function x1.name)))) ((when x1.initval) (mv nil (fatal :type :vl-bad-function-vardecl :msg "In ~a0, ~s1 has an initial value, which is ~ not supported." :args (list function x1.name))))) (vl-fun-vardecllist-types-okp (cdr x) warnings function))))
Theorem:
(defthm booleanp-of-vl-fun-vardecllist-types-okp.okp (b* (((mv ?okp ?warnings) (vl-fun-vardecllist-types-okp x warnings function))) (booleanp okp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-warninglist-p-of-vl-fun-vardecllist-types-okp.warnings (b* (((mv ?okp ?warnings) (vl-fun-vardecllist-types-okp x warnings function))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-simplereglist-p-when-vl-fun-vardecllist-types-okp (b* (((mv okp ?warnings) (vl-fun-vardecllist-types-okp x warnings function))) (implies okp (vl-simplereglist-p x))))