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.

[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";

[keyboardDrummer]

I think we'd need at least some format instances in Imperative & Lambda

In that case, isn't this PR creating duplication (and thus extra maintenance) for Imperative and Lambda, since for those it needs to define both the ASTToCst code, and the ToFormat instances?

I'll be straightforward: I don't think the DDM is an idiomatic solution to the problem of defining grammars. I think it will always suffer from requiring back and forth CSTToAst and ASTToCST translations, which impacts maintainability and performance, while the alternative of having a grammar library that attaches directly to a Lean type won't. Regarding Ion serialization, I think you can derive that directly from Lean types without needing the DDM or a grammar, and that this leads to more idiomatic types in the connecting applications. For Laurel, the Java interop types that result from the current DDM based serialization are not idiomatic, and I'm planning to replace this with serialization that doesn't rely on the DDM Laurel grammar.

Besides the CSTToAst and ASTToCST issue, another issue I think the DDM has is that it does not allow you to write arbitrary code to do preprocessing before printing. How will you use the DDM to do something like what we're doing here: https://github.com/strata-org/Strata/blob/main/Strata/DL/Lambda/LExpr.lean#L584 ? I think you would have to write a sort of DDM extension.

If the ASTToCST + DDM based printing won't print Lambda expressions as well as the ToFormat instances, should we use it at all?

[keyboardDrummer]

Shouldn't this PR delete most of the ToFormat instances in Language/Core, like the ones for procedure?

[shigoel]

Shouldn't this PR delete most of the ToFormat instances in Language/Core, like the ones for procedure?

I'd like to do that in a separate PR, once this translation has had some miles on it. Also, I suspect we may want to retain some format instances for debugging (e.g., for viewing metadata), but I haven't thought this through entirely yet.

[shigoel]

If the ASTToCST + DDM based printing won't print Lambda expressions as well as the ToFormat instances, should we use it at all?

I have a separate PR coming to print Lambda expressions using the DDM. That'd render the VCs in Core's DDM syntax too.