You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Certain functions get translated into "stateful" operations in macaw, e.g. write_mem or gpr_set. During normalization, functions are split into a distinct function representing each (sub)-field of its result type. This splitting is sound from a functional interpretation, but can introduce duplicate expressions if they are shared in the computation of each out put.
When these "stateful" function are duplicated, however, the resulting action occurs multiple times, and also is not necessary evaluated in the correct order.
This indicates that some structs should be retained in the normalized spec, which are exclusively used to manage the control flow of stateful operations. These don't require a logical representation in the expressions outputted by macaw, but instead would be translated into haskell-level tuples.
The text was updated successfully, but these errors were encountered:
Certain functions get translated into "stateful" operations in macaw, e.g.
write_mem
orgpr_set
. During normalization, functions are split into a distinct function representing each (sub)-field of its result type. This splitting is sound from a functional interpretation, but can introduce duplicate expressions if they are shared in the computation of each out put.When these "stateful" function are duplicated, however, the resulting action occurs multiple times, and also is not necessary evaluated in the correct order.
This indicates that some structs should be retained in the normalized spec, which are exclusively used to manage the control flow of stateful operations. These don't require a logical representation in the expressions outputted by macaw, but instead would be translated into haskell-level tuples.
The text was updated successfully, but these errors were encountered: