Support for FunAsSeq

[konnov]

Closes #569. Instead of translating FunAsSeq to SMT, we are simply using its TLA+ definition via MkSeq.

• 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
• Entry added to UNRELEASED.md for any new functionality

[codecov-commenter]

Codecov Report

Merging #1442 (ffa7048) into unstable (830fa65) will decrease coverage by 0.02%.
The diff coverage is 0.00%.

❗ Current head ffa7048 differs from pull request most recent head ee186df. Consider uploading reports for the commit ee186df to get more accurate results

@@             Coverage Diff              @@
##           unstable    #1442      +/-   ##
============================================
- Coverage     74.57%   74.54%   -0.03%     
============================================
  Files           360      360              
  Lines         11437    11430       -7     
  Branches        552      541      -11     
============================================
- Hits           8529     8521       -8     
- Misses         2908     2909       +1     

Impacted Files	Coverage Δ
.../at/forsyte/apalache/tla/imp/StandardLibrary.scala	100.00% <ø> (ø)
...forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala	93.36% <ø> (-0.06%)	⬇️
...in/scala/at/forsyte/apalache/tla/lir/Builder.scala	99.08% <ø> (-0.01%)	⬇️
...t/forsyte/apalache/tla/lir/oper/ApalacheOper.scala	66.07% <0.00%> (-6.66%)	⬇️
...syte/apalache/tla/pp/SetMembershipSimplifier.scala	100.00% <0.00%> (ø)
...he/io/annotations/parser/CommentPreprocessor.scala	93.97% <0.00%> (+1.20%)	⬆️
...at/forsyte/apalache/tla/pp/InlinerOfUserOper.scala	97.77% <0.00%> (+4.16%)	⬆️

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 830fa65...ee186df. Read the comment docs.

[Kukovec]

Looks fine, but I wonder if we couldn't change the interface of FunAsSeq(fn, maxSeqLen) to FunAsSeq(fn) instead, and just compute maxSeqLen == FoldSet(MaxOf2, 0, DOMAIN fn) (at the cost of performance)

[Kukovec]

Why not just delete the object, if you're going to add require(false)?

[konnov]

I also wanted to delete the object. But it is better to keep it as documentation.

[konnov]

Looks fine, but I wonder if we couldn't change the interface of FunAsSeq(fn, maxSeqLen) to FunAsSeq(fn) instead, and just compute maxSeqLen == FoldSet(MaxOf2, 0, DOMAIN fn) (at the cost of performance)

That would not help us, as MkSeq requires a constant length.

[konnov]

However, we should think further. Maybe there is a way to implement FunAsSeq without passing constant length directly.