		Search-engine friendly clone of the ACL2 documentation.

Evaluation

Step*

Attempt to exhaustively perform execution steps from a state.

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

If the state is terminating, then we return either the final result or an error outcome. If the state is nonterminating, we return the nonterminating outcome.

This function is not executable.

Definitions and Theorems

Function: step*

(defun step* (estate program)
 (declare (xargs :guard (and (eval-state-p estate)
                             (programp program))))
 (let ((__function__ 'step*))
   (declare (ignorable __function__))
   (if
     (terminatingp estate program)
     (b* ((end-estate (stepn estate
                             (terminatingp-witness estate program)
                             program)))
       (eval-state-case
            end-estate
            :init (prog2$ (impossible)
                          (ec-call (exec-outcome-fix :irrelevant)))
            :trans (prog2$ (impossible)
                           (ec-call (exec-outcome-fix :irrelevant)))
            :final (exec-outcome-terminating end-estate.result)
            :error (exec-outcome-error)))
     (exec-outcome-nonterminating))))

Theorem: exec-outcome-p-of-step*

(defthm exec-outcome-p-of-step*
  (b* ((outcome (step* estate program)))
    (exec-outcome-p outcome))
  :rule-classes :rewrite)