		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)))