|
|
|---|
|
|
|
|---|
Flatten a statement.
(flatten-statement stmt env) → new-stmt
For a variable declaration, we flatten the initializer. The variable declaration remains, even if the initializer is a constant expression: here we only propagate actual constants, not also variables that happen to have a constant value. The latter kind of transformation will be handled separately.
Constant declarations are handled not here but in the ACL2 function to flatten lists of statements. The reason is that constant declarations are incorporated into the flattening environments and removed; the removal does not produce any statement in that place. Because of that, the code in this ACL2 function for the constant declaration case should be unreachable.
For an assignment, we flatten the left-hand side and the right-hand side. In the current version of Leo flattening the left-hand side has no effect in type-correct code, where the left-hand side is always a variable.
For a return statement, we flatten the expression.
For now we reject loop statements, because we only do constant propagation and unfolding. We will do loop unrolling later.
Conditional statements are flattened in two phases. The first phase, carried out in these ACL2 functions here, homomorphically flattens their constituents. The second phase, carried out in simplify-flattened-if, simplifies the resulting constituents.
For a console statement, we transform its arguments.
For a block, we flatten its statements.