[FEATURE] CHOOSE over sets of functions of functions

[konnov]

This discussion shows an example of using CHOOSE for defining a hash function.

Here is an MWE:

--------------- MODULE TestHash --------------                                   
EXTENDS Integers

BitString == [1..6 -> {0,1}]

AllowedStrings == {"a", "b", "c", "d", "e"}

\* @type: (Str -> (Int -> Int)) => Bool;
IsInjective(f) ==
    \A a,b \in DOMAIN f : f[a] = f[b] => a = b

hash ==
    CHOOSE i \in [AllowedStrings -> BitString]:
        IsInjective(i)

Init == TRUE

Next == TRUE

Inv == hash["a"] /= hash["b"]
==============================================

Apalache fails when rewriting the filter expression:

apalache-mc check --inv=Inv TestHash.tla
...
State 0: Checking 1 state invariants                              I@08:42:24.563
(Please report an issue at: [https://github.com/informalsystems/apalache/issues],scala.NotImplementedError: A set filter over FinFunSet[FinSet[str], FinFunSet[FinSet[Int], FinSet[Int]]] is not implemented)
Unhandled exception                                               E@08:42:24.581
scala.NotImplementedError: A set filter over FinFunSet[FinSet[str], FinFunSet[FinSet[Int], FinSet[Int]]] is not implemented
	at at.forsyte.apalache.tla.bmcmt.rules.SetFilterRule.apply(SetFilterRule.scala:32)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:336)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive$1(SymbStateRewriterImpl.scala:368)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:402)
	at at.forsyte.apalache.tla.bmcmt.rules.ChooseRule.apply(ChooseRule.scala:45)
...

At least, we should produce an error message that this feature is not supported yet.

[thpani]

Related: #2762