Make pretty-printed core more readable

effekt/js/src/main/scala/effekt/EffektConfig.scala

@@ -39,4 +39,6 @@ trait EffektConfig {
   def timed() = false
 
   def debug() = false
+
+  def printDetailedIR(): Boolean = false
 }

effekt/jvm/src/main/scala/effekt/EffektConfig.scala

@@ -164,6 +164,15 @@ class EffektConfig(args: Seq[String]) extends REPLConfig(args.takeWhile(_ != "--
     group = debugging
   )
 
+  val detailedIR: ScallopOption[Boolean] = toggle(
+    "detailed-ir",
+    descrYes = "Print detailed IR with all annotations",
+    default = Some(false),
+    noshort = true,
+    prefix = "no-",
+    group = debugging
+  )
+
   val showDocumentation: ScallopOption[Boolean] = toggle(
     "show-documentation",
     descrYes = "Show all documented statements as a JSON",
@@ -263,6 +272,8 @@ class EffektConfig(args: Seq[String]) extends REPLConfig(args.takeWhile(_ != "--
 
   def timed(): Boolean = time.isSupplied && !server()
 
+  def printDetailedIR(): Boolean = detailedIR()
+
   validateFilesIsDirectory(includePath)
 
   // force some other configs manually to initialize them when compiling with native-image

effekt/jvm/src/test/scala/effekt/core/CoreTests.scala

@@ -19,11 +19,11 @@ trait CoreTests extends munit.FunSuite {
         |=====================
         |Got:
         |----
-        |${effekt.core.PrettyPrinter.format(obtained).layout}
+        |${effekt.core.ReparsablePrettyPrinter.format(obtained).layout}
         |
         |Expected:
         |---------
-        |${effekt.core.PrettyPrinter.format(expected).layout}
+        |${effekt.core.ReparsablePrettyPrinter.format(expected).layout}
         |
         |""".stripMargin
     })
@@ -34,11 +34,11 @@ trait CoreTests extends munit.FunSuite {
         |=====================
         |Got:
         |----
-        |${effekt.core.PrettyPrinter.format(obtained)}
+        |${effekt.core.ReparsablePrettyPrinter.format(obtained)}
         |
         |Expected:
         |---------
-        |${effekt.core.PrettyPrinter.format(expected)}
+        |${effekt.core.ReparsablePrettyPrinter.format(expected)}
         |
         |""".stripMargin
     })
@@ -47,19 +47,19 @@ trait CoreTests extends munit.FunSuite {
                             expected: ModuleDecl,
                             clue: => Any = "values are not alpha-equivalent",
                             names: Names = Names(defaultNames))(using Location): Unit = {
-    val renamer = TestRenamer(names)
+    val renamer = TestRenamer(names, preserveUserAnnotatedPrefix=false)
     val obtainedRenamed = renamer(obtained)
     val expectedRenamed = renamer(expected)
-    val obtainedPrinted = effekt.core.PrettyPrinter.format(obtainedRenamed).layout
-    val expectedPrinted = effekt.core.PrettyPrinter.format(expectedRenamed).layout
+    val obtainedPrinted = effekt.core.ReparsablePrettyPrinter.format(obtainedRenamed).layout
+    val expectedPrinted = effekt.core.ReparsablePrettyPrinter.format(expectedRenamed).layout
     assertEquals(obtainedPrinted, expectedPrinted)
     shouldBeEqual(obtainedRenamed, expectedRenamed, clue)
   }
   def assertAlphaEquivalentStatements(obtained: Stmt,
                             expected: Stmt,
                             clue: => Any = "values are not alpha-equivalent",
                             names: Names = Names(defaultNames))(using Location): Unit = {
-    val renamer = TestRenamer(names)
+    val renamer = TestRenamer(names, preserveUserAnnotatedPrefix=false)
     shouldBeEqual(renamer(obtained), renamer(expected), clue)
   }
   def parse(input: String,

effekt/jvm/src/test/scala/effekt/core/ReparseTests.scala

@@ -75,11 +75,11 @@ class ReparseTests extends CoreTests {
     }
     val renamer = TestRenamer(Names(defaultNames))
     val expectedRenamed = renamer(coreMod)
-    val printed = core.PrettyPrinter.format(expectedRenamed).layout
+    val printed = core.ReparsablePrettyPrinter.format(expectedRenamed).layout
     val reparsed: ModuleDecl = parse(printed)(using Location.empty)
     val reparsedRenamed = renamer(reparsed)
-    val reparsedPrinted = core.PrettyPrinter.format(reparsedRenamed).layout
-    val expectedPrinted = core.PrettyPrinter.format(expectedRenamed).layout
+    val reparsedPrinted = core.ReparsablePrettyPrinter.format(reparsedRenamed).layout
+    val expectedPrinted = printed
     assertEquals(reparsedPrinted, expectedPrinted)
   }
 

effekt/jvm/src/test/scala/effekt/core/TestRenamerTests.scala

@@ -12,10 +12,10 @@ class TestRenamerTests extends CoreTests {
                       names: Names = Names(defaultNames))(using munit.Location) = {
     val pInput = parse(input, "input", names)
     val pExpected = parse(renamed, "expected", names)
-    val renamer = new TestRenamer(names, "renamed") // use "renamed" as prefix so we can refer to it
+    val renamer = new TestRenamer(names, "_renamed_") // use "renamed" as prefix so we can refer to it
     val obtained = renamer(pInput)
-    val obtainedPrinted = effekt.core.PrettyPrinter.format(obtained).layout
-    val expectedPrinted = effekt.core.PrettyPrinter.format(pExpected).layout
+    val obtainedPrinted = effekt.core.ReparsablePrettyPrinter.format(obtained).layout
+    val expectedPrinted = effekt.core.ReparsablePrettyPrinter.format(pExpected).layout
     assertEquals(obtainedPrinted, expectedPrinted)
     shouldBeEqual(obtained, pExpected, clue)
   }
@@ -31,7 +31,7 @@ class TestRenamerTests extends CoreTests {
     val expected =
       """module main
         |
-        |def renamed0() = {
+        |def foo_renamed_0() = {
         |  return (bar: (Int) => Int @ {})(baz: Int)
         |}
         |""".stripMargin
@@ -51,11 +51,11 @@ class TestRenamerTests extends CoreTests {
     val expected =
       """module main
         |
-        |def renamed0() = {
-        |  val renamed1: Int = {
-        |    renamed0: (Int) => Int @ {}(4)
+        |def foo_renamed_0() = {
+        |  val x_renamed_1: Int = {
+        |    foo_renamed_0: (Int) => Int @ {}(4)
         |  };
-        |  return renamed1: Int
+        |  return x_renamed_1: Int
         |}
         |""".stripMargin
     assertRenamedTo(input, expected)
@@ -73,9 +73,9 @@ class TestRenamerTests extends CoreTests {
     val expected =
       """module main
         |
-        |def renamed0() = {
-        |  var renamed1 @ global = (renamed0: (Int) => Int @ {})(4);
-        |  return renamed1: Int
+        |def foo_renamed_0() = {
+        |  var x_renamed_1 @ global = (foo_renamed_0: (Int) => Int @ {})(4);
+        |  return x_renamed_1: Int
         |}
         |""".stripMargin
     assertRenamedTo(input, expected)
@@ -85,15 +85,15 @@ class TestRenamerTests extends CoreTests {
     val input =
       """module main
         |
-        |def renamed0(renamed1: Int) = {
-        |  return renamed1: Int
+        |def f(x: Int) = {
+        |  return x: Int
         |}
         |""".stripMargin
     val expected =
       """module main
         |
-        |def renamed0(renamed1: Int) = {
-        |  return renamed1: Int
+        |def f_renamed_0(x_renamed_1: Int) = {
+        |  return x_renamed_1: Int
         |}
         |""".stripMargin
     assertRenamedTo(input, expected)
@@ -113,14 +113,14 @@ class TestRenamerTests extends CoreTests {
     val expected =
       """module main
         |
-        |type renamed1 {
-        |  renamed0(a: Int, b: Int)
+        |type Data_renamed_1 {
+        |  X_renamed_0(a: Int, b: Int)
         |}
         |
-        |def renamed2() = {
+        |def foo_renamed_2() = {
         |  12 match {
-        |    X : { (renamed3: Int, renamed4: Int) =>
-        |      return renamed3: Int
+        |    X : { (aa_renamed_3: Int, bb_renamed_4: Int) =>
+        |      return aa_renamed_3: Int
         |    }
         |  }
         |}
@@ -139,8 +139,8 @@ class TestRenamerTests extends CoreTests {
     val expected =
       """module main
         |
-        |def renamed0['renamed1](renamed2: renamed1) = {
-        |  return renamed2: Identity[renamed1]
+        |def foo_renamed_0['A_renamed_1](a_renamed_2: A_renamed_1) = {
+        |  return a_renamed_2: Identity[A_renamed_1]
         |}
         |""".stripMargin
     assertRenamedTo(input, expected)
@@ -161,17 +161,17 @@ class TestRenamerTests extends CoreTests {
     val expected =
       """module main
         |
-        |def renamed0() = {
+        |def bar_renamed_0() = {
         |  return 1
         |}
-        |def renamed1() = {
-        |  def renamed2() = {
-        |    renamed0: () => Unit @ {}()
+        |def main_renamed_1() = {
+        |  def foo_renamed_2() = {
+        |    bar_renamed_0: () => Unit @ {}()
         |  }
-        |  def renamed3() = {
+        |  def bar_renamed_3() = {
         |    return 2
         |  }
-        |  renamed2: () => Unit @ {}()
+        |  foo_renamed_2: () => Unit @ {}()
         |}
         |""".stripMargin
 
@@ -191,10 +191,10 @@ class TestRenamerTests extends CoreTests {
     val expected =
       """module main
         |
-        |def renamed0() = {
-        |  let renamed1 = 1
-        |  let renamed2 = 2
-        |  return renamed2: Int
+        |def main_renamed_0() = {
+        |  let x_renamed_1 = 1
+        |  let x_renamed_2 = 2
+        |  return x_renamed_2: Int
         |}
         |""".stripMargin
 

effekt/shared/src/main/scala/effekt/core/DeclarationContext.scala

@@ -1,7 +1,7 @@
 package effekt.core
 
 import effekt.util.messages.ErrorReporter
-import PrettyPrinter.*
+import HumanReadablePrettyPrinter.*
 
 /**
  * Context for transformations of a [[core.ModuleDecl]] that provides the declarations for this module.

effekt/shared/src/main/scala/effekt/core/PrettyPrinter.scala

@@ -4,14 +4,12 @@ package core
 import effekt.core.Type.{PromptSymbol, ResumeSymbol}
 import effekt.source.FeatureFlag
 import kiama.output.ParenPrettyPrinter
+import kiama.output.PrettyPrinterTypes.Document
 
 import scala.language.implicitConversions
 import effekt.symbols.{Name, Wildcard, builtins}
 
-object PrettyPrinter extends ParenPrettyPrinter {
-
-  import kiama.output.PrettyPrinterTypes.Document
-
+class PrettyPrinter(printDetails: Boolean) extends ParenPrettyPrinter {
   override val defaultIndent = 2
 
   def format(t: ModuleDecl): Document =
@@ -52,9 +50,9 @@ object PrettyPrinter extends ParenPrettyPrinter {
     // The order of toplevel items must match the parser (where the order is currently fixed).
     val includes = vsep(m.includes.map { im => "import" <+> im })
     val decls = vsep(m.declarations.map(toDoc))
-    val externs = vsep(m.externs.map(toDoc))
+    val externs = if printDetails then vsep(m.externs.map(toDoc)) else emptyDoc
     val defs = toDoc(m.definitions)
-    val exports = vsep(m.exports.map { id => "export" <+> toDoc(id) })
+    val exports = if printDetails then vsep(m.exports.map { id => "export" <+> toDoc(id) }) else emptyDoc
 
     "module" <+> m.path <>
       emptyline <>
@@ -97,7 +95,7 @@ object PrettyPrinter extends ParenPrettyPrinter {
 
   def toDoc(b: Block, preventBraces: Boolean = false): Doc = b match {
     case BlockVar(id, tpe, capt) =>
-      toDoc(id) <> ":" <+> toDoc(tpe) <+> "@" <+> toDoc(capt)
+      toDoc(id) <> (if printDetails then ":" <+> toDoc(tpe) <+> "@" <+> toDoc(capt) else emptyDoc)
     case BlockLit(tps, cps, vps, bps, body) =>
       val doc = space <> paramsToDoc(tps, cps, vps, bps) <+> "=>" <+> nest(line <> toDocStmts(body)) <> line
       if preventBraces then doc else braces { doc }
@@ -112,17 +110,26 @@ object PrettyPrinter extends ParenPrettyPrinter {
   //def toDoc(n: Name): Doc = n.toString
 
   def toDoc(s: symbols.Symbol): Doc = {
-    builtins.coreBuiltinSymbolToString(s).getOrElse(s.name.name)
+    // 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)
   }
 
   def toDoc(e: Expr): Doc = e match {
     case Literal((), _)            => "()"
     case Literal(s: String, _)     => stringLiteral(s)
     case Literal(value, _)         => value.toString
-    case ValueVar(id, tpe)         => toDoc(id) <> ":" <+> toDoc(tpe)
+    case ValueVar(id, tpe)         => toDoc(id) <> (if printDetails then ":" <+> toDoc(tpe) else emptyDoc)
 
-    case PureApp(b, targs, vargs)  => parens(toDoc(b)) <> argsToDoc(targs, vargs, Nil)
-    case Make(data, tag, targs, vargs)    => "make" <+> toDoc(data) <+> toDoc(tag) <> argsToDoc(targs, vargs, Nil)
+    case PureApp(b, targs, vargs)  => (if printDetails then parens(toDoc(b)) else toDoc(b)) <> argsToDoc(targs, vargs, Nil)
+    case Make(data, tag, targs, vargs) =>
+      if printDetails then 
+        "make" <+> toDoc(data) <+> toDoc(tag) <> argsToDoc(targs, vargs, Nil)
+      else 
+        "make" <+> toDoc(tag) <> argsToDoc(targs, vargs, Nil)
 
     case Box(b, capt) => "box" <+> toDoc(capt) <+> toDoc(b)
   }
@@ -223,14 +230,16 @@ object PrettyPrinter extends ParenPrettyPrinter {
 
     case Val(id, tpe, binding, body) =>
       // RHS must be a single `stmt`, so we have to wrap it in a block.
-      "val" <+> toDoc(id) <> ":" <+> toDoc(tpe) <+> "=" <+> block(toDocStmts(binding)) <> ";" <> line <>
+      val pBinding = if printDetails then block(toDocStmts(binding)) else toDocStmts(binding)
+      "val" <+> toDoc(id) <> ":" <+> toDoc(tpe) <+> "=" <+> pBinding <> ";" <> line <>
         toDocStmts(body)
 
     case App(b, targs, vargs, bargs) =>
       toDoc(b) <> argsToDoc(targs, vargs, bargs)
 
     case Invoke(b, method, methodTpe, targs, vargs, bargs) =>
-      toDoc(b) <> "." <> toDoc(method) <> ":" <+> toDoc(methodTpe) <> argsToDoc(targs, vargs, bargs)
+      val pTpe = if printDetails then ":" <+> toDoc(methodTpe) else emptyDoc
+      toDoc(b) <> "." <> toDoc(method) <> pTpe <> argsToDoc(targs, vargs, bargs)
 
     case If(cond, thn, els) =>
       "if" <+> parens(toDoc(cond)) <+> block(toDocStmts(thn)) <+> "else" <+> block(toDocStmts(els))
@@ -341,3 +350,15 @@ object PrettyPrinter extends ParenPrettyPrinter {
     multi <> s <> multi
   }
 }
+
+/**
+ * Instance of PrettyPrinter that produces output that can be parsed back by the core parser.
+ * This corresponds to the `--detailed-ir` command line flag.
+ */
+object ReparsablePrettyPrinter extends PrettyPrinter(true) {}
+
+/**
+ * Instance of PrettyPrinter that produces less verbose, more human-readable output.
+ * This is the default behavior for the `--ir-write-all` and `--ir-show` command line flags.
+ */
+object HumanReadablePrettyPrinter extends PrettyPrinter(false) {}

effekt/jvm/src/test/scala/effekt/core/TestRenamer.scala → effekt/shared/src/main/scala/effekt/core/TestRenamer.scala

@@ -1,7 +1,7 @@
 package effekt.core
 
-import effekt.{Template, core, symbols}
 import effekt.symbols.builtins
+import effekt.{Template, core, symbols}
 
 /**
  * Freshens bound names in a given term for tests.
@@ -14,7 +14,7 @@ import effekt.symbols.builtins
  *
  * @param C the context is used to copy annotations from old symbols to fresh symbols
  */
-class TestRenamer(names: Names = Names(Map.empty), prefix: String = "_") extends core.Tree.Rewrite {
+class TestRenamer(names: Names = Names(Map.empty), prefix: String = "$", preserveUserAnnotatedPrefix: Boolean = true) extends core.Tree.Rewrite {
 
   // list of scopes that map bound symbols to their renamed variants.
   private var scopes: List[Map[Id, Id]] = List.empty
@@ -31,14 +31,26 @@ class TestRenamer(names: Names = Names(Map.empty), prefix: String = "_") extends
     if (names.isKnown(id)) {
       return names.getKnown(id).get
     }
+    // To generate human-readable names, we include the user-provided string.
+    // To ensure idempotent printing, we strip any existing prefix from the name.
+    // This assumes that user-provided names to not include `prefix`.
+    val userName = if (id.name.name.contains(prefix)) {
+      id.name.name.substring(0, id.name.name.lastIndexOf(prefix))
+    } else {
+      id.name.name
+    }
+    // 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 ""
     // HACK: This is an unfortunate hack.
     // TestRenamer is often used to check for alpha-equivalence by renaming both sides of a comparison.
     // However, Effekt requires globally unique Barendregt indices for all symbols, so just creating fresh
     // Ids is not sufficient. We also need to cache these fresh Ids, so that both sides of an alpha-equivalence
     // comparison get the same fresh Id for a given original Id.
     // This is achieved by generating a deterministic string `uniqueName` on both sides, and looking it up in `names`,
     // which generates a unique Id for it once and reuses it on subsequent lookups.
-    val uniqueName = prefix + suffix.toString
+    val uniqueName = userPart + prefix + suffix.toString
     suffix = suffix + 1
     names.idFor(uniqueName)