From 012ac77209a163740413bdbdc636fd50eb8ffdde Mon Sep 17 00:00:00 2001 From: Florian Cassayre Date: Thu, 7 Apr 2022 13:43:44 +0200 Subject: [PATCH] Improve support for string interpolators using macros --- .gitignore | 3 + .../florian/masterproject/front/fol/FOL.scala | 4 ++ .../fol/definitions/FormulaDefinitions.scala | 6 +- .../fol/definitions/TermDefinitions.scala | 6 +- .../florian/masterproject/front/front.scala | 5 ++ .../front/parser/FrontMacro.scala | 60 +++++++++++++++++++ .../front/parser/FrontReader.scala | 13 ---- .../printer/FrontPositionedPrinter.scala | 20 ++++--- .../masterproject/front/proof/Proof.scala | 4 ++ .../proof/sequent/SequentDefinitions.scala | 21 ++----- .../masterproject/front/FrontMacroTests.scala | 18 ++++++ 11 files changed, 122 insertions(+), 38 deletions(-) create mode 100644 src/main/scala/me/cassayre/florian/masterproject/front/parser/FrontMacro.scala create mode 100644 src/test/scala/me/cassayre/florian/masterproject/front/FrontMacroTests.scala diff --git a/.gitignore b/.gitignore index bd96b7f..8d529a9 100644 --- a/.gitignore +++ b/.gitignore @@ -3,3 +3,6 @@ target .bsp releases +.vscode +.metals +.bloop diff --git a/src/main/scala/me/cassayre/florian/masterproject/front/fol/FOL.scala b/src/main/scala/me/cassayre/florian/masterproject/front/fol/FOL.scala index c35af8d..dabd380 100644 --- a/src/main/scala/me/cassayre/florian/masterproject/front/fol/FOL.scala +++ b/src/main/scala/me/cassayre/florian/masterproject/front/fol/FOL.scala @@ -5,6 +5,7 @@ import me.cassayre.florian.masterproject.front.fol.conversions.from.* import me.cassayre.florian.masterproject.front.fol.definitions.* import me.cassayre.florian.masterproject.front.fol.ops.* import me.cassayre.florian.masterproject.front.fol.utils.* +import me.cassayre.florian.masterproject.front.printer.FrontPositionedPrinter object FOL extends FormulaDefinitions with TermConversionsTo with FormulaConversionsTo @@ -12,6 +13,9 @@ object FOL extends FormulaDefinitions with TermUtils with FormulaUtils with TermOps with FormulaOps { + override protected def pretty(term: Term): String = FrontPositionedPrinter.prettyTerm(term) + override protected def pretty(formula: Formula): String = FrontPositionedPrinter.prettyFormula(formula) + type LabelType = Label type SchematicLabelType = SchematicLabel type LabeledTreeType[A <: Label] = LabeledTree[A] diff --git a/src/main/scala/me/cassayre/florian/masterproject/front/fol/definitions/FormulaDefinitions.scala b/src/main/scala/me/cassayre/florian/masterproject/front/fol/definitions/FormulaDefinitions.scala index d2d7cc5..6b56d1c 100644 --- a/src/main/scala/me/cassayre/florian/masterproject/front/fol/definitions/FormulaDefinitions.scala +++ b/src/main/scala/me/cassayre/florian/masterproject/front/fol/definitions/FormulaDefinitions.scala @@ -1,8 +1,12 @@ package me.cassayre.florian.masterproject.front.fol.definitions trait FormulaDefinitions extends FormulaLabelDefinitions with TermDefinitions { + + protected def pretty(formula: Formula): String - sealed abstract class Formula extends LabeledTree[FormulaLabel] + sealed abstract class Formula extends LabeledTree[FormulaLabel] { + override def toString: String = pretty(this) + } final case class PredicateFormula protected(label: PredicateLabel[?], args: Seq[Term]) extends Formula object PredicateFormula { diff --git a/src/main/scala/me/cassayre/florian/masterproject/front/fol/definitions/TermDefinitions.scala b/src/main/scala/me/cassayre/florian/masterproject/front/fol/definitions/TermDefinitions.scala index a3422c3..27126c1 100644 --- a/src/main/scala/me/cassayre/florian/masterproject/front/fol/definitions/TermDefinitions.scala +++ b/src/main/scala/me/cassayre/florian/masterproject/front/fol/definitions/TermDefinitions.scala @@ -2,7 +2,11 @@ package me.cassayre.florian.masterproject.front.fol.definitions trait TermDefinitions extends TermLabelDefinitions { - sealed abstract class Term extends LabeledTree[TermLabel] + protected def pretty(term: Term): String + + sealed abstract class Term extends LabeledTree[TermLabel] { + override def toString: String = pretty(this) + } final case class VariableTerm(label: VariableLabel) extends Term diff --git a/src/main/scala/me/cassayre/florian/masterproject/front/front.scala b/src/main/scala/me/cassayre/florian/masterproject/front/front.scala index 4a8e5c9..f61541d 100644 --- a/src/main/scala/me/cassayre/florian/masterproject/front/front.scala +++ b/src/main/scala/me/cassayre/florian/masterproject/front/front.scala @@ -3,7 +3,12 @@ package me.cassayre.florian.masterproject.front import me.cassayre.florian.masterproject.front.fol.FOL import me.cassayre.florian.masterproject.front.proof.Proof import me.cassayre.florian.masterproject.front.unification +import me.cassayre.florian.masterproject.front.parser +import me.cassayre.florian.masterproject.front.printer export FOL.* export Proof.* export unification.Unifier +export parser.FrontReader +export parser.FrontMacro.* +export printer.FrontPositionedPrinter diff --git a/src/main/scala/me/cassayre/florian/masterproject/front/parser/FrontMacro.scala b/src/main/scala/me/cassayre/florian/masterproject/front/parser/FrontMacro.scala new file mode 100644 index 0000000..629585e --- /dev/null +++ b/src/main/scala/me/cassayre/florian/masterproject/front/parser/FrontMacro.scala @@ -0,0 +1,60 @@ +package me.cassayre.florian.masterproject.front.parser + +import me.cassayre.florian.masterproject.front.fol.FOL.* +import me.cassayre.florian.masterproject.front.proof.Proof.* +import me.cassayre.florian.masterproject.front.printer.FrontPositionedPrinter + +// Note: on Intellij you may want to disable syntax highlighting for this file +// ("File Types" => "Text" => "Ignored Files and Folders", add "FrontMacro.scala") + +object FrontMacro { + + import scala.quoted.* + + extension (inline sc: StringContext) + inline def term(inline args: Any*): Term = ${ termImpl('sc, 'args) } + inline def formula(inline args: Any*): Formula = ${ formulaImpl('sc, 'args) } + inline def sequent(inline args: Any*): Sequent = ${ sequentImpl('sc, 'args) } + inline def partial(inline args: Any*): PartialSequent = ${ partialImpl('sc, 'args) } + + private def termImpl(sc: Expr[StringContext], args: Expr[Seq[Any]])(using Quotes): Expr[Term] = + '{ FrontReader.readTerm(${rawStringImpl(sc, args)}) } + private def formulaImpl(sc: Expr[StringContext], args: Expr[Seq[Any]])(using Quotes): Expr[Formula] = + '{ FrontReader.readFormula(${rawStringImpl(sc, args)}) } + private def sequentImpl(sc: Expr[StringContext], args: Expr[Seq[Any]])(using Quotes): Expr[Sequent] = + '{ FrontReader.readSequent(${rawStringImpl(sc, args)}) } + private def partialImpl(sc: Expr[StringContext], args: Expr[Seq[Any]])(using Quotes): Expr[PartialSequent] = + '{ FrontReader.readPartialSequent(${rawStringImpl(sc, args)}) } + + + private def rawStringImpl(sc: Expr[StringContext], args: Expr[Seq[Any]])(using q: Quotes): Expr[String] = { + import q.reflect._ + + val argsSeq: Seq[Expr[Any]] = args match { + case Varargs(es) => es + } + val argsSeqString: Seq[Expr[String]] = argsSeq.map { + case '{ $s: String } => s + case '{ $f: SchematicConnectorLabel[?] } => '{ s"??${${f}.id}" } + case '{ $f: SchematicFunctionLabel[?] | SchematicPredicateLabel[?] } => '{ s"?${${f}.id}" } + case '{ $f: ConstantFunctionLabel[?] | ConstantPredicateLabel[?] | ConstantConnectorLabel[?] } => '{ s"${${f}.id}" } + case '{ $other } => '{ ${other}.toString } + } + val partsSeq: Seq[Expr[String]] = sc match { + case '{ StringContext($vs: _*) } => + vs match { case Varargs(es) => es } + } + val rawParts: Seq[String] = partsSeq.map(_.asTerm).map { + case Literal(c: Constant) => c.value.toString + } + val argsSeqWithEmpty: Seq[Expr[String]] = argsSeqString :+ '{""} + val allExprs: Seq[Expr[Any]] = rawParts.zip(argsSeqWithEmpty).flatMap { case (p: String, a: Expr[Any]) => + Seq(Expr(p), a) + } + val exprString: Expr[String] = allExprs.map(e => '{ ${e}.toString }).reduce { + case (l: Expr[Any], r: Expr[Any]) => '{ $l + $r } + } + exprString + } + +} diff --git a/src/main/scala/me/cassayre/florian/masterproject/front/parser/FrontReader.scala b/src/main/scala/me/cassayre/florian/masterproject/front/parser/FrontReader.scala index 78b1ae8..4f4bc19 100644 --- a/src/main/scala/me/cassayre/florian/masterproject/front/parser/FrontReader.scala +++ b/src/main/scala/me/cassayre/florian/masterproject/front/parser/FrontReader.scala @@ -33,17 +33,4 @@ object FrontReader { def readPartialSequent(str: String, ascii: Boolean = true, multiline: Boolean = false): PartialSequent = FrontResolver.resolvePartialSequent(FrontParser.parsePartialSequent(lexing(str, ascii, multiline))) - - - private def mkString(sc: StringContext, args: Seq[Any]): String = { - assert(sc.parts.size == args.size + 1) - sc.parts.zip(args.map(_.toString) :+ "").flatMap { case (p, a) => Seq(p, a) }.mkString - } - - extension (sc: StringContext) - def term(args: Any*): Term = readTerm(mkString(sc, args)) - def formula(args: Any*): Formula = readFormula(mkString(sc, args)) - def sequent(args: Any*): Sequent = readSequent(mkString(sc, args)) - def partial(args: Any*): PartialSequent = readPartialSequent(mkString(sc, args)) - } diff --git a/src/main/scala/me/cassayre/florian/masterproject/front/printer/FrontPositionedPrinter.scala b/src/main/scala/me/cassayre/florian/masterproject/front/printer/FrontPositionedPrinter.scala index 1fc594b..9bbc5bc 100644 --- a/src/main/scala/me/cassayre/florian/masterproject/front/printer/FrontPositionedPrinter.scala +++ b/src/main/scala/me/cassayre/florian/masterproject/front/printer/FrontPositionedPrinter.scala @@ -20,31 +20,35 @@ object FrontPositionedPrinter { } + private val rName = "[a-zA-Z_][a-zA-Z0-9_]*".r + private def isNamePrintable(name: String): Boolean = rName.matches(name) + private def isTermPrintableInternal(term: Term, variables: Set[String]): Boolean = term match { case VariableTerm(label) => - assert(variables.contains(label.id)) // By assumption + assert(variables.contains(label.id)) // By assumption, thus `isNamePrintable` is true true case FunctionTerm(label, args) => val isLabelPrintable = label match { case SchematicFunctionLabel(id, _) => !variables.contains(id) case _ => true } - isLabelPrintable && args.forall(isTermPrintableInternal(_, variables)) + isNamePrintable(label.id) && isLabelPrintable && args.forall(isTermPrintableInternal(_, variables)) } private def isTermPrintable(term: Term, freeVariables: Set[VariableLabel]): Boolean = - isWellFormed(term) && isTermPrintableInternal(term, freeVariables.map(_.id)) + freeVariables.map(_.id).forall(isNamePrintable) && isWellFormed(term) && isTermPrintableInternal(term, freeVariables.map(_.id)) private def isFormulaPrintableInternal(formula: Formula, variables: Set[String]): Boolean = formula match { - case PredicateFormula(label, args) => args.forall(isTermPrintableInternal(_, variables)) - case ConnectorFormula(label, args) => args.forall(isFormulaPrintableInternal(_, variables)) + case PredicateFormula(label, args) => + (!label.isInstanceOf[SchematicLabelType] || isNamePrintable(label.id)) && args.forall(isTermPrintableInternal(_, variables)) + case ConnectorFormula(label, args) => + (!label.isInstanceOf[SchematicLabelType] || isNamePrintable(label.id)) && args.forall(isFormulaPrintableInternal(_, variables)) case BinderFormula(label, bound, inner) => - assert(!variables.contains(bound.id)) // By assumption - isFormulaPrintableInternal(inner, variables + bound.id) + isNamePrintable(bound.id) && !variables.contains(bound.id) && isFormulaPrintableInternal(inner, variables + bound.id) } private def isFormulaPrintable(formula: Formula, freeVariables: Set[VariableLabel]): Boolean = - isWellFormed(formula) && isFormulaPrintableInternal(formula, freeVariables.map(_.id)) + freeVariables.map(_.id).forall(isNamePrintable) && isWellFormed(formula) && isFormulaPrintableInternal(formula, freeVariables.map(_.id)) private def mkSep(items: FrontPrintNode*)(separator: FrontLeaf): IndexedSeq[FrontPrintNode] = { diff --git a/src/main/scala/me/cassayre/florian/masterproject/front/proof/Proof.scala b/src/main/scala/me/cassayre/florian/masterproject/front/proof/Proof.scala index 6f7578f..c4ce050 100644 --- a/src/main/scala/me/cassayre/florian/masterproject/front/proof/Proof.scala +++ b/src/main/scala/me/cassayre/florian/masterproject/front/proof/Proof.scala @@ -1,5 +1,6 @@ package me.cassayre.florian.masterproject.front.proof +import me.cassayre.florian.masterproject.front.printer.FrontPositionedPrinter import me.cassayre.florian.masterproject.front.proof.state.* import me.cassayre.florian.masterproject.front.proof.predef.* @@ -7,6 +8,9 @@ object Proof extends ProofInterfaceDefinitions with PredefRulesDefinitions with PredefTacticsDefinitions { + override protected def pretty(sequent: Sequent): String = FrontPositionedPrinter.prettySequent(sequent) + override protected def pretty(sequent: PartialSequent): String = FrontPositionedPrinter.prettyPartialSequent(sequent) + val introHypo: RuleHypothesis.type = RuleHypothesis val introLAnd: RuleIntroductionLeftAnd.type = RuleIntroductionLeftAnd val introRAnd: RuleIntroductionRightAnd.type = RuleIntroductionRightAnd diff --git a/src/main/scala/me/cassayre/florian/masterproject/front/proof/sequent/SequentDefinitions.scala b/src/main/scala/me/cassayre/florian/masterproject/front/proof/sequent/SequentDefinitions.scala index 33a97d3..6e9dcb9 100644 --- a/src/main/scala/me/cassayre/florian/masterproject/front/proof/sequent/SequentDefinitions.scala +++ b/src/main/scala/me/cassayre/florian/masterproject/front/proof/sequent/SequentDefinitions.scala @@ -5,6 +5,9 @@ import me.cassayre.florian.masterproject.front.fol.FOL.* trait SequentDefinitions { + protected def pretty(sequent: Sequent): String + protected def pretty(sequent: PartialSequent): String + sealed abstract class SequentBase { val left: IndexedSeq[Formula] val right: IndexedSeq[Formula] @@ -12,24 +15,12 @@ trait SequentDefinitions { def formulas: IndexedSeq[Formula] = left ++ right } - // TODO this should be handled by its own printer - private def prettySequent(left: Seq[Formula], right: Seq[Formula], partialLeft: Boolean = false, partialRight: Boolean = false): String = { - def prettySequence(seq: Seq[Formula], leftSide: Boolean, partial: Boolean): String = { - val strs = seq.map(Printer.prettyFormula(_)) - val rest = "..." - val strs1 = if (partial) if (leftSide) rest +: strs else strs :+ rest else strs - strs1.mkString("; ") - } - - s"${prettySequence(left, true, partialLeft)} ⊢ ${prettySequence(right, false, partialRight)}" - } - final case class Sequent(left: IndexedSeq[Formula], right: IndexedSeq[Formula]) extends SequentBase { - override def toString: String = prettySequent(left, right) + override def toString: String = pretty(this) } final case class PartialSequent(left: IndexedSeq[Formula], right: IndexedSeq[Formula], partialLeft: Boolean = true, partialRight: Boolean = true) extends SequentBase { - override def toString: String = prettySequent(left, right, partialLeft, partialRight) + override def toString: String = pretty(this) } def functionsOfSequent(sequent: SequentBase): Set[FunctionLabel[?]] = sequent.formulas.flatMap(functionsOf).toSet @@ -44,7 +35,7 @@ trait SequentDefinitions { def schematicConnectorsOfSequent(sequent: SequentBase): Set[SchematicConnectorLabel[?]] = sequent.formulas.flatMap(schematicConnectorsOf).toSet - + def freeVariablesOfSequent(sequent: SequentBase): Set[VariableLabel] = sequent.formulas.flatMap(freeVariablesOf).toSet def declaredBoundVariablesOfSequent(sequent: SequentBase): Set[VariableLabel] = diff --git a/src/test/scala/me/cassayre/florian/masterproject/front/FrontMacroTests.scala b/src/test/scala/me/cassayre/florian/masterproject/front/FrontMacroTests.scala new file mode 100644 index 0000000..e61d11b --- /dev/null +++ b/src/test/scala/me/cassayre/florian/masterproject/front/FrontMacroTests.scala @@ -0,0 +1,18 @@ +package me.cassayre.florian.masterproject.front + +import org.scalatest.funsuite.AnyFunSuite +import me.cassayre.florian.masterproject.front.* + +class FrontMacroTests extends AnyFunSuite { + + test("string interpolation macros") { + term"g(x, y)" + formula"a /\ b \/ c => d" + sequent"a; b |- c" + partial"a |- b; ..." + + val p = ConstantPredicateLabel("p", 2) + assert(formula"$p(x, y)".toString == s"p(x, y)") // Currently limited support for label interpolation, very few safety guarantees + } + +}