		Search-engine friendly clone of the ACL2 documentation.

Interpreter

Interpret

Exhaustively execute a function call.

Signature
(interpret function arguments program) → value?
Arguments: function — Guard (symbol-valuep function).; arguments — Guard (value-listp arguments).; program — Guard (programp program).
Returns: value? — A value-optionp.

This is a program-mode executable counterpart of the logic-mode non-executable function exec-call. It is a possibly non-terminating interpreter.

Definitions and Theorems

Function: interpret

(defun interpret (function arguments program)
       (declare (xargs :guard (and (symbol-valuep function)
                                   (value-listp arguments)
                                   (programp program))))
       (let ((__function__ 'interpret))
            (declare (ignorable __function__))
            (interpret-loop (eval-state-init function arguments)
                            program)))