Fix uninterpreted functions in keys of Maps and Sets

[ttuegel]

Fixes #2012.

• Introduce type Kore.Internal.Key.Key, which represents concrete patterns used as keys in maps and sets.
• Only allow Key to be constructed from TermLike which are constructor-like.
• The assertion about non-constructor-like keys in maps and sets is removed because the change to a Key type makes that branch of code dead.

---

Review checklist

The author performs the actions on the checklist. The reviewer evaluates the work and checks the boxes as they are completed.

• Summary. Write a summary of the changes. Explain what you did to fix the issue, and why you did it. Present the changes in a logical order. Instead of writing a summary in the pull request, you may push a clean Git history.
• Documentation. Write documentation for new functions. Update documentation for functions that changed, or complete documentation where it is missing.
• Tests. Write unit tests for every change. Write the unit tests that were missing before the changes. Include any examples from the reported issue as integration tests.
• Clean up. The changes are already clean. Clean up anything near the changes that you noticed while working. This does not mean only spatially near the changes, but logically near: any code that interacts with the changes!

[ttuegel]

I still need to fix up the unit tests, but I was able to test this against the C semantics. I can execute beyond the error about uninterpreted functions (which can't be thrown anymore, anyway). However, I discovered that the C semantics also requires using Set in the keys of Map, so I will have to add support for that.

[ana-pantilie]

I left a few minor suggestions, and I have some questions about the integration tests.

[ana-pantilie]

Why did the simplified attribute change here? (Here and in other places in the output.)

Edit: I think the reason is that now these patterns are considered constructor-like, but I'll leave this comment here in case I'm wrong.

[ttuegel]

Yes, it's because built-in lists are now considered constructor-like.

[ana-pantilie]

Why are the attribute comments missing? (Here and in other places in the expected output.)

[ttuegel]

This is a Key, so the Unparse instance isn't going through TermLike (which is what creates the comments). The comments aren't necessary because all Key are functional constructor-like patterns.

[MirceaS]

why did we get rid of HasCallStack?

[ttuegel]

This function doesn't throw errors anymore.