(vl-evatomlist-delay-substitution x edge-dependent-delayp ss scopes) → (mv warnings subst)
Function:
(defun vl-evatomlist-delay-substitution (x edge-dependent-delayp ss scopes) (declare (xargs :guard (and (vl-evatomlist-p x) (vl-scopestack-p ss) (vl-elabscopes-p scopes)))) (let ((__function__ 'vl-evatomlist-delay-substitution)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv nil nil)) ((vl-evatom x1) (vl-evatom-fix (car x))) (warnings nil) ((unless (vl-expr-case x1.expr :vl-index (and (vl-partselect-case x1.expr.part :none) (atom x1.expr.indices)) :otherwise nil)) (vl-evatomlist-delay-substitution (cdr x) edge-dependent-delayp ss scopes)) ((mv err opinfo) (vl-index-expr-typetrace x1.expr ss scopes)) ((when err) (vl-evatomlist-delay-substitution (cdr x) edge-dependent-delayp ss scopes)) ((vl-operandinfo opinfo)) ((unless (and (vl-hidtrace-resolved-p opinfo.hidtrace) (eql (vl-seltrace-unres-count opinfo.seltrace) 0))) (vl-evatomlist-delay-substitution (cdr x) edge-dependent-delayp ss scopes)) (warnings (if (or opinfo.seltrace opinfo.part) (warn :type :vl-always-trigger-dubiously-translated :msg "Event trigger expression ~a0 has selects on it; we ~ probably don't deal well with this yet." :args (list x1)) warnings)) ((mv err var) (vl-operandinfo-base-svar opinfo ss)) ((when err) (vl-evatomlist-delay-substitution (cdr x) edge-dependent-delayp ss scopes)) (expr (sv::make-svex-var :name var)) (delay-expr (if edge-dependent-delayp (case x1.type (:vl-noedge expr) (:vl-posedge (sv::make-svex-call :fn 'sv::? :args (list (sv::make-svex-call :fn 'sv::bitsel :args (list (sv::svex-quote (sv::2vec 0)) expr)) expr (sv::svex-add-delay expr 1)))) (:vl-negedge (sv::make-svex-call :fn 'sv::? :args (list (sv::make-svex-call :fn 'sv::bitsel :args (list (sv::svex-quote (sv::2vec 0)) expr)) (sv::svex-add-delay expr 1) expr))) (:vl-edge expr)) expr)) ((wmv warnings rest) (vl-evatomlist-delay-substitution (cdr x) edge-dependent-delayp ss scopes))) (mv warnings (cons (cons var delay-expr) rest)))))
Theorem:
(defthm vl-warninglist-p-of-vl-evatomlist-delay-substitution.warnings (b* (((mv ?warnings common-lisp::?subst) (vl-evatomlist-delay-substitution x edge-dependent-delayp ss scopes))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-evatomlist-delay-substitution.subst (b* (((mv ?warnings common-lisp::?subst) (vl-evatomlist-delay-substitution x edge-dependent-delayp ss scopes))) (and (sv::svex-alist-p subst) (sv::svarlist-addr-p (sv::svex-alist-vars subst)) (sv::svarlist-addr-p (sv::svex-alist-keys subst)))) :rule-classes :rewrite)
Theorem:
(defthm vl-evatomlist-delay-substitution-of-vl-evatomlist-fix-x (equal (vl-evatomlist-delay-substitution (vl-evatomlist-fix x) edge-dependent-delayp ss scopes) (vl-evatomlist-delay-substitution x edge-dependent-delayp ss scopes)))
Theorem:
(defthm vl-evatomlist-delay-substitution-vl-evatomlist-equiv-congruence-on-x (implies (vl-evatomlist-equiv x x-equiv) (equal (vl-evatomlist-delay-substitution x edge-dependent-delayp ss scopes) (vl-evatomlist-delay-substitution x-equiv edge-dependent-delayp ss scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-evatomlist-delay-substitution-of-vl-scopestack-fix-ss (equal (vl-evatomlist-delay-substitution x edge-dependent-delayp (vl-scopestack-fix ss) scopes) (vl-evatomlist-delay-substitution x edge-dependent-delayp ss scopes)))
Theorem:
(defthm vl-evatomlist-delay-substitution-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-evatomlist-delay-substitution x edge-dependent-delayp ss scopes) (vl-evatomlist-delay-substitution x edge-dependent-delayp ss-equiv scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-evatomlist-delay-substitution-of-vl-elabscopes-fix-scopes (equal (vl-evatomlist-delay-substitution x edge-dependent-delayp ss (vl-elabscopes-fix scopes)) (vl-evatomlist-delay-substitution x edge-dependent-delayp ss scopes)))
Theorem:
(defthm vl-evatomlist-delay-substitution-vl-elabscopes-equiv-congruence-on-scopes (implies (vl-elabscopes-equiv scopes scopes-equiv) (equal (vl-evatomlist-delay-substitution x edge-dependent-delayp ss scopes) (vl-evatomlist-delay-substitution x edge-dependent-delayp ss scopes-equiv))) :rule-classes :congruence)