		Search-engine friendly clone of the ACL2 documentation.

Dynamic-semantics

Exec-literal

Execute a literal.

Signature
(exec-literal lit cstate) → outcome
Arguments: lit — Guard (literalp lit).; cstate — Guard (cstatep cstate).
Returns: outcome — Type (eoutcome-resultp outcome).

Executing a literal returns a single value and does not change the computation state.

Definitions and Theorems

Function: exec-literal

(defun exec-literal (lit cstate)
  (declare (xargs :guard (and (literalp lit) (cstatep cstate))))
  (let ((__function__ 'exec-literal))
    (declare (ignorable __function__))
    (b* (((okf val) (eval-literal lit)))
      (make-eoutcome :cstate cstate
                     :values (list val)))))

Theorem: eoutcome-resultp-of-exec-literal

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

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

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

Theorem: exec-literal-of-literal-fix-lit

(defthm exec-literal-of-literal-fix-lit
  (equal (exec-literal (literal-fix lit) cstate)
         (exec-literal lit cstate)))

Theorem: exec-literal-literal-equiv-congruence-on-lit

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

Theorem: exec-literal-of-cstate-fix-cstate

(defthm exec-literal-of-cstate-fix-cstate
  (equal (exec-literal lit (cstate-fix cstate))
         (exec-literal lit cstate)))

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

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