Python Prelude in Laurel

[keyboardDrummer]

Changes

• Improve support for datatypes in Laurel
• In the Python through Laurel pipeline, replace the use of CorePrelude.lean with PythonPreludeInLaurel.lean

Caveat, there is still a CorePreludeForLaurel.lean file as well. This is needed to hold axioms that Python requires in Core. Laurel does not support axioms so using a separate Core file is a good workaround. A long term solution would be that the Python pipeline stops relying on axioms.

Caveat2, because DDM parsing also does a form of resolution, CorePreludeForLaurel.lean needs a lot of type definitions that are already provided in PythonPreludeInLaurel.lean. Ideally we'd find a way so that's no longer necessary, using something like #strata_parsing_only

Caveat3, two procedures have been left in CorePreludeForLaurel.lean because their contracts contain labelled requires/ensures and Laurel does not support that. I'm not sure whether we should add support for that. I think this can be made obsolete by having traces for failed assertions.

Tested

• Added T16_Datatypes.lean test for Laurel datatypes
• Updated Python expect files for Laurel because the reported locations are different

[thanhnguyen-aws]

We will use the "PythonLaurelCorePrelude" in this PR #489 for Python-> Laurel translation instead of the "CorePrelude".

[keyboardDrummer]

We will use the "PythonLaurelCorePrelude" in this PR #489 for Python-> Laurel translation instead of the "CorePrelude".

Yes, this PR conflicts with that one, but I think that's OK we can resolve the conflicts. I don't mind resolving them in whatever PR gets merged last.