Rules about write-var.
The theorem about write-var turns it into update-var,
similarly to create-var being turned into add-var.
The condition for the replacemenet is captured by
We also include the executable counterpart of typep in the list of rules related to write-var. This is needed to discharge some typep hypotheses that arise during symbolic execution and are applied to quoted constants. We may arrange things in the future so that these quoted constants do not arise and thus there is no need for the executable counterpart of typep to be included in the list of rules here.
Also see atc-write-static-var-rules
for a rule that relates
Function:
(defun write-var-aux-okp (var val scopes) (declare (xargs :guard (and (identp var) (valuep val) (scope-listp scopes)))) (let ((__function__ 'write-var-aux-okp)) (declare (ignorable __function__)) (b* (((when (endp scopes)) nil) (scope (scope-fix (car scopes))) (pair (omap::assoc (ident-fix var) scope)) ((when (consp pair)) (equal (type-of-value (cdr pair)) (type-of-value val)))) (write-var-aux-okp var val (cdr scopes)))))
Theorem:
(defthm booleanp-of-write-var-aux-okp (b* ((yes/no (write-var-aux-okp var val scopes))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm write-var-aux-okp-of-ident-fix-var (equal (write-var-aux-okp (ident-fix var) val scopes) (write-var-aux-okp var val scopes)))
Theorem:
(defthm write-var-aux-okp-ident-equiv-congruence-on-var (implies (ident-equiv var var-equiv) (equal (write-var-aux-okp var val scopes) (write-var-aux-okp var-equiv val scopes))) :rule-classes :congruence)
Theorem:
(defthm write-var-aux-okp-of-value-fix-val (equal (write-var-aux-okp var (value-fix val) scopes) (write-var-aux-okp var val scopes)))
Theorem:
(defthm write-var-aux-okp-value-equiv-congruence-on-val (implies (value-equiv val val-equiv) (equal (write-var-aux-okp var val scopes) (write-var-aux-okp var val-equiv scopes))) :rule-classes :congruence)
Theorem:
(defthm write-var-aux-okp-of-scope-list-fix-scopes (equal (write-var-aux-okp var val (scope-list-fix scopes)) (write-var-aux-okp var val scopes)))
Theorem:
(defthm write-var-aux-okp-scope-list-equiv-congruence-on-scopes (implies (scope-list-equiv scopes scopes-equiv) (equal (write-var-aux-okp var val scopes) (write-var-aux-okp var val scopes-equiv))) :rule-classes :congruence)
Function:
(defun write-var-okp (var val compst) (declare (xargs :guard (and (identp var) (valuep val) (compustatep compst)))) (declare (xargs :guard (> (compustate-frames-number compst) 0))) (let ((__function__ 'write-var-okp)) (declare (ignorable __function__)) (b* ((scopes (frame->scopes (top-frame compst))) (autop (var-in-scopes-p var scopes)) ((when autop) (write-var-aux-okp var val scopes)) (static (compustate->static compst)) (pair (omap::assoc (ident-fix var) static))) (and (consp pair) (equal (type-of-value (cdr pair)) (type-of-value val))))))
Theorem:
(defthm booleanp-of-write-var-okp (b* ((yes/no (write-var-okp var val compst))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm write-var-okp-of-ident-fix-var (equal (write-var-okp (ident-fix var) val compst) (write-var-okp var val compst)))
Theorem:
(defthm write-var-okp-ident-equiv-congruence-on-var (implies (ident-equiv var var-equiv) (equal (write-var-okp var val compst) (write-var-okp var-equiv val compst))) :rule-classes :congruence)
Theorem:
(defthm write-var-okp-of-value-fix-val (equal (write-var-okp var (value-fix val) compst) (write-var-okp var val compst)))
Theorem:
(defthm write-var-okp-value-equiv-congruence-on-val (implies (value-equiv val val-equiv) (equal (write-var-okp var val compst) (write-var-okp var val-equiv compst))) :rule-classes :congruence)
Theorem:
(defthm write-var-okp-of-compustate-fix-compst (equal (write-var-okp var val (compustate-fix compst)) (write-var-okp var val compst)))
Theorem:
(defthm write-var-okp-compustate-equiv-congruence-on-compst (implies (compustate-equiv compst compst-equiv) (equal (write-var-okp var val compst) (write-var-okp var val compst-equiv))) :rule-classes :congruence)
Theorem:
(defthm write-var-okp-of-enter-scope (equal (write-var-okp var val (enter-scope compst)) (write-var-okp var val compst)))
Theorem:
(defthm write-var-okp-of-add-var (equal (write-var-okp var val (add-var var2 val2 compst)) (if (equal (ident-fix var) (ident-fix var2)) (equal (type-of-value val2) (type-of-value val)) (write-var-okp var val compst))))
Theorem:
(defthm write-var-okp-of-update-var (equal (write-var-okp var val (update-var var2 val2 compst)) (if (equal (ident-fix var) (ident-fix var2)) (equal (type-of-value val2) (type-of-value val)) (write-var-okp var val compst))))
Theorem:
(defthm write-var-okp-of-update-static-var (implies (not (equal (ident-fix var) (ident-fix var2))) (equal (write-var-okp var val (update-static-var var2 val2 compst)) (write-var-okp var val compst))))
Theorem:
(defthm write-var-okp-of-update-object (equal (write-var-okp var val (update-object objdes obj compst)) (write-var-okp var val compst)))
Theorem:
(defthm write-var-okp-when-valuep-of-read-var (implies (and (syntaxp (symbolp compst)) (> (compustate-frames-number compst) 0) (equal old-val (read-var var compst)) (valuep old-val)) (equal (write-var-okp var val compst) (equal (type-of-value val) (type-of-value old-val)))))
Theorem:
(defthm write-var-to-update-var (implies (and (> (compustate-frames-number compst) 0) (write-var-okp var val compst)) (equal (write-var var val compst) (update-var var val compst))))
Theorem:
(defthm write-var-to-write-static-var (implies (not (var-autop var compst)) (equal (write-var var val compst) (write-static-var var val compst))))