Use reader-monad bracketing combinators for extending bound variable environment in translator #1254
Labels
subsystem: saw-core-coq
Issues related to converting saw-core to Gallina for use with the Coq/Rocq theorem prover
tech debt
Issues that document or involve technical debt
Currently the term translation monad is just a state monad, and the local variable environment is just one of the fields in the mutable monad state, which can be updated at any time. As @eddywestbrook suggests in the comment thread of GaloisInc/saw-core-coq#29, it would be more principled to use reader-monad-style operations to manage the local variable environment. Following this discipline will make the code easier to understand and make errors easier to avoid.
So instead of
we should use only bracketing combinators like
that explicitly delimit the scope of the
Ident
that is added to the local environment.The text was updated successfully, but these errors were encountered: