The unsafe builder leverages native scala objects, and is not susceptible to stack-depth issues, unlike the State-based builder.
The changes introduced are as follows:
ScopeUnsafeBuilder is added as an analogue to ScopedBuilder, from existing unsafe builder components
Unsafe components have been changed to trait from class to facilitate inheritance
Constructors for typed operator parameters have been separated out and are reused across both builders
tlaU is added as a convenience instance, analogous to at.forsyte.apalache.tla.types.tla
BuilderUT and BuilderT have been added to the convenience imports, representing TlaEx and TBuilderInstruction respectively. All instances of TBuilderInstruction have been replaced with BuilderT
In oreder to avoid even more refactoring, imports of the scoped builder, at.forsyte.apalache.tla.types.tla have been systematically replaced with at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}.
Places where map was used over BuilderT (e.g. _.map(simplifier.simplifyShallow)) have been replaced with abstract methods (e.g. applySimplifyShallowToBuilderEx), overloaded for BuilderT and BuilderUT.
No rule or data structure semantics have been modified.
make fmt-fix
(or had formatting run automatically on all files edited)./unreleased/
for any new functionalityThe unsafe builder leverages native scala objects, and is not susceptible to stack-depth issues, unlike the
State
-based builder.The changes introduced are as follows:
ScopeUnsafeBuilder
is added as an analogue toScopedBuilder
, from existing unsafe builder componentstrait
fromclass
to facilitate inheritancetlaU
is added as a convenience instance, analogous toat.forsyte.apalache.tla.types.tla
BuilderUT
andBuilderT
have been added to the convenience imports, representingTlaEx
andTBuilderInstruction
respectively. All instances ofTBuilderInstruction
have been replaced withBuilderT
at.forsyte.apalache.tla.types.tla
have been systematically replaced withat.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
.map
was used overBuilderT
(e.g._.map(simplifier.simplifyShallow)
) have been replaced with abstract methods (e.g.applySimplifyShallowToBuilderEx
), overloaded forBuilderT
andBuilderUT
.No rule or data structure semantics have been modified.