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 introduces 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 turn off reporting of resolution errors. I'll resolve that in a follow-up PR.

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

• Fix issue in DDM parsing caused by Lean.Name.toString inserting guillemets "« »"
• 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.

Testing

Refactoring. No changes to existing tests. I will follow-up with first removing the hacks, and then adding tests containing name conflicts that'll make use of this new resolution phase.

[joscoh]

Do you have any tests for these changes (e.g. ensuring resolution works, Laurel programs with datatypes)?