		Search-engine friendly clone of the ACL2 documentation.

Dynamic-semantics

Exec-path

Execute a path.

Signature
(exec-path path cstate) → outcome
Arguments: path — Guard (pathp path).; cstate — Guard (cstatep cstate).
Returns: outcome — Type (eoutcome-resultp outcome).

We look up the variable in the computation state. This always returns a single value, and does not change the computation state.

Definitions and Theorems

Function: exec-path

(defun exec-path (path cstate)
  (declare (xargs :guard (and (pathp path) (cstatep cstate))))
  (let ((__function__ 'exec-path))
    (declare (ignorable __function__))
    (b* (((okf var) (path-to-var path))
         ((okf val) (read-var-value var cstate)))
      (make-eoutcome :cstate cstate
                     :values (list val)))))

Theorem: eoutcome-resultp-of-exec-path

(defthm eoutcome-resultp-of-exec-path
  (b* ((outcome (exec-path path cstate)))
    (eoutcome-resultp outcome))
  :rule-classes :rewrite)

Theorem: error-info-wfp-of-exec-path

(defthm error-info-wfp-of-exec-path
  (b* ((?outcome (exec-path path cstate)))
    (implies (reserrp outcome)
             (error-info-wfp outcome))))

Theorem: exec-path-of-path-fix-path

(defthm exec-path-of-path-fix-path
  (equal (exec-path (path-fix path) cstate)
         (exec-path path cstate)))

Theorem: exec-path-path-equiv-congruence-on-path

(defthm exec-path-path-equiv-congruence-on-path
  (implies (path-equiv path path-equiv)
           (equal (exec-path path cstate)
                  (exec-path path-equiv cstate)))
  :rule-classes :congruence)

Theorem: exec-path-of-cstate-fix-cstate

(defthm exec-path-of-cstate-fix-cstate
  (equal (exec-path path (cstate-fix cstate))
         (exec-path path cstate)))

Theorem: exec-path-cstate-equiv-congruence-on-cstate

(defthm exec-path-cstate-equiv-congruence-on-cstate
  (implies (cstate-equiv cstate cstate-equiv)
           (equal (exec-path path cstate)
                  (exec-path path cstate-equiv)))
  :rule-classes :congruence)