I believe lambox' evaluation strategy is strict by default.
However in the AST there are two nodes for lazy and force:
https://github.com/MetaCoq/metacoq/blob/1d9755adac8bf50d884c75236f7b860ffc0114a5/erasure/theories/EAst.v#L44-L45
We may want to compile some things lazily. Not everything, as this would introduce too much overhead, but for example, stdlib's if_then_else_ should definitely be compiled to lazy branches, so that only one of them gets evaluated.
Alternatively, if_then_else_ compiles to a case on the boolean, so if it is marked as INLINE then no problem, but it isn't, and lambox call-by-value semantics means both branches would get evaluated when calling if_then_else_.
I believe lambox' evaluation strategy is strict by default.
However in the AST there are two nodes for lazy and force:
https://github.com/MetaCoq/metacoq/blob/1d9755adac8bf50d884c75236f7b860ffc0114a5/erasure/theories/EAst.v#L44-L45
We may want to compile some things lazily. Not everything, as this would introduce too much overhead, but for example, stdlib's
if_then_else_should definitely be compiled to lazy branches, so that only one of them gets evaluated.Alternatively,
if_then_else_compiles to a case on the boolean, so if it is marked asINLINEthen no problem, but it isn't, and lambox call-by-value semantics means both branches would get evaluated when callingif_then_else_.