quint icon indicating copy to clipboard operation
quint copied to clipboard

Name resolution in the simulator fails on builtin operators used at higher order

Open shonfeder opened this issue 1 year ago • 1 comments

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.

shonfeder avatar Jan 12 '24 02:01 shonfeder

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

bugarela avatar Jan 12 '24 12:01 bugarela