Improve support for string interpolators using macros

.gitignore

@@ -3,3 +3,6 @@
 target
 .bsp
 releases
+.vscode
+.metals
+.bloop

src/main/scala/me/cassayre/florian/masterproject/front/fol/FOL.scala

@@ -5,13 +5,17 @@ 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
   with TermConversionsFrom with FormulaConversionsFrom
   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]

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 {

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
 

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

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
+  }
+
+}

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))
-
 }

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] = {

src/main/scala/me/cassayre/florian/masterproject/front/proof/Proof.scala

@@ -1,12 +1,16 @@
 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.*
 
 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

src/main/scala/me/cassayre/florian/masterproject/front/proof/sequent/SequentDefinitions.scala

@@ -5,31 +5,22 @@ 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]
 
     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] =

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
+  }
+
+}