Skip to content

Make pretty-printed core more readable#1237

Merged
b-studios merged 11 commits into
masterfrom
improve-core-pretty
Dec 16, 2025
Merged

Make pretty-printed core more readable#1237
b-studios merged 11 commits into
masterfrom
improve-core-pretty

Conversation

@timsueberkrueb

@timsueberkrueb timsueberkrueb commented Dec 1, 2025

Copy link
Copy Markdown
Contributor

In #1181 we made the core pretty printer a lot more verbose in order to enable re-parsing. However, the additional verbosity hinders human inspection and debugging. This PR aims to mitigate this by splitting the core pretty printer in two instances:

  • ReparsablePrettyPrinter is fully verbose and can be re-parsed with core.Parser
  • HumanReadablePrettyPrinter is less verbose (and thus more readable) but cannot be re-parsed

// For many purposes, we would like to include the user-annotated name in the fresh id,
// so that printed terms are more readable.
// However, we do not want to include it when checking for alpha-equivalence in tests.
val userPart = if preserveUserAnnotatedPrefix then userName else ""

@timsueberkrueb timsueberkrueb Dec 1, 2025

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We can probably get rid of this by moving the userName logic to idFor. We need to be careful with this, though, as idFor is also used by core.Parser.

@timsueberkrueb timsueberkrueb changed the title WIP: Make pretty-printed core more readable Make pretty-printed core more readable Dec 1, 2025
Comment thread effekt/shared/src/main/scala/effekt/core/PrettyPrinter.scala Outdated
@timsueberkrueb timsueberkrueb marked this pull request as ready for review December 1, 2025 14:40
@marvinborner

Copy link
Copy Markdown
Member

You may want to use --debug instead of --detailed-ir, as we do for more debug information in the LLVM IR.

@timsueberkrueb

timsueberkrueb commented Dec 9, 2025

Copy link
Copy Markdown
Contributor Author

Also remove some of the captures currently printed by default. It would also be good to highlight get and put as keywords in the VSCode plugin.

@timsueberkrueb

Copy link
Copy Markdown
Contributor Author

Corresponding VSCode extension PR: effekt-lang/effekt-vscode#163

@jiribenes

Copy link
Copy Markdown
Contributor

Q from the meeting: does util.show(...) show the ID in addition to the string?

@timsueberkrueb

Copy link
Copy Markdown
Contributor Author

I just checked: it always prints some ids:

  • If --debug is not set, it prints the Barendregt ids actually used internally in the compiler
  • If --debug is set, it runs in the reparsable mode (printDetailed, currently conflated with the debug mode) and prints a deterministic id starting from zero.
  def toDoc(s: symbols.Symbol): Doc = {
    // In human-readable mode, we show the name together with the actual Barendregt id.
    // This allows the user to connect the symbol to the internal representation when debugging.
    // In reparsable mode, we just show the string part, which should be freshened by the TestRenamer before printing.
    // The TestRenamer does not rename the Barendregt id because that would violate the internal invariant of having
    // just a single global Barendregt namespace.
    builtins.coreBuiltinSymbolToString(s).getOrElse(if printDetails then s.name.name else s.show)
  }

I can change this behavior to always print the internal Barendregt ids except when deterministic ids are needed for test cases.

@b-studios b-studios merged commit dd7a9f1 into master Dec 16, 2025
8 checks passed
@b-studios b-studios deleted the improve-core-pretty branch December 16, 2025 16:13
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants