		Search-engine friendly clone of the ACL2 documentation.

Evaluation

Step

Evaluation step from any state that is not final or error.

Signature
(step estate program) → new-estate
Arguments: estate — Guard (eval-state-p estate).; program — Guard (programp program).
Returns: new-estate — Type (eval-state-p new-estate).

No evaluation step may take place from a final or error state. Instead, an evaluation step may always take place from an initial or transitional state.

Definitions and Theorems

Function: step

(defun step (estate program)
  (declare (xargs :guard (and (eval-state-p estate)
                              (programp program))))
  (declare (xargs :guard (not (member-eq (eval-state-kind estate)
                                         '(:final :error)))))
  (let ((__function__ 'step))
    (declare (ignorable __function__))
    (eval-state-case
         estate
         :init (step-from-init estate.function estate.arguments)
         :trans (step-from-trans estate.stack program)
         :final (prog2$ (impossible)
                        (eval-state-fix estate))
         :error (prog2$ (impossible)
                        (eval-state-fix estate)))))

Theorem: eval-state-p-of-step

(defthm eval-state-p-of-step
  (b* ((new-estate (step estate program)))
    (eval-state-p new-estate))
  :rule-classes :rewrite)

Theorem: step-of-eval-state-fix-estate

(defthm step-of-eval-state-fix-estate
  (equal (step (eval-state-fix estate) program)
         (step estate program)))

Theorem: step-eval-state-equiv-congruence-on-estate

(defthm step-eval-state-equiv-congruence-on-estate
  (implies (eval-state-equiv estate estate-equiv)
           (equal (step estate program)
                  (step estate-equiv program)))
  :rule-classes :congruence)

Theorem: step-of-program-fix-program

(defthm step-of-program-fix-program
  (equal (step estate (program-fix program))
         (step estate program)))

Theorem: step-program-equiv-congruence-on-program

(defthm step-program-equiv-congruence-on-program
  (implies (program-equiv program program-equiv)
           (equal (step estate program)
                  (step estate program-equiv)))
  :rule-classes :congruence)