From f0b6101d90121776711f02eb956155d3674201ab Mon Sep 17 00:00:00 2001
From: Katja Goltsova <katja.goltsova@protonmail.com>
Date: Mon, 3 Oct 2022 18:24:05 +0200
Subject: [PATCH] Use scallion-based printer to pretty print proofs
---
.../src/main/scala/lisa/utils/Printer.scala | 174 +-----------------
1 file changed, 3 insertions(+), 171 deletions(-)
diff --git a/lisa-utils/src/main/scala/lisa/utils/Printer.scala b/lisa-utils/src/main/scala/lisa/utils/Printer.scala
index f6e3c259..75c5837e 100644
--- a/lisa-utils/src/main/scala/lisa/utils/Printer.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/Printer.scala
@@ -15,116 +15,6 @@ object Printer {
private def commaSeparator(compact: Boolean, symbol: String = ","): String = s"$symbol${spaceSeparator(compact)}"
- private def prettyParentheses(content: String): String = s"(${content})"
-
- private def prettyFunction(name: String, args: Seq[String], compact: Boolean, dropParentheses: Boolean = true): String = {
- if (dropParentheses && args.isEmpty) name else s"$name(${args.mkString(commaSeparator(compact))})"
- }
-
- private def prettyInfix(operator: String, left: String, right: String, compact: Boolean): String =
- Seq(left, operator, right).mkString(spaceSeparator(compact))
-
- // Special symbols that aren't defined in this theory
- private val (membership, subsetOf, sameCardinality) = (
- ConstantPredicateLabel("set_membership", 2),
- ConstantPredicateLabel("subset_of", 2),
- ConstantPredicateLabel("same_cardinality", 2)
- )
- private val (emptySet, unorderedPair, orderedPair, singleton, powerSet, unionSet) = (
- ConstantFunctionLabel("empty_set", 0),
- ConstantFunctionLabel("unordered_pair", 2),
- ConstantFunctionLabel("ordered_pair", 2),
- ConstantFunctionLabel("singleton", 1),
- ConstantFunctionLabel("power_set", 1),
- ConstantFunctionLabel("union", 1)
- )
-
- private val nonAtomicPredicates: Set[PredicateLabel] = Set(equality, membership, subsetOf, sameCardinality) // Predicates which require parentheses (for readability)
-
- private def prettyFormulaInternal(formula: Formula, isRightMost: Boolean, compact: Boolean): String = formula match {
- case PredicateFormula(label, args) =>
- label match {
- case `equality` =>
- args match {
- case Seq(l, r) => prettyInfix(label.id, prettyTerm(l), prettyTerm(r), compact)
- case _ => throw new Exception
- }
- case `membership` =>
- args match {
- case Seq(l, r) => prettyInfix("∈", prettyTerm(l), prettyTerm(r), compact)
- case _ => throw new Exception
- }
- case `subsetOf` =>
- args match {
- case Seq(l, r) => prettyInfix("⊆", prettyTerm(l), prettyTerm(r), compact)
- case _ => throw new Exception
- }
- case `sameCardinality` =>
- args match {
- case Seq(l, r) => prettyInfix("~", prettyTerm(l), prettyTerm(r), compact)
- case _ => throw new Exception
- }
- case _ =>
- val labelString = label match {
- case ConstantPredicateLabel(id, _) => id
- case s: SchematicPredicateLabel => s"?${s.id}"
- }
- prettyFunction(labelString, args.map(prettyTerm(_, compact)), compact)
- }
- case ConnectorFormula(label, args) =>
- (label, args) match {
- case (Neg, Seq(arg)) =>
- val isAtomic = arg match {
- case PredicateFormula(label, _) => !nonAtomicPredicates.contains(label)
- case ConnectorFormula(Neg, _) => true
- case _ => false
- }
- val bodyString = prettyFormulaInternal(arg, isRightMost, compact)
- val bodyParenthesized = if (isAtomic) bodyString else prettyParentheses(bodyString)
- s"${label.id}${bodyParenthesized}"
- case (binary @ (Implies | Iff | And | Or), Seq(l, r)) =>
- val precedences: Map[ConnectorLabel, Int] = Map(
- And -> 1,
- Or -> 2,
- Implies -> 3,
- Iff -> 4
- )
- val precedence = precedences(binary)
- val isLeftParentheses = l match {
- case _: BinderFormula => true
- case PredicateFormula(leftLabel, _) => nonAtomicPredicates.contains(leftLabel)
- case ConnectorFormula(leftLabel, _) => precedences.get(leftLabel).exists(_ >= precedence)
- }
- val isRightParentheses = r match {
- case _: BinderFormula => !isRightMost
- case PredicateFormula(leftLabel, _) => nonAtomicPredicates.contains(leftLabel)
- case ConnectorFormula(rightLabel, _) => precedences.get(rightLabel).exists(_ > precedence)
- }
- val (leftString, rightString) = (prettyFormulaInternal(l, isLeftParentheses, compact), prettyFormulaInternal(r, isRightMost || isRightParentheses, compact))
- val leftParenthesized = if (isLeftParentheses) prettyParentheses(leftString) else leftString
- val rightParenthesized = if (isRightParentheses) prettyParentheses(rightString) else rightString
- prettyInfix(label.id, leftParenthesized, rightParenthesized, compact)
- case (nary @ (And | Or), args) if args.nonEmpty =>
- // Rewriting to match the above case; namely op(a) --> a, and op(a, ...rest) --> op(a, op(...rest))
- // Empty args aren't allowed here
- // Invariant: args.size > 2
- if (args.sizeIs == 1) {
- prettyFormulaInternal(args.head, isRightMost, compact)
- } else {
- prettyFormulaInternal(ConnectorFormula(nary, Seq(args.head, ConnectorFormula(nary, args.tail))), isRightMost, compact)
- }
- case _ => prettyFunction(label.id, args.map(a => prettyFormulaInternal(a, isRightMost, compact)), compact)
- }
- case BinderFormula(label, bound, inner) =>
- def accumulateNested(f: Formula, acc: Seq[VariableLabel]): (Seq[VariableLabel], Formula) = f match {
- case BinderFormula(`label`, nestBound, nestInner) => accumulateNested(nestInner, nestBound +: acc)
- case _ => (acc, f)
- }
-
- val (bounds, innerNested) = accumulateNested(inner, Seq(bound))
- Seq(s"${label.id}${bounds.reverse.map(_.id).mkString(commaSeparator(compact))}.", prettyFormulaInternal(innerNested, true, compact)).mkString(spaceSeparator(compact))
- }
-
/**
* Returns a string representation of this formula. See also [[prettyTerm]].
* Example output:
@@ -136,7 +26,7 @@ object Printer {
* @param compact whether spaces should be omitted between tokens
* @return the string representation of this formula
*/
- def prettyFormula(formula: Formula, compact: Boolean = false): String = prettyFormulaInternal(formula, true, compact)
+ def prettyFormula(formula: Formula, compact: Boolean = false): String = Parser.printFormula(formula)
/**
* Returns a string representation of this term. See also [[prettyFormula]].
@@ -149,48 +39,7 @@ object Printer {
* @param compact whether spaces should be omitted between tokens
* @return the string representation of this term
*/
- def prettyTerm(term: Term, compact: Boolean = false): String = term match {
- case VariableTerm(label) => s"?${label.id}"
- case FunctionTerm(label, args) =>
- label match {
- case `emptySet` =>
- args match {
- case Seq() => prettyFunction("∅", Seq.empty, compact, dropParentheses = true)
- case _ => throw new Exception
- }
- case `unorderedPair` =>
- args match {
- case Seq(l, r) => s"{${Seq(l, r).map(prettyTerm(_, compact)).mkString(commaSeparator(compact))}}"
- case _ => throw new Exception
- }
- case `orderedPair` =>
- args match {
- case Seq(l, r) => s"(${Seq(l, r).map(prettyTerm(_, compact)).mkString(commaSeparator(compact))})"
- case _ => throw new Exception
- }
- case `singleton` =>
- args match {
- case Seq(s) => s"{${prettyTerm(s)}}"
- case _ => throw new Exception
- }
- case `powerSet` =>
- args match {
- case Seq(s) => prettyFunction("P", Seq(prettyTerm(s)), compact)
- case _ => throw new Exception
- }
- case `unionSet` =>
- args match {
- case Seq(s) => prettyFunction("U", Seq(prettyTerm(s)), compact)
- case _ => throw new Exception
- }
- case _ =>
- val labelString = label match {
- case ConstantFunctionLabel(id, _) => id
- case SchematicFunctionLabel(id, _) => s"?$id"
- }
- prettyFunction(labelString, args.map(prettyTerm(_, compact)), compact)
- }
- }
+ def prettyTerm(term: Term, compact: Boolean = false): String = Parser.printTerm(term)
/**
* Returns a string representation of this sequent.
@@ -203,23 +52,7 @@ object Printer {
* @param compact whether spaces should be omitted between tokens
* @return the string representation of this sequent
*/
- def prettySequent(sequent: Sequent, compact: Boolean = false): String = {
- def prettyFormulas(set: Set[Formula]): String = set.toSeq.map(prettyFormula(_, compact)).sorted.mkString(commaSeparator(compact, ";"))
-
- Seq(prettyFormulas(sequent.left), "⊢", prettyFormulas(sequent.right)).filter(_.nonEmpty).mkString(spaceSeparator(compact))
- }
-
- /**
- * Returns a string representation of the line number in a proof.
- * Example output:
- * <pre>
- * 0:2:1
- * </pre>
- *
- * @param line the line number
- * @return the string representation of this line number
- */
- def prettyLineNumber(line: Seq[Int]): String = line.mkString(":")
+ def prettySequent(sequent: Sequent, compact: Boolean = false): String = Parser.printSequent(sequent)
/**
* Returns a string representation of this proof.
@@ -347,5 +180,4 @@ object Printer {
}
def prettySCProof(proof: SCProof): String = prettySCProof(SCValidProof(proof), false)
-
}
--
GitLab