search

epfl-lara / inox

Solver for higher-order functional programs, used by Stainless
Apache License 2.0
88 stars 20 forks source link

Key not found error when using --debug=tip from Stainless #148

Closed jad-hamza closed 3 years ago

jad-hamza commented 3 years ago

The error arises here: https://github.com/epfl-lara/inox/blob/775294883f9037ed4e67651786c621d467a66255/src/main/scala/inox/tip/Printer.scala#L164 on a tuple of two elements, while the tuples map is empty.

I guess declareStructuralSort isn't called on that Tuple beforehand. The Stainless example (I can minimize and post the example if needed) contains an ADT with two type parameters and an array of pairs inside MyADT[A, B](a: Array[(A, B)], ...).

samarion commented 3 years ago

It seems like we don't deal with tuple types inside ADTs correctly.

You can probably fix this by extracting the tuple type caching logic here into a getGenericTupleType method and using it inside both declareStructuralSort and declareDatatypes.

samarion commented 3 years ago

@jad-hamza IIRC you fixed this already, right?

jad-hamza commented 3 years ago

Yes, thanks!