Add a resolution phase to Laurel

[keyboardDrummer]

Changes

Instead of redefining how to do name resolution in each phase in the translation from Laurel to Core, define resolution once in a single phase. Currently resolution is done again after each phase. This introduced partially duplicated work but we expect to reduce that in the future using caching.

The Python through Laurel pipeline currently can not resolve each reference because it adds some prelude definitions, that are referenced by the generated code, only at the Core level instead of at the Laurel level. To still enable the Python through Laurel pipeline to work, I had to add a few hacks in the code that were less explicit before this PR. In a follow-up PR, I will create a Laurel-level prelude for Python through Laurel, so that we won't need those hacks any more.

For Laurel tests, this PR includes changes to ensure that the program resolves without errors after each phase:

• Datatype support has been improved. References to the type of a datatype now translate to Core correctly. There's now grammar support for datatypes
• The prelude for Laurel is now added during HeapParameterization phase, since that's the phase that depends on these definitions, instead of after the translation to Core.
• The typeTag: TypeTag field of the composite datatype is only added to that datatype during the typeHierarchy phase, since that's the phase where TypeTag is defined.
• const,select and update are now added as part of CoreDefinitionsForLaurel.lean, as Laurel functions with an "External" body, meaning they're ignored during the translation to Core. This way, references to them can be resolved during resolution.
• During HeapParameterization, fields for composite type definitions are deleted, so their names don't conflict with the constructors of the generated Field datatype
• Small refactoring to simplify the definition of Forall and Exists, by reusing the Parameter type.

Misc:

• Reduce output when panics occur by using a softPanic that does not print the stacktrace.

Testing