Support higher-order definitions in the simulator

[konnov]

We have to support higher-order definitions at some point:

>>> def foo(bar, n) = bar(n)
...
TypeError: Cannot read properties of undefined (reading 'length')

It looks like we would need type information for bar, in order to produce the right number of registers in the simulator. This calls for integration with the type checker.

@bugarela, are higher-order operators supported by the type checker already?

[bugarela]

There are no significant blockers (as far as I'm aware) to supporting them on the type checker, but I also didn't test it at all as I was not prioritizing this. I'll try it out on both type and effect checking and get a better sense of where we are at. My intuition is that they should work with some potentital small adjustments.

[bugarela]

Update: at least for this example, it does work in the type checker but not in the effect checker.

1: t1
2: t2
3: ((t1) => t2, t1) => t2
/home/gabriela/projects/tnt/examples/test.tnt:13:21 - error: Signature not found for operator: bar
Trying to infer effect for operator application in bar(n)

13:   def foo(bar, n) = bar(n)
                        ^^^^^^

The third line contains the inferred type for the operator: ((t1) => t2, t1) => t2 (I want to improve the UX of the type inferrer here so this type is shown as something like ∀ a, b . ((a) => b, a) => b.

As for the effect checker, I have to refactor it to use the same context representation as I did later with types, and then it should work. At the moment, it uses different representations for operators and values, and it is looking up bar at the operators map. I believe this change should be enough to fix the issue, I'll do that next.

[konnov]

To support higher-order operators in user definitions, we have to know the parameter types. This requires the refactoring planned in #624.

[konnov]

We can pass user-defined operators in the built-in operators. I don't think it is a high-impact feature actually.

[konnov]

Made some progress in igor/ho-221 and got blocked by #624 this time :)

[shonfeder]

I get the same crash trying to apply a named operator in, e.g., a fold:

node:internal/readline/emitKeypressEvents:74
            throw err;
            ^

TypeError: Cannot read properties of undefined (reading 'length')
    at CompilerVisitor.applyFold (/apalache/quint/quint/dist/src/runtime/impl/compilerImpl.js:736:49)
    at CompilerVisitor.exitApp (/apalache/quint/quint/dist/src/runtime/impl/compilerImpl.js:439:22)
    at walkExpression (/apalache/quint/quint/dist/src/IRVisitor.js:283:25)
    at walkDefinition (/apalache/quint/quint/dist/src/IRVisitor.js:209:13)
    at /apalache/quint/quint/dist/src/runtime/compile.js:93:71
    at Array.forEach (<anonymous>)
    at /apalache/quint/quint/dist/src/runtime/compile.js:93:25
    at Array.forEach (<anonymous>)
    at compile (/apalache/quint/quint/dist/src/runtime/compile.js:91:26)
    at /apalache/quint/quint/dist/src/runtime/compile.js:145:21

i'm wondering if we can make the behavior here, so that, even if hit an unknown unepected corner of the language, repl still doesn't crash?