adding length to FunAsSeq

[konnov]

After discussing FunAsSeq in #1442, I have added another parameter to this operator:

(**
 * As TLA+ is untyped, one can use function- and sequence-specific operators
 * interchangeably. However, to maintain correctness w.r.t. our type-system,
 * an explicit cast is needed when using functions as sequences.
 *
 * The parameters have the following meaning:
 *
 *  - fn is the function from 1..len that should be interpreted as a sequence.
 *  - len is the length of the sequence, len = Cardinality(DOMAIN fn),
 *    len may be a variable, a computable expression, etc.
 *  - capacity is a static upper bound on the length, that is, len <= capacity.
 *
 * @type: ((Int -> a), Int, Int) => Seq(a);
 *)
FunAsSeq(fn, len, capacity) ==
    LET __FunAsSeq_elem_ctor(i) == fn[i] IN
    SubSeq(MkSeq(capacity, __FunAsSeq_elem_ctor), 1, len)

This new form lets the user to specify the actual length of the sequence, which may be unknown in advance, while providing the tool with a statically known bound.

• 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

❗ No coverage uploaded for pull request base (unstable@386c1c8). Click here to learn what that means.
The diff coverage is n/a.

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

@@             Coverage Diff             @@
##             unstable    #1450   +/-   ##
===========================================
  Coverage            ?   74.58%           
===========================================
  Files               ?      359           
  Lines               ?    11440           
  Branches            ?      546           
===========================================
  Hits                ?     8533           
  Misses              ?     2907           
  Partials            ?        0           

Impacted Files	Coverage Δ
...t/forsyte/apalache/tla/bmcmt/rules/MkSeqRule.scala	68.96% <ø> (ø)

---

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 386c1c8...2aa752d. Read the comment docs.

[konnov]

@Kukovec, what do you think?

[Kukovec]

LGTM, assuming we're happy with the current error message for "constant" LET-INs