		Search-engine friendly clone of the ACL2 documentation.

Dynamic-semantics

Exec-ident

Execute a variable.

Signature
(exec-ident id compst) → eval
Arguments: id — Guard (identp id).; compst — Guard (compustatep compst).
Returns: eval — Type (expr-value-resultp eval).

We obtain the object designator of the variable, propagating errors. We read the value from the object designator, which is guaranteed to work as proved in read-object.

Definitions and Theorems

Function: exec-ident

(defun exec-ident (id compst)
  (declare (xargs :guard (and (identp id) (compustatep compst))))
  (let ((__function__ 'exec-ident))
    (declare (ignorable __function__))
    (b* ((objdes (objdesign-of-var id compst))
         ((unless objdes)
          (error (list :no-object-designator (ident-fix id))))
         (val (read-object objdes compst)))
      (make-expr-value :value val
                       :object objdes))))

Theorem: expr-value-resultp-of-exec-ident

(defthm expr-value-resultp-of-exec-ident
  (b* ((eval (exec-ident id compst)))
    (expr-value-resultp eval))
  :rule-classes :rewrite)

Theorem: exec-ident-of-ident-fix-id

(defthm exec-ident-of-ident-fix-id
  (equal (exec-ident (ident-fix id) compst)
         (exec-ident id compst)))

Theorem: exec-ident-ident-equiv-congruence-on-id

(defthm exec-ident-ident-equiv-congruence-on-id
  (implies (ident-equiv id id-equiv)
           (equal (exec-ident id compst)
                  (exec-ident id-equiv compst)))
  :rule-classes :congruence)

Theorem: exec-ident-of-compustate-fix-compst

(defthm exec-ident-of-compustate-fix-compst
  (equal (exec-ident id (compustate-fix compst))
         (exec-ident id compst)))

Theorem: exec-ident-compustate-equiv-congruence-on-compst

(defthm exec-ident-compustate-equiv-congruence-on-compst
  (implies (compustate-equiv compst compst-equiv)
           (equal (exec-ident id compst)
                  (exec-ident id compst-equiv)))
  :rule-classes :congruence)