Use heuristics to detect whether a block contains a tree

This commit is contained in:
Joscha 2025-02-06 22:09:03 +01:00
parent 5f510bb9b9
commit fac0f3605d
3 changed files with 12 additions and 4 deletions

View file

@ -12,16 +12,21 @@ val lineRe = "^\\s*§(?<block>.*)$".r
class Conf(args: Seq[String]) extends ScallopConf(args): class Conf(args: Seq[String]) extends ScallopConf(args):
val path: ScallopOption[Path] = trailArg[Path]() val path: ScallopOption[Path] = trailArg[Path]()
val indent: ScallopOption[Int] = opt[Int](default = Some(2))
val blockRegex: ScallopOption[String] = opt[String](default = Some(blockRe.regex)) val blockRegex: ScallopOption[String] = opt[String](default = Some(blockRe.regex))
val lineRegex: ScallopOption[String] = opt[String](default = Some(lineRe.regex)) val lineRegex: ScallopOption[String] = opt[String](default = Some(lineRe.regex))
val indent: ScallopOption[Int] = opt[Int](default = Some(2))
val noHeuristics: ScallopOption[Boolean] = opt[Boolean]()
verify() verify()
@main @main
def main(args: String*): Unit = def main(args: String*): Unit =
val conf = new Conf(args) val conf = new Conf(args)
val formatter = val formatter = Formatter(
Formatter(indent = conf.indent(), blockRe = Regex(conf.blockRegex()), lineRe = Regex(conf.lineRegex())) blockRe = Regex(conf.blockRegex()),
lineRe = Regex(conf.lineRegex()),
indent = conf.indent(),
heuristics = !conf.noHeuristics(),
)
reformat(conf.path(), formatter) reformat(conf.path(), formatter)
def reformat(path: Path, formatter: Formatter): Unit = def reformat(path: Path, formatter: Formatter): Unit =

View file

@ -7,7 +7,7 @@ import scala.util.boundary
import scala.util.matching.Regex import scala.util.matching.Regex
import scala.util.matching.Regex.Match import scala.util.matching.Regex.Match
case class Formatter(indent: Int, blockRe: Regex, lineRe: Regex): case class Formatter(blockRe: Regex, lineRe: Regex, indent: Int, heuristics: Boolean):
private val blockReI = blockRe.pattern.namedGroups().get("block") private val blockReI = blockRe.pattern.namedGroups().get("block")
private val lineReI = lineRe.pattern.namedGroups().get("block") private val lineReI = lineRe.pattern.namedGroups().get("block")
@ -26,6 +26,7 @@ case class Formatter(indent: Int, blockRe: Regex, lineRe: Regex):
private def parseBlock(text: String, m: Match): Option[BlockInfo] = boundary: private def parseBlock(text: String, m: Match): Option[BlockInfo] = boundary:
val block = parseBlockLines(m.group(blockReI)).getOrElse(boundary.break(None)) val block = parseBlockLines(m.group(blockReI)).getOrElse(boundary.break(None))
val tree = Parser(block.content).parse.getOrElse(boundary.break(None)) val tree = Parser(block.content).parse.getOrElse(boundary.break(None))
if heuristics && tree.containsNoLines then return None
Some(BlockInfo( Some(BlockInfo(
block = block, block = block,
tree = tree, tree = tree,

View file

@ -43,6 +43,8 @@ case class ProofTree(premises: Seq[ProofTree] = Seq(), line: Option[String] = No
combined.copy(conclusionStart = belowCentered.start, conclusionEnd = belowCentered.end) combined.copy(conclusionStart = belowCentered.start, conclusionEnd = belowCentered.end)
def containsNoLines: Boolean = line.isEmpty && premises.forall(_.containsNoLines)
object ProofTree: object ProofTree:
def empty: ProofTree = ProofTree() def empty: ProofTree = ProofTree()
def star: ProofTree = ProofTree().addConclusion("*") def star: ProofTree = ProofTree().addConclusion("*")