|
|
|---|
|
|
|
|---|
Execute an expression.
(exec-expression expr env limit) → evalue+denv
We use separate ACL2 functions for variables and constants, and for literals.
For unary and binary expressions, first we execute the operand(s). For binary expressions, we execute them from left to right, threading through the environment. We propagate errors from the operand(s). We use separate ACL2 functions to calculate the final result.
For a conditional expression, we first execute the test, which must return a boolean. If the boolean is true, we execute the `then' branch; if the boolean is false, we execute the `else' branch.
For a tuple expression, we first evaluate the sub-expressions, then put them together into a tuple value.
For a tuple component expression, we first evaluate the sub-expression. If the result is a location, we return a location for the component. If the result is a value, we ensure that it is a tuple value, and we return the component value (if the index is in range).
For a struct expression, we evaluate its components, and we create a struct value from them.
For a struct component expression, we first evaluate the sub-expression. If the result is a location, we return a location for the component. If the result is a value, we ensure that it is a struct value, and we return the component value (if the component is among the declared ones for the struct type).
For a fucntion call, we first evaluate the argument expressions. Then we call a separate ACL2 function to handle the call.