(vl-fundecl-to-svex x ss scopes config) → (mv ok warnings svex constraints)
Function:
(defun vl-fundecl-to-svex (x ss scopes config) (declare (xargs :guard (and (vl-fundecl-p x) (vl-scopestack-p ss) (vl-elabscopes-p scopes) (vl-simpconfig-p config)))) (let ((__function__ 'vl-fundecl-to-svex)) (declare (ignorable __function__)) (b* (((vl-fundecl x) (vl-fundecl-fix x)) (warnings nil) ((vwmv ok vttree localvars varstmts) (vl-vardecllist->svstmts (vl-delete-vardecls (cons x.name (vl-portdecllist->names x.portdecls)) x.vardecls) ss scopes)) (var-constraints (vttree-constraints-to-svstmts vttree)) ((unless ok) (mv nil warnings (svex-x) nil)) (x.body (vl-stmt-strip-nullstmts x.body)) ((vl-simpconfig config)) ((wmv ok warnings svstmts) (vl-stmt->svstmts x.body ss scopes (make-svstmt-config :nonblockingp nil :uniquecase-conservative config.uniquecase-conservative :uniquecase-constraints config.uniquecase-constraints) (vl-idexpr x.name))) ((unless ok) (mv nil warnings (svex-x) nil)) (svstmts (append-without-guard var-constraints (list (sv::make-svstmt-scope :locals localvars :body (append-without-guard varstmts svstmts))))) ((wmv ok warnings svstate constraints blk-masks nonblk-masks) (time$ (sv::svstmtlist-compile-top svstmts :sclimit config.sc-limit :nb-delayp nil) :mintime 1/2 :msg "; vl-fundecl-to-svex: compiling ~s0: ~st sec, ~sa bytes" :args (list x.name))) (- (fast-alist-free blk-masks) (fast-alist-free nonblk-masks)) ((unless ok) (mv nil warnings (svex-x) nil)) ((sv::svstate svstate)) (expr (sv::svstack-lookup (sv::make-svar :name x.name) svstate.blkst)) (- (sv::svstate-free svstate)) ((unless expr) (mv nil (warn :type :vl-fundecl-to-svex-fail :msg "Function has no return value") (svex-x) nil))) (mv t (ok) expr constraints))))
Theorem:
(defthm vl-warninglist-p-of-vl-fundecl-to-svex.warnings (b* (((mv ?ok ?warnings ?svex ?constraints) (vl-fundecl-to-svex x ss scopes config))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm svex-p-of-vl-fundecl-to-svex.svex (b* (((mv ?ok ?warnings ?svex ?constraints) (vl-fundecl-to-svex x ss scopes config))) (sv::svex-p svex)) :rule-classes :rewrite)
Theorem:
(defthm constraintlist-p-of-vl-fundecl-to-svex.constraints (b* (((mv ?ok ?warnings ?svex ?constraints) (vl-fundecl-to-svex x ss scopes config))) (sv::constraintlist-p constraints)) :rule-classes :rewrite)
Theorem:
(defthm vars-of-vl-fundecl-to-svex (b* (((mv ?ok ?warnings ?svex ?constraints) (vl-fundecl-to-svex x ss scopes config))) (and (sv::svarlist-addr-p (sv::svex-vars svex)) (sv::svarlist-addr-p (sv::constraintlist-vars constraints)))))
Theorem:
(defthm vl-fundecl-to-svex-of-vl-fundecl-fix-x (equal (vl-fundecl-to-svex (vl-fundecl-fix x) ss scopes config) (vl-fundecl-to-svex x ss scopes config)))
Theorem:
(defthm vl-fundecl-to-svex-vl-fundecl-equiv-congruence-on-x (implies (vl-fundecl-equiv x x-equiv) (equal (vl-fundecl-to-svex x ss scopes config) (vl-fundecl-to-svex x-equiv ss scopes config))) :rule-classes :congruence)
Theorem:
(defthm vl-fundecl-to-svex-of-vl-scopestack-fix-ss (equal (vl-fundecl-to-svex x (vl-scopestack-fix ss) scopes config) (vl-fundecl-to-svex x ss scopes config)))
Theorem:
(defthm vl-fundecl-to-svex-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-fundecl-to-svex x ss scopes config) (vl-fundecl-to-svex x ss-equiv scopes config))) :rule-classes :congruence)
Theorem:
(defthm vl-fundecl-to-svex-of-vl-elabscopes-fix-scopes (equal (vl-fundecl-to-svex x ss (vl-elabscopes-fix scopes) config) (vl-fundecl-to-svex x ss scopes config)))
Theorem:
(defthm vl-fundecl-to-svex-vl-elabscopes-equiv-congruence-on-scopes (implies (vl-elabscopes-equiv scopes scopes-equiv) (equal (vl-fundecl-to-svex x ss scopes config) (vl-fundecl-to-svex x ss scopes-equiv config))) :rule-classes :congruence)
Theorem:
(defthm vl-fundecl-to-svex-of-vl-simpconfig-fix-config (equal (vl-fundecl-to-svex x ss scopes (vl-simpconfig-fix config)) (vl-fundecl-to-svex x ss scopes config)))
Theorem:
(defthm vl-fundecl-to-svex-vl-simpconfig-equiv-congruence-on-config (implies (vl-simpconfig-equiv config config-equiv) (equal (vl-fundecl-to-svex x ss scopes config) (vl-fundecl-to-svex x ss scopes config-equiv))) :rule-classes :congruence)