The latest state of expr_parser

langs/tla/TLAParser.scala

@@ -177,6 +177,72 @@ object TLAParser extends PassSeq:
       ).void
 
     nodeSpanMatchedBy(impl).map(RawExpression.apply)
+  end rawExpression
+
+  def rawConjunction(col: Integer): SeqPattern[RawExpression] =
+    val simpleCases: SeqPattern[Unit] =
+      anyChild.void <* not(
+        tok(expressionDelimiters*)
+          | tok(defns./\).filter(node =>
+            val s = node.sourceRange
+            s.source.lines.lineColAtOffset(s.offset)._2 > col,
+          )
+          // stop at operator definitions: all valid patterns leading to == here
+          | operatorDefnBeginnings,
+      )
+
+    lazy val quantifierBound: SeqPattern[EmptyTuple] =
+      skip(
+        tok(TupleGroup).as(EmptyTuple)
+          | repeatedSepBy1(`,`)(Alpha),
+      )
+        ~ skip(defns.`\\in`)
+        ~ skip(defer(impl))
+        ~ trailing
+
+    lazy val quantifierBounds: SeqPattern[Unit] =
+      repeatedSepBy1(`,`)(quantifierBound).void
+
+    lazy val forallExists: SeqPattern[EmptyTuple] =
+      skip(
+        tok(LaTexLike).src("\\A") | tok(LaTexLike).src("\\AA") | tok(LaTexLike)
+          .src("\\E") | tok(LaTexLike).src("\\EE"),
+      )
+        ~ skip(quantifierBounds | repeatedSepBy1(`,`)(Alpha))
+        ~ skip(`:`)
+        ~ trailing
+
+    lazy val choose: SeqPattern[EmptyTuple] =
+      skip(defns.CHOOSE)
+        ~ skip(quantifierBound | repeatedSepBy1(`,`)(Alpha))
+        ~ skip(`:`)
+        ~ trailing
+
+    lazy val lambda: SeqPattern[EmptyTuple] =
+      skip(defns.LAMBDA)
+        ~ skip(repeatedSepBy1(`,`)(Alpha))
+        ~ skip(`:`)
+        ~ trailing
+
+    // this is an over-approximation of what can show up
+    // in an identifier prefix
+    // TODO: why does the grammar make it look like it goes the other way round?
+    lazy val idFrag: SeqPattern[EmptyTuple] =
+      skip(`!`)
+        ~ skip(`:`)
+        ~ trailing
+
+    lazy val impl: SeqPattern[Unit] =
+      repeated1(
+        forallExists
+          | choose
+          | lambda
+          | idFrag
+          | simpleCases, // last, otherwise it eats parts of the above
+      ).void
+
+    nodeSpanMatchedBy(impl).map(RawExpression.apply)
+  end rawConjunction
 
   val proofDelimiters: Seq[Token] = Seq(
     defns.ASSUME,
@@ -715,66 +781,3 @@ object TLAParser extends PassSeq:
             ~ trailing,
         ).rewrite: (local, op) =>
           splice(lang.Local(op.unparent()).like(local))
-
-  // TODO: finish expression parsing
-  // val buildExpressions = passDef:
-  //   wellformed := prevWellformed.makeDerived:
-  //     val removedCases = Seq(
-  //       TLAReader.StringLiteral,
-  //       TLAReader.NumberLiteral,
-  //       TLAReader.TupleGroup,
-  //     )
-  //     lang.Module.Defns.removeCases(removedCases*)
-  //     lang.Module.Defns.addCases(lang.Expr)
-  //     TLAReader.groupTokens.foreach: tok =>
-  //       tok.removeCases(removedCases*)
-  //       tok.addCases(lang.Expr)
-
-  //     lang.Expr.importFrom(tla.wellformed)
-  //     lang.Expr.addCases(lang.TmpGroupExpr)
-
-  //     lang.TmpGroupExpr ::= lang.Expr
-
-  //   pass(once = false, strategy = pass.bottomUp)
-  //     .rules:
-  //       on(
-  //         TLAReader.StringLiteral
-  //       ).rewrite: lit =>
-  //         splice(lang.Expr(lang.Expr.StringLiteral().like(lit)))
-  //       | on(
-  //         TLAReader.NumberLiteral
-  //       ).rewrite: lit =>
-  //         splice(lang.Expr(lang.Expr.NumberLiteral().like(lit)))
-  //       | on(
-  //         field(TLAReader.Alpha)
-  //         ~ field(
-  //           tok(TLAReader.ParenthesesGroup) *> children(
-  //             repeatedSepBy(`,`)(lang.Expr)
-  //           )
-  //         )
-  //         ~ trailing
-  //       ).rewrite: (name, params) =>
-  //         splice(lang.Expr(lang.Expr.OpCall(
-  //           lang.Id().like(name),
-  //           lang.Expr.OpCall.Params(params.iterator.map(_.unparent())),
-  //         )))
-  //       | on(
-  //         TLAReader.Alpha
-  //       ).rewrite: name =>
-  //         splice(lang.Expr(lang.Expr.OpCall(
-  //           lang.Id().like(name),
-  //           lang.Expr.OpCall.Params(),
-  //         )))
-  //       | on(
-  //         tok(TLAReader.ParenthesesGroup) *> onlyChild(lang.Expr)
-  //       ).rewrite: expr =>
-  /* // mark this group as an expression, but leave evidence that it is a group
-   * (for operator precedence handling) */
-  //         splice(lang.Expr(lang.TmpGroupExpr(expr.unparent())))
-  //       | on(
-  //         tok(TLAReader.TupleGroup).product(children(
-  //           field(repeatedSepBy(`,`)(lang.Expr))
-  //           ~ eof
-  //         ))
-  //       ).rewrite: (lit, elems) =>
-  //         splice(lang.Expr(lang.Expr.TupleLiteral(elems.iterator.map(_.unparent()))))

langs/tla/TLAParser.test.scala

@@ -16,8 +16,9 @@ package forja.langs.tla
 
 import forja.*
 import forja.source.{Source, SourceRange}
+import forja.test.WithTLACorpus
 
-class TLAParserTests extends munit.FunSuite, test.WithTLACorpus:
+class TLAParserTests extends munit.FunSuite, WithTLACorpus:
   self =>
 
   /* TODO: skip the TLAPS files; parsing that seems like a waste of time for
@@ -37,6 +38,7 @@ class TLAParserTests extends munit.FunSuite, test.WithTLACorpus:
       // )
       // , tracer = Manip.RewriteDebugTracer(os.pwd / "dbg_passes")
     )
+    ExprParser(top)
 
     // re-enable if interesting:
     // val folder = os.SubPath(file.subRelativeTo(clonesDir).segments.init)

langs/tla/defns.scala

@@ -74,7 +74,9 @@ object defns:
   case object PROPOSITION extends ReservedWord
   case object ONLY extends ReservedWord
 
-  sealed trait Operator extends Token, HasSpelling
+  sealed trait Operator extends Token, HasSpelling:
+    def highPrecedence: Int
+    def lowPrecedence: Int
 
   object Operator:
     lazy val instances: IArray[Operator] =
@@ -100,7 +102,7 @@ object defns:
 
   sealed trait InfixOperator(
       val lowPrecedence: Int,
-      val highPredecence: Int,
+      val highPrecedence: Int,
       val isAssociative: Boolean = false,
   ) extends Operator
   object InfixOperator extends util.HasInstanceArray[InfixOperator]
@@ -209,7 +211,9 @@ object defns:
   case object `\\supset` extends InfixOperator(5, 5)
   case object `%%` extends InfixOperator(10, 11, true)
 
-  sealed trait PostfixOperator(val predecence: Int) extends Operator
+  sealed trait PostfixOperator(val precedence: Int) extends Operator:
+    def highPrecedence: Int = precedence
+    def lowPrecedence: Int = precedence
   object PostfixOperator extends util.HasInstanceArray[PostfixOperator]
 
   case object `^+` extends PostfixOperator(15)

langs/tla/package.scala

@@ -100,6 +100,7 @@ object lang extends WellformedDef:
           Expr.SetLiteral,
           Expr.TupleLiteral,
           Expr.RecordLiteral,
+          Expr.RecordSetLiteral,
           Expr.Project,
           Expr.OpCall,
           Expr.FnCall,
@@ -180,14 +181,20 @@ object lang extends WellformedDef:
           ),
         )
 
-    object Case extends t(repeated(Case.Branch, minCount = 1)):
+    object Case extends t(fields(Case.Branches, Case.Other)):
+      object Branches extends t(repeated(Branch, minCount = 1))
       object Branch
           extends t(
             fields(
               Expr,
               Expr,
             ),
           )
+      object Other
+          extends t(
+            choice(Expr, Other.None),
+          ):
+        object None extends t(Atom)
     end Case
 
     object Let

src/Builtin.scala

@@ -18,7 +18,7 @@ import cats.syntax.all.given
 
 object Builtin:
   object Error extends Token:
-    def apply(msg: String, ast: Node.Child): Node =
+    def apply(msg: String, ast: Node.Child*): Node =
       Error(
         Error.Message().at(msg),
         Error.AST(ast),

src/Node.scala

@@ -391,7 +391,7 @@ object Node:
 
       require(
         results.size == 1,
-        s"token(s) not found ${(tok +: toks).map(_.name).mkString(", ")}",
+        s"token(s) not found ${(tok +: toks).map(_.name).mkString(", ")}, in ${this.toShortString()}",
       )
       results.head
 

src/PassSeq.scala

@@ -24,15 +24,16 @@ import scala.collection.mutable
 transparent trait PassSeq:
   def inputWellformed: Wellformed
   final def outputWellformed: Wellformed =
-    assert(entriesSealed)
+    allPasses // compute allPasses, needed to enforce complete initialization
     entries.last.wellformed
 
   private val entries = mutable.ListBuffer.empty[PassSeq.Entry]
   private var entriesSealed = false
 
   protected def prevWellformed(using BuildCtx): Wellformed =
-    require(entries.nonEmpty, "there is no previous Wellformed")
-    entries.last.wellformed
+    if entries.isEmpty
+    then inputWellformed
+    else entries.last.wellformed
 
   protected object wellformed:
     def :=(using ctx: BuildCtx)(wellformed: Wellformed): Unit =

src/wf/Wellformed.scala

@@ -166,11 +166,9 @@ final class Wellformed private (
             done:
               val wrongSize = parent.children.size
               parent.children = List(
-                Node(Builtin.Error)(
-                  Builtin.Error.Message(
-                    s"$desc should have exactly ${fields.size} children, but it had $wrongSize instead",
-                  ),
-                  Builtin.Error.AST(parent.unparentedChildren),
+                Builtin.Error(
+                  s"$desc should have exactly ${fields.size} children, but it had $wrongSize instead",
+                  parent.unparentedChildren.toSeq*,
                 ),
               )
           else
@@ -206,11 +204,9 @@ final class Wellformed private (
             done:
               val wrongSize = parent.children.size
               parent.children = List(
-                Node(Builtin.Error)(
-                  Builtin.Error.Message(
-                    s"$desc should have at least $minCount children, but it had $wrongSize instead",
-                  ),
-                  Builtin.Error.AST(parent.unparentedChildren),
+                Builtin.Error(
+                  s"$desc should have at least $minCount children, but it had $wrongSize instead",
+                  parent.unparentedChildren.toSeq*,
                 ),
               )
           else
@@ -531,6 +527,15 @@ object Wellformed:
               s"$token's shape is not appropriate for adding cases ($shape)",
             )
 
+      def deleteShape(): Unit =
+        token match
+          case Node.Top =>
+            require(topShapeOpt.nonEmpty)
+            topShapeOpt = None
+          case token: Token =>
+            require(assigns.contains(token))
+            assigns.remove(token)
+
       def importFrom(wf2: Wellformed): Unit =
         def fillFromShape(shape: Shape): Unit =
           shape match
@@ -557,6 +562,7 @@ object Wellformed:
             topShapeOpt = Some(wf2.topShape)
             fillFromShape(wf2.topShape)
           case token: Token => fillFromTokenOrEmbed(token)
+      end importFrom
 
     private[forja] def build(): Wellformed =
       require(topShapeOpt.nonEmpty)