quint
quint copied to clipboard
Name resolution in the simulator fails on builtin operators used at higher order
iadd
is the builtin for addition:
>>> iadd(1,1)
2
But if we try to supply it to a 2nd order operator, name resolution fails:
>>> def f(g) = g(1, 1)
>>> f(iadd)
compile error: error: [QNT502] Name iadd not found
f(iadd)
^^^^
This occurs in both the REPL and when running tests, but parsing and typechecking works as expected.
After a quick investigation, I see that the problem is that we only define what do to with builtin operators in the evaluation process when visiting an operator application. In this case, the operator is a name expression.
I believe the solution will be to move the builtin operator definitions from the switch statement inside exitApp
to the actual context, so it is retrieved in exitName
like the user operators
https://github.com/informalsystems/quint/blob/b806f4081276867df4ce06b485ec51125e65678e/quint/src/runtime/impl/compilerImpl.ts#L429-L990