Add existing implementation

src/main/scala/Main.scala

@@ -1,6 +0,0 @@
-@main
-def hello(): Unit =
-  println("Hello world!")
-  println(msg)
-
-def msg = "I was compiled by Scala 3. :)"

src/main/scala/de/plugh/asciiprooftree/Main.scala

@@ -0,0 +1,14 @@
+package de.plugh.asciiprooftree
+
+import java.nio.file.Path
+
+@main
+def main(args: String*): Unit = args match
+  case Seq() => run()
+  case Seq(path) => run(Path.of(path))
+  case Seq(path, marker) => run(Path.of(path), marker)
+  case _ =>
+    println("Usage: asciiprooftree [path] [marker]")
+    System.exit(1)
+
+def run(path: Path = Path.of(""), marker: String = "§"): Unit = println(s"$path $marker")

src/main/scala/de/plugh/asciiprooftree/tree/FormattedProofTree.scala

@@ -0,0 +1,27 @@
+package de.plugh.asciiprooftree.tree
+
+case class FormattedProofTree(lines: Lines, conclusionStart: Int, conclusionEnd: Int):
+  def shift(delta: Int): FormattedProofTree = FormattedProofTree(
+    lines = lines.shift(delta),
+    conclusionStart = conclusionStart + delta,
+    conclusionEnd = conclusionEnd + delta,
+  )
+
+  def extend(line: Line): FormattedProofTree = copy(lines = lines.extend(line))
+
+  def joinHorizontally(right: FormattedProofTree): FormattedProofTree = FormattedProofTree.joinHorizontally(this, right)
+
+  override def toString: String = lines.toString
+
+object FormattedProofTree:
+  val separation = 3
+
+  def empty: FormattedProofTree = FormattedProofTree(lines = Lines.empty, conclusionStart = 0, conclusionEnd = 0)
+
+  def joinHorizontally(left: FormattedProofTree, right: FormattedProofTree): FormattedProofTree =
+    val (lines, deltaRight) = left.lines.joinHorizontally(right.lines)
+    FormattedProofTree(
+      lines = lines,
+      conclusionStart = left.conclusionStart min (right.conclusionStart + deltaRight),
+      conclusionEnd = left.conclusionEnd max (right.conclusionEnd + deltaRight),
+    )

src/main/scala/de/plugh/asciiprooftree/tree/Line.scala

@@ -0,0 +1,49 @@
+package de.plugh.asciiprooftree.tree
+
+case class Line(text: String, start: Int = 0):
+  val width: Int = text.codePointCount(0, text.length)
+  val end: Int = start + width
+
+  def at(i: Int): Option[Int] =
+    if i < start || i >= end then return None
+    Some(text.codePointAt(text.offsetByCodePoints(0, i - start)))
+
+  def indexOf(str: String): Option[Int] =
+    val result = text.indexOf(str)
+    if result < 0 then return None
+    Some(start + text.codePointCount(0, result))
+
+  /** The distance from the right side of this line to the left side of the other line. */
+  def distanceTo(right: Line): Int = right.start - end
+
+  def shift(delta: Int): Line = copy(start = start + delta)
+
+  def join(right: Line): Line =
+    val between = distanceTo(right)
+    require(between >= 0, "lines overlap")
+    copy(text = this.text + (" " * between) + right.text)
+
+  /** Take a slice of this line. The range specified must overlap or touch the text of the line. */
+  def slice(start: Int, end: Int): Line =
+    require(start <= end, "end before start")
+    require(start <= this.end && this.start <= end, "non-overlapping range")
+    val clampedStart = start max this.start
+    val clampedEnd = end min this.end
+    val sliceStart = text.offsetByCodePoints(0, clampedStart - this.start)
+    val sliceEnd = text.offsetByCodePoints(sliceStart, clampedEnd - clampedStart)
+    Line(text = text.slice(sliceStart, sliceEnd), start = clampedStart)
+
+  def sliceOpt(start: Int, end: Int): Option[Line] =
+    if end < this.start || this.end < start then return None
+    Some(slice(start, end))
+
+  def trim: Line =
+    var textStart = 0
+    while textStart < text.length && text.codePointAt(textStart) == ' ' do textStart += 1
+    var textEnd = text.length
+    while textStart < textEnd && text.codePointBefore(textEnd) == ' ' do textEnd -= 1
+    slice(start + textStart, start + textEnd)
+
+  override def toString: String =
+    require(start >= 0)
+    " " * start + text

src/main/scala/de/plugh/asciiprooftree/tree/Lines.scala

@@ -0,0 +1,37 @@
+package de.plugh.asciiprooftree.tree
+
+case class Lines(lines: IndexedSeq[Line]):
+  def height: Int = lines.length
+  def at(y: Int): Option[Line] = lines.lift(y)
+
+  def shift(delta: Int): Lines = Lines(lines.map(_.shift(delta)))
+  def extend(line: Line): Lines = Lines(line +: lines)
+
+  def joinHorizontally(right: Lines): (Lines, Int) = Lines.joinHorizontally(this, right)
+
+  override def toString: String = lines.reverse.mkString("\n")
+
+object Lines:
+  def empty: Lines = Lines(IndexedSeq())
+
+  private def minDelta(left: Option[Line], right: Option[Line], separation: Int): Int = (left, right) match
+    case (Some(left), Some(right)) => (separation - left.distanceTo(right)).max(0)
+    case _ => 0
+
+  private def minDeltaForVisualSeparation(left: Lines, right: Lines, separation: Int): Int =
+    var result = 0
+    for y <- 0 until (left.height max right.height) do
+      result = result.max(minDelta(left.at(y), right.at(y - 1), separation))
+      result = result.max(minDelta(left.at(y), right.at(y), separation))
+      result = result.max(minDelta(left.at(y), right.at(y + 1), separation))
+    result
+
+  def joinHorizontally(left: Lines, right: Lines, separation: Int = 3): (Lines, Int) =
+    val deltaRight = minDeltaForVisualSeparation(left, right, separation)
+    val lines =
+      for y <- 0 until (left.height max right.height) yield (left.at(y), right.at(y)) match
+        case (Some(left), Some(right)) => left.join(right.shift(deltaRight))
+        case (Some(left), None) => left
+        case (None, Some(right)) => right.shift(deltaRight)
+        case (None, None) => ???
+    (Lines(lines), deltaRight)

src/main/scala/de/plugh/asciiprooftree/tree/Parser.scala

@@ -0,0 +1,71 @@
+package de.plugh.asciiprooftree.tree
+
+import scala.annotation.tailrec
+
+case class Parser(lines: Lines):
+  private def at(y: Int, start: Int, end: Int): Option[Line] = lines.at(y).flatMap(_.sliceOpt(start, end))
+
+  def parse: Option[ProofTree] = parseAt(0, 0, Integer.MAX_VALUE)
+
+  def parseAt(y: Int, start: Int, end: Int): Option[ProofTree] =
+    val line = at(y, start, end) match
+      case Some(value) => value.trim
+      case None => return None
+
+    val split = splitAtWhitespace(line)
+    if split.isEmpty then None
+    else if split.length == 1 then Some(parseSingleTreeAt(y, split.head))
+    else Some(parseMultipleTreesAt(y, split))
+
+  private def parseSingleTreeAt(y: Int, line: Line): ProofTree =
+    if line.text == "*" then return ProofTree.star
+    val (aboveStart, aboveEnd) = extendRange(y + 1, line.start, line.end)
+    val above = parseAt(y + 1, aboveStart, aboveEnd).getOrElse(ProofTree.empty)
+    parseAsLine(line) match
+      case Some(rule) => above.addLine(rule.getOrElse(""))
+      case None => above.addConclusion(line.text)
+
+  private def parseMultipleTreesAt(y: Int, lines: Seq[Line]): ProofTree =
+    ProofTree(premises = lines.map(parseSingleTreeAt(y, _)))
+
+  private def parseAsLine(line: Line): Option[Option[String]] = """^-+( (\S.*))?$"""
+    .r
+    .findFirstMatchIn(line.text)
+    .map(m => Option[String](m.group(2)))
+
+  private def splitAtWhitespace(line: Line, atLeast: Int = 3): Seq[Line] =
+    val trimmed = line.trim
+    trimmed.indexOf(" " * atLeast) match
+      case None if trimmed.text.isEmpty => Seq()
+      case None => Seq(trimmed)
+      case Some(start) =>
+        val left = trimmed.slice(trimmed.start, start)
+        val right = trimmed.slice(start, trimmed.end)
+        left +: splitAtWhitespace(right, atLeast)
+
+  private def extendRange(y: Int, start: Int, end: Int): (Int, Int) =
+    val line = lines.at(y) match
+      case Some(value) => value
+      case None => return (start, end)
+    val newStart = extendRangeStart(line, start, spaceAllowed = true)
+    val newEnd = extendRangeEnd(line, end, spaceAllowed = true)
+    (newStart, newEnd)
+
+  @tailrec
+  private def extendRangeStart(line: Line, start: Int, spaceAllowed: Boolean): Int = line.at(start - 1) match
+    case Some(' ') if spaceAllowed => extendRangeStart(line, start - 1, spaceAllowed = false)
+    case Some(c) if !Character.isWhitespace(c) => extendRangeStart(line, start - 1, spaceAllowed = true)
+    case _ => start
+
+  @tailrec
+  private def extendRangeEnd(line: Line, end: Int, spaceAllowed: Boolean): Int = line.at(end) match
+    case Some(' ') if spaceAllowed => extendRangeEnd(line, end + 1, spaceAllowed = false)
+    case Some(c) if !Character.isWhitespace(c) => extendRangeEnd(line, end + 1, spaceAllowed = true)
+    case _ => end
+
+object Parser:
+  def apply(lines: Seq[String]): Parser =
+    val trimmedLines = lines.map(Line(_).trim)
+    Parser(Lines(trimmedLines.toIndexedSeq))
+
+  def apply(text: String): Parser = apply(text.linesIterator.toSeq.reverse)

src/main/scala/de/plugh/asciiprooftree/tree/ProofTree.scala

@@ -0,0 +1,48 @@
+package de.plugh.asciiprooftree.tree
+
+case class ProofTree(premises: Seq[ProofTree] = Seq(), line: Option[String] = None, conclusion: Option[String] = None):
+  def addPremise(premise: ProofTree): ProofTree = copy(premises = premises :+ premise)
+  def addPremiseBefore(premise: ProofTree): ProofTree = copy(premises = premise +: premises)
+
+  def addLine(rule: String = ""): ProofTree =
+    if this.conclusion.isEmpty && this.line.isEmpty then copy(line = Some(rule))
+    else ProofTree().addPremise(this).addLine(rule)
+
+  def addConclusion(conclusion: String): ProofTree =
+    if this.conclusion.isEmpty then copy(conclusion = Some(conclusion))
+    else ProofTree().addPremise(this).addConclusion(conclusion)
+
+  private def formatLine(start: Int, end: Int, rule: String): Line =
+    val lineStr = "-" * (end - start)
+    val lineText = if rule.isEmpty then lineStr else s"$lineStr $rule"
+    Line(lineText, start)
+
+  def formatted: FormattedProofTree =
+    val fPremises = premises.map(_.formatted).reduceOption(_.joinHorizontally(_)).getOrElse(FormattedProofTree.empty)
+
+    val lConclusion = conclusion match
+      case Some(conclusion) => Line(conclusion)
+      case None => return line match
+          case Some(rule) => fPremises.extend(formatLine(fPremises.conclusionStart, fPremises.conclusionEnd, rule))
+          case None => fPremises
+
+    val aboveMiddle = (fPremises.conclusionStart + fPremises.conclusionEnd) / 2
+    val belowMiddle = (lConclusion.start + lConclusion.end) / 2
+
+    val (aboveCentered, belowCentered) =
+      if aboveMiddle < belowMiddle then (fPremises.shift(belowMiddle - aboveMiddle), lConclusion)
+      else if aboveMiddle > belowMiddle then (fPremises, lConclusion.shift(aboveMiddle - belowMiddle))
+      else (fPremises, lConclusion)
+
+    val combined = line match
+      case Some(rule) =>
+        val lineStart = aboveCentered.conclusionStart min belowCentered.start
+        val lineEnd = aboveCentered.conclusionEnd max belowCentered.end
+        aboveCentered.extend(formatLine(lineStart, lineEnd, rule)).extend(belowCentered)
+      case None => aboveCentered.extend(belowCentered)
+
+    combined.copy(conclusionStart = belowCentered.start, conclusionEnd = belowCentered.end)
+
+object ProofTree:
+  def empty: ProofTree = ProofTree()
+  def star: ProofTree = ProofTree().addConclusion("*")

src/main/scala/de/plugh/asciiprooftree/tree/Sequent.scala

@@ -0,0 +1,6 @@
+package de.plugh.asciiprooftree.tree
+
+case class Sequent(ante: String, succ: String):
+  override def toString: String = Seq(Some(ante).filter(_.isBlank), Some("⊢"), Some(succ).filter(_.isBlank))
+    .flatten
+    .mkString(" ")