		Search-engine friendly clone of the ACL2 documentation.

Interpreter

Exec

Program-mode interpreter for Imp.

Signature
(exec cfg) → *
Arguments: cfg — Guard (configp cfg).

If the configuration has no commands, we return the final environment. Otherwise, we step the configuration and we recursively call the interprete.

Definitions and Theorems

Function: exec

(defun exec (cfg)
       (declare (xargs :guard (configp cfg)))
       (if (consp (config->comms cfg))
           (exec (step cfg))
           (config->env cfg)))