		Search-engine friendly clone of the ACL2 documentation.

Interpreter

Interpret-loop

Exhaustively apply step to an evaluation state.

Signature
(interpret-loop estate program) → value?
Arguments: estate — Guard (eval-state-p estate).; program — Guard (programp program).
Returns: value? — A value-optionp.

We stop when we reach a final state or an error state. In the first case, we return the value in the final state. In the second case, we return nil. Or we may not terminate.

This is a program-mode executable counterpart of the logic-mode non-executable function step*.

Definitions and Theorems

Function: interpret-loop

(defun interpret-loop (estate program)
  (declare (xargs :guard (and (eval-state-p estate)
                              (programp program))))
  (let ((__function__ 'interpret-loop))
    (declare (ignorable __function__))
    (eval-state-case estate
                     :init (interpret-loop (step estate program)
                                           program)
                     :trans (interpret-loop (step estate program)
                                            program)
                     :final estate.result
                     :error nil)))