Pretty printer for Core's semantic AST

[shigoel]

Description of changes:

Translation from Core's AST to DDM's CST (generated using #strata_gen) for pretty-printing Core constructs.

New Files
Translator: Strata/Languages/Core/DDMTransform/ASTtoCST.lean
Tests: StrataTest/Languages/Core/TestASTtoCST.lean

NOTE: DDM's type variable printing using mformat has been changed from tvar!<n> to just <n>.

Revamping the existing translator in Strata/Languages/Core/DDMTransform/Translate.lean to use DDM's #strata_gen'd AST is out of scope for this PR.

Known issues

• Constructs unsupported in this PR (coming soon):
  -- Sub-functions (functions defined inside procedures)

• We generate some bound variables' names during translation because the semantic AST currently does not preserve them (e.g., bvars in quantifiers). We can log the identifier names during CST -> AST translation in the latter's metadata field and recover them in the future.

• Misc. formatting issues
  -- Remove extra parentheses around constructors in datatypes, assignments, etc.
  -- Remove extra indentation from the last brace of a block and the end keyword of a mutual block.

(NOTE: a large bulk of this PR was created using Claude)

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[keyboardDrummer]

The implementation looks good, but if I understand correctly, most of the codebase will still use the existing ToFormat definitions for printing Core code.

Shouldn't this PR remove those ToFormat definitions and replace all usage of them with this DDM based approach, so that we don't have to maintain both ASTToCST.lean and the format definitions?

[shigoel]

The implementation looks good, but if I understand correctly, most of the codebase will still use the existing ToFormat definitions for printing Core code.

Shouldn't this PR remove those ToFormat definitions and replace all usage of them with this DDM based approach, so that we don't have to maintain both ASTToCST.lean and the format definitions?

I think we'd need at least some format instances in Imperative & Lambda, but you're right, we shouldn't need to maintain Core-specific instances. I'll try removing Core-specific instances with this implementation.

[shigoel]

@keyboardDrummer Changed the default format instance for Core programs, as requested.

[joehendrix]

Grammar.lean:194 — Spurious parens on assignment LHS (e.g., (y) := x). v inherits maxPrec which triggers parenthesization.

Suggested fix:

op assign (tp : Type, v : Lhs, e : tp) : Statement => v:0 " := " e ";\n";