From f411db572de9ba268dfdedd4a04aa9edbbfece50 Mon Sep 17 00:00:00 2001 From: Joscha Date: Wed, 4 Sep 2024 16:06:34 +0200 Subject: [PATCH] Add existing implementation --- src/main/scala/Main.scala | 6 -- .../scala/de/plugh/asciiprooftree/Main.scala | 14 ++++ .../tree/FormattedProofTree.scala | 27 +++++++ .../de/plugh/asciiprooftree/tree/Line.scala | 49 +++++++++++++ .../de/plugh/asciiprooftree/tree/Lines.scala | 37 ++++++++++ .../de/plugh/asciiprooftree/tree/Parser.scala | 71 +++++++++++++++++++ .../plugh/asciiprooftree/tree/ProofTree.scala | 48 +++++++++++++ .../plugh/asciiprooftree/tree/Sequent.scala | 6 ++ 8 files changed, 252 insertions(+), 6 deletions(-) delete mode 100644 src/main/scala/Main.scala create mode 100644 src/main/scala/de/plugh/asciiprooftree/Main.scala create mode 100644 src/main/scala/de/plugh/asciiprooftree/tree/FormattedProofTree.scala create mode 100644 src/main/scala/de/plugh/asciiprooftree/tree/Line.scala create mode 100644 src/main/scala/de/plugh/asciiprooftree/tree/Lines.scala create mode 100644 src/main/scala/de/plugh/asciiprooftree/tree/Parser.scala create mode 100644 src/main/scala/de/plugh/asciiprooftree/tree/ProofTree.scala create mode 100644 src/main/scala/de/plugh/asciiprooftree/tree/Sequent.scala diff --git a/src/main/scala/Main.scala b/src/main/scala/Main.scala deleted file mode 100644 index c193594..0000000 --- a/src/main/scala/Main.scala +++ /dev/null @@ -1,6 +0,0 @@ -@main -def hello(): Unit = - println("Hello world!") - println(msg) - -def msg = "I was compiled by Scala 3. :)" diff --git a/src/main/scala/de/plugh/asciiprooftree/Main.scala b/src/main/scala/de/plugh/asciiprooftree/Main.scala new file mode 100644 index 0000000..907f75e --- /dev/null +++ b/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") diff --git a/src/main/scala/de/plugh/asciiprooftree/tree/FormattedProofTree.scala b/src/main/scala/de/plugh/asciiprooftree/tree/FormattedProofTree.scala new file mode 100644 index 0000000..ebfe294 --- /dev/null +++ b/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), + ) diff --git a/src/main/scala/de/plugh/asciiprooftree/tree/Line.scala b/src/main/scala/de/plugh/asciiprooftree/tree/Line.scala new file mode 100644 index 0000000..993ce96 --- /dev/null +++ b/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 diff --git a/src/main/scala/de/plugh/asciiprooftree/tree/Lines.scala b/src/main/scala/de/plugh/asciiprooftree/tree/Lines.scala new file mode 100644 index 0000000..ca98ba3 --- /dev/null +++ b/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) diff --git a/src/main/scala/de/plugh/asciiprooftree/tree/Parser.scala b/src/main/scala/de/plugh/asciiprooftree/tree/Parser.scala new file mode 100644 index 0000000..62f50ea --- /dev/null +++ b/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) diff --git a/src/main/scala/de/plugh/asciiprooftree/tree/ProofTree.scala b/src/main/scala/de/plugh/asciiprooftree/tree/ProofTree.scala new file mode 100644 index 0000000..f40855b --- /dev/null +++ b/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("*") diff --git a/src/main/scala/de/plugh/asciiprooftree/tree/Sequent.scala b/src/main/scala/de/plugh/asciiprooftree/tree/Sequent.scala new file mode 100644 index 0000000..e48efad --- /dev/null +++ b/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(" ")