PI-week: Refactor Transpile

[Kukovec]

• Tests added for any new code
• Ran make fmt-fix (or had formatting run automatically on all files edited)
• Documentation added for any new functionality
• Entries added to ./unreleased/ for any new functionality

This PR attempts to change the way the internal transpilation is performed, and, to a lesser extent, the SMT term representation.

The main issue is, that SMT separates two concepts: terms, and declarations/definitions. In an effort to make the transpilation "side-effect free", FunDef was introduced as a Term, which represented a function, to be defined in the SMT header, but used (by name) wherever FunDef appeared in the syntax tree. Later, a Collector would traverse the tree again, and extract the function definitions, along with any uninterpreted literals, which also needed to be declared.
This is clunky, and does not scale with extensions to Terms. Instead, the new approach introduces rules as State computations over a class which holds SMT declarations. This way, rules conceptually still translate TLA to SMT terms directly, but the internal declarations class keeps track of any declarations or definitions, which need to be introduced along the way.

The PR also includes minor QoL changes, such as replacing case classes without parameters with case objects, and standardizing the use of Seq (instead of a mix of Seq and List).

[codecov-commenter]

Codecov Report

Merging #2720 (462b034) into main (72e0965) will increase coverage by 0.33%.
The diff coverage is 53.96%.

❗ Current head 462b034 differs from pull request most recent head 95b61e8. Consider uploading reports for the commit 95b61e8 to get more accurate results

@@            Coverage Diff             @@
##             main    #2720      +/-   ##
==========================================
+ Coverage   78.55%   78.89%   +0.33%     
==========================================
  Files         463      463              
  Lines       15904    15870      -34     
  Branches     2563     2572       +9     
==========================================
+ Hits        12493    12520      +27     
+ Misses       3411     3350      -61     

Files Changed	Coverage Δ
...apalache/tla/bmcmt/rules/vmt/TermToVMTWriter.scala	0.00% <0.00%> (ø)
...palache/tla/bmcmt/rules/vmt/TlaExToVMTWriter.scala	0.00% <0.00%> (ø)
...lache/tla/bmcmt/rules/vmt/ToTermRewriterImpl.scala	90.00% <ø> (ø)
...forsyte/apalache/tla/bmcmt/rules/vmt/VMTExpr.scala	0.00% <0.00%> (ø)
...la/at/forsyte/apalache/tla/lir/formulas/Base.scala	0.00% <ø> (ø)
...t/forsyte/apalache/tla/lir/formulas/Integers.scala	0.00% <0.00%> (-100.00%)	⬇️
...forsyte/apalache/tla/bmcmt/rules/vmt/EUFRule.scala	53.12% <47.05%> (+19.79%)	⬆️
...orsyte/apalache/tla/bmcmt/rules/vmt/BoolRule.scala	69.23% <63.63%> (-8.55%)	⬇️
...rsyte/apalache/tla/bmcmt/rules/vmt/ValueRule.scala	77.27% <75.00%> (+1.08%)	⬆️
...ala/at/forsyte/apalache/tla/lir/formulas/EUF.scala	89.47% <83.33%> (-3.86%)	⬇️
... and 5 more

... and 3 files with indirect coverage changes

📣 We’re building smart automated test selection to slash your CI/CD build times. Learn more

📢 Have feedback on the report? Share it here.

[konnov]

Looks good!

[rodrigo7491]

Thanks for the changes @Kukovec!