From bd8f0010251420aa73265c7768a638993a6308db Mon Sep 17 00:00:00 2001 From: Kuter Bora Date: Wed, 12 Feb 2025 16:38:23 -0800 Subject: [PATCH 1/9] Parsing Expressions Step 1 --- Node.scala | 2 +- PassSeq.scala | 7 +- Wellformed.scala | 10 +++ tla/ExprParser.scala | 117 +++++++++++++++++++++++++++++ tla/ExprParser.test.scala | 151 ++++++++++++++++++++++++++++++++++++++ tla/TLAParser.scala | 122 +++++++++++++++--------------- 6 files changed, 344 insertions(+), 65 deletions(-) create mode 100644 tla/ExprParser.scala create mode 100644 tla/ExprParser.test.scala diff --git a/Node.scala b/Node.scala index cbf67fa..82ab3f8 100644 --- a/Node.scala +++ b/Node.scala @@ -385,7 +385,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 diff --git a/PassSeq.scala b/PassSeq.scala index 60b8267..f28866b 100644 --- a/PassSeq.scala +++ b/PassSeq.scala @@ -21,15 +21,16 @@ import dsl.* 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 = diff --git a/Wellformed.scala b/Wellformed.scala index 91d93cc..b3c8fe1 100644 --- a/Wellformed.scala +++ b/Wellformed.scala @@ -524,6 +524,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 @@ -550,6 +559,7 @@ object Wellformed: topShapeOpt = Some(wf2.topShape) fillFromShape(wf2.topShape) case token: Token => fillFromTokenOrEmbed(token) + end importFrom private[Wellformed] def build(): Wellformed = require(topShapeOpt.nonEmpty) diff --git a/tla/ExprParser.scala b/tla/ExprParser.scala new file mode 100644 index 0000000..7445602 --- /dev/null +++ b/tla/ExprParser.scala @@ -0,0 +1,117 @@ +package distcompiler.tla + +import cats.syntax.all.given + +import distcompiler.* +import dsl.* +import distcompiler.Builtin.{Error, SourceMarker} +import distcompiler.tla.TLAReader +import distcompiler.tla.TLAParser.rawExpression +import distcompiler.Manip.ops.pass.bottomUp + +object ExprParser extends PassSeq: + import distcompiler.dsl.* + import distcompiler.Builtin.{Error, SourceMarker} + import TLAReader.* + def inputWellformed: Wellformed = TLAParser.outputWellformed + + val buildExpressions = passDef: + wellformed := prevWellformed.makeDerived: + val removedCases = Seq( + TLAReader.StringLiteral, + TLAReader.NumberLiteral, + TLAReader.TupleGroup + ) + TLAReader.groupTokens.foreach: tok => + tok.removeCases(removedCases*) + tok.addCases(tokens.Expr) + + tokens.Expr.deleteShape() + tokens.Expr.importFrom(tla.wellformed) + tokens.Expr.addCases(tokens.Expr) + + pass(once = false, strategy = pass.bottomUp) + .rules: + on( + parent(tokens.Expr) *> + TLAReader.NumberLiteral + ).rewrite: lit => + splice(tokens.Expr(tokens.Expr.NumberLiteral().like(lit))) + | on( + parent(tokens.Expr) *> + TLAReader.StringLiteral + ).rewrite: lit => + splice(tokens.Expr(tokens.Expr.StringLiteral().like(lit))) + // TODO: Set Literal + | on( + parent(tokens.Expr) *> + tok(TLAReader.TupleGroup).product( + children( + field(repeatedSepBy(`,`)(rawExpression)) + ~ eof + ) + ) + ).rewrite: (lit, elems) => + splice( + tokens.Expr( + tokens.Expr.TupleLiteral(elems.iterator.map(_.mkNode)).like(lit) + ) + ) + // TODO: Record Literal + // TODO: Project + | on( + parent(tokens.Expr) *> + field(tokens.Expr) + ~ field(tok(defns.InfixOperator.instances*)) + ~ field(tokens.Expr) + ~ trailing + ).rewrite: (left, op, right) => + splice( + tokens.Expr( + tokens.Expr + .OpCall( + tokens.OpSym(op.unparent()), + tokens.Expr.OpCall.Params(left.unparent(), right.unparent()) + ) + .like(op) + ) + ) + // TODO: other kinds of OpCalls + // TODO: Fn Call + // TODO: if + // TODO: Case + // TODO: Let + // TODO: Exists + // TODO: Forall + // TODO: Function + // TODO: SetComprehension + // TODO: SetRefinement + // TODO: Choose + // TODO: Except + // TODO: Lambda + | on( + parent(tokens.Expr) *> + tok(TLAReader.ParenthesesGroup) *> + children: + field(rawExpression) + ~ eof + ).rewrite: expr => + splice( + tokens.Expr(expr.mkNode) + ) + end buildExpressions + + val removeNestedExpr = passDef: + wellformed := prevWellformed.makeDerived: + tokens.Expr.removeCases(tokens.Expr) + + pass(once = true, strategy = bottomUp) + .rules: + on( + tok(tokens.Expr) *> + onlyChild(tokens.Expr) + ).rewrite: child => + splice( + child.unparent() + ) + end removeNestedExpr diff --git a/tla/ExprParser.test.scala b/tla/ExprParser.test.scala new file mode 100644 index 0000000..4a38325 --- /dev/null +++ b/tla/ExprParser.test.scala @@ -0,0 +1,151 @@ +package distcompiler.tla + +import distcompiler.* +import Builtin.{Error, SourceMarker} + +// scala-cli test . -- '*ExprParser*' + +class ExprParserTests extends munit.FunSuite: + extension (str: String) + def parseStr: Node.Top = + val wrapped_str = + Source.fromString( + s"""---- MODULE TestMod ---- + |EXTENDS Naturals + |VARIABLE temp + | + |Init == $str + |==== + """.stripMargin + ) + val top = TLAReader(SourceRange.entire(wrapped_str)) + TLAParser(top) + ExprParser(top) + Node.Top( + top(tokens.Module)(tokens.Module.Defns)(tokens.Operator)( + tokens.Expr + ).unparentedChildren + ) + + extension (top: Node.Top) + def parseNode: Node.Top = + val freshTop = Node.Top( + tokens.Module( + tokens.Id("TestMod"), + tokens.Module.Extends(), + tokens.Module.Defns( + tokens.Operator( + tokens.Id("test"), + tokens.Operator.Params(), + tokens.Expr( + top.unparentedChildren + ) + ) + ) + ) + ) + ExprParser(freshTop) + Node.Top( + freshTop(tokens.Module)(tokens.Module.Defns)(tokens.Operator)( + tokens.Expr + ).unparentedChildren + ) + + test("NumberLiteral"): + assertEquals("1".parseStr, Node.Top(tokens.Expr.NumberLiteral("1"))) + + test("StringLiteral"): + assertEquals( + "\"string\"".parseStr, + Node.Top(tokens.Expr.StringLiteral("string")) + ) + assertEquals( + "\"string\\nnewline\"".parseStr, + Node.Top(tokens.Expr.StringLiteral("string\nnewline")) + ) + + test("TupleLiteral"): + assertEquals( + "<<1, 2, 3>>".parseStr, + Node.Top( + tokens.Expr.TupleLiteral( + tokens.Expr(tokens.Expr.NumberLiteral("1")), + tokens.Expr(tokens.Expr.NumberLiteral("2")), + tokens.Expr(tokens.Expr.NumberLiteral("3")) + ) + ) + ) + + test("Single Binary Operator"): + assertEquals( + "5 + 6".parseStr, + Node.Top( + tokens.Expr.OpCall( + tokens.OpSym( + defns.+("+") + ), + tokens.Expr.OpCall.Params( + tokens.Expr(tokens.Expr.NumberLiteral("5")), + tokens.Expr(tokens.Expr.NumberLiteral("6")) + ) + ) + ) + ) + assertEquals( + "5 $ 6".parseStr, + Node.Top( + tokens.Expr.OpCall( + tokens.OpSym(defns.$("$")), + tokens.Expr.OpCall.Params( + tokens.Expr(tokens.Expr.NumberLiteral("5")), + tokens.Expr(tokens.Expr.NumberLiteral("6")) + ) + ) + ) + ) + + test("ParenthesesGroup"): + assertEquals( + "(1)".parseStr, + Node.Top(tokens.Expr.NumberLiteral("1")) + ) + assertEquals( + "(((1)))".parseStr, + Node.Top(tokens.Expr.NumberLiteral("1")) + ) + assertEquals( + "(5 + 6)".parseStr, + Node.Top( + tokens.Expr.OpCall( + tokens.OpSym( + defns.+("+") + ), + tokens.Expr.OpCall.Params( + tokens.Expr(tokens.Expr.NumberLiteral("5")), + tokens.Expr(tokens.Expr.NumberLiteral("6")) + ) + ) + ) + ) + assertEquals( + "(1 + 2) * 3".parseStr, + Node.Top( + tokens.Expr.OpCall( + tokens.OpSym( + defns.*("*") + ), + tokens.Expr.OpCall.Params( + tokens.Expr(tokens.Expr.OpCall( + tokens.OpSym( + defns.+("+") + ), + tokens.Expr.OpCall.Params( + tokens.Expr(tokens.Expr.NumberLiteral("1")), + tokens.Expr(tokens.Expr.NumberLiteral("2")) + ) + )), + tokens.Expr(tokens.Expr.NumberLiteral("3")) + ) + ) + ) + ) \ No newline at end of file diff --git a/tla/TLAParser.scala b/tla/TLAParser.scala index 88fbe71..9235da6 100644 --- a/tla/TLAParser.scala +++ b/tla/TLAParser.scala @@ -711,64 +711,64 @@ object TLAParser extends PassSeq: ).rewrite: (local, op) => splice(tokens.Local(op.unparent()).like(local)) - // TODO: finish expression parsing - // val buildExpressions = passDef: - // wellformed := prevWellformed.makeDerived: - // val removedCases = Seq( - // TLAReader.StringLiteral, - // TLAReader.NumberLiteral, - // TLAReader.TupleGroup, - // ) - // tokens.Module.Defns.removeCases(removedCases*) - // tokens.Module.Defns.addCases(tokens.Expr) - // TLAReader.groupTokens.foreach: tok => - // tok.removeCases(removedCases*) - // tok.addCases(tokens.Expr) - - // tokens.Expr.importFrom(tla.wellformed) - // tokens.Expr.addCases(tokens.TmpGroupExpr) - - // tokens.TmpGroupExpr ::= tokens.Expr - - // pass(once = false, strategy = pass.bottomUp) - // .rules: - // on( - // TLAReader.StringLiteral - // ).rewrite: lit => - // splice(tokens.Expr(tokens.Expr.StringLiteral().like(lit))) - // | on( - // TLAReader.NumberLiteral - // ).rewrite: lit => - // splice(tokens.Expr(tokens.Expr.NumberLiteral().like(lit))) - // | on( - // field(TLAReader.Alpha) - // ~ field( - // tok(TLAReader.ParenthesesGroup) *> children( - // repeatedSepBy(`,`)(tokens.Expr) - // ) - // ) - // ~ trailing - // ).rewrite: (name, params) => - // splice(tokens.Expr(tokens.Expr.OpCall( - // tokens.Id().like(name), - // tokens.Expr.OpCall.Params(params.iterator.map(_.unparent())), - // ))) - // | on( - // TLAReader.Alpha - // ).rewrite: name => - // splice(tokens.Expr(tokens.Expr.OpCall( - // tokens.Id().like(name), - // tokens.Expr.OpCall.Params(), - // ))) - // | on( - // tok(TLAReader.ParenthesesGroup) *> onlyChild(tokens.Expr) - // ).rewrite: expr => - // // mark this group as an expression, but leave evidence that it is a group (for operator precedence handling) - // splice(tokens.Expr(tokens.TmpGroupExpr(expr.unparent()))) - // | on( - // tok(TLAReader.TupleGroup).product(children( - // field(repeatedSepBy(`,`)(tokens.Expr)) - // ~ eof - // )) - // ).rewrite: (lit, elems) => - // splice(tokens.Expr(tokens.Expr.TupleLiteral(elems.iterator.map(_.unparent())))) +// TODO: finish expression parsing +// val buildExpressions = passDef: +// wellformed := prevWellformed.makeDerived: +// val removedCases = Seq( +// TLAReader.StringLiteral, +// TLAReader.NumberLiteral, +// TLAReader.TupleGroup, +// ) +// tokens.Module.Defns.removeCases(removedCases*) +// tokens.Module.Defns.addCases(tokens.Expr) +// TLAReader.groupTokens.foreach: tok => +// tok.removeCases(removedCases*) +// tok.addCases(tokens.Expr) + +// tokens.Expr.importFrom(tla.wellformed) +// tokens.Expr.addCases(tokens.TmpGroupExpr) + +// tokens.TmpGroupExpr ::= tokens.Expr + +// pass(once = false, strategy = pass.bottomUp) +// .rules: +// on( +// TLAReader.StringLiteral +// ).rewrite: lit => +// splice(tokens.Expr(tokens.Expr.StringLiteral().like(lit))) +// | on( +// TLAReader.NumberLiteral +// ).rewrite: lit => +// splice(tokens.Expr(tokens.Expr.NumberLiteral().like(lit))) +// | on( +// field(TLAReader.Alpha) +// ~ field( +// tok(TLAReader.ParenthesesGroup) *> children( +// repeatedSepBy(`,`)(tokens.Expr) +// ) +// ) +// ~ trailing +// ).rewrite: (name, params) => +// splice(tokens.Expr(tokens.Expr.OpCall( +// tokens.Id().like(name), +// tokens.Expr.OpCall.Params(params.iterator.map(_.unparent())), +// ))) +// | on( +// TLAReader.Alpha +// ).rewrite: name => +// splice(tokens.Expr(tokens.Expr.OpCall( +// tokens.Id().like(name), +// tokens.Expr.OpCall.Params(), +// ))) +// | on( +// tok(TLAReader.ParenthesesGroup) *> onlyChild(tokens.Expr) +// ).rewrite: expr => +// // mark this group as an expression, but leave evidence that it is a group (for operator precedence handling) +// splice(tokens.Expr(tokens.TmpGroupExpr(expr.unparent()))) +// | on( +// tok(TLAReader.TupleGroup).product(children( +// field(repeatedSepBy(`,`)(tokens.Expr)) +// ~ eof +// )) +// ).rewrite: (lit, elems) => +// splice(tokens.Expr(tokens.Expr.TupleLiteral(elems.iterator.map(_.unparent())))) From 7036ba6c50ff3d585a471be3cbb6a4f43b59721b Mon Sep 17 00:00:00 2001 From: Kuter Bora Date: Thu, 13 Feb 2025 18:00:47 -0800 Subject: [PATCH 2/9] ExprParser Sets and Records --- tla/ExprParser.scala | 58 +++++++++++++++++++++++++++------ tla/ExprParser.test.scala | 68 +++++++++++++++++++++++++++------------ tla/package.scala | 1 + 3 files changed, 96 insertions(+), 31 deletions(-) diff --git a/tla/ExprParser.scala b/tla/ExprParser.scala index 7445602..cea6a60 100644 --- a/tla/ExprParser.scala +++ b/tla/ExprParser.scala @@ -33,7 +33,7 @@ object ExprParser extends PassSeq: pass(once = false, strategy = pass.bottomUp) .rules: on( - parent(tokens.Expr) *> + parent(tokens.Expr) *> TLAReader.NumberLiteral ).rewrite: lit => splice(tokens.Expr(tokens.Expr.NumberLiteral().like(lit))) @@ -42,23 +42,61 @@ object ExprParser extends PassSeq: TLAReader.StringLiteral ).rewrite: lit => splice(tokens.Expr(tokens.Expr.StringLiteral().like(lit))) - // TODO: Set Literal + | on( + parent(tokens.Expr) *> + tok(TLAReader.BracesGroup) *> + children: + field(repeatedSepBy(`,`)(rawExpression)) + ~ eof + ).rewrite: exprs => + splice( + tokens.Expr( + tokens.Expr.SetLiteral(exprs.iterator.map(_.mkNode)) + )) | on( parent(tokens.Expr) *> tok(TLAReader.TupleGroup).product( children( field(repeatedSepBy(`,`)(rawExpression)) ~ eof - ) - ) + )) ).rewrite: (lit, elems) => splice( tokens.Expr( tokens.Expr.TupleLiteral(elems.iterator.map(_.mkNode)).like(lit) - ) - ) - // TODO: Record Literal + )) + | on( + parent(tokens.Expr) *> + tok(TLAReader.SqBracketsGroup) *> + children: + repeatedSepBy(`,`)( + field(TLAReader.Alpha) + ~ skip(`|->`) + ~ field(rawExpression) + ~ trailing + ) + ).rewrite: fields => + splice( + tokens.Expr( + tokens.Expr.RecordLiteral( + fields.iterator.map( + (opCall, expr) => + tokens.Expr.RecordLiteral.Field( + tokens.Id().like(opCall.unparent()), + expr.mkNode + ) + )))) // TODO: Project + | on( + parent(tokens.Expr) *> + TLAReader.Alpha + ).rewrite: name => + splice( + tokens.Expr( + tokens.Expr.OpCall( + tokens.Id().like(name), + tokens.Expr.OpCall.Params(), + ))) | on( parent(tokens.Expr) *> field(tokens.Expr) @@ -74,8 +112,8 @@ object ExprParser extends PassSeq: tokens.Expr.OpCall.Params(left.unparent(), right.unparent()) ) .like(op) - ) - ) + )) + // ~ field(tok(defns.InfixOperator.instances.filter(_.isAssociative)*)) // TODO: other kinds of OpCalls // TODO: Fn Call // TODO: if @@ -98,7 +136,7 @@ object ExprParser extends PassSeq: ).rewrite: expr => splice( tokens.Expr(expr.mkNode) - ) + ) end buildExpressions val removeNestedExpr = passDef: diff --git a/tla/ExprParser.test.scala b/tla/ExprParser.test.scala index 4a38325..c20a278 100644 --- a/tla/ExprParser.test.scala +++ b/tla/ExprParser.test.scala @@ -39,11 +39,7 @@ class ExprParserTests extends munit.FunSuite: tokens.Operator.Params(), tokens.Expr( top.unparentedChildren - ) - ) - ) - ) - ) + ))))) ExprParser(freshTop) Node.Top( freshTop(tokens.Module)(tokens.Module.Defns)(tokens.Operator)( @@ -64,6 +60,16 @@ class ExprParserTests extends munit.FunSuite: Node.Top(tokens.Expr.StringLiteral("string\nnewline")) ) + test("Set Literal"): + assertEquals( + "{1, 2, 3}".parseStr, + Node.Top( + tokens.Expr.SetLiteral( + tokens.Expr(tokens.Expr.NumberLiteral("1")), + tokens.Expr(tokens.Expr.NumberLiteral("2")), + tokens.Expr(tokens.Expr.NumberLiteral("3")) + ))) + test("TupleLiteral"): assertEquals( "<<1, 2, 3>>".parseStr, @@ -72,9 +78,41 @@ class ExprParserTests extends munit.FunSuite: tokens.Expr(tokens.Expr.NumberLiteral("1")), tokens.Expr(tokens.Expr.NumberLiteral("2")), tokens.Expr(tokens.Expr.NumberLiteral("3")) + ))) + + test("RecordLiteral"): + assertEquals( + "[x |-> 2, y |-> 3]".parseStr, + Node.Top( + tokens.Expr.RecordLiteral( + tokens.Expr.RecordLiteral.Field( + // tokens.Expr.OpCall( + // tokens.Id("x"), + // tokens.Expr.OpCall.Params() + // ), + tokens.Id("x"), + tokens.Expr(tokens.Expr.NumberLiteral("2")) + ), + tokens.Expr.RecordLiteral.Field( + // tokens.Expr.OpCall( + // tokens.Id("y"), + // tokens.Expr.OpCall.Params() + // ), + tokens.Id("y"), + tokens.Expr(tokens.Expr.NumberLiteral("3")) + ), ) ) ) + + test("Name"): + assertEquals( + "x".parseStr, + Node.Top( + tokens.Expr.OpCall( + tokens.Id("x"), + tokens.Expr.OpCall.Params() + ))) test("Single Binary Operator"): assertEquals( @@ -87,10 +125,7 @@ class ExprParserTests extends munit.FunSuite: tokens.Expr.OpCall.Params( tokens.Expr(tokens.Expr.NumberLiteral("5")), tokens.Expr(tokens.Expr.NumberLiteral("6")) - ) - ) - ) - ) + )))) assertEquals( "5 $ 6".parseStr, Node.Top( @@ -99,10 +134,7 @@ class ExprParserTests extends munit.FunSuite: tokens.Expr.OpCall.Params( tokens.Expr(tokens.Expr.NumberLiteral("5")), tokens.Expr(tokens.Expr.NumberLiteral("6")) - ) - ) - ) - ) + )))) test("ParenthesesGroup"): assertEquals( @@ -123,10 +155,7 @@ class ExprParserTests extends munit.FunSuite: tokens.Expr.OpCall.Params( tokens.Expr(tokens.Expr.NumberLiteral("5")), tokens.Expr(tokens.Expr.NumberLiteral("6")) - ) - ) - ) - ) + )))) assertEquals( "(1 + 2) * 3".parseStr, Node.Top( @@ -145,7 +174,4 @@ class ExprParserTests extends munit.FunSuite: ) )), tokens.Expr(tokens.Expr.NumberLiteral("3")) - ) - ) - ) - ) \ No newline at end of file + )))) \ No newline at end of file diff --git a/tla/package.scala b/tla/package.scala index 16b5149..c332fea 100644 --- a/tla/package.scala +++ b/tla/package.scala @@ -170,6 +170,7 @@ val wellformed: Wellformed = t.Expr.TupleLiteral, t.Expr.RecordLiteral, t.Expr.Project, + t.Expr.RecordSetLiteral, t.Expr.OpCall, t.Expr.FnCall, t.Expr.If, From 871afa5579f921562b19fd7a4932fcea17782eee Mon Sep 17 00:00:00 2001 From: Kuter Bora Date: Wed, 19 Feb 2025 01:01:40 -0800 Subject: [PATCH 3/9] Parsing If, Case, Sets, Records, Projection --- tla/ExprParser.scala | 107 ++++++++++++++++++++++++++++++---- tla/ExprParser.test.scala | 117 ++++++++++++++++++++++++++++++++------ 2 files changed, 197 insertions(+), 27 deletions(-) diff --git a/tla/ExprParser.scala b/tla/ExprParser.scala index cea6a60..3d6ce88 100644 --- a/tla/ExprParser.scala +++ b/tla/ExprParser.scala @@ -30,6 +30,7 @@ object ExprParser extends PassSeq: tokens.Expr.importFrom(tla.wellformed) tokens.Expr.addCases(tokens.Expr) + // TODO: assign the correct source with .like() pass(once = false, strategy = pass.bottomUp) .rules: on( @@ -69,7 +70,7 @@ object ExprParser extends PassSeq: parent(tokens.Expr) *> tok(TLAReader.SqBracketsGroup) *> children: - repeatedSepBy(`,`)( + repeatedSepBy1(`,`)( field(TLAReader.Alpha) ~ skip(`|->`) ~ field(rawExpression) @@ -86,10 +87,57 @@ object ExprParser extends PassSeq: expr.mkNode ) )))) - // TODO: Project + // TOOD: projection should match before Names are assigned | on( parent(tokens.Expr) *> - TLAReader.Alpha + field(tokens.Expr.withChildren( + field(tokens.Expr.OpCall) + ~ eof + )) // TODO: can this be a function call? as in, can param be non empty? + ~ skip(tok(defns.`.`)) + ~ field(tokens.Expr.withChildren( + field(tokens.Expr.OpCall.withChildren( + field(tokens.Id) + ~ skip(tokens.Expr.OpCall.Params) // TODO: these have to be empty + ~ eof + )) + ~ eof + )) + ~ trailing + ).rewrite: (id1, id2) => + splice( + tokens.Expr( + tokens.Expr.Project( + tokens.Expr( + id1.unparent() + ), + id2.unparent() + ))) + | on( // TODO: is this even legal? + parent(tokens.Expr) *> + field(tokens.Expr) // TODO: ensure this is a record? + ~ skip(tok(defns.`.`)) + ~ field(tokens.Expr.withChildren( + field(tokens.Expr.OpCall.withChildren( + field(tokens.Id) + ~ skip(tokens.Expr.OpCall.Params) // TODO: these have to be empty + ~ eof + )) + ~ eof + )) + ~ trailing + ).rewrite: (expr, id) => + splice( + tokens.Expr( + tokens.Expr.Project( + expr.unparent(), + id.unparent() + ))) + // TODO: second project + // TODO: recordSetLiteral + | on( + parent(tokens.Expr) *> + TLAReader.Alpha ).rewrite: name => splice( tokens.Expr( @@ -97,27 +145,66 @@ object ExprParser extends PassSeq: tokens.Id().like(name), tokens.Expr.OpCall.Params(), ))) - | on( + // TODO: calls + | on( parent(tokens.Expr) *> field(tokens.Expr) - ~ field(tok(defns.InfixOperator.instances*)) + // TODO: proper filter + ~ field(tok(defns.InfixOperator.instances.filter(i => i.highPredecence < 17)*)) ~ field(tokens.Expr) ~ trailing ).rewrite: (left, op, right) => splice( tokens.Expr( - tokens.Expr - .OpCall( + tokens.Expr.OpCall( tokens.OpSym(op.unparent()), tokens.Expr.OpCall.Params(left.unparent(), right.unparent()) ) .like(op) )) // ~ field(tok(defns.InfixOperator.instances.filter(_.isAssociative)*)) - // TODO: other kinds of OpCalls + // TODO: prefix + // TODO: infix assoc + // TODO: infix non assoc // TODO: Fn Call - // TODO: if - // TODO: Case + | on( + parent(tokens.Expr) *> + skip(defns.IF) + ~ field(tokens.Expr) + ~ skip(defns.THEN) + ~ field(tokens.Expr) + ~ skip(defns.ELSE) + ~ field(tokens.Expr) + ~ trailing + ).rewrite: (pred, t, f) => + splice( + tokens.Expr.If( + pred.unparent(), + t.unparent(), + f.unparent() + )) + | on( + parent(tokens.Expr) *> + skip(defns.CASE) + ~ field( + repeatedSepBy(defns.`[]`)( + field(tokens.Expr) + ~ skip(defns.-) + ~ skip(defns.>) + ~ field(tokens.Expr) + ~ trailing + )) + ~ eof + // TODO: optional OTHER + ).rewrite: cases => + splice( + tokens.Expr( + tokens.Expr.Case( + cases.iterator.map((pred, branch) => + tokens.Expr.Case.Branch( + pred.unparent(), + branch.unparent(), + ))))) // TODO: Let // TODO: Exists // TODO: Forall diff --git a/tla/ExprParser.test.scala b/tla/ExprParser.test.scala index c20a278..6d1bf67 100644 --- a/tla/ExprParser.test.scala +++ b/tla/ExprParser.test.scala @@ -86,25 +86,45 @@ class ExprParserTests extends munit.FunSuite: Node.Top( tokens.Expr.RecordLiteral( tokens.Expr.RecordLiteral.Field( - // tokens.Expr.OpCall( - // tokens.Id("x"), - // tokens.Expr.OpCall.Params() - // ), tokens.Id("x"), tokens.Expr(tokens.Expr.NumberLiteral("2")) ), tokens.Expr.RecordLiteral.Field( - // tokens.Expr.OpCall( - // tokens.Id("y"), - // tokens.Expr.OpCall.Params() - // ), tokens.Id("y"), tokens.Expr(tokens.Expr.NumberLiteral("3")) - ), - ) - ) - ) + )))) + + // TODO: test record set + test("Projection (Record Field Acess)"): + assertEquals( + "x.y".parseStr, + Node.Top( + tokens.Expr.Project( + tokens.Expr( + tokens.Expr.OpCall( + tokens.Id("x"), + tokens.Expr.OpCall.Params() + )), + tokens.Id("y")))) + assertEquals( + "[y |-> 2].y".parseStr, + Node.Top( + tokens.Expr.Project( + tokens.Expr( + tokens.Expr.RecordLiteral( + tokens.Expr.RecordLiteral.Field( + tokens.Id("y"), + tokens.Expr(tokens.Expr.NumberLiteral("2")) + ) + )), + tokens.Id("y")))) + // TODO: r["f"] and [x -> 1]["x"] + // assertEquals( + // "x[\"y\"]".parseStr, + // Node.Top() + // ) + test("Name"): assertEquals( "x".parseStr, @@ -127,14 +147,74 @@ class ExprParserTests extends munit.FunSuite: tokens.Expr(tokens.Expr.NumberLiteral("6")) )))) assertEquals( - "5 $ 6".parseStr, + "5 $ x".parseStr, Node.Top( tokens.Expr.OpCall( tokens.OpSym(defns.$("$")), tokens.Expr.OpCall.Params( tokens.Expr(tokens.Expr.NumberLiteral("5")), - tokens.Expr(tokens.Expr.NumberLiteral("6")) + tokens.Expr( + tokens.Expr.OpCall( + tokens.Id("x"), + tokens.Expr.OpCall.Params() + )))))) + + // TODO: test calls + + test("If"): + assertEquals( + """IF A + |THEN 1 + |ELSE 2""".stripMargin.parseStr, + Node.Top( + tokens.Expr.If( + tokens.Expr( + tokens.Expr.OpCall( + tokens.Id("A"), + tokens.Expr.OpCall.Params() + )), + tokens.Expr(tokens.Expr.NumberLiteral("1")), + tokens.Expr(tokens.Expr.NumberLiteral("2")) + ))) + + test("Case"): + assertEquals( + """CASE A -> 1 + | [] B -> 2""".stripMargin.parseStr, + Node.Top( + tokens.Expr.Case( + tokens.Expr.Case.Branch( + tokens.Expr(tokens.Expr.OpCall( + tokens.Id("A"), + tokens.Expr.OpCall.Params() + )), + tokens.Expr(tokens.Expr.NumberLiteral("1")) + ), + tokens.Expr.Case.Branch( + tokens.Expr(tokens.Expr.OpCall( + tokens.Id("B"), + tokens.Expr.OpCall.Params() + )), + tokens.Expr(tokens.Expr.NumberLiteral("2")) )))) + // TODO: test optional OTHER + // assertEquals( + // """CASE A -> 1 + // | [] B -> 2 + // | OTHER -> 3""".stripMargin.parseStr, + // Node.Top( + // ) + // ) + + // TODO: test Let + // TODO: test Exists + // TODO: test Forall + // TODO: test Function + // TODO: test SetComprehension + // TODO: test SetRefinement + // TODO: test Choose + // TODO: test Except + // TODO: test Lambda test("ParenthesesGroup"): assertEquals( @@ -142,9 +222,12 @@ class ExprParserTests extends munit.FunSuite: Node.Top(tokens.Expr.NumberLiteral("1")) ) assertEquals( - "(((1)))".parseStr, - Node.Top(tokens.Expr.NumberLiteral("1")) - ) + "(((x)))".parseStr, + Node.Top( + tokens.Expr.OpCall( + tokens.Id("x"), + tokens.Expr.OpCall.Params() + ))) assertEquals( "(5 + 6)".parseStr, Node.Top( From c75939d003cb6bb338db8f75afbc528709fdb0f6 Mon Sep 17 00:00:00 2001 From: Kuter Bora Date: Tue, 4 Mar 2025 21:04:45 -0800 Subject: [PATCH 4/9] op precedence attempts --- tla/ExprParser.scala | 463 ++++++++++++++++++++++++++++++-------- tla/ExprParser.test.scala | 292 +++++++++++++++++------- tla/defns.scala | 2 +- tla/package.scala | 13 +- 4 files changed, 590 insertions(+), 180 deletions(-) diff --git a/tla/ExprParser.scala b/tla/ExprParser.scala index 3d6ce88..98db250 100644 --- a/tla/ExprParser.scala +++ b/tla/ExprParser.scala @@ -8,6 +8,7 @@ import distcompiler.Builtin.{Error, SourceMarker} import distcompiler.tla.TLAReader import distcompiler.tla.TLAParser.rawExpression import distcompiler.Manip.ops.pass.bottomUp +import distcompiler.tla.defns.THEOREM object ExprParser extends PassSeq: import distcompiler.dsl.* @@ -21,19 +22,35 @@ object ExprParser extends PassSeq: TLAReader.StringLiteral, TLAReader.NumberLiteral, TLAReader.TupleGroup + // TODO: remove cases ) TLAReader.groupTokens.foreach: tok => tok.removeCases(removedCases*) tok.addCases(tokens.Expr) + tokens.Expr.TmpInfixGroup ::= fields( + choice(defns.InfixOperator.instances*), + tokens.Expr, + tokens.Expr + ) + tokens.Expr.deleteShape() tokens.Expr.importFrom(tla.wellformed) - tokens.Expr.addCases(tokens.Expr) + tokens.Expr.addCases(tokens.Expr, tokens.Id, tokens.Expr.TmpInfixGroup) // TODO: assign the correct source with .like() pass(once = false, strategy = pass.bottomUp) .rules: on( + parent(tokens.Expr) *> + TLAReader.Alpha + ).rewrite: name => + splice( + // TODO??? + tokens.Expr( + tokens.Id().like(name) + )) + | on( parent(tokens.Expr) *> TLAReader.NumberLiteral ).rewrite: lit => @@ -70,119 +87,85 @@ object ExprParser extends PassSeq: parent(tokens.Expr) *> tok(TLAReader.SqBracketsGroup) *> children: - repeatedSepBy1(`,`)( - field(TLAReader.Alpha) - ~ skip(`|->`) - ~ field(rawExpression) - ~ trailing - ) + field( + repeatedSepBy1(`,`)( + field(TLAReader.Alpha) + ~ skip(`|->`) + ~ field(rawExpression) + ~ trailing + )) + ~ eof ).rewrite: fields => splice( tokens.Expr( tokens.Expr.RecordLiteral( fields.iterator.map( - (opCall, expr) => + (alpha, expr) => tokens.Expr.RecordLiteral.Field( - tokens.Id().like(opCall.unparent()), + tokens.Id().like(alpha.unparent()), expr.mkNode - ) - )))) - // TOOD: projection should match before Names are assigned + ))))) | on( parent(tokens.Expr) *> - field(tokens.Expr.withChildren( - field(tokens.Expr.OpCall) - ~ eof - )) // TODO: can this be a function call? as in, can param be non empty? - ~ skip(tok(defns.`.`)) + field(tokens.Expr) + ~ skip(defns.`.`) ~ field(tokens.Expr.withChildren( - field(tokens.Expr.OpCall.withChildren( - field(tokens.Id) - ~ skip(tokens.Expr.OpCall.Params) // TODO: these have to be empty - ~ eof - )) - ~ eof - )) + field(tokens.Id) + ~ eof + )) ~ trailing - ).rewrite: (id1, id2) => + ).rewrite: (expr, id) => splice( tokens.Expr( tokens.Expr.Project( tokens.Expr( - id1.unparent() + expr.unparent() ), - id2.unparent() - ))) - | on( // TODO: is this even legal? - parent(tokens.Expr) *> - field(tokens.Expr) // TODO: ensure this is a record? - ~ skip(tok(defns.`.`)) - ~ field(tokens.Expr.withChildren( - field(tokens.Expr.OpCall.withChildren( - field(tokens.Id) - ~ skip(tokens.Expr.OpCall.Params) // TODO: these have to be empty - ~ eof - )) - ~ eof - )) - ~ trailing - ).rewrite: (expr, id) => - splice( - tokens.Expr( - tokens.Expr.Project( - expr.unparent(), id.unparent() ))) - // TODO: second project - // TODO: recordSetLiteral | on( parent(tokens.Expr) *> - TLAReader.Alpha - ).rewrite: name => + tok(TLAReader.SqBracketsGroup) *> + children: + field( + repeatedSepBy1(`,`)( + field(TLAReader.Alpha) + ~ skip(`:`) + ~ field(rawExpression) + ~ trailing + )) + ~ eof + ).rewrite: fields => splice( tokens.Expr( - tokens.Expr.OpCall( - tokens.Id().like(name), - tokens.Expr.OpCall.Params(), - ))) - // TODO: calls + tokens.Expr.RecordSetLiteral( + fields.iterator.map( + (alpha, expr) => + tokens.Expr.RecordSetLiteral.Field( + tokens.Id().like(alpha.unparent()), + expr.mkNode + ))))) + // TODO: all OpCall | on( parent(tokens.Expr) *> field(tokens.Expr) - // TODO: proper filter - ~ field(tok(defns.InfixOperator.instances.filter(i => i.highPredecence < 17)*)) + ~ field(tok(defns.InfixOperator.instances.filter(i => i.highPrecedence < 17)*)) // TODO: probably dont do this filter ~ field(tokens.Expr) - ~ trailing + ~ eof // eof here? ).rewrite: (left, op, right) => + println("\nFound Op: " + op + "Rewriting as: \n") + println(tokens.Expr(tokens.Expr.TmpInfixGroup( + op.unparent(), + left.unparent(), + right.unparent() + ))) splice( - tokens.Expr( - tokens.Expr.OpCall( - tokens.OpSym(op.unparent()), - tokens.Expr.OpCall.Params(left.unparent(), right.unparent()) - ) - .like(op) - )) - // ~ field(tok(defns.InfixOperator.instances.filter(_.isAssociative)*)) - // TODO: prefix - // TODO: infix assoc - // TODO: infix non assoc + tokens.Expr(tokens.Expr.TmpInfixGroup( + op.unparent(), + left.unparent(), + right.unparent() + ))) // TODO: Fn Call - | on( - parent(tokens.Expr) *> - skip(defns.IF) - ~ field(tokens.Expr) - ~ skip(defns.THEN) - ~ field(tokens.Expr) - ~ skip(defns.ELSE) - ~ field(tokens.Expr) - ~ trailing - ).rewrite: (pred, t, f) => - splice( - tokens.Expr.If( - pred.unparent(), - t.unparent(), - f.unparent() - )) | on( parent(tokens.Expr) *> skip(defns.CASE) @@ -194,20 +177,67 @@ object ExprParser extends PassSeq: ~ field(tokens.Expr) ~ trailing )) + ~ field( + optional( + skip(defns.OTHER) + ~ skip(defns.-) + ~ skip(defns.>) + ~ field(tokens.Expr) + ~ eof + ) + ) ~ eof - // TODO: optional OTHER - ).rewrite: cases => + ).rewrite: (cases, other) => splice( tokens.Expr( tokens.Expr.Case( - cases.iterator.map((pred, branch) => - tokens.Expr.Case.Branch( - pred.unparent(), - branch.unparent(), - ))))) - // TODO: Let - // TODO: Exists - // TODO: Forall + tokens.Expr.Case.Branches( + cases.iterator.map((pred, branch) => + tokens.Expr.Case.Branch( + pred.unparent(), + branch.unparent(), + ))), + tokens.Expr.Case.Other( + other match + case None => tokens.Expr.Case.Other.None() + case Some(expr) => expr.unparent() + ) + ))) + | on( + parent(tokens.Expr) *> + field(tok(TLAReader.LetGroup).product( + children( + field( + repeated1: + tok(tokens.Operator) // ???: is this correct usage of | + | tok(tokens.ModuleDefinition) + | tok(tokens.Recursive) + ) + ~ eof + ) + )) + ~ field(tokens.Expr) + ~ trailing + ).rewrite: (let, expr) => + splice( + tokens.Expr( + tokens.Expr.Let( + tokens.Expr.Let.Defns( + let._2.iterator.map(_.unparent()) + ), + expr.unparent() + )).like(let._1) + ) + // ???: Exists and Forall + // | on( + // parent(tokens.Expr) *> + // field(TLAReader.LaTexLike) + // ~ field(tokens.Expr) + // ~ field(TLAReader.`:`) + // ~ field(tokens.Expr) + // ~ eof + // ).rewrite: thing => + // ??? // TODO: Function // TODO: SetComprehension // TODO: SetRefinement @@ -224,8 +254,251 @@ object ExprParser extends PassSeq: splice( tokens.Expr(expr.mkNode) ) + | on( + parent(tokens.Expr) *> + skip(defns.IF) + ~ field(tokens.Expr) + ~ skip(defns.THEN) + ~ field(tokens.Expr) + ~ skip(defns.ELSE) + ~ field(tokens.Expr) + ~ trailing + ).rewrite: (pred, t, f) => + splice( + tokens.Expr.If( + pred.unparent(), + t.unparent(), + f.unparent() + )) end buildExpressions + val orderOperations = passDef: + wellformed := prevWellformed.makeDerived: + tokens.Expr.TmpInfixGroup.Checked ::= fields( + choice(defns.InfixOperator.instances*), + tokens.Expr, + tokens.Expr + ) + tokens.Expr.removeCases(tokens.Expr.TmpInfixGroup) + tokens.Expr.addCases(tokens.Expr.TmpInfixGroup.Checked) + + pass(once = false, strategy = pass.bottomUp) + .rules: + on( + parent(tokens.Expr) *> + field(tokens.Expr.TmpInfixGroup.withChildren( + field(tok(defns.InfixOperator.instances*)) + ~ field(tokens.Expr.withChildren( + field(tokens.Expr.TmpInfixGroup.Checked.withChildren( + field(tok(defns.InfixOperator.instances*)) + ~ field(tokens.Expr) + ~ field(tokens.Expr) + ~ eof + )) + ~ eof + )) + ~ field(tokens.Expr) + ~ eof + )) + ~ eof + ).rewrite: (cur_op, left, right) => + left match + case (op, expr1, expr2) => + (cur_op.token, op.token) match + case (cur_tok: defns.InfixOperator, child_tok: defns.InfixOperator) => + if (cur_tok.highPrecedence > child_tok.highPrecedence) { + println("\nbad order: rewriting left in: ") + println("\ncur_op: " + cur_op) + println("\nleft: " + left) + println("\nright: " + right) + println("\nas: " + + tokens.Expr.TmpInfixGroup( + op.unparent(), + expr1.unparent(), + tokens.Expr(tokens.Expr.TmpInfixGroup( + cur_op.unparent(), + expr2.unparent(), + right.unparent() + )))) + splice( + tokens.Expr.TmpInfixGroup( + op.unparent(), + expr1.unparent(), + tokens.Expr(tokens.Expr.TmpInfixGroup( + cur_op.unparent(), + expr2.unparent(), + right.unparent() + )))) + } else if (cur_tok.lowPrecedence < child_tok.lowPrecedence) { + println("\ngood order: Checked Left") + splice( + tokens.Expr.TmpInfixGroup.Checked( + cur_op.unparent(), + tokens.Expr(tokens.Expr.TmpInfixGroup.Checked( + op.unparent(), + expr1.unparent(), + expr2.unparent() + )), + right.unparent() + )) + } else if (cur_tok.isAssociative && child_tok.isAssociative) { + println("\nassoc found: Checked Left") + splice( + tokens.Expr.TmpInfixGroup.Checked( + cur_op.unparent(), + tokens.Expr(tokens.Expr.TmpInfixGroup.Checked( + op.unparent(), + expr1.unparent(), + expr2.unparent() + )), + right.unparent() + )) + } else { + println("\nError") + splice(tokens.Expr.SomeKindOfError()) + } + | on( + parent(tokens.Expr) *> + field(tokens.Expr.TmpInfixGroup.withChildren( + field(tok(defns.InfixOperator.instances*)) + ~ field(tokens.Expr) + ~ field(tokens.Expr.withChildren( + field(tokens.Expr.TmpInfixGroup.Checked.withChildren( + field(tok(defns.InfixOperator.instances*)) + ~ field(tokens.Expr) + ~ field(tokens.Expr) + ~ eof + )) + ~ eof + )) + ~ eof + )) + ~ eof + ).rewrite: (cur_op, left, right) => + right match + case (op, expr1, expr2) => + (cur_op.token, op.token) match + case (cur_tok: defns.InfixOperator, child_tok: defns.InfixOperator) => + if (cur_tok.highPrecedence > child_tok.highPrecedence) { + println("\nbad order: rewriting right in: ") + println("\ncur_op: " + cur_op) + println("\nleft: " + left) + println("\nright: " + right) + println("\n as:" + + tokens.Expr.TmpInfixGroup( + op.unparent(), + tokens.Expr(tokens.Expr.TmpInfixGroup( + cur_op.unparent(), + left.unparent(), + expr1.unparent() + )), + expr2.unparent())) + splice( + tokens.Expr.TmpInfixGroup( + op.unparent(), + tokens.Expr(tokens.Expr.TmpInfixGroup( + cur_op.unparent(), + left.unparent(), + expr1.unparent() + )), + expr2.unparent())) + } else if (cur_tok.lowPrecedence < child_tok.lowPrecedence) { + println("\ngood order: Checked Right") + splice( + tokens.Expr.TmpInfixGroup.Checked( + cur_op.unparent(), + left.unparent(), + tokens.Expr(tokens.Expr.TmpInfixGroup.Checked( + op.unparent(), + expr1.unparent(), + expr2.unparent() + )))) + } else if (cur_tok.isAssociative && child_tok.isAssociative) { + println("\nassoc found: Checked Right") + splice( + tokens.Expr.TmpInfixGroup.Checked( + cur_op.unparent(), + left.unparent(), + tokens.Expr(tokens.Expr.TmpInfixGroup.Checked( + op.unparent(), + expr1.unparent(), + expr2.unparent() + )))) + } else { + println("\nError") + splice(tokens.Expr.SomeKindOfError()) + } + | on( + parent(tokens.Expr) *> + field(tokens.Expr.TmpInfixGroup.withChildren( + field(tok(defns.InfixOperator.instances*)) + ~ field(tokens.Expr) + ~ field(tokens.Expr) + ~ trailing + )) + ~ trailing + ).rewrite: (op, left, right) => + println("\nchecking off :") + println("\nOp: " + op) + println("\nLeft: " + left) + println("\nRight: " + right) + println("\nAs: " + + tokens.Expr.TmpInfixGroup.Checked( + op.unparent(), + left.unparent(), + right.unparent() + )) + splice( + tokens.Expr.TmpInfixGroup.Checked( + op.unparent(), + left.unparent(), + right.unparent() + )) + end orderOperations + + val resolveOperations = passDef: + wellformed := prevWellformed.makeDerived: + tokens.Expr.removeCases(tokens.Expr.TmpInfixGroup.Checked) + + pass(once = false, strategy = pass.bottomUp) + .rules: + on( + parent(tokens.Expr) *> + field(tokens.Expr.TmpInfixGroup.Checked.withChildren( + field(tok(defns.InfixOperator.instances*)) + ~ field(tokens.Expr) + ~ field(tokens.Expr) + ~ eof + )) + ~ eof + ).rewrite: (op, right, left) => + splice( + tokens.Expr(tokens.Expr.OpCall( + tokens.OpSym(op.unparent()), + tokens.Expr.OpCall.Params( + right.unparent(), + left.unparent() + )))) + end resolveOperations + + val resolveAlphas = passDef: + wellformed := prevWellformed.makeDerived: + tokens.Expr.removeCases(tokens.Id) + + pass(once = false, strategy = pass.bottomUp) + .rules: + on( + parent(tokens.Expr) *> + tokens.Id + ).rewrite: name => + splice( + tokens.Expr( + tokens.Expr.OpCall( + name.unparent(), + tokens.Expr.OpCall.Params(), + ))) + end resolveAlphas + val removeNestedExpr = passDef: wellformed := prevWellformed.makeDerived: tokens.Expr.removeCases(tokens.Expr) diff --git a/tla/ExprParser.test.scala b/tla/ExprParser.test.scala index 6d1bf67..0cc9a02 100644 --- a/tla/ExprParser.test.scala +++ b/tla/ExprParser.test.scala @@ -69,6 +69,10 @@ class ExprParserTests extends munit.FunSuite: tokens.Expr(tokens.Expr.NumberLiteral("2")), tokens.Expr(tokens.Expr.NumberLiteral("3")) ))) + assertEquals( + "{}".parseStr, + Node.Top(tokens.Expr.SetLiteral()) + ) test("TupleLiteral"): assertEquals( @@ -79,6 +83,11 @@ class ExprParserTests extends munit.FunSuite: tokens.Expr(tokens.Expr.NumberLiteral("2")), tokens.Expr(tokens.Expr.NumberLiteral("3")) ))) + assertEquals( + "<<>>".parseStr, + Node.Top( + tokens.Expr.TupleLiteral() + )) test("RecordLiteral"): assertEquals( @@ -93,8 +102,6 @@ class ExprParserTests extends munit.FunSuite: tokens.Id("y"), tokens.Expr(tokens.Expr.NumberLiteral("3")) )))) - - // TODO: test record set test("Projection (Record Field Acess)"): assertEquals( @@ -107,6 +114,18 @@ class ExprParserTests extends munit.FunSuite: tokens.Expr.OpCall.Params() )), tokens.Id("y")))) + assertEquals( + "x.y.z".parseStr, + Node.Top( + tokens.Expr.Project( + tokens.Expr(tokens.Expr.Project( + tokens.Expr( + tokens.Expr.OpCall( + tokens.Id("x"), + tokens.Expr.OpCall.Params() + )), + tokens.Id("y"))), + tokens.Id("z")))) assertEquals( "[y |-> 2].y".parseStr, Node.Top( @@ -119,11 +138,19 @@ class ExprParserTests extends munit.FunSuite: ) )), tokens.Id("y")))) - // TODO: r["f"] and [x -> 1]["x"] - // assertEquals( - // "x[\"y\"]".parseStr, - // Node.Top() - // ) + + test("RecordSetLiteral"): + assertEquals( + "[x : {1, 2}]".parseStr, + Node.Top( + tokens.Expr.RecordSetLiteral( + tokens.Expr.RecordSetLiteral.Field( + tokens.Id("x"), + tokens.Expr( + tokens.Expr.SetLiteral( + tokens.Expr(tokens.Expr.NumberLiteral("1")), + tokens.Expr(tokens.Expr.NumberLiteral("2")) + )))))) test("Name"): assertEquals( @@ -134,32 +161,88 @@ class ExprParserTests extends munit.FunSuite: tokens.Expr.OpCall.Params() ))) - test("Single Binary Operator"): + // test("Single Binary Operator"): + // assertEquals( + // "5 + 6".parseStr, + // Node.Top( + // tokens.Expr.OpCall( + // tokens.OpSym( + // defns.+("+") + // ), + // tokens.Expr.OpCall.Params( + // tokens.Expr(tokens.Expr.NumberLiteral("5")), + // tokens.Expr(tokens.Expr.NumberLiteral("6")) + // )))) + // assertEquals( + // "5 $ x".parseStr, + // Node.Top( + // tokens.Expr.OpCall( + // tokens.OpSym(defns.$("$")), + // tokens.Expr.OpCall.Params( + // tokens.Expr(tokens.Expr.NumberLiteral("5")), + // tokens.Expr( + // tokens.Expr.OpCall( + // tokens.Id("x"), + // tokens.Expr.OpCall.Params() + // )))))) + + test("Precedence: Infix Operators"): assertEquals( - "5 + 6".parseStr, + "5 * 6 + 7".parseStr, Node.Top( tokens.Expr.OpCall( tokens.OpSym( defns.+("+") ), tokens.Expr.OpCall.Params( - tokens.Expr(tokens.Expr.NumberLiteral("5")), - tokens.Expr(tokens.Expr.NumberLiteral("6")) - )))) - assertEquals( - "5 $ x".parseStr, - Node.Top( - tokens.Expr.OpCall( - tokens.OpSym(defns.$("$")), - tokens.Expr.OpCall.Params( - tokens.Expr(tokens.Expr.NumberLiteral("5")), tokens.Expr( tokens.Expr.OpCall( - tokens.Id("x"), - tokens.Expr.OpCall.Params() - )))))) - - // TODO: test calls + tokens.OpSym( + defns.*("*") + ), + tokens.Expr.OpCall.Params( + tokens.Expr(tokens.Expr.NumberLiteral("5")), + tokens.Expr(tokens.Expr.NumberLiteral("6")) + ))), + tokens.Expr(tokens.Expr.NumberLiteral("7")))))) + // assertEquals( + // "1 + 8 * 6 - 9 * 3".parseStr, + // Node.Top()) + // Node.Top( + // tokens.Expr.OpCall( + // tokens.OpSym( + // defns.-("-") + // ), + // tokens.Expr.OpCall.Params( + // tokens.Expr.OpCall( + // tokens.OpSym( + // defns.+("+") + // ), + // tokens.Expr.OpCall.Params( + // tokens.Expr(tokens.Expr.NumberLiteral("1")), + // tokens.Expr( + // tokens.Expr.OpCall( + // tokens.OpSym( + // defns.*("*") + // ), + // tokens.Expr.OpCall.Params( + // tokens.Expr(tokens.Expr.NumberLiteral("8")), + // tokens.Expr(tokens.Expr.NumberLiteral("6")) + // ))))), + // tokens.Expr( + // tokens.Expr.OpCall( + // tokens.OpSym( + // defns.*("*") + // ), + // tokens.Expr.OpCall.Params( + // tokens.Expr(tokens.Expr.NumberLiteral("9")), + // tokens.Expr(tokens.Expr.NumberLiteral("3")) + // ))))))) + // test("FnCall"): ???: what about x[a, b, c] - needs to be parsed to (Expr, Expr) + // assertEquals( + // "x[\"y\"]".parseStr, + // Node.Top() + // ) test("If"): assertEquals( @@ -183,38 +266,83 @@ class ExprParserTests extends munit.FunSuite: | [] B -> 2""".stripMargin.parseStr, Node.Top( tokens.Expr.Case( - tokens.Expr.Case.Branch( - tokens.Expr(tokens.Expr.OpCall( - tokens.Id("A"), - tokens.Expr.OpCall.Params() + tokens.Expr.Case.Branches( + tokens.Expr.Case.Branch( + tokens.Expr(tokens.Expr.OpCall( + tokens.Id("A"), + tokens.Expr.OpCall.Params() + )), + tokens.Expr(tokens.Expr.NumberLiteral("1")) + ), + tokens.Expr.Case.Branch( + tokens.Expr(tokens.Expr.OpCall( + tokens.Id("B"), + tokens.Expr.OpCall.Params() + )), + tokens.Expr(tokens.Expr.NumberLiteral("2")) )), - tokens.Expr(tokens.Expr.NumberLiteral("1")) - ), - tokens.Expr.Case.Branch( - tokens.Expr(tokens.Expr.OpCall( - tokens.Id("B"), - tokens.Expr.OpCall.Params() + tokens.Expr.Case.Other(tokens.Expr.Case.Other.None()) + ))) + assertEquals( + """CASE A -> 1 + | [] B -> 2 + | OTHER -> 3""".stripMargin.parseStr, + Node.Top( + tokens.Expr.Case( + tokens.Expr.Case.Branches( + tokens.Expr.Case.Branch( + tokens.Expr(tokens.Expr.OpCall( + tokens.Id("A"), + tokens.Expr.OpCall.Params() + )), + tokens.Expr(tokens.Expr.NumberLiteral("1")) + ), + tokens.Expr.Case.Branch( + tokens.Expr(tokens.Expr.OpCall( + tokens.Id("B"), + tokens.Expr.OpCall.Params() + )), + tokens.Expr(tokens.Expr.NumberLiteral("2")) )), - tokens.Expr(tokens.Expr.NumberLiteral("2")) + tokens.Expr.Case.Other( + tokens.Expr(tokens.Expr.NumberLiteral("3")) )))) - // TODO: test optional OTHER - // assertEquals( - // """CASE A -> 1 - // | [] B -> 2 - // | OTHER -> 3""".stripMargin.parseStr, - // Node.Top( - // ) - // ) - // TODO: test Let - // TODO: test Exists - // TODO: test Forall - // TODO: test Function - // TODO: test SetComprehension - // TODO: test SetRefinement - // TODO: test Choose - // TODO: test Except - // TODO: test Lambda + test("LET"): + assertEquals( + """LET x == 1 + |y == 2 + |IN {y, x}""".stripMargin.parseStr, + Node.Top( + tokens.Expr.Let( + tokens.Expr.Let.Defns( + tokens.Operator( + tokens.Id("x"), + tokens.Operator.Params(), + tokens.Expr(tokens.Expr.NumberLiteral("1")) + ), + tokens.Operator( + tokens.Id("y"), + tokens.Operator.Params(), + tokens.Expr(tokens.Expr.NumberLiteral("2")) + ) + ), + tokens.Expr( + tokens.Expr.SetLiteral( + tokens.Expr(tokens.Expr.OpCall( + tokens.Id("y"), + tokens.Expr.OpCall.Params() + )), + tokens.Expr(tokens.Expr.OpCall( + tokens.Id("x"), + tokens.Expr.OpCall.Params() + ))))))) + + // test("Exists"): + // assertEquals( + // "\\E x \\in {1, 2, 3} : x = 2".parseStr, + // Node.Top() + // ) test("ParenthesesGroup"): assertEquals( @@ -228,33 +356,33 @@ class ExprParserTests extends munit.FunSuite: tokens.Id("x"), tokens.Expr.OpCall.Params() ))) - assertEquals( - "(5 + 6)".parseStr, - Node.Top( - tokens.Expr.OpCall( - tokens.OpSym( - defns.+("+") - ), - tokens.Expr.OpCall.Params( - tokens.Expr(tokens.Expr.NumberLiteral("5")), - tokens.Expr(tokens.Expr.NumberLiteral("6")) - )))) - assertEquals( - "(1 + 2) * 3".parseStr, - Node.Top( - tokens.Expr.OpCall( - tokens.OpSym( - defns.*("*") - ), - tokens.Expr.OpCall.Params( - tokens.Expr(tokens.Expr.OpCall( - tokens.OpSym( - defns.+("+") - ), - tokens.Expr.OpCall.Params( - tokens.Expr(tokens.Expr.NumberLiteral("1")), - tokens.Expr(tokens.Expr.NumberLiteral("2")) - ) - )), - tokens.Expr(tokens.Expr.NumberLiteral("3")) - )))) \ No newline at end of file + // assertEquals( + // "(5 + 6)".parseStr, + // Node.Top( + // tokens.Expr.OpCall( + // tokens.OpSym( + // defns.+("+") + // ), + // tokens.Expr.OpCall.Params( + // tokens.Expr(tokens.Expr.NumberLiteral("5")), + // tokens.Expr(tokens.Expr.NumberLiteral("6")) + // )))) + // assertEquals( + // "(1 + 2) * 3".parseStr, + // Node.Top( + // tokens.Expr.OpCall( + // tokens.OpSym( + // defns.*("*") + // ), + // tokens.Expr.OpCall.Params( + // tokens.Expr(tokens.Expr.OpCall( + // tokens.OpSym( + // defns.+("+") + // ), + // tokens.Expr.OpCall.Params( + // tokens.Expr(tokens.Expr.NumberLiteral("1")), + // tokens.Expr(tokens.Expr.NumberLiteral("2")) + // ) + // )), + // tokens.Expr(tokens.Expr.NumberLiteral("3")) + // )))) \ No newline at end of file diff --git a/tla/defns.scala b/tla/defns.scala index dcf1cb3..d3bd9e0 100644 --- a/tla/defns.scala +++ b/tla/defns.scala @@ -100,7 +100,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] diff --git a/tla/package.scala b/tla/package.scala index c332fea..a2c5020 100644 --- a/tla/package.scala +++ b/tla/package.scala @@ -201,7 +201,7 @@ val wellformed: Wellformed = t.Id ) t.Expr.RecordSetLiteral ::= repeated( - t.Expr.RecordLiteral.Field, + t.Expr.RecordSetLiteral.Field, minCount = 1 ) t.Expr.RecordSetLiteral.Field ::= fields( @@ -223,11 +223,20 @@ val wellformed: Wellformed = t.Expr ) - t.Expr.Case ::= repeated(t.Expr.Case.Branch, minCount = 1) + t.Expr.Case ::= fields( + t.Expr.Case.Branches, + t.Expr.Case.Other + ) + t.Expr.Case.Branches ::= repeated(t.Expr.Case.Branch, minCount = 1) t.Expr.Case.Branch ::= fields( t.Expr, t.Expr ) + t.Expr.Case.Other ::= choice( + t.Expr, + t.Expr.Case.Other.None + ) + t.Expr.Case.Other.None ::= Atom t.Expr.Let ::= fields( t.Expr.Let.Defns, From 6a8a30e9da1344566ad5bbfd0f09bd8da95962f7 Mon Sep 17 00:00:00 2001 From: Kuter Bora Date: Wed, 5 Mar 2025 16:37:40 -0800 Subject: [PATCH 5/9] precedence step 2 --- tla/ExprParser.test.scala | 86 ++++++++++++++++++--------------------- 1 file changed, 40 insertions(+), 46 deletions(-) diff --git a/tla/ExprParser.test.scala b/tla/ExprParser.test.scala index 0cc9a02..59f76c3 100644 --- a/tla/ExprParser.test.scala +++ b/tla/ExprParser.test.scala @@ -187,57 +187,51 @@ class ExprParserTests extends munit.FunSuite: // )))))) test("Precedence: Infix Operators"): + // assertEquals( + // "5 * 6 + 7".parseStr, + // Node.Top( + // tokens.Expr.OpCall( + // tokens.OpSym( + // defns.+("+") + // ), + // tokens.Expr.OpCall.Params( + // tokens.Expr( + // tokens.Expr.OpCall( + // tokens.OpSym( + // defns.*("*") + // ), + // tokens.Expr.OpCall.Params( + // tokens.Expr(tokens.Expr.NumberLiteral("5")), + // tokens.Expr(tokens.Expr.NumberLiteral("6")) + // ))), + // tokens.Expr(tokens.Expr.NumberLiteral("7")))))) assertEquals( - "5 * 6 + 7".parseStr, + "1 + 8 * 6 - 9 * 3".parseStr, Node.Top( tokens.Expr.OpCall( - tokens.OpSym( - defns.+("+") - ), + tokens.OpSym(defns.+("+")), tokens.Expr.OpCall.Params( - tokens.Expr( - tokens.Expr.OpCall( - tokens.OpSym( - defns.*("*") - ), - tokens.Expr.OpCall.Params( - tokens.Expr(tokens.Expr.NumberLiteral("5")), - tokens.Expr(tokens.Expr.NumberLiteral("6")) - ))), - tokens.Expr(tokens.Expr.NumberLiteral("7")))))) + tokens.Expr(tokens.Expr.NumberLiteral("1")), + tokens.Expr(tokens.Expr.OpCall( + tokens.OpSym(defns.-("-")), + tokens.Expr.OpCall.Params( + tokens.Expr(tokens.Expr.OpCall( + tokens.OpSym(defns.*("*")), + tokens.Expr.OpCall.Params( + tokens.Expr(tokens.Expr.NumberLiteral("8")), + tokens.Expr(tokens.Expr.NumberLiteral("6")) + ))), + tokens.Expr(tokens.Expr.OpCall( + tokens.OpSym(defns.*("*")), + tokens.Expr.OpCall.Params( + tokens.Expr(tokens.Expr.NumberLiteral("9")), + tokens.Expr(tokens.Expr.NumberLiteral("3")) + )))))))))) // assertEquals( - // "1 + 8 * 6 - 9 * 3".parseStr, - // Node.Top()) - // Node.Top( - // tokens.Expr.OpCall( - // tokens.OpSym( - // defns.-("-") - // ), - // tokens.Expr.OpCall.Params( - // tokens.Expr.OpCall( - // tokens.OpSym( - // defns.+("+") - // ), - // tokens.Expr.OpCall.Params( - // tokens.Expr(tokens.Expr.NumberLiteral("1")), - // tokens.Expr( - // tokens.Expr.OpCall( - // tokens.OpSym( - // defns.*("*") - // ), - // tokens.Expr.OpCall.Params( - // tokens.Expr(tokens.Expr.NumberLiteral("8")), - // tokens.Expr(tokens.Expr.NumberLiteral("6")) - // ))))), - // tokens.Expr( - // tokens.Expr.OpCall( - // tokens.OpSym( - // defns.*("*") - // ), - // tokens.Expr.OpCall.Params( - // tokens.Expr(tokens.Expr.NumberLiteral("9")), - // tokens.Expr(tokens.Expr.NumberLiteral("3")) - // ))))))) + // "1 + 1 + 3 * 4".parseStr, + // Node.Top() + // ) + // test("FnCall"): ???: what about x[a, b, c] - needs to be parsed to (Expr, Expr) // assertEquals( // "x[\"y\"]".parseStr, From 81e04c78c3a785f796a4571a3af0ecf6c865a06d Mon Sep 17 00:00:00 2001 From: Kuter Bora Date: Tue, 1 Apr 2025 20:52:35 -0700 Subject: [PATCH 6/9] conjunction alignment step 1 --- tla/ExprParser.scala | 913 +++++++++++++++++++++++++++++--------- tla/ExprParser.test.scala | 594 +++++++++++++++++++++---- tla/TLAParser.scala | 63 +++ tla/TLAParser.test.scala | 3 +- tla/defns.scala | 10 +- tla/package.scala | 5 +- 6 files changed, 1273 insertions(+), 315 deletions(-) diff --git a/tla/ExprParser.scala b/tla/ExprParser.scala index 98db250..3023e8e 100644 --- a/tla/ExprParser.scala +++ b/tla/ExprParser.scala @@ -9,12 +9,135 @@ import distcompiler.tla.TLAReader import distcompiler.tla.TLAParser.rawExpression import distcompiler.Manip.ops.pass.bottomUp import distcompiler.tla.defns.THEOREM +import distcompiler.tla.TLAParser.RawExpression +import distcompiler.tla.TLAParser.rawConjunction object ExprParser extends PassSeq: import distcompiler.dsl.* import distcompiler.Builtin.{Error, SourceMarker} import TLAReader.* def inputWellformed: Wellformed = TLAParser.outputWellformed + // TODO: make private + def highPredInfixInfix(op: defns.InfixOperator): SeqPattern[SeqPattern.Fields[Tuple1[(Node, Node, Node)]]] = + field(tokens.Expr.withChildren( + field(tokens.Expr.TmpInfixGroup.withChildren( + field(tok(defns.InfixOperator.instances*) + .filter(op2 => + op2.token match + case op2Token : defns.InfixOperator => + op.highPrecedence > op2Token.highPrecedence)) + ~ field(tokens.Expr) + ~ field(tokens.Expr) + ~ eof + )) + ~ eof + )) + def highPredInfixUnary(op: defns.InfixOperator): SeqPattern[SeqPattern.Fields[Tuple1[(Node, Node)]]] = + field(tokens.Expr.withChildren( + field(tokens.Expr.TmpUnaryGroup.withChildren( + field(tok(defns.PrefixOperator.instances*) + .filter(op2 => + op2.token match + case op2Token : defns.PrefixOperator => + op.highPrecedence > op2Token.highPrecedence + case op2Token : defns.PostfixOperator => + op.highPrecedence > op2Token.precedence)) + ~ field(tokens.Expr) + ~ eof + )) + ~ eof + )) + def highPredUnaryInfix(op: defns.Operator): SeqPattern[SeqPattern.Fields[Tuple1[(Node, Node, Node)]]] = + field(tokens.Expr.withChildren( + field(tokens.Expr.TmpInfixGroup.withChildren( + field(tok(defns.InfixOperator.instances*) + .filter(op2 => + op2.token match + case op2Token : defns.InfixOperator => + op.highPrecedence > op2Token.highPrecedence)) + ~ field(tokens.Expr) + ~ field(tokens.Expr) + ~ eof + )) + ~ eof + )) + + def badPredInfixInfix(op: defns.InfixOperator): SeqPattern[SeqPattern.Fields[Tuple1[(Node, Node, Node)]]] = + field(tokens.Expr.withChildren( + field(tokens.Expr.TmpInfixGroup.withChildren( + field(tok(defns.InfixOperator.instances*) + .filter(op2 => + op2.token match + case op2Token : defns.InfixOperator => + !((op.highPrecedence > op2Token.highPrecedence) + || (op.lowPrecedence < op2Token.lowPrecedence) + || ((op == op2Token) && op.isAssociative)) + )) + ~ field(tokens.Expr) + ~ field(tokens.Expr) + ~ eof + )) + ~ eof + )) + def badPredInfixUnary(op: defns.InfixOperator): SeqPattern[SeqPattern.Fields[Tuple1[(Node, Node)]]] = + field(tokens.Expr.withChildren( + field(tokens.Expr.TmpUnaryGroup.withChildren( + field(tok(defns.PrefixOperator.instances*) + .filter(op2 => + op2.token match + case op2Token : defns.PrefixOperator => + !((op.highPrecedence > op2Token.highPrecedence) + || (op.lowPrecedence < op2Token.lowPrecedence)) + case op2Token : defns.PostfixOperator => + !((op.highPrecedence > op2Token.precedence) + || (op.lowPrecedence < op2Token.precedence)))) + ~ field(tokens.Expr) + ~ eof + )) + ~ eof + )) + def badPredUnaryInfix(op: defns.Operator): SeqPattern[SeqPattern.Fields[Tuple1[(Node, Node, Node)]]] = + field(tokens.Expr.withChildren( + field(tokens.Expr.TmpInfixGroup.withChildren( + field(tok(defns.InfixOperator.instances*) + .filter(op2 => + op2.token match + case op2Token : defns.InfixOperator => + !((op.highPrecedence > op2Token.highPrecedence) + || (op.lowPrecedence < op2Token.lowPrecedence)))) + ~ field(tokens.Expr) + ~ field(tokens.Expr) + ~ eof + )) + ~ eof + )) + + def matchQuantifierId() :SeqPattern[(Node, TLAParser.RawExpression)] = + parent(tokens.Expr) *> + field(TLAReader.Alpha) + ~ skip(defns.`\\in`) + ~ field(rawExpression) + ~ trailing + def matchQuantifierIds() :SeqPattern[(List[Node], TLAParser.RawExpression)] = + parent(tokens.Expr) *> + field(tok(TLAReader.TupleGroup).withChildren( + field(repeatedSepBy(`,`)(tok(TLAReader.Alpha))) + ~ eof + )) + ~ skip(defns.`\\in`) + ~ field(rawExpression) + ~ trailing + + + // TODO??? Pass structure + + // conjunction alignment + // OpCall, QunatifierBound, Temporal Logic - set + // Literals, Let, If, Case, FnCall, TmpCall + // Resolve TmpCalls + // Check for assoc related errors + // Resolve Ids + // Remove parenthesis val buildExpressions = passDef: wellformed := prevWellformed.makeDerived: @@ -33,20 +156,204 @@ object ExprParser extends PassSeq: tokens.Expr, tokens.Expr ) + tokens.Expr.TmpUnaryGroup ::= fields( + choice((defns.PrefixOperator.instances ++ defns.PostfixOperator.instances)*), + tokens.Expr, + ) tokens.Expr.deleteShape() tokens.Expr.importFrom(tla.wellformed) - tokens.Expr.addCases(tokens.Expr, tokens.Id, tokens.Expr.TmpInfixGroup) + tokens.Expr.addCases( + tokens.Expr, + tokens.Expr.TmpInfixGroup, + tokens.Expr.TmpUnaryGroup) // TODO: assign the correct source with .like() - pass(once = false, strategy = pass.bottomUp) + // TODO??: find a more consistent order of passes + + pass(once = false, strategy = pass.bottomUp) // conjunction alignment + .rules: + on( + parent(tokens.Expr) *> + field( + (field(tok(defns./\)) + ~ field(rawConjunction) + ~ field(tok(defns./\)) + ~ field(rawConjunction) + ~ trailing + ).filter(things => + things match + case (and1 : Node, r1, and2 : Node, r2) => + val s1 = and1.sourceRange + val s2 = and2.sourceRange + // println("\nCol 1: " + s1.source.lines.lineColAtOffset(s1.offset)) + // println("\nCol 2: " + s2.source.lines.lineColAtOffset(s2.offset)) + s1.source.lines.lineColAtOffset(s1.offset)._2 == s2.source.lines.lineColAtOffset(s2.offset)._2 + )) + ~ eof + ).rewrite: (and1, r1, and2, r2) => + splice( + tokens.Expr( + and1.unparent(), + tokens.Expr.OpCall( + tokens.OpSym(and2.unparent()), + tokens.Expr.OpCall.Params( + r1.mkNode, + r2.mkNode + )))) + *> pass(once = false, strategy = pass.bottomUp) + // remove the leading /\, this should not be its own pass + // join with the prev once rawExpression2 is done + .rules: + on( + field(tokens.Expr.withChildren( + skip(defns./\) + ~ field(tokens.Expr) + ~ eof + )) + ~ eof + ).rewrite: expr => + splice(expr.unparent()) + | on( + field(tokens.Expr.withChildren( + skip(defns./\) + ~ field(rawExpression) + ~ eof + )) + ~ eof + ).rewrite: expr => + splice(expr.mkNode) + *> pass(once = false, strategy = pass.bottomUp) // resolve quantifiers/opCall + .rules: + on( + parent(tokens.Expr) *> + field(TLAReader.Alpha) + ~ field(TLAReader.ParenthesesGroup.withChildren( + field(repeatedSepBy(`,`)(rawExpression)) + ~ eof + )) + ~ trailing + ).rewrite: (fun, args) => + splice( + tokens.Expr(tokens.Expr.OpCall( + tokens.Id().like(fun), + tokens.Expr.OpCall.Params( + args.iterator.map(_.mkNode) + )))) + // TODO: Exists, Forall, Choose + // TODO: refactor and simplify + | on( + parent(tokens.Expr) *> + skip(tok(TLAReader.LaTexLike).src("\\E")) + ~ field(repeatedSepBy1(`,`)(matchQuantifierId())) + ~ skip(TLAReader.`:`) + ~ field(rawExpression) + ~ trailing + ).rewrite: (qBounds, expr) => + splice( + tokens.Expr(tokens.Expr.Exists( + tokens.QuantifierBounds( + qBounds.iterator.map( + (id, qExpr) => + tokens.QuantifierBound( + tokens.Id().like(id), + qExpr.mkNode + ))), + expr.mkNode + ))) + | on( + parent(tokens.Expr) *> + skip(tok(TLAReader.LaTexLike).src("\\E")) + ~ field(repeatedSepBy1(`,`)(matchQuantifierIds())) + ~ skip(TLAReader.`:`) + ~ field(rawExpression) + ~ trailing + ).rewrite: (qBounds, expr) => + splice( + tokens.Expr(tokens.Expr.Exists( + tokens.QuantifierBounds( + qBounds.iterator.map( + (ids, qExpr) => + tokens.QuantifierBound( + tokens.Ids( + ids.iterator.map( + id => tokens.Id().like(id) + ) + ), + qExpr.mkNode + ))), + expr.mkNode + ))) + | on( + parent(tokens.Expr) *> + skip(tok(TLAReader.LaTexLike).src("\\A")) + ~ field(repeatedSepBy1(`,`)(matchQuantifierId())) + ~ skip(TLAReader.`:`) + ~ field(rawExpression) + ~ trailing + ).rewrite: (qBounds, expr) => + splice( + tokens.Expr(tokens.Expr.Forall( + tokens.QuantifierBounds( + qBounds.iterator.map( + (id, qExpr) => + tokens.QuantifierBound( + tokens.Id().like(id), + qExpr.mkNode + ))), + expr.mkNode + ))) + | on( + parent(tokens.Expr) *> + skip(tok(TLAReader.LaTexLike).src("\\A")) + ~ field(repeatedSepBy1(`,`)(matchQuantifierIds())) + ~ skip(TLAReader.`:`) + ~ field(rawExpression) + ~ trailing + ).rewrite: (qBounds, expr) => + splice( + tokens.Expr(tokens.Expr.Forall( + tokens.QuantifierBounds( + qBounds.iterator.map( + (ids, qExpr) => + tokens.QuantifierBound( + tokens.Ids( + ids.iterator.map( + id => tokens.Id().like(id) + ) + ), + qExpr.mkNode + ))), + expr.mkNode + ))) + | on( + parent(tokens.Expr) *> + skip(tok(defns.CHOOSE)) + ~ field(matchQuantifierId()) + ~ skip(TLAReader.`:`) + ~ field(rawExpression) + ~ trailing + ).rewrite: (qBound, expr) => + qBound match + case (id, qExpr) => + splice( + tokens.Expr(tokens.Expr.Choose( + tokens.QuantifierBound( + tokens.Id().like(id), + qExpr.mkNode + ), + expr.mkNode + ))) + // TODO: tuple qbound + // id nil + // tuple nil + *> pass(once = false, strategy = pass.bottomUp) .rules: on( parent(tokens.Expr) *> TLAReader.Alpha ).rewrite: name => splice( - // TODO??? tokens.Expr( tokens.Id().like(name) )) @@ -145,27 +452,61 @@ object ExprParser extends PassSeq: tokens.Id().like(alpha.unparent()), expr.mkNode ))))) - // TODO: all OpCall | on( parent(tokens.Expr) *> field(tokens.Expr) - ~ field(tok(defns.InfixOperator.instances.filter(i => i.highPrecedence < 17)*)) // TODO: probably dont do this filter + ~ field(tok(defns.InfixOperator.instances.filter(_ != defns.`.`)*)) ~ field(tokens.Expr) - ~ eof // eof here? + ~ eof ).rewrite: (left, op, right) => - println("\nFound Op: " + op + "Rewriting as: \n") - println(tokens.Expr(tokens.Expr.TmpInfixGroup( + splice( + tokens.Expr(tokens.Expr.TmpInfixGroup( op.unparent(), left.unparent(), right.unparent() ))) + | on( + parent(tokens.Expr) *> + field(tok(defns.PrefixOperator.instances*)) + ~ field(tokens.Expr) + ~ eof + ).rewrite: (op, expr) => splice( - tokens.Expr(tokens.Expr.TmpInfixGroup( + tokens.Expr(tokens.Expr.TmpUnaryGroup( op.unparent(), - left.unparent(), - right.unparent() + expr.unparent(), ))) - // TODO: Fn Call + | on( + parent(tokens.Expr) *> + field(tokens.Expr) + ~ field(tok(defns.PostfixOperator.instances*)) + ~ trailing + ).rewrite: (expr, op) => + splice( + tokens.Expr(tokens.Expr.TmpUnaryGroup( + op.unparent(), + expr.unparent(), + ))) + | on( + parent(tokens.Expr) *> + field(tokens.Expr) + ~ field(tok(TLAReader.SqBracketsGroup) *> + children: + field(repeatedSepBy(`,`)(rawExpression)) + ~ eof + ) + ~ eof + ).rewrite: (callee, args) => + splice( + tokens.Expr(tokens.Expr.FnCall( + callee.unparent(), + args match + case List(expr) => + expr.mkNode + case _ => + tokens.Expr(tokens.Expr.TupleLiteral( + args.iterator.map(_.mkNode) + ))))) | on( parent(tokens.Expr) *> skip(defns.CASE) @@ -209,7 +550,7 @@ object ExprParser extends PassSeq: children( field( repeated1: - tok(tokens.Operator) // ???: is this correct usage of | + tok(tokens.Operator) | tok(tokens.ModuleDefinition) | tok(tokens.Recursive) ) @@ -228,22 +569,14 @@ object ExprParser extends PassSeq: expr.unparent() )).like(let._1) ) - // ???: Exists and Forall - // | on( - // parent(tokens.Expr) *> - // field(TLAReader.LaTexLike) - // ~ field(tokens.Expr) - // ~ field(TLAReader.`:`) - // ~ field(tokens.Expr) - // ~ eof - // ).rewrite: thing => - // ??? // TODO: Function - // TODO: SetComprehension - // TODO: SetRefinement + // TODO: SetComprehension {expr : x \in y} + // TODO: SetRefinement {x \in y : bool} + // {x \in y : p \in q} TODO: look in the book // TODO: Choose // TODO: Except // TODO: Lambda + // TODO a \x b \ a | on( parent(tokens.Expr) *> tok(TLAReader.ParenthesesGroup) *> @@ -270,234 +603,372 @@ object ExprParser extends PassSeq: t.unparent(), f.unparent() )) + *> pass(once = false, strategy = pass.bottomUp) // resolve Alphas + .rules: + on( + parent(tokens.Expr) *> + tokens.Id + ).rewrite: name => + splice( + tokens.Expr( + tokens.Expr.OpCall( + name.unparent(), + tokens.Expr.OpCall.Params(), + ))) end buildExpressions - val orderOperations = passDef: + val reorderOperations = passDef: wellformed := prevWellformed.makeDerived: - tokens.Expr.TmpInfixGroup.Checked ::= fields( - choice(defns.InfixOperator.instances*), - tokens.Expr, - tokens.Expr - ) - tokens.Expr.removeCases(tokens.Expr.TmpInfixGroup) - tokens.Expr.addCases(tokens.Expr.TmpInfixGroup.Checked) - + tokens.Expr.removeCases( + tokens.Expr.TmpInfixGroup, + tokens.Expr.TmpUnaryGroup) pass(once = false, strategy = pass.bottomUp) .rules: on( parent(tokens.Expr) *> - field(tokens.Expr.TmpInfixGroup.withChildren( - field(tok(defns.InfixOperator.instances*)) - ~ field(tokens.Expr.withChildren( - field(tokens.Expr.TmpInfixGroup.Checked.withChildren( - field(tok(defns.InfixOperator.instances*)) - ~ field(tokens.Expr) - ~ field(tokens.Expr) - ~ eof - )) - ~ eof - )) - ~ field(tokens.Expr) - ~ eof - )) + field(tokens.Expr.TmpInfixGroup.withChildren: + defns.InfixOperator.instances + .iterator + .map: op => + field(op) + ~ highPredInfixInfix(op) + ~ field(tokens.Expr) + ~ eof + .reduce(_ | _)) ~ eof - ).rewrite: (cur_op, left, right) => + ).rewrite: (curOp, left, right) => left match case (op, expr1, expr2) => - (cur_op.token, op.token) match - case (cur_tok: defns.InfixOperator, child_tok: defns.InfixOperator) => - if (cur_tok.highPrecedence > child_tok.highPrecedence) { - println("\nbad order: rewriting left in: ") - println("\ncur_op: " + cur_op) - println("\nleft: " + left) - println("\nright: " + right) - println("\nas: " + + splice( + tokens.Expr.TmpInfixGroup( + op.unparent(), + expr1.unparent(), + tokens.Expr(tokens.Expr.TmpInfixGroup( + curOp.unparent(), + expr2.unparent(), + right.unparent() + )))) + | on( + parent(tokens.Expr) *> + field(tokens.Expr.TmpInfixGroup.withChildren: + defns.InfixOperator.instances + .iterator + .map: op => + field(op) + ~ field(tokens.Expr) + ~ highPredInfixInfix(op) + ~ eof + .reduce(_ | _)) + ~ eof + ).rewrite: (curOp, left, right) => + right match + case (op, expr1, expr2) => + splice( + tokens.Expr.TmpInfixGroup( + op.unparent(), + tokens.Expr(tokens.Expr.TmpInfixGroup( + curOp.unparent(), + left.unparent(), + expr1.unparent() + )), + expr2.unparent())) + | on( + parent(tokens.Expr) *> + field(tokens.Expr.TmpInfixGroup.withChildren: + defns.InfixOperator.instances + .iterator + .map: op => + field(op) + ~ highPredInfixUnary(op) + ~ field(tokens.Expr) + ~ eof + .reduce(_ | _)) + ~ eof + ).rewrite: (curOp, left, right) => + left match + case (op, expr) => + splice( + tokens.Expr.TmpUnaryGroup( + op.unparent(), + tokens.Expr(tokens.Expr.TmpInfixGroup( + curOp.unparent(), + expr.unparent(), + right.unparent() + )))) + | on( + parent(tokens.Expr) *> + field(tokens.Expr.TmpInfixGroup.withChildren: + defns.InfixOperator.instances + .iterator + .map: op => + field(op) + ~ field(tokens.Expr) + ~ highPredInfixUnary(op) + ~ eof + .reduce(_ | _)) + ~ eof + ).rewrite: (curOp, left, right) => + right match + case (op, expr) => + splice( + tokens.Expr.TmpUnaryGroup( + op.unparent(), + tokens.Expr(tokens.Expr.TmpInfixGroup( + curOp.unparent(), + left.unparent(), + expr.unparent() + )))) + | on( + parent(tokens.Expr) *> + field(tokens.Expr.TmpUnaryGroup.withChildren: + defns.PrefixOperator.instances + .iterator + .map: op => + field(op) + ~ highPredUnaryInfix(op) + ~ eof + .reduce(_ | _)) + ~ eof + ).rewrite: (curOp, infixGroup) => + infixGroup match + case (op, left, right) => + splice( + tokens.Expr.TmpInfixGroup( + op.unparent(), + tokens.Expr(tokens.Expr.TmpUnaryGroup( + curOp.unparent(), + left.unparent() + )), + right.unparent())) + | on( + parent(tokens.Expr) *> + field(tokens.Expr.TmpUnaryGroup.withChildren: + defns.PostfixOperator.instances + .iterator + .map: op => + field(op) + ~ highPredUnaryInfix(op) + ~ eof + .reduce(_ | _)) + ~ eof + ).rewrite: (curOp, infixGroup) => + infixGroup match + case (op, left, right) => + splice( + tokens.Expr.TmpInfixGroup( + op.unparent(), + left.unparent(), + tokens.Expr(tokens.Expr.TmpUnaryGroup( + curOp.unparent(), + right.unparent() + )))) + *> pass(once = false, strategy = pass.bottomUp) // assoc related errors + .rules: + on( + parent(tokens.Expr) *> + field(tokens.Expr.TmpInfixGroup.withChildren: + defns.InfixOperator.instances + .iterator + .map: op => + field(op) + ~ badPredInfixInfix(op) + ~ field(tokens.Expr) + ~ eof + .reduce(_ | _)) + ~ eof + ).rewrite: (curOp, left, right) => + left match + case (op, expr1, expr2) => + splice( + Node(Builtin.Error)( + Builtin.Error.Message( // todo: use src + s"$curOp and $op must have different precedence, or be duplicates of an associative operator." + ), + Builtin.Error.AST( + tokens.Expr.TmpInfixGroup( + curOp.unparent(), tokens.Expr.TmpInfixGroup( op.unparent(), expr1.unparent(), - tokens.Expr(tokens.Expr.TmpInfixGroup( - cur_op.unparent(), - expr2.unparent(), - right.unparent() - )))) - splice( + expr2.unparent() + ), + right.unparent())))) + | on( + parent(tokens.Expr) *> + field(tokens.Expr.TmpInfixGroup.withChildren: + defns.InfixOperator.instances + .iterator + .map: op => + field(op) + ~ field(tokens.Expr) + ~ badPredInfixInfix((op)) + ~ eof + .reduce(_ | _)) + ~ eof + ).rewrite: (curOp, left, right) => + right match + case (op, expr1, expr2) => + splice( + Node(Builtin.Error)( + Builtin.Error.Message( + s"$curOp and $op must have different precedence, or be duplicates of an associative operator." + ), + Builtin.Error.AST( + tokens.Expr.TmpInfixGroup( + curOp.unparent(), + left.unparent(), tokens.Expr.TmpInfixGroup( op.unparent(), expr1.unparent(), - tokens.Expr(tokens.Expr.TmpInfixGroup( - cur_op.unparent(), - expr2.unparent(), - right.unparent() - )))) - } else if (cur_tok.lowPrecedence < child_tok.lowPrecedence) { - println("\ngood order: Checked Left") - splice( - tokens.Expr.TmpInfixGroup.Checked( - cur_op.unparent(), - tokens.Expr(tokens.Expr.TmpInfixGroup.Checked( - op.unparent(), - expr1.unparent(), - expr2.unparent() - )), - right.unparent() - )) - } else if (cur_tok.isAssociative && child_tok.isAssociative) { - println("\nassoc found: Checked Left") - splice( - tokens.Expr.TmpInfixGroup.Checked( - cur_op.unparent(), - tokens.Expr(tokens.Expr.TmpInfixGroup.Checked( - op.unparent(), - expr1.unparent(), - expr2.unparent() - )), - right.unparent() - )) - } else { - println("\nError") - splice(tokens.Expr.SomeKindOfError()) - } + expr2.unparent() + ))))) | on( parent(tokens.Expr) *> - field(tokens.Expr.TmpInfixGroup.withChildren( - field(tok(defns.InfixOperator.instances*)) - ~ field(tokens.Expr) - ~ field(tokens.Expr.withChildren( - field(tokens.Expr.TmpInfixGroup.Checked.withChildren( - field(tok(defns.InfixOperator.instances*)) - ~ field(tokens.Expr) - ~ field(tokens.Expr) - ~ eof - )) - ~ eof - )) - ~ eof - )) + field(tokens.Expr.TmpInfixGroup.withChildren: + defns.InfixOperator.instances + .iterator + .map: op => + field(op) + ~ badPredInfixUnary(op) + ~ field(tokens.Expr) + ~ eof + .reduce(_ | _)) ~ eof - ).rewrite: (cur_op, left, right) => + ).rewrite: (curOp, left, right) => + left match + case (op, expr) => + splice( + Node(Builtin.Error)( + Builtin.Error.Message( + s"$curOp and $op must have different precedence." + ), + Builtin.Error.AST( + tokens.Expr.TmpInfixGroup( + curOp.unparent(), + tokens.Expr.TmpUnaryGroup( + op.unparent(), + expr.unparent(), + )), + right.unparent() + ))) + | on( + parent(tokens.Expr) *> + field(tokens.Expr.TmpInfixGroup.withChildren: + defns.InfixOperator.instances + .iterator + .map: op => + field(op) + ~ field(tokens.Expr) + ~ badPredInfixUnary(op) + ~ eof + .reduce(_ | _)) + ~ eof + ).rewrite: (curOp, left, right) => right match - case (op, expr1, expr2) => - (cur_op.token, op.token) match - case (cur_tok: defns.InfixOperator, child_tok: defns.InfixOperator) => - if (cur_tok.highPrecedence > child_tok.highPrecedence) { - println("\nbad order: rewriting right in: ") - println("\ncur_op: " + cur_op) - println("\nleft: " + left) - println("\nright: " + right) - println("\n as:" + - tokens.Expr.TmpInfixGroup( + case (op, expr) => + splice( + Node(Builtin.Error)( + Builtin.Error.Message( + s"$curOp and $op must have different precedence." + ), + Builtin.Error.AST( + tokens.Expr.TmpInfixGroup( + curOp.unparent(), + left.unparent(), + tokens.Expr.TmpUnaryGroup( op.unparent(), - tokens.Expr(tokens.Expr.TmpInfixGroup( - cur_op.unparent(), - left.unparent(), - expr1.unparent() - )), - expr2.unparent())) - splice( + expr.unparent() + ))))) + | on( + parent(tokens.Expr) *> + field(tokens.Expr.TmpUnaryGroup.withChildren: + defns.PrefixOperator.instances + .iterator + .map: op => + field(op) + ~ badPredUnaryInfix(op) + ~ eof + .reduce(_ | _)) + ~ eof + ).rewrite: (curOp, infixGroup) => + infixGroup match + case (op, left, right) => + splice( + Node(Builtin.Error)( + Builtin.Error.Message( + s"$curOp and $op must have different precedence." + ), + Builtin.Error.AST( + tokens.Expr.UnaryGroup( + curOp.unparent(), tokens.Expr.TmpInfixGroup( op.unparent(), - tokens.Expr(tokens.Expr.TmpInfixGroup( - cur_op.unparent(), - left.unparent(), - expr1.unparent() - )), - expr2.unparent())) - } else if (cur_tok.lowPrecedence < child_tok.lowPrecedence) { - println("\ngood order: Checked Right") - splice( - tokens.Expr.TmpInfixGroup.Checked( - cur_op.unparent(), - left.unparent(), - tokens.Expr(tokens.Expr.TmpInfixGroup.Checked( - op.unparent(), - expr1.unparent(), - expr2.unparent() - )))) - } else if (cur_tok.isAssociative && child_tok.isAssociative) { - println("\nassoc found: Checked Right") - splice( - tokens.Expr.TmpInfixGroup.Checked( - cur_op.unparent(), left.unparent(), - tokens.Expr(tokens.Expr.TmpInfixGroup.Checked( - op.unparent(), - expr1.unparent(), - expr2.unparent() - )))) - } else { - println("\nError") - splice(tokens.Expr.SomeKindOfError()) - } + right.unparent() + ))))) | on( - parent(tokens.Expr) *> + parent(tokens.Expr) *> + field(tokens.Expr.TmpUnaryGroup.withChildren: + defns.PostfixOperator.instances + .iterator + .map: op => + field(op) + ~ badPredUnaryInfix(op) + ~ eof + .reduce(_ | _)) + ~ eof + ).rewrite: (curOp, infixGroup) => + infixGroup match + case (op, left, right) => + splice( + Node(Builtin.Error)( + Builtin.Error.Message( + s"$curOp and $op must have different precedence." + ), + Builtin.Error.AST( + tokens.Expr.UnaryGroup( + curOp.unparent(), + tokens.Expr.TmpInfixGroup( + op.unparent(), + left.unparent(), + right.unparent() + ))))) + *> pass(once = false, strategy = pass.bottomUp) + .rules: + on( + parent(tokens.Expr) *> field(tokens.Expr.TmpInfixGroup.withChildren( field(tok(defns.InfixOperator.instances*)) ~ field(tokens.Expr) ~ field(tokens.Expr) - ~ trailing - )) - ~ trailing - ).rewrite: (op, left, right) => - println("\nchecking off :") - println("\nOp: " + op) - println("\nLeft: " + left) - println("\nRight: " + right) - println("\nAs: " + - tokens.Expr.TmpInfixGroup.Checked( - op.unparent(), - left.unparent(), - right.unparent() - )) - splice( - tokens.Expr.TmpInfixGroup.Checked( - op.unparent(), - left.unparent(), - right.unparent() - )) - end orderOperations - - val resolveOperations = passDef: - wellformed := prevWellformed.makeDerived: - tokens.Expr.removeCases(tokens.Expr.TmpInfixGroup.Checked) - - pass(once = false, strategy = pass.bottomUp) - .rules: - on( - parent(tokens.Expr) *> - field(tokens.Expr.TmpInfixGroup.Checked.withChildren( - field(tok(defns.InfixOperator.instances*)) - ~ field(tokens.Expr) - ~ field(tokens.Expr) - ~ eof - )) ~ eof - ).rewrite: (op, right, left) => - splice( - tokens.Expr(tokens.Expr.OpCall( - tokens.OpSym(op.unparent()), - tokens.Expr.OpCall.Params( - right.unparent(), - left.unparent() - )))) - end resolveOperations - - val resolveAlphas = passDef: - wellformed := prevWellformed.makeDerived: - tokens.Expr.removeCases(tokens.Id) - - pass(once = false, strategy = pass.bottomUp) - .rules: - on( + )) + ~ eof + ).rewrite: (op, right, left) => + splice( + tokens.Expr(tokens.Expr.OpCall( + tokens.OpSym(op.unparent()), + tokens.Expr.OpCall.Params( + right.unparent(), + left.unparent() + )))) + | on( parent(tokens.Expr) *> - tokens.Id - ).rewrite: name => + field(tokens.Expr.TmpUnaryGroup.withChildren( + field(tok(defns.PrefixOperator.instances*) + | tok(defns.PostfixOperator.instances*)) + ~ field(tokens.Expr) + ~ eof + )) + ~ eof + ).rewrite: (op, expr) => splice( - tokens.Expr( - tokens.Expr.OpCall( - name.unparent(), - tokens.Expr.OpCall.Params(), - ))) - end resolveAlphas + tokens.Expr(tokens.Expr.OpCall( + tokens.OpSym(op.unparent()), + tokens.Expr.OpCall.Params( + expr.unparent(), + )))) + end reorderOperations val removeNestedExpr = passDef: wellformed := prevWellformed.makeDerived: diff --git a/tla/ExprParser.test.scala b/tla/ExprParser.test.scala index 59f76c3..8b8f734 100644 --- a/tla/ExprParser.test.scala +++ b/tla/ExprParser.test.scala @@ -26,6 +26,25 @@ class ExprParserTests extends munit.FunSuite: tokens.Expr ).unparentedChildren ) + extension (str: String) + def withoutParse: Node.Top = + val wrapped_str = + Source.fromString( + s"""---- MODULE TestMod ---- + |EXTENDS Naturals + |VARIABLE temp + | + |Init == $str + |==== + """.stripMargin + ) + val top = TLAReader(SourceRange.entire(wrapped_str)) + TLAParser(top) + Node.Top( + top(tokens.Module)(tokens.Module.Defns)(tokens.Operator)( + tokens.Expr + ).unparentedChildren + ) extension (top: Node.Top) def parseNode: Node.Top = @@ -161,50 +180,72 @@ class ExprParserTests extends munit.FunSuite: tokens.Expr.OpCall.Params() ))) - // test("Single Binary Operator"): - // assertEquals( - // "5 + 6".parseStr, - // Node.Top( - // tokens.Expr.OpCall( - // tokens.OpSym( - // defns.+("+") - // ), - // tokens.Expr.OpCall.Params( - // tokens.Expr(tokens.Expr.NumberLiteral("5")), - // tokens.Expr(tokens.Expr.NumberLiteral("6")) - // )))) - // assertEquals( - // "5 $ x".parseStr, - // Node.Top( - // tokens.Expr.OpCall( - // tokens.OpSym(defns.$("$")), - // tokens.Expr.OpCall.Params( - // tokens.Expr(tokens.Expr.NumberLiteral("5")), - // tokens.Expr( - // tokens.Expr.OpCall( - // tokens.Id("x"), - // tokens.Expr.OpCall.Params() - // )))))) + test("Single Binary Operator"): + assertEquals( + "5 + 6".parseStr, + Node.Top( + tokens.Expr.OpCall( + tokens.OpSym( + defns.+("+") + ), + tokens.Expr.OpCall.Params( + tokens.Expr(tokens.Expr.NumberLiteral("5")), + tokens.Expr(tokens.Expr.NumberLiteral("6")) + )))) + assertEquals( + "5 $ x".parseStr, + Node.Top( + tokens.Expr.OpCall( + tokens.OpSym(defns.$("$")), + tokens.Expr.OpCall.Params( + tokens.Expr(tokens.Expr.NumberLiteral("5")), + tokens.Expr( + tokens.Expr.OpCall( + tokens.Id("x"), + tokens.Expr.OpCall.Params() + )))))) + + test("Single Unary Operator"): + assertEquals( + "UNION A".parseStr, + Node.Top(tokens.Expr.OpCall( + tokens.OpSym(defns.UNION("UNION")), + tokens.Expr.OpCall.Params( + tokens.Expr( + tokens.Expr.OpCall( + tokens.Id("A"), + tokens.Expr.OpCall.Params() + )))))) + assertEquals( + "x'".parseStr, + Node.Top(tokens.Expr.OpCall( + tokens.OpSym(defns.`'`("'")), + tokens.Expr.OpCall.Params( + tokens.Expr( + tokens.Expr.OpCall( + tokens.Id("x"), + tokens.Expr.OpCall.Params() + )))))) - test("Precedence: Infix Operators"): - // assertEquals( - // "5 * 6 + 7".parseStr, - // Node.Top( - // tokens.Expr.OpCall( - // tokens.OpSym( - // defns.+("+") - // ), - // tokens.Expr.OpCall.Params( - // tokens.Expr( - // tokens.Expr.OpCall( - // tokens.OpSym( - // defns.*("*") - // ), - // tokens.Expr.OpCall.Params( - // tokens.Expr(tokens.Expr.NumberLiteral("5")), - // tokens.Expr(tokens.Expr.NumberLiteral("6")) - // ))), - // tokens.Expr(tokens.Expr.NumberLiteral("7")))))) + test("Precedence: Infix - Infix"): + assertEquals( + "5 * 6 + 7".parseStr, + Node.Top( + tokens.Expr.OpCall( + tokens.OpSym( + defns.+("+") + ), + tokens.Expr.OpCall.Params( + tokens.Expr( + tokens.Expr.OpCall( + tokens.OpSym( + defns.*("*") + ), + tokens.Expr.OpCall.Params( + tokens.Expr(tokens.Expr.NumberLiteral("5")), + tokens.Expr(tokens.Expr.NumberLiteral("6")) + ))), + tokens.Expr(tokens.Expr.NumberLiteral("7")))))) assertEquals( "1 + 8 * 6 - 9 * 3".parseStr, Node.Top( @@ -227,16 +268,185 @@ class ExprParserTests extends munit.FunSuite: tokens.Expr(tokens.Expr.NumberLiteral("9")), tokens.Expr(tokens.Expr.NumberLiteral("3")) )))))))))) - // assertEquals( - // "1 + 1 + 3 * 4".parseStr, - // Node.Top() - // ) - // test("FnCall"): ???: what about x[a, b, c] - needs to be parsed to (Expr, Expr) + test("Precedence: Infix - Prefix"): + assertEquals( + "~x /\\ y".parseStr, + Node.Top(tokens.Expr.OpCall( + tokens.OpSym(defns./\("/\\")), + tokens.Expr.OpCall.Params( + tokens.Expr(tokens.Expr.OpCall( + tokens.OpSym(defns.~("~")), + tokens.Expr.OpCall.Params( + tokens.Expr(tokens.Expr.OpCall( + tokens.Id("x"), + tokens.Expr.OpCall.Params() + ))))), + tokens.Expr(tokens.Expr.OpCall( + tokens.Id("y"), + tokens.Expr.OpCall.Params() + )))))) + assertEquals( + "~x \\in y".parseStr, + Node.Top(tokens.Expr.OpCall( + tokens.OpSym(defns.~("~")), + tokens.Expr.OpCall.Params( + tokens.Expr(tokens.Expr.OpCall( + tokens.OpSym(defns.`\\in`("\\in")), + tokens.Expr.OpCall.Params( + tokens.Expr(tokens.Expr.OpCall( + tokens.Id("x"), + tokens.Expr.OpCall.Params() + )), + tokens.Expr(tokens.Expr.OpCall( + tokens.Id("y"), + tokens.Expr.OpCall.Params() + ))))))))) + + test("Precedence: Infix - Postfix"): + assertEquals( + "1 + x' * 2".parseStr, + Node.Top(tokens.Expr.OpCall( + tokens.OpSym(defns.+("+")), + tokens.Expr.OpCall.Params( + tokens.Expr(tokens.Expr.NumberLiteral("1")), + tokens.Expr(tokens.Expr.OpCall( + tokens.OpSym(defns.*("*")), + tokens.Expr.OpCall.Params( + tokens.Expr(tokens.Expr.OpCall( + tokens.OpSym(defns.`'`("'")), + tokens.Expr.OpCall.Params( + tokens.Expr(tokens.Expr.OpCall( + tokens.Id("x"), + tokens.Expr.OpCall.Params() + ))))), + tokens.Expr(tokens.Expr.NumberLiteral("2")) + ))))))) + + test("Precedence: Unary - Unary"): + assertEquals( + "[] ~x".parseStr, + Node.Top( + tokens.Expr.OpCall( + tokens.OpSym(defns.`[]`("[]")), + tokens.Expr.OpCall.Params( + tokens.Expr(tokens.Expr.OpCall( + tokens.OpSym(defns.~("~")), + tokens.Expr.OpCall.Params( + tokens.Expr(tokens.Expr.OpCall( + tokens.Id("x"), + tokens.Expr.OpCall.Params() + ))))))))) + + // TODO???: postfix postfix: never allowed + + test("Precedence: Associative"): + assertEquals( + "1 + 2 + 3".parseStr, + Node.Top( + tokens.Expr.OpCall( + tokens.OpSym(defns.+("+")), + tokens.Expr.OpCall.Params( + tokens.Expr(tokens.Expr.NumberLiteral("1")), + tokens.Expr(tokens.Expr.OpCall( + tokens.OpSym(defns.+("+")), + tokens.Expr.OpCall.Params( + tokens.Expr(tokens.Expr.NumberLiteral("2")), + tokens.Expr(tokens.Expr.NumberLiteral("3")) + ))))))) + assertEquals( + "1 * 2 / 3".parseStr, + Node.Top(tokens.Expr( + Node(Builtin.Error)( + Builtin.Error.Message( + s"distcompiler.tla.defns.* and distcompiler.tla.defns./ must have different precedence, or be duplicates of an associative operator." + ), + Builtin.Error.AST( + tokens.Expr.TmpInfixGroup( + defns.*("*"), + tokens.Expr(tokens.Expr.NumberLiteral("1")), + tokens.Expr.TmpInfixGroup( + defns./("/"), + tokens.Expr(tokens.Expr.NumberLiteral("2")), + tokens.Expr(tokens.Expr.NumberLiteral("3")) + ))))))) + + // Builtin Error should stop rewrite rules + // TODO???: error message structure + // TODO: depends on the location of resolveAlphas + // test("Precedence: Error"): + // assertEquals( + // "x \\in A \\in B".parseStr, + // Node.Top(tokens.Expr( + // Node(Builtin.Error)( + // Builtin.Error.Message( + // s"26:distcompiler.tla.defns.\\in and 26:distcompiler.tla.defns.\\in must have different precedence, or be duplicates of an associative operator." + // ), + // Builtin.Error.AST( + // tokens.Expr.TmpInfixGroup( + // defns.`\\in`("\\in"), + // tokens.Expr(tokens.Id("x")), + // tokens.Expr.TmpInfixGroup( + // defns.`\\in`("\\in"), + // tokens.Expr(tokens.Id("A")), + // tokens.Expr(tokens.Id("B")) + // ))))))) // assertEquals( - // "x[\"y\"]".parseStr, - // Node.Top() - // ) + // "x \\in A = B".parseStr, + // Node.Top(tokens.Expr( + // Node(Builtin.Error)( + // Builtin.Error.Message( + // s"26:distcompiler.tla.defns.\\in and distcompiler.tla.defns.= must have different precedence, or be duplicates of an associative operator." + // ), + // Builtin.Error.AST( + // tokens.Expr.TmpInfixGroup( + // defns.`\\in`("\\in"), + // tokens.Expr(tokens.Id("x")), + // tokens.Expr.TmpInfixGroup( + // defns.`=`("="), + // tokens.Expr(tokens.Id("A")), + // tokens.Expr(tokens.Id("B")) + // ))))))) + + test("OpCall"): + assertEquals( + "testFun(1, 2, 3)".parseStr, + Node.Top( + tokens.Expr.OpCall( + tokens.Id("testFun"), + tokens.Expr.OpCall.Params( + tokens.Expr(tokens.Expr.NumberLiteral("1")), + tokens.Expr(tokens.Expr.NumberLiteral("2")), + tokens.Expr(tokens.Expr.NumberLiteral("3")) + )))) + + // TODO: conjunction alignment + + test("FnCall"): + assertEquals( + "x[\"y\"]".parseStr, + Node.Top( + tokens.Expr.FnCall( + tokens.Expr(tokens.Expr.OpCall( + tokens.Id("x"), + tokens.Expr.OpCall.Params() + )), + tokens.Expr(tokens.Expr.StringLiteral("y")) + ))) + assertEquals( + "x[1, 2, 3]".parseStr, + Node.Top( + tokens.Expr.FnCall( + tokens.Expr(tokens.Expr.OpCall( + tokens.Id("x"), + tokens.Expr.OpCall.Params() + )), + tokens.Expr(tokens.Expr.TupleLiteral( + tokens.Expr(tokens.Expr.NumberLiteral("1")), + tokens.Expr(tokens.Expr.NumberLiteral("2")), + tokens.Expr(tokens.Expr.NumberLiteral("3")), + )) + ))) test("If"): assertEquals( @@ -332,11 +542,175 @@ class ExprParserTests extends munit.FunSuite: tokens.Expr.OpCall.Params() ))))))) - // test("Exists"): - // assertEquals( - // "\\E x \\in {1, 2, 3} : x = 2".parseStr, - // Node.Top() - // ) + test("Exists"): + assertEquals( + "\\E x \\in {1, 2, 3} : x = 2".parseStr, + Node.Top( + tokens.Expr.Exists( + tokens.QuantifierBounds( + tokens.QuantifierBound( + tokens.Id("x"), + tokens.Expr(tokens.Expr.SetLiteral( + tokens.Expr(tokens.Expr.NumberLiteral("1")), + tokens.Expr(tokens.Expr.NumberLiteral("2")), + tokens.Expr(tokens.Expr.NumberLiteral("3")) + )))), + tokens.Expr(tokens.Expr.OpCall( + tokens.OpSym(defns.`=`("=")), + tokens.Expr.OpCall.Params( + tokens.Expr(tokens.Expr.OpCall( + tokens.Id("x"), + tokens.Expr.OpCall.Params() + )), + tokens.Expr(tokens.Expr.NumberLiteral("2")) + )))))) + assertEquals( + "\\E <> \\in {1, 2, 3} : x = 2".parseStr, + Node.Top( + tokens.Expr.Exists( + tokens.QuantifierBounds( + tokens.QuantifierBound( + tokens.Ids( + tokens.Id("x"), + tokens.Id("y"), + tokens.Id("z") + ), + tokens.Expr(tokens.Expr.SetLiteral( + tokens.Expr(tokens.Expr.NumberLiteral("1")), + tokens.Expr(tokens.Expr.NumberLiteral("2")), + tokens.Expr(tokens.Expr.NumberLiteral("3")) + )))), + tokens.Expr(tokens.Expr.OpCall( + tokens.OpSym(defns.`=`("=")), + tokens.Expr.OpCall.Params( + tokens.Expr(tokens.Expr.OpCall( + tokens.Id("x"), + tokens.Expr.OpCall.Params() + )), + tokens.Expr(tokens.Expr.NumberLiteral("2")) + )))))) + assertEquals( + "\\E x \\in {1, 2, 3}, y \\in {4, 5, 6} : x = 2".parseStr, + Node.Top( + tokens.Expr.Exists( + tokens.QuantifierBounds( + tokens.QuantifierBound( + tokens.Id("x"), + tokens.Expr(tokens.Expr.SetLiteral( + tokens.Expr(tokens.Expr.NumberLiteral("1")), + tokens.Expr(tokens.Expr.NumberLiteral("2")), + tokens.Expr(tokens.Expr.NumberLiteral("3")) + ))), + tokens.QuantifierBound( + tokens.Id("y"), + tokens.Expr(tokens.Expr.SetLiteral( + tokens.Expr(tokens.Expr.NumberLiteral("4")), + tokens.Expr(tokens.Expr.NumberLiteral("5")), + tokens.Expr(tokens.Expr.NumberLiteral("6")) + )))), + tokens.Expr(tokens.Expr.OpCall( + tokens.OpSym(defns.`=`("=")), + tokens.Expr.OpCall.Params( + tokens.Expr(tokens.Expr.OpCall( + tokens.Id("x"), + tokens.Expr.OpCall.Params() + )), + tokens.Expr(tokens.Expr.NumberLiteral("2")) + )))))) + + test("Forall"): + assertEquals( + "\\A x \\in {1, 2, 3} : x = 2".parseStr, + Node.Top( + tokens.Expr.Forall( + tokens.QuantifierBounds( + tokens.QuantifierBound( + tokens.Id("x"), + tokens.Expr(tokens.Expr.SetLiteral( + tokens.Expr(tokens.Expr.NumberLiteral("1")), + tokens.Expr(tokens.Expr.NumberLiteral("2")), + tokens.Expr(tokens.Expr.NumberLiteral("3")) + )))), + tokens.Expr(tokens.Expr.OpCall( + tokens.OpSym(defns.`=`("=")), + tokens.Expr.OpCall.Params( + tokens.Expr(tokens.Expr.OpCall( + tokens.Id("x"), + tokens.Expr.OpCall.Params() + )), + tokens.Expr(tokens.Expr.NumberLiteral("2")) + )))))) + + // TODO: AA EE ?? + + test("Temporal Logic Combined"): + assertEquals( + "s /\\ \\E x \\in y : z /\\ \\E p \\in q : r".parseStr, //TODO???: confirm which one should come first? + Node.Top( + tokens.Expr.OpCall( + tokens.OpSym(defns./\("/\\")), + tokens.Expr.OpCall.Params( + tokens.Expr(tokens.Expr.OpCall( + tokens.Id("s"), + tokens.Expr.OpCall.Params() + )), + tokens.Expr(tokens.Expr.Exists( + tokens.QuantifierBounds( + tokens.QuantifierBound( + tokens.Id("x"), + tokens.Expr(tokens.Expr.OpCall( + tokens.Id("y"), + tokens.Expr.OpCall.Params() + )))), + tokens.Expr(tokens.Expr.OpCall( + tokens.OpSym(defns./\("/\\")), + tokens.Expr.OpCall.Params( + tokens.Expr(tokens.Expr.OpCall( + tokens.Id("z"), + tokens.Expr.OpCall.Params() + )), + tokens.Expr(tokens.Expr.Exists( + tokens.QuantifierBounds( + tokens.QuantifierBound( + tokens.Id("p"), + tokens.Expr(tokens.Expr.OpCall( + tokens.Id("q"), + tokens.Expr.OpCall.Params() + )))), + tokens.Expr(tokens.Expr.OpCall( + tokens.Id("r"), + tokens.Expr.OpCall.Params() + ))))))))))))) + + // todo: function + // todo: set comprehension + // todo: set refinement + // todo: lamda ??? Order2, grammar just says Expr + + test("Choose"): + assertEquals( + "CHOOSE x \\in {1, 2, 3} : x = 2".parseStr, + Node.Top( + tokens.Expr.Choose( + tokens.QuantifierBound( + tokens.Id("x"), + tokens.Expr(tokens.Expr.SetLiteral( + tokens.Expr(tokens.Expr.NumberLiteral("1")), + tokens.Expr(tokens.Expr.NumberLiteral("2")), + tokens.Expr(tokens.Expr.NumberLiteral("3")) + ))), + tokens.Expr(tokens.Expr.OpCall( + tokens.OpSym(defns.`=`("=")), + tokens.Expr.OpCall.Params( + tokens.Expr(tokens.Expr.OpCall( + tokens.Id("x"), + tokens.Expr.OpCall.Params() + )), + tokens.Expr(tokens.Expr.NumberLiteral("2")) + )))))) + // todo: id nil, tuple expr, tuple nil + + // todo: except test("ParenthesesGroup"): assertEquals( @@ -350,33 +724,81 @@ class ExprParserTests extends munit.FunSuite: tokens.Id("x"), tokens.Expr.OpCall.Params() ))) - // assertEquals( - // "(5 + 6)".parseStr, - // Node.Top( - // tokens.Expr.OpCall( - // tokens.OpSym( - // defns.+("+") - // ), - // tokens.Expr.OpCall.Params( - // tokens.Expr(tokens.Expr.NumberLiteral("5")), - // tokens.Expr(tokens.Expr.NumberLiteral("6")) - // )))) - // assertEquals( - // "(1 + 2) * 3".parseStr, - // Node.Top( - // tokens.Expr.OpCall( - // tokens.OpSym( - // defns.*("*") - // ), - // tokens.Expr.OpCall.Params( - // tokens.Expr(tokens.Expr.OpCall( - // tokens.OpSym( - // defns.+("+") - // ), - // tokens.Expr.OpCall.Params( - // tokens.Expr(tokens.Expr.NumberLiteral("1")), - // tokens.Expr(tokens.Expr.NumberLiteral("2")) - // ) - // )), - // tokens.Expr(tokens.Expr.NumberLiteral("3")) - // )))) \ No newline at end of file + assertEquals( + "(5 + 6)".parseStr, + Node.Top( + tokens.Expr.OpCall( + tokens.OpSym( + defns.+("+") + ), + tokens.Expr.OpCall.Params( + tokens.Expr(tokens.Expr.NumberLiteral("5")), + tokens.Expr(tokens.Expr.NumberLiteral("6")) + )))) + assertEquals( + "(1 + 2) * 3".parseStr, + Node.Top( + tokens.Expr.OpCall( + tokens.OpSym( + defns.*("*") + ), + tokens.Expr.OpCall.Params( + tokens.Expr(tokens.Expr.OpCall( + tokens.OpSym( + defns.+("+") + ), + tokens.Expr.OpCall.Params( + tokens.Expr(tokens.Expr.NumberLiteral("1")), + tokens.Expr(tokens.Expr.NumberLiteral("2")) + ) + )), + tokens.Expr(tokens.Expr.NumberLiteral("3")) + )))) + + test("Conjunctions"): + assertEquals( + "/\\ 1".parseStr, + Node.Top( + tokens.Expr.NumberLiteral("1") + )) + assertEquals( + "/\\ 1 \\/ 2".parseStr, + Node.Top( + tokens.Expr.OpCall( + tokens.OpSym(defns.\/("\\/")), + tokens.Expr.OpCall.Params( + tokens.Expr(tokens.Expr.NumberLiteral("1")), + tokens.Expr(tokens.Expr.NumberLiteral("2")) + )))) + assertEquals( + s""" + |/\\ 1 + |/\\ 2 + |""".stripMargin.parseStr, + Node.Top( + tokens.Expr.OpCall( + tokens.OpSym(defns./\("/\\")), + tokens.Expr.OpCall.Params( + tokens.Expr(tokens.Expr.NumberLiteral("1")), + tokens.Expr(tokens.Expr.NumberLiteral("2")) + )))) + assertEquals( + s""" + |/\\ 1 \\/ 1 + |/\\ 2 \\/ 2 + |/\\ 3 \\/ 3 + |""".stripMargin.parseStr, + Node.Top()) + + + // /\ 1 + // /\ 2 + // /\ 3 + + // /\ 1 + // /\ 2 + // /\ 3 + // /\ 4 + // /\ 5 + // /\ 6 + diff --git a/tla/TLAParser.scala b/tla/TLAParser.scala index 9235da6..86e907a 100644 --- a/tla/TLAParser.scala +++ b/tla/TLAParser.scala @@ -173,6 +173,69 @@ object TLAParser extends PassSeq: ).void nodeSpanMatchedBy(impl).map(RawExpression.apply) + end rawExpression + + lazy val rawConjunction: SeqPattern[RawExpression] = + val simpleCases: SeqPattern[Unit] = + anyChild.void <* not( + tok(expressionDelimiters*) + | tok(defns./\) + // 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, diff --git a/tla/TLAParser.test.scala b/tla/TLAParser.test.scala index 988f4a3..94ada11 100644 --- a/tla/TLAParser.test.scala +++ b/tla/TLAParser.test.scala @@ -14,7 +14,7 @@ package distcompiler.tla -import distcompiler.* +import distcompiler.*, distcompiler.tla.ExprParser class TLAParserTests extends munit.FunSuite, test.WithTLACorpus: self => @@ -36,6 +36,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) diff --git a/tla/defns.scala b/tla/defns.scala index d3bd9e0..397f1cf 100644 --- a/tla/defns.scala +++ b/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] = @@ -209,10 +211,12 @@ 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) case object `^*` extends PostfixOperator(15) case object `^#` extends PostfixOperator(15) - case object `'` extends PostfixOperator(15) + case object `'` extends PostfixOperator(15) diff --git a/tla/package.scala b/tla/package.scala index a2c5020..1c898ec 100644 --- a/tla/package.scala +++ b/tla/package.scala @@ -296,10 +296,7 @@ val wellformed: Wellformed = t.Expr ) t.Expr.Lambda.Params ::= repeated( - choice( - t.Id, - t.Order2 - ), + t.Id, minCount = 1 ) From 0da75530e7aad04cb93365003730f3e4fa912ddf Mon Sep 17 00:00:00 2001 From: Kuter Bora Date: Thu, 24 Apr 2025 21:31:51 -0700 Subject: [PATCH 7/9] end of term commit --- tla/ExprParser.scala | 74 ++++++--------- tla/ExprParser.test.scala | 189 +++++++++++++++++++++++++++++--------- tla/TLAParser.scala | 6 +- 3 files changed, 178 insertions(+), 91 deletions(-) diff --git a/tla/ExprParser.scala b/tla/ExprParser.scala index 3023e8e..f658531 100644 --- a/tla/ExprParser.scala +++ b/tla/ExprParser.scala @@ -111,7 +111,6 @@ object ExprParser extends PassSeq: )) ~ eof )) - def matchQuantifierId() :SeqPattern[(Node, TLAParser.RawExpression)] = parent(tokens.Expr) *> field(TLAReader.Alpha) @@ -126,19 +125,11 @@ object ExprParser extends PassSeq: )) ~ skip(defns.`\\in`) ~ field(rawExpression) - ~ trailing - - - // TODO??? Pass structure - - // conjunction alignment - // OpCall, QunatifierBound, Temporal Logic - set - // Literals, Let, If, Case, FnCall, TmpCall - // Resolve TmpCalls - // Check for assoc related errors - // Resolve Ids - // Remove parenthesis + ~ trailing + // replace all tokens.Expr(contents...) with + // tokens.Expr(tokens.ExprTry, contents...) + val buildExpressions = passDef: wellformed := prevWellformed.makeDerived: val removedCases = Seq( @@ -169,18 +160,16 @@ object ExprParser extends PassSeq: tokens.Expr.TmpUnaryGroup) // TODO: assign the correct source with .like() - // TODO??: find a more consistent order of passes pass(once = false, strategy = pass.bottomUp) // conjunction alignment .rules: on( parent(tokens.Expr) *> - field( - (field(tok(defns./\)) - ~ field(rawConjunction) + (field(tok(defns./\)) + ~ field(rawConjunction(1)) ~ field(tok(defns./\)) - ~ field(rawConjunction) - ~ trailing + ~ field(rawConjunction(1)) + ~ eof ).filter(things => things match case (and1 : Node, r1, and2 : Node, r2) => @@ -189,32 +178,29 @@ object ExprParser extends PassSeq: // println("\nCol 1: " + s1.source.lines.lineColAtOffset(s1.offset)) // println("\nCol 2: " + s2.source.lines.lineColAtOffset(s2.offset)) s1.source.lines.lineColAtOffset(s1.offset)._2 == s2.source.lines.lineColAtOffset(s2.offset)._2 - )) - ~ eof + ) ).rewrite: (and1, r1, and2, r2) => splice( + and1.unparent(), tokens.Expr( - and1.unparent(), tokens.Expr.OpCall( tokens.OpSym(and2.unparent()), tokens.Expr.OpCall.Params( r1.mkNode, r2.mkNode )))) - *> pass(once = false, strategy = pass.bottomUp) - // remove the leading /\, this should not be its own pass - // join with the prev once rawExpression2 is done + *> pass(once = false, strategy = pass.bottomUp) // remove leading /\, remove paren .rules: + // on( + // field(tokens.Expr.withChildren( + // skip(defns./\) + // ~ field(tokens.Expr) + // ~ eof + // )) + // ~ eof + // ).rewrite: expr => + // splice(expr.unparent()) on( - field(tokens.Expr.withChildren( - skip(defns./\) - ~ field(tokens.Expr) - ~ eof - )) - ~ eof - ).rewrite: expr => - splice(expr.unparent()) - | on( field(tokens.Expr.withChildren( skip(defns./\) ~ field(rawExpression) @@ -223,6 +209,16 @@ object ExprParser extends PassSeq: ~ eof ).rewrite: expr => splice(expr.mkNode) + | on( + parent(tokens.Expr) *> + tok(TLAReader.ParenthesesGroup) *> + children: + field(rawExpression) + ~ eof + ).rewrite: rawExpr => + splice( + tokens.Expr(rawExpr.mkNode) + ) *> pass(once = false, strategy = pass.bottomUp) // resolve quantifiers/opCall .rules: on( @@ -577,16 +573,6 @@ object ExprParser extends PassSeq: // TODO: Except // TODO: Lambda // TODO a \x b \ a - | on( - parent(tokens.Expr) *> - tok(TLAReader.ParenthesesGroup) *> - children: - field(rawExpression) - ~ eof - ).rewrite: expr => - splice( - tokens.Expr(expr.mkNode) - ) | on( parent(tokens.Expr) *> skip(defns.IF) diff --git a/tla/ExprParser.test.scala b/tla/ExprParser.test.scala index 8b8f734..88901aa 100644 --- a/tla/ExprParser.test.scala +++ b/tla/ExprParser.test.scala @@ -645,7 +645,7 @@ class ExprParserTests extends munit.FunSuite: test("Temporal Logic Combined"): assertEquals( - "s /\\ \\E x \\in y : z /\\ \\E p \\in q : r".parseStr, //TODO???: confirm which one should come first? + "s /\\ \\E x \\in y : z /\\ \\E p \\in q : r".parseStr, Node.Top( tokens.Expr.OpCall( tokens.OpSym(defns./\("/\\")), @@ -685,7 +685,7 @@ class ExprParserTests extends munit.FunSuite: // todo: function // todo: set comprehension // todo: set refinement - // todo: lamda ??? Order2, grammar just says Expr + // todo: lambda test("Choose"): assertEquals( @@ -712,7 +712,7 @@ class ExprParserTests extends munit.FunSuite: // todo: except - test("ParenthesesGroup"): + test("Parentheses"): assertEquals( "(1)".parseStr, Node.Top(tokens.Expr.NumberLiteral("1")) @@ -754,51 +754,150 @@ class ExprParserTests extends munit.FunSuite: )), tokens.Expr(tokens.Expr.NumberLiteral("3")) )))) - - test("Conjunctions"): - assertEquals( - "/\\ 1".parseStr, - Node.Top( - tokens.Expr.NumberLiteral("1") - )) - assertEquals( - "/\\ 1 \\/ 2".parseStr, - Node.Top( - tokens.Expr.OpCall( - tokens.OpSym(defns.\/("\\/")), - tokens.Expr.OpCall.Params( - tokens.Expr(tokens.Expr.NumberLiteral("1")), - tokens.Expr(tokens.Expr.NumberLiteral("2")) - )))) assertEquals( - s""" - |/\\ 1 - |/\\ 2 - |""".stripMargin.parseStr, + "(\\A x \\in {1, 2, 3} : x = 2)".parseStr, Node.Top( - tokens.Expr.OpCall( - tokens.OpSym(defns./\("/\\")), - tokens.Expr.OpCall.Params( - tokens.Expr(tokens.Expr.NumberLiteral("1")), - tokens.Expr(tokens.Expr.NumberLiteral("2")) - )))) - assertEquals( - s""" - |/\\ 1 \\/ 1 - |/\\ 2 \\/ 2 - |/\\ 3 \\/ 3 - |""".stripMargin.parseStr, - Node.Top()) + tokens.Expr.Forall( + tokens.QuantifierBounds( + tokens.QuantifierBound( + tokens.Id("x"), + tokens.Expr(tokens.Expr.SetLiteral( + tokens.Expr(tokens.Expr.NumberLiteral("1")), + tokens.Expr(tokens.Expr.NumberLiteral("2")), + tokens.Expr(tokens.Expr.NumberLiteral("3")) + )))), + tokens.Expr(tokens.Expr.OpCall( + tokens.OpSym(defns.`=`("=")), + tokens.Expr.OpCall.Params( + tokens.Expr(tokens.Expr.OpCall( + tokens.Id("x"), + tokens.Expr.OpCall.Params() + )), + tokens.Expr(tokens.Expr.NumberLiteral("2")) + )))))) + + // test("Conjunctions"): + // assertEquals( + // "/\\ 1".parseStr, + // Node.Top( + // tokens.Expr.NumberLiteral("1") + // )) + // assertEquals( + // "/\\ 1 \\/ 2".parseStr, + // Node.Top( + // tokens.Expr.OpCall( + // tokens.OpSym(defns.\/("\\/")), + // tokens.Expr.OpCall.Params( + // tokens.Expr(tokens.Expr.NumberLiteral("1")), + // tokens.Expr(tokens.Expr.NumberLiteral("2")) + // )))) + // assertEquals( + // s""" + // |/\\ 1 + // |/\\ 2 + // |""".stripMargin.parseStr, + // Node.Top( + // tokens.Expr.OpCall( + // tokens.OpSym(defns./\("/\\")), + // tokens.Expr.OpCall.Params( + // tokens.Expr(tokens.Expr.NumberLiteral("1")), + // tokens.Expr(tokens.Expr.NumberLiteral("2")) + // )))) + // assertEquals( + // s""" + // |/\\ 1 \\/ 1 + // |/\\ 2 \\/ 2 + // |/\\ 3 \\/ 3 + // |""".stripMargin.parseStr, + // Node.Top(tokens.Expr.OpCall( + // tokens.OpSym(defns./\("/\\")), + // tokens.Expr.OpCall.Params( + // tokens.Expr(tokens.Expr.OpCall( + // tokens.OpSym(defns.\/("\\/")), + // tokens.Expr.OpCall.Params( + // tokens.Expr(tokens.Expr.NumberLiteral("1")), + // tokens.Expr(tokens.Expr.NumberLiteral("1")) + // ) + // )), + // tokens.Expr(tokens.Expr.OpCall( + // tokens.OpSym(defns./\("/\\")), + // tokens.Expr.OpCall.Params( + // tokens.Expr(tokens.Expr.OpCall( + // tokens.OpSym(defns.\/("\\/")), + // tokens.Expr.OpCall.Params( + // tokens.Expr(tokens.Expr.NumberLiteral("2")), + // tokens.Expr(tokens.Expr.NumberLiteral("2")) + // ))), + // tokens.Expr(tokens.Expr.OpCall( + // tokens.OpSym(defns.\/("\\/")), + // tokens.Expr.OpCall.Params( + // tokens.Expr(tokens.Expr.NumberLiteral("3")), + // tokens.Expr(tokens.Expr.NumberLiteral("3")) + // )))))))))) + + // assertEquals( + // s""" + // |/\\ 1 + // | /\\ 2 + // |/\\ 3 + // |""".stripMargin.parseStr, + // Node.Top( + // tokens.Expr.OpCall( + // tokens.OpSym(defns./\("/\\")), + // tokens.Expr.OpCall.Params( + // tokens.Expr(tokens.Expr.OpCall( + // tokens.OpSym(defns./\("/\\")), + // tokens.Expr.OpCall.Params( + // tokens.Expr(tokens.Expr.NumberLiteral("1")), + // tokens.Expr(tokens.Expr.NumberLiteral("2")) + // ) + // )), + // tokens.Expr(tokens.Expr.NumberLiteral("3")) + // ) + // ) + // )) + + // assertEquals( + // s""" + // |/\\ \\E x \in {1, 2, 3} : 1 + // | /\\ 2 + // |""".stripMargin.parseStr, + // Node.Top( + // tokens.Expr.NumberLiteral("1") + // )) + // assertEquals( + // s""" + // |/\\ \\E x \in {1, 2, 3} : 1 + // |/\\ 2 + // |""".stripMargin.parseStr, + // Node.Top( + // tokens.Expr.NumberLiteral("1") + // )) - // /\ 1 - // /\ 2 - // /\ 3 + // assertEquals( + // s""" + // | /\\ \\E x \in {1, 2, 3} : 1 + // |/\\ 2 + // |""".stripMargin.parseStr, + // Node.Top( + // tokens.Expr.NumberLiteral("1") + // )) - // /\ 1 - // /\ 2 - // /\ 3 - // /\ 4 - // /\ 5 - // /\ 6 + // assertEquals( + // s""" + // |/\\ 1 + // | /\\ 2 + // | /\\ 3 + // | /\\ 4 + // |/\\ 5 + // | /\\ 6 + // |""".stripMargin.parseStr, + // Node.Top( + // tokens.Expr.NumberLiteral("1") + // )) +// TODO +// paren +// conjucntion +// lamda function set diff --git a/tla/TLAParser.scala b/tla/TLAParser.scala index 86e907a..1a85a99 100644 --- a/tla/TLAParser.scala +++ b/tla/TLAParser.scala @@ -175,11 +175,13 @@ object TLAParser extends PassSeq: nodeSpanMatchedBy(impl).map(RawExpression.apply) end rawExpression - lazy val rawConjunction: SeqPattern[RawExpression] = + def rawConjunction(col : Integer): SeqPattern[RawExpression] = val simpleCases: SeqPattern[Unit] = anyChild.void <* not( tok(expressionDelimiters*) - | tok(defns./\) + | 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 ) From 6bd012c0192c75423f490c45a45cb220d0720d16 Mon Sep 17 00:00:00 2001 From: Kuter Bora Date: Fri, 9 May 2025 14:32:02 -0700 Subject: [PATCH 8/9] latest files --- tla/ExprParser.scala | 22 +++++++++---------- tla/ExprParser.test.scala | 45 ++++++++++++++++++--------------------- 2 files changed, 31 insertions(+), 36 deletions(-) diff --git a/tla/ExprParser.scala b/tla/ExprParser.scala index f658531..e80d553 100644 --- a/tla/ExprParser.scala +++ b/tla/ExprParser.scala @@ -209,16 +209,6 @@ object ExprParser extends PassSeq: ~ eof ).rewrite: expr => splice(expr.mkNode) - | on( - parent(tokens.Expr) *> - tok(TLAReader.ParenthesesGroup) *> - children: - field(rawExpression) - ~ eof - ).rewrite: rawExpr => - splice( - tokens.Expr(rawExpr.mkNode) - ) *> pass(once = false, strategy = pass.bottomUp) // resolve quantifiers/opCall .rules: on( @@ -236,8 +226,6 @@ object ExprParser extends PassSeq: tokens.Expr.OpCall.Params( args.iterator.map(_.mkNode) )))) - // TODO: Exists, Forall, Choose - // TODO: refactor and simplify | on( parent(tokens.Expr) *> skip(tok(TLAReader.LaTexLike).src("\\E")) @@ -589,6 +577,16 @@ object ExprParser extends PassSeq: t.unparent(), f.unparent() )) + | on( + parent(tokens.Expr) *> + tok(TLAReader.ParenthesesGroup) *> + children: + field(rawExpression) + ~ eof + ).rewrite: rawExpr => + splice( + tokens.Expr(rawExpr.mkNode) + ) *> pass(once = false, strategy = pass.bottomUp) // resolve Alphas .rules: on( diff --git a/tla/ExprParser.test.scala b/tla/ExprParser.test.scala index 88901aa..e28c838 100644 --- a/tla/ExprParser.test.scala +++ b/tla/ExprParser.test.scala @@ -371,9 +371,6 @@ class ExprParserTests extends munit.FunSuite: tokens.Expr(tokens.Expr.NumberLiteral("3")) ))))))) - // Builtin Error should stop rewrite rules - // TODO???: error message structure - // TODO: depends on the location of resolveAlphas // test("Precedence: Error"): // assertEquals( // "x \\in A \\in B".parseStr, @@ -754,27 +751,27 @@ class ExprParserTests extends munit.FunSuite: )), tokens.Expr(tokens.Expr.NumberLiteral("3")) )))) - assertEquals( - "(\\A x \\in {1, 2, 3} : x = 2)".parseStr, - Node.Top( - tokens.Expr.Forall( - tokens.QuantifierBounds( - tokens.QuantifierBound( - tokens.Id("x"), - tokens.Expr(tokens.Expr.SetLiteral( - tokens.Expr(tokens.Expr.NumberLiteral("1")), - tokens.Expr(tokens.Expr.NumberLiteral("2")), - tokens.Expr(tokens.Expr.NumberLiteral("3")) - )))), - tokens.Expr(tokens.Expr.OpCall( - tokens.OpSym(defns.`=`("=")), - tokens.Expr.OpCall.Params( - tokens.Expr(tokens.Expr.OpCall( - tokens.Id("x"), - tokens.Expr.OpCall.Params() - )), - tokens.Expr(tokens.Expr.NumberLiteral("2")) - )))))) + // assertEquals( + // "\\A x \\in {1, 2, 3} : x = (2)".parseStr, + // Node.Top( + // tokens.Expr.Forall( + // tokens.QuantifierBounds( + // tokens.QuantifierBound( + // tokens.Id("x"), + // tokens.Expr(tokens.Expr.SetLiteral( + // tokens.Expr(tokens.Expr.NumberLiteral("1")), + // tokens.Expr(tokens.Expr.NumberLiteral("2")), + // tokens.Expr(tokens.Expr.NumberLiteral("3")) + // )))), + // tokens.Expr(tokens.Expr.OpCall( + // tokens.OpSym(defns.`=`("=")), + // tokens.Expr.OpCall.Params( + // tokens.Expr(tokens.Expr.OpCall( + // tokens.Id("x"), + // tokens.Expr.OpCall.Params() + // )), + // tokens.Expr(tokens.Expr.NumberLiteral("2")) + // )))))) // test("Conjunctions"): // assertEquals( From 2bd2d39bdd5b5803064000efd7e93f3baaafdc75 Mon Sep 17 00:00:00 2001 From: Finn Hackett Date: Fri, 23 May 2025 01:45:37 +0000 Subject: [PATCH 9/9] run code cleanup scripts --- langs/tla/ExprParser.scala | 1142 ++++++++++++++++++------------- langs/tla/ExprParser.test.scala | 1135 ++++++++++++++++++------------ langs/tla/TLAParser.scala | 19 +- langs/tla/TLAParser.test.scala | 3 +- langs/tla/defns.scala | 2 +- langs/tla/package.scala | 7 +- 6 files changed, 1393 insertions(+), 915 deletions(-) diff --git a/langs/tla/ExprParser.scala b/langs/tla/ExprParser.scala index 9b50d06..d2ccc34 100644 --- a/langs/tla/ExprParser.scala +++ b/langs/tla/ExprParser.scala @@ -1,3 +1,17 @@ +// Copyright 2024-2025 Forja Team +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + package forja.langs.tla import cats.syntax.all.given @@ -5,6 +19,7 @@ import cats.syntax.all.given import forja.* import forja.dsl.* import forja.wf.Wellformed + import TLAReader.* import TLAParser.{rawExpression, rawConjunction} @@ -14,146 +29,200 @@ object ExprParser extends PassSeq: def inputWellformed: Wellformed = TLAParser.outputWellformed // TODO: make private - def highPredInfixInfix(op: defns.InfixOperator): SeqPattern[SeqPattern.Fields[Tuple1[(Node, Node, Node)]]] = - field(lang.Expr.withChildren( - field(TmpInfixGroup.withChildren( - field(tok(defns.InfixOperator.instances*) - .filter(op2 => - op2.token match - case op2Token : defns.InfixOperator => - op.highPrecedence > op2Token.highPrecedence)) - ~ field(lang.Expr) - ~ field(lang.Expr) - ~ eof - )) - ~ eof - )) - def highPredInfixUnary(op: defns.InfixOperator): SeqPattern[SeqPattern.Fields[Tuple1[(Node, Node)]]] = - field(lang.Expr.withChildren( - field(TmpUnaryGroup.withChildren( - field(tok(defns.PrefixOperator.instances*) - .filter(op2 => - op2.token match - case op2Token : defns.PrefixOperator => - op.highPrecedence > op2Token.highPrecedence - case op2Token : defns.PostfixOperator => - op.highPrecedence > op2Token.precedence)) - ~ field(lang.Expr) - ~ eof - )) - ~ eof - )) - def highPredUnaryInfix(op: defns.Operator): SeqPattern[SeqPattern.Fields[Tuple1[(Node, Node, Node)]]] = - field(lang.Expr.withChildren( - field(TmpInfixGroup.withChildren( - field(tok(defns.InfixOperator.instances*) - .filter(op2 => - op2.token match - case op2Token : defns.InfixOperator => - op.highPrecedence > op2Token.highPrecedence)) - ~ field(lang.Expr) - ~ field(lang.Expr) - ~ eof - )) - ~ eof - )) + def highPredInfixInfix( + op: defns.InfixOperator, + ): SeqPattern[SeqPattern.Fields[Tuple1[(Node, Node, Node)]]] = + field( + lang.Expr.withChildren( + field( + TmpInfixGroup.withChildren( + field( + tok(defns.InfixOperator.instances*) + .filter(op2 => + op2.token match + case op2Token: defns.InfixOperator => + op.highPrecedence > op2Token.highPrecedence, + ), + ) + ~ field(lang.Expr) + ~ field(lang.Expr) + ~ eof, + ), + ) + ~ eof, + ), + ) + def highPredInfixUnary( + op: defns.InfixOperator, + ): SeqPattern[SeqPattern.Fields[Tuple1[(Node, Node)]]] = + field( + lang.Expr.withChildren( + field( + TmpUnaryGroup.withChildren( + field( + tok(defns.PrefixOperator.instances*) + .filter(op2 => + op2.token match + case op2Token: defns.PrefixOperator => + op.highPrecedence > op2Token.highPrecedence + case op2Token: defns.PostfixOperator => + op.highPrecedence > op2Token.precedence, + ), + ) + ~ field(lang.Expr) + ~ eof, + ), + ) + ~ eof, + ), + ) + def highPredUnaryInfix( + op: defns.Operator, + ): SeqPattern[SeqPattern.Fields[Tuple1[(Node, Node, Node)]]] = + field( + lang.Expr.withChildren( + field( + TmpInfixGroup.withChildren( + field( + tok(defns.InfixOperator.instances*) + .filter(op2 => + op2.token match + case op2Token: defns.InfixOperator => + op.highPrecedence > op2Token.highPrecedence, + ), + ) + ~ field(lang.Expr) + ~ field(lang.Expr) + ~ eof, + ), + ) + ~ eof, + ), + ) - def badPredInfixInfix(op: defns.InfixOperator): SeqPattern[SeqPattern.Fields[Tuple1[(Node, Node, Node)]]] = - field(lang.Expr.withChildren( - field(TmpInfixGroup.withChildren( - field(tok(defns.InfixOperator.instances*) - .filter(op2 => - op2.token match - case op2Token : defns.InfixOperator => - !((op.highPrecedence > op2Token.highPrecedence) - || (op.lowPrecedence < op2Token.lowPrecedence) - || ((op == op2Token) && op.isAssociative)) - )) - ~ field(lang.Expr) - ~ field(lang.Expr) - ~ eof - )) - ~ eof - )) - def badPredInfixUnary(op: defns.InfixOperator): SeqPattern[SeqPattern.Fields[Tuple1[(Node, Node)]]] = - field(lang.Expr.withChildren( - field(TmpUnaryGroup.withChildren( - field(tok(defns.PrefixOperator.instances*) - .filter(op2 => - op2.token match - case op2Token : defns.PrefixOperator => - !((op.highPrecedence > op2Token.highPrecedence) - || (op.lowPrecedence < op2Token.lowPrecedence)) - case op2Token : defns.PostfixOperator => - !((op.highPrecedence > op2Token.precedence) - || (op.lowPrecedence < op2Token.precedence)))) - ~ field(lang.Expr) - ~ eof - )) - ~ eof - )) - def badPredUnaryInfix(op: defns.Operator): SeqPattern[SeqPattern.Fields[Tuple1[(Node, Node, Node)]]] = - field(lang.Expr.withChildren( - field(TmpInfixGroup.withChildren( - field(tok(defns.InfixOperator.instances*) - .filter(op2 => - op2.token match - case op2Token : defns.InfixOperator => - !((op.highPrecedence > op2Token.highPrecedence) - || (op.lowPrecedence < op2Token.lowPrecedence)))) - ~ field(lang.Expr) - ~ field(lang.Expr) - ~ eof - )) - ~ eof - )) - def matchQuantifierId() :SeqPattern[(Node, TLAParser.RawExpression)] = + def badPredInfixInfix( + op: defns.InfixOperator, + ): SeqPattern[SeqPattern.Fields[Tuple1[(Node, Node, Node)]]] = + field( + lang.Expr.withChildren( + field( + TmpInfixGroup.withChildren( + field( + tok(defns.InfixOperator.instances*) + .filter(op2 => + op2.token match + case op2Token: defns.InfixOperator => + !((op.highPrecedence > op2Token.highPrecedence) + || (op.lowPrecedence < op2Token.lowPrecedence) + || ((op == op2Token) && op.isAssociative)), + ), + ) + ~ field(lang.Expr) + ~ field(lang.Expr) + ~ eof, + ), + ) + ~ eof, + ), + ) + def badPredInfixUnary( + op: defns.InfixOperator, + ): SeqPattern[SeqPattern.Fields[Tuple1[(Node, Node)]]] = + field( + lang.Expr.withChildren( + field( + TmpUnaryGroup.withChildren( + field( + tok(defns.PrefixOperator.instances*) + .filter(op2 => + op2.token match + case op2Token: defns.PrefixOperator => + !((op.highPrecedence > op2Token.highPrecedence) + || (op.lowPrecedence < op2Token.lowPrecedence)) + case op2Token: defns.PostfixOperator => + !((op.highPrecedence > op2Token.precedence) + || (op.lowPrecedence < op2Token.precedence)), + ), + ) + ~ field(lang.Expr) + ~ eof, + ), + ) + ~ eof, + ), + ) + def badPredUnaryInfix( + op: defns.Operator, + ): SeqPattern[SeqPattern.Fields[Tuple1[(Node, Node, Node)]]] = + field( + lang.Expr.withChildren( + field( + TmpInfixGroup.withChildren( + field( + tok(defns.InfixOperator.instances*) + .filter(op2 => + op2.token match + case op2Token: defns.InfixOperator => + !((op.highPrecedence > op2Token.highPrecedence) + || (op.lowPrecedence < op2Token.lowPrecedence)), + ), + ) + ~ field(lang.Expr) + ~ field(lang.Expr) + ~ eof, + ), + ) + ~ eof, + ), + ) + def matchQuantifierId(): SeqPattern[(Node, TLAParser.RawExpression)] = parent(lang.Expr) *> field(TLAReader.Alpha) ~ skip(defns.`\\in`) ~ field(rawExpression) ~ trailing - def matchQuantifierIds() :SeqPattern[(List[Node], TLAParser.RawExpression)] = + def matchQuantifierIds(): SeqPattern[(List[Node], TLAParser.RawExpression)] = parent(lang.Expr) *> - field(tok(TLAReader.TupleGroup).withChildren( - field(repeatedSepBy(`,`)(tok(TLAReader.Alpha))) - ~ eof - )) + field( + tok(TLAReader.TupleGroup).withChildren( + field(repeatedSepBy(`,`)(tok(TLAReader.Alpha))) + ~ eof, + ), + ) ~ skip(defns.`\\in`) ~ field(rawExpression) - ~ trailing + ~ trailing // replace all lang.Expr(contents...) with // lang.Expr(lang.ExprTry, contents...) - + val buildExpressions = passDef: wellformed := prevWellformed.makeDerived: val removedCases = Seq( TLAReader.StringLiteral, TLAReader.NumberLiteral, - TLAReader.TupleGroup + TLAReader.TupleGroup, // TODO: remove cases ) TLAReader.groupTokens.foreach: tok => tok.removeCases(removedCases*) tok.addCases(lang.Expr) - + TmpInfixGroup ::= fields( choice(defns.InfixOperator.instances*), lang.Expr, - lang.Expr + lang.Expr, ) TmpUnaryGroup ::= fields( - choice((defns.PrefixOperator.instances ++ defns.PostfixOperator.instances)*), + choice( + (defns.PrefixOperator.instances ++ defns.PostfixOperator.instances)*, + ), lang.Expr, ) lang.Expr.deleteShape() lang.Expr.importFrom(lang.wf) - lang.Expr.addCases( - lang.Expr, - TmpInfixGroup, - TmpUnaryGroup) + lang.Expr.addCases(lang.Expr, TmpInfixGroup, TmpUnaryGroup) // TODO: assign the correct source with .like() @@ -165,16 +234,19 @@ object ExprParser extends PassSeq: ~ field(rawConjunction(1)) ~ field(tok(defns./\)) ~ field(rawConjunction(1)) - ~ eof - ).filter(things => + ~ eof).filter(things => things match - case (and1 : Node, r1, and2 : Node, r2) => + case (and1: Node, r1, and2: Node, r2) => val s1 = and1.sourceRange val s2 = and2.sourceRange - // println("\nCol 1: " + s1.source.lines.lineColAtOffset(s1.offset)) - // println("\nCol 2: " + s2.source.lines.lineColAtOffset(s2.offset)) - s1.source.lines.lineColAtOffset(s1.offset)._2 == s2.source.lines.lineColAtOffset(s2.offset)._2 - ) + /* println("\nCol 1: " + + * s1.source.lines.lineColAtOffset(s1.offset)) */ + /* println("\nCol 2: " + + * s2.source.lines.lineColAtOffset(s2.offset)) */ + s1.source.lines + .lineColAtOffset(s1.offset) + ._2 == s2.source.lines.lineColAtOffset(s2.offset)._2, + ), ).rewrite: (and1, r1, and2, r2) => splice( and1.unparent(), @@ -183,9 +255,15 @@ object ExprParser extends PassSeq: lang.OpSym(and2.unparent()), lang.Expr.OpCall.Params( r1.mkNode, - r2.mkNode - )))) - *> pass(once = false, strategy = pass.bottomUp) // remove leading /\, remove paren + r2.mkNode, + ), + ), + ), + ) + *> pass( + once = false, + strategy = pass.bottomUp, + ) // remove leading /\, remove paren .rules: // on( // field(lang.Expr.withChildren( @@ -197,133 +275,159 @@ object ExprParser extends PassSeq: // ).rewrite: expr => // splice(expr.unparent()) on( - field(lang.Expr.withChildren( - skip(defns./\) - ~ field(rawExpression) - ~ eof - )) - ~ eof + field( + lang.Expr.withChildren( + skip(defns./\) + ~ field(rawExpression) + ~ eof, + ), + ) + ~ eof, ).rewrite: expr => - splice(expr.mkNode) - *> pass(once = false, strategy = pass.bottomUp) // resolve quantifiers/opCall + splice(expr.mkNode) + *> pass( + once = false, + strategy = pass.bottomUp, + ) // resolve quantifiers/opCall .rules: on( - parent(lang.Expr) *> + parent(lang.Expr) *> field(TLAReader.Alpha) - ~ field(TLAReader.ParenthesesGroup.withChildren( + ~ field( + TLAReader.ParenthesesGroup.withChildren( field(repeatedSepBy(`,`)(rawExpression)) - ~ eof - )) - ~ trailing + ~ eof, + ), + ) + ~ trailing, ).rewrite: (fun, args) => splice( - lang.Expr(lang.Expr.OpCall( - lang.Id().like(fun), - lang.Expr.OpCall.Params( - args.iterator.map(_.mkNode) - )))) + lang.Expr( + lang.Expr.OpCall( + lang.Id().like(fun), + lang.Expr.OpCall.Params( + args.iterator.map(_.mkNode), + ), + ), + ), + ) | on( parent(lang.Expr) *> skip(tok(TLAReader.LaTexLike).src("\\E")) ~ field(repeatedSepBy1(`,`)(matchQuantifierId())) ~ skip(TLAReader.`:`) ~ field(rawExpression) - ~ trailing + ~ trailing, ).rewrite: (qBounds, expr) => - splice( - lang.Expr(lang.Expr.Exists( + splice( + lang.Expr( + lang.Expr.Exists( lang.QuantifierBounds( - qBounds.iterator.map( - (id, qExpr) => - lang.QuantifierBound( - lang.Id().like(id), - qExpr.mkNode - ))), - expr.mkNode - ))) + qBounds.iterator.map((id, qExpr) => + lang.QuantifierBound( + lang.Id().like(id), + qExpr.mkNode, + ), + ), + ), + expr.mkNode, + ), + ), + ) | on( parent(lang.Expr) *> skip(tok(TLAReader.LaTexLike).src("\\E")) ~ field(repeatedSepBy1(`,`)(matchQuantifierIds())) ~ skip(TLAReader.`:`) ~ field(rawExpression) - ~ trailing + ~ trailing, ).rewrite: (qBounds, expr) => - splice( - lang.Expr(lang.Expr.Exists( + splice( + lang.Expr( + lang.Expr.Exists( lang.QuantifierBounds( - qBounds.iterator.map( - (ids, qExpr) => - lang.QuantifierBound( - lang.Ids( - ids.iterator.map( - id => lang.Id().like(id) - ) - ), - qExpr.mkNode - ))), - expr.mkNode - ))) + qBounds.iterator.map((ids, qExpr) => + lang.QuantifierBound( + lang.Ids( + ids.iterator.map(id => lang.Id().like(id)), + ), + qExpr.mkNode, + ), + ), + ), + expr.mkNode, + ), + ), + ) | on( parent(lang.Expr) *> skip(tok(TLAReader.LaTexLike).src("\\A")) ~ field(repeatedSepBy1(`,`)(matchQuantifierId())) ~ skip(TLAReader.`:`) ~ field(rawExpression) - ~ trailing + ~ trailing, ).rewrite: (qBounds, expr) => - splice( - lang.Expr(lang.Expr.Forall( + splice( + lang.Expr( + lang.Expr.Forall( lang.QuantifierBounds( - qBounds.iterator.map( - (id, qExpr) => - lang.QuantifierBound( - lang.Id().like(id), - qExpr.mkNode - ))), - expr.mkNode - ))) + qBounds.iterator.map((id, qExpr) => + lang.QuantifierBound( + lang.Id().like(id), + qExpr.mkNode, + ), + ), + ), + expr.mkNode, + ), + ), + ) | on( parent(lang.Expr) *> skip(tok(TLAReader.LaTexLike).src("\\A")) ~ field(repeatedSepBy1(`,`)(matchQuantifierIds())) ~ skip(TLAReader.`:`) ~ field(rawExpression) - ~ trailing + ~ trailing, ).rewrite: (qBounds, expr) => - splice( - lang.Expr(lang.Expr.Forall( + splice( + lang.Expr( + lang.Expr.Forall( lang.QuantifierBounds( - qBounds.iterator.map( - (ids, qExpr) => - lang.QuantifierBound( - lang.Ids( - ids.iterator.map( - id => lang.Id().like(id) - ) - ), - qExpr.mkNode - ))), - expr.mkNode - ))) + qBounds.iterator.map((ids, qExpr) => + lang.QuantifierBound( + lang.Ids( + ids.iterator.map(id => lang.Id().like(id)), + ), + qExpr.mkNode, + ), + ), + ), + expr.mkNode, + ), + ), + ) | on( parent(lang.Expr) *> skip(tok(defns.CHOOSE)) ~ field(matchQuantifierId()) ~ skip(TLAReader.`:`) ~ field(rawExpression) - ~ trailing + ~ trailing, ).rewrite: (qBound, expr) => - qBound match - case (id, qExpr) => - splice( - lang.Expr(lang.Expr.Choose( + qBound match + case (id, qExpr) => + splice( + lang.Expr( + lang.Expr.Choose( lang.QuantifierBound( lang.Id().like(id), - qExpr.mkNode + qExpr.mkNode, ), - expr.mkNode - ))) + expr.mkNode, + ), + ), + ) // TODO: tuple qbound // id nil // tuple nil @@ -331,183 +435,216 @@ object ExprParser extends PassSeq: .rules: on( parent(lang.Expr) *> - TLAReader.Alpha + TLAReader.Alpha, ).rewrite: name => splice( lang.Expr( - lang.Id().like(name) - )) + lang.Id().like(name), + ), + ) | on( - parent(lang.Expr) *> - TLAReader.NumberLiteral + parent(lang.Expr) *> + TLAReader.NumberLiteral, ).rewrite: lit => splice(lang.Expr(lang.Expr.NumberLiteral().like(lit))) | on( parent(lang.Expr) *> - TLAReader.StringLiteral + TLAReader.StringLiteral, ).rewrite: lit => splice(lang.Expr(lang.Expr.StringLiteral().like(lit))) | on( parent(lang.Expr) *> tok(TLAReader.BracesGroup) *> - children: - field(repeatedSepBy(`,`)(rawExpression)) - ~ eof + children: + field(repeatedSepBy(`,`)(rawExpression)) + ~ eof, ).rewrite: exprs => splice( lang.Expr( - lang.Expr.SetLiteral(exprs.iterator.map(_.mkNode)) - )) + lang.Expr.SetLiteral(exprs.iterator.map(_.mkNode)), + ), + ) | on( parent(lang.Expr) *> tok(TLAReader.TupleGroup).product( children( field(repeatedSepBy(`,`)(rawExpression)) - ~ eof - )) + ~ eof, + ), + ), ).rewrite: (lit, elems) => splice( lang.Expr( - lang.Expr.TupleLiteral(elems.iterator.map(_.mkNode)).like(lit) - )) + lang.Expr.TupleLiteral(elems.iterator.map(_.mkNode)).like(lit), + ), + ) | on( parent(lang.Expr) *> tok(TLAReader.SqBracketsGroup) *> - children: - field( - repeatedSepBy1(`,`)( - field(TLAReader.Alpha) - ~ skip(`|->`) - ~ field(rawExpression) - ~ trailing - )) - ~ eof + children: + field( + repeatedSepBy1(`,`)( + field(TLAReader.Alpha) + ~ skip(`|->`) + ~ field(rawExpression) + ~ trailing, + ), + ) + ~ eof, ).rewrite: fields => splice( lang.Expr( lang.Expr.RecordLiteral( - fields.iterator.map( - (alpha, expr) => - lang.Expr.RecordLiteral.Field( - lang.Id().like(alpha.unparent()), - expr.mkNode - ))))) + fields.iterator.map((alpha, expr) => + lang.Expr.RecordLiteral.Field( + lang.Id().like(alpha.unparent()), + expr.mkNode, + ), + ), + ), + ), + ) | on( parent(lang.Expr) *> field(lang.Expr) ~ skip(defns.`.`) - ~ field(lang.Expr.withChildren( - field(lang.Id) - ~ eof - )) - ~ trailing + ~ field( + lang.Expr.withChildren( + field(lang.Id) + ~ eof, + ), + ) + ~ trailing, ).rewrite: (expr, id) => splice( lang.Expr( lang.Expr.Project( lang.Expr( - expr.unparent() + expr.unparent(), ), - id.unparent() - ))) + id.unparent(), + ), + ), + ) | on( parent(lang.Expr) *> tok(TLAReader.SqBracketsGroup) *> - children: - field( - repeatedSepBy1(`,`)( - field(TLAReader.Alpha) - ~ skip(`:`) - ~ field(rawExpression) - ~ trailing - )) - ~ eof + children: + field( + repeatedSepBy1(`,`)( + field(TLAReader.Alpha) + ~ skip(`:`) + ~ field(rawExpression) + ~ trailing, + ), + ) + ~ eof, ).rewrite: fields => splice( lang.Expr( lang.Expr.RecordSetLiteral( - fields.iterator.map( - (alpha, expr) => - lang.Expr.RecordSetLiteral.Field( - lang.Id().like(alpha.unparent()), - expr.mkNode - ))))) - | on( + fields.iterator.map((alpha, expr) => + lang.Expr.RecordSetLiteral.Field( + lang.Id().like(alpha.unparent()), + expr.mkNode, + ), + ), + ), + ), + ) + | on( parent(lang.Expr) *> field(lang.Expr) ~ field(tok(defns.InfixOperator.instances.filter(_ != defns.`.`)*)) ~ field(lang.Expr) - ~ eof + ~ eof, ).rewrite: (left, op, right) => splice( - lang.Expr(TmpInfixGroup( - op.unparent(), - left.unparent(), - right.unparent() - ))) + lang.Expr( + TmpInfixGroup( + op.unparent(), + left.unparent(), + right.unparent(), + ), + ), + ) | on( parent(lang.Expr) *> - field(tok(defns.PrefixOperator.instances*)) - ~ field(lang.Expr) - ~ eof + field(tok(defns.PrefixOperator.instances*)) + ~ field(lang.Expr) + ~ eof, ).rewrite: (op, expr) => splice( - lang.Expr(TmpUnaryGroup( - op.unparent(), - expr.unparent(), - ))) + lang.Expr( + TmpUnaryGroup( + op.unparent(), + expr.unparent(), + ), + ), + ) | on( parent(lang.Expr) *> - field(lang.Expr) - ~ field(tok(defns.PostfixOperator.instances*)) - ~ trailing + field(lang.Expr) + ~ field(tok(defns.PostfixOperator.instances*)) + ~ trailing, ).rewrite: (expr, op) => splice( - lang.Expr(TmpUnaryGroup( - op.unparent(), - expr.unparent(), - ))) + lang.Expr( + TmpUnaryGroup( + op.unparent(), + expr.unparent(), + ), + ), + ) | on( parent(lang.Expr) *> field(lang.Expr) - ~ field(tok(TLAReader.SqBracketsGroup) *> - children: - field(repeatedSepBy(`,`)(rawExpression)) - ~ eof - ) - ~ eof + ~ field( + tok(TLAReader.SqBracketsGroup) *> + children: + field(repeatedSepBy(`,`)(rawExpression)) + ~ eof, + ) + ~ eof, ).rewrite: (callee, args) => splice( - lang.Expr(lang.Expr.FnCall( - callee.unparent(), - args match - case List(expr) => - expr.mkNode - case _ => - lang.Expr(lang.Expr.TupleLiteral( - args.iterator.map(_.mkNode) - ))))) + lang.Expr( + lang.Expr.FnCall( + callee.unparent(), + args match + case List(expr) => + expr.mkNode + case _ => + lang.Expr( + lang.Expr.TupleLiteral( + args.iterator.map(_.mkNode), + ), + ), + ), + ), + ) | on( parent(lang.Expr) *> skip(defns.CASE) ~ field( repeatedSepBy(defns.`[]`)( field(lang.Expr) - ~ skip(defns.-) - ~ skip(defns.>) - ~ field(lang.Expr) - ~ trailing - )) + ~ skip(defns.-) + ~ skip(defns.>) + ~ field(lang.Expr) + ~ trailing, + ), + ) ~ field( - optional( - skip(defns.OTHER) + optional( + skip(defns.OTHER) ~ skip(defns.-) ~ skip(defns.>) ~ field(lang.Expr) - ~ eof - ) - ) - ~ eof + ~ eof, + ), + ) + ~ eof, ).rewrite: (cases, other) => splice( lang.Expr( @@ -517,41 +654,50 @@ object ExprParser extends PassSeq: lang.Expr.Case.Branch( pred.unparent(), branch.unparent(), - ))), + ), + ), + ), lang.Expr.Case.Other( other match - case None => lang.Expr.Case.Other.None() - case Some(expr) => expr.unparent() - ) - ))) + case None => lang.Expr.Case.Other.None() + case Some(expr) => expr.unparent(), + ), + ), + ), + ) | on( parent(lang.Expr) *> - field(tok(TLAReader.LetGroup).product( - children( - field( - repeated1: - tok(lang.Operator) - | tok(lang.ModuleDefinition) - | tok(lang.Recursive) - ) - ~ eof - ) - )) + field( + tok(TLAReader.LetGroup).product( + children( + field( + repeated1: + tok(lang.Operator) + | tok(lang.ModuleDefinition) + | tok(lang.Recursive), + ) + ~ eof, + ), + ), + ) ~ field(lang.Expr) - ~ trailing - ).rewrite: (let, expr) => - splice( - lang.Expr( + ~ trailing, + ).rewrite: (let, expr) => + splice( + lang + .Expr( lang.Expr.Let( lang.Expr.Let.Defns( - let._2.iterator.map(_.unparent()) + let._2.iterator.map(_.unparent()), ), - expr.unparent() - )).like(let._1) - ) + expr.unparent(), + ), + ) + .like(let._1), + ) // TODO: Function // TODO: SetComprehension {expr : x \in y} - // TODO: SetRefinement {x \in y : bool} + // TODO: SetRefinement {x \in y : bool} // {x \in y : p \in q} TODO: look in the book // TODO: Choose // TODO: Except @@ -565,57 +711,57 @@ object ExprParser extends PassSeq: ~ field(lang.Expr) ~ skip(defns.ELSE) ~ field(lang.Expr) - ~ trailing + ~ trailing, ).rewrite: (pred, t, f) => splice( lang.Expr.If( pred.unparent(), t.unparent(), - f.unparent() - )) + f.unparent(), + ), + ) | on( parent(lang.Expr) *> tok(TLAReader.ParenthesesGroup) *> - children: - field(rawExpression) - ~ eof + children: + field(rawExpression) + ~ eof, ).rewrite: rawExpr => splice( - lang.Expr(rawExpr.mkNode) + lang.Expr(rawExpr.mkNode), ) *> pass(once = false, strategy = pass.bottomUp) // resolve Alphas .rules: on( parent(lang.Expr) *> - lang.Id + lang.Id, ).rewrite: name => splice( lang.Expr( lang.Expr.OpCall( name.unparent(), lang.Expr.OpCall.Params(), - ))) + ), + ), + ) end buildExpressions val reorderOperations = passDef: wellformed := prevWellformed.makeDerived: - lang.Expr.removeCases( - TmpInfixGroup, - TmpUnaryGroup) + lang.Expr.removeCases(TmpInfixGroup, TmpUnaryGroup) pass(once = false, strategy = pass.bottomUp) .rules: on( parent(lang.Expr) *> field(TmpInfixGroup.withChildren: - defns.InfixOperator.instances - .iterator - .map: op => - field(op) + defns.InfixOperator.instances.iterator + .map: op => + field(op) ~ highPredInfixInfix(op) ~ field(lang.Expr) ~ eof - .reduce(_ | _)) - ~ eof + .reduce(_ | _)) + ~ eof, ).rewrite: (curOp, left, right) => left match case (op, expr1, expr2) => @@ -623,114 +769,129 @@ object ExprParser extends PassSeq: TmpInfixGroup( op.unparent(), expr1.unparent(), - lang.Expr(TmpInfixGroup( - curOp.unparent(), - expr2.unparent(), - right.unparent() - )))) - | on( + lang.Expr( + TmpInfixGroup( + curOp.unparent(), + expr2.unparent(), + right.unparent(), + ), + ), + ), + ) + | on( parent(lang.Expr) *> field(TmpInfixGroup.withChildren: - defns.InfixOperator.instances - .iterator - .map: op => - field(op) + defns.InfixOperator.instances.iterator + .map: op => + field(op) ~ field(lang.Expr) ~ highPredInfixInfix(op) ~ eof - .reduce(_ | _)) - ~ eof + .reduce(_ | _)) + ~ eof, ).rewrite: (curOp, left, right) => right match case (op, expr1, expr2) => splice( TmpInfixGroup( op.unparent(), - lang.Expr(TmpInfixGroup( - curOp.unparent(), - left.unparent(), - expr1.unparent() - )), - expr2.unparent())) + lang.Expr( + TmpInfixGroup( + curOp.unparent(), + left.unparent(), + expr1.unparent(), + ), + ), + expr2.unparent(), + ), + ) | on( parent(lang.Expr) *> field(TmpInfixGroup.withChildren: - defns.InfixOperator.instances - .iterator - .map: op => - field(op) + defns.InfixOperator.instances.iterator + .map: op => + field(op) ~ highPredInfixUnary(op) ~ field(lang.Expr) ~ eof - .reduce(_ | _)) - ~ eof + .reduce(_ | _)) + ~ eof, ).rewrite: (curOp, left, right) => left match case (op, expr) => splice( TmpUnaryGroup( op.unparent(), - lang.Expr(TmpInfixGroup( - curOp.unparent(), - expr.unparent(), - right.unparent() - )))) + lang.Expr( + TmpInfixGroup( + curOp.unparent(), + expr.unparent(), + right.unparent(), + ), + ), + ), + ) | on( parent(lang.Expr) *> field(TmpInfixGroup.withChildren: - defns.InfixOperator.instances - .iterator - .map: op => - field(op) + defns.InfixOperator.instances.iterator + .map: op => + field(op) ~ field(lang.Expr) ~ highPredInfixUnary(op) ~ eof - .reduce(_ | _)) - ~ eof + .reduce(_ | _)) + ~ eof, ).rewrite: (curOp, left, right) => right match case (op, expr) => splice( TmpUnaryGroup( op.unparent(), - lang.Expr(TmpInfixGroup( - curOp.unparent(), - left.unparent(), - expr.unparent() - )))) + lang.Expr( + TmpInfixGroup( + curOp.unparent(), + left.unparent(), + expr.unparent(), + ), + ), + ), + ) | on( parent(lang.Expr) *> field(TmpUnaryGroup.withChildren: - defns.PrefixOperator.instances - .iterator - .map: op => - field(op) + defns.PrefixOperator.instances.iterator + .map: op => + field(op) ~ highPredUnaryInfix(op) ~ eof - .reduce(_ | _)) - ~ eof + .reduce(_ | _)) + ~ eof, ).rewrite: (curOp, infixGroup) => infixGroup match case (op, left, right) => splice( TmpInfixGroup( op.unparent(), - lang.Expr(TmpUnaryGroup( - curOp.unparent(), - left.unparent() - )), - right.unparent())) + lang.Expr( + TmpUnaryGroup( + curOp.unparent(), + left.unparent(), + ), + ), + right.unparent(), + ), + ) | on( parent(lang.Expr) *> field(TmpUnaryGroup.withChildren: - defns.PostfixOperator.instances - .iterator - .map: op => - field(op) + defns.PostfixOperator.instances.iterator + .map: op => + field(op) ~ highPredUnaryInfix(op) ~ eof - .reduce(_ | _)) - ~ eof + .reduce(_ | _)) + ~ eof, ).rewrite: (curOp, infixGroup) => infixGroup match case (op, left, right) => @@ -738,31 +899,34 @@ object ExprParser extends PassSeq: TmpInfixGroup( op.unparent(), left.unparent(), - lang.Expr(TmpUnaryGroup( - curOp.unparent(), - right.unparent() - )))) + lang.Expr( + TmpUnaryGroup( + curOp.unparent(), + right.unparent(), + ), + ), + ), + ) *> pass(once = false, strategy = pass.bottomUp) // assoc related errors .rules: on( parent(lang.Expr) *> field(TmpInfixGroup.withChildren: - defns.InfixOperator.instances - .iterator - .map: op => - field(op) + defns.InfixOperator.instances.iterator + .map: op => + field(op) ~ badPredInfixInfix(op) ~ field(lang.Expr) ~ eof - .reduce(_ | _)) - ~ eof + .reduce(_ | _)) + ~ eof, ).rewrite: (curOp, left, right) => left match case (op, expr1, expr2) => splice( Node(Builtin.Error)( Builtin.Error.Message( // todo: use src - s"$curOp and $op must have different precedence, or be duplicates of an associative operator." + s"$curOp and $op must have different precedence, or be duplicates of an associative operator.", ), Builtin.Error.AST( TmpInfixGroup( @@ -770,28 +934,31 @@ object ExprParser extends PassSeq: TmpInfixGroup( op.unparent(), expr1.unparent(), - expr2.unparent() + expr2.unparent(), ), - right.unparent())))) + right.unparent(), + ), + ), + ), + ) | on( parent(lang.Expr) *> field(TmpInfixGroup.withChildren: - defns.InfixOperator.instances - .iterator - .map: op => - field(op) + defns.InfixOperator.instances.iterator + .map: op => + field(op) ~ field(lang.Expr) ~ badPredInfixInfix((op)) ~ eof - .reduce(_ | _)) - ~ eof + .reduce(_ | _)) + ~ eof, ).rewrite: (curOp, left, right) => right match case (op, expr1, expr2) => splice( Node(Builtin.Error)( Builtin.Error.Message( - s"$curOp and $op must have different precedence, or be duplicates of an associative operator." + s"$curOp and $op must have different precedence, or be duplicates of an associative operator.", ), Builtin.Error.AST( TmpInfixGroup( @@ -800,27 +967,30 @@ object ExprParser extends PassSeq: TmpInfixGroup( op.unparent(), expr1.unparent(), - expr2.unparent() - ))))) + expr2.unparent(), + ), + ), + ), + ), + ) | on( parent(lang.Expr) *> field(TmpInfixGroup.withChildren: - defns.InfixOperator.instances - .iterator - .map: op => - field(op) + defns.InfixOperator.instances.iterator + .map: op => + field(op) ~ badPredInfixUnary(op) ~ field(lang.Expr) ~ eof - .reduce(_ | _)) - ~ eof + .reduce(_ | _)) + ~ eof, ).rewrite: (curOp, left, right) => left match case (op, expr) => splice( Node(Builtin.Error)( Builtin.Error.Message( - s"$curOp and $op must have different precedence." + s"$curOp and $op must have different precedence.", ), Builtin.Error.AST( TmpInfixGroup( @@ -828,28 +998,30 @@ object ExprParser extends PassSeq: TmpUnaryGroup( op.unparent(), expr.unparent(), - )), - right.unparent() - ))) + ), + ), + right.unparent(), + ), + ), + ) | on( parent(lang.Expr) *> field(TmpInfixGroup.withChildren: - defns.InfixOperator.instances - .iterator - .map: op => - field(op) + defns.InfixOperator.instances.iterator + .map: op => + field(op) ~ field(lang.Expr) ~ badPredInfixUnary(op) ~ eof - .reduce(_ | _)) - ~ eof + .reduce(_ | _)) + ~ eof, ).rewrite: (curOp, left, right) => right match case (op, expr) => splice( Node(Builtin.Error)( Builtin.Error.Message( - s"$curOp and $op must have different precedence." + s"$curOp and $op must have different precedence.", ), Builtin.Error.AST( TmpInfixGroup( @@ -857,19 +1029,22 @@ object ExprParser extends PassSeq: left.unparent(), TmpUnaryGroup( op.unparent(), - expr.unparent() - ))))) + expr.unparent(), + ), + ), + ), + ), + ) | on( parent(lang.Expr) *> field(TmpUnaryGroup.withChildren: - defns.PrefixOperator.instances - .iterator - .map: op => - field(op) + defns.PrefixOperator.instances.iterator + .map: op => + field(op) ~ badPredUnaryInfix(op) ~ eof - .reduce(_ | _)) - ~ eof + .reduce(_ | _)) + ~ eof, ).rewrite: (curOp, infixGroup) => infixGroup match case (op, left, right) => @@ -887,14 +1062,13 @@ object ExprParser extends PassSeq: | on( parent(lang.Expr) *> field(TmpUnaryGroup.withChildren: - defns.PostfixOperator.instances - .iterator - .map: op => - field(op) + defns.PostfixOperator.instances.iterator + .map: op => + field(op) ~ badPredUnaryInfix(op) ~ eof - .reduce(_ | _)) - ~ eof + .reduce(_ | _)) + ~ eof, ).rewrite: (curOp, infixGroup) => infixGroup match case (op, left, right) => @@ -905,7 +1079,7 @@ object ExprParser extends PassSeq: TmpInfixGroup( op.unparent(), left.unparent(), - right.unparent() + right.unparent(), ), ), ) @@ -913,37 +1087,51 @@ object ExprParser extends PassSeq: .rules: on( parent(lang.Expr) *> - field(TmpInfixGroup.withChildren( - field(tok(defns.InfixOperator.instances*)) - ~ field(lang.Expr) - ~ field(lang.Expr) - ~ eof - )) - ~ eof + field( + TmpInfixGroup.withChildren( + field(tok(defns.InfixOperator.instances*)) + ~ field(lang.Expr) + ~ field(lang.Expr) + ~ eof, + ), + ) + ~ eof, ).rewrite: (op, right, left) => splice( - lang.Expr(lang.Expr.OpCall( - lang.OpSym(op.unparent()), - lang.Expr.OpCall.Params( - right.unparent(), - left.unparent() - )))) + lang.Expr( + lang.Expr.OpCall( + lang.OpSym(op.unparent()), + lang.Expr.OpCall.Params( + right.unparent(), + left.unparent(), + ), + ), + ), + ) | on( parent(lang.Expr) *> - field(TmpUnaryGroup.withChildren( - field(tok(defns.PrefixOperator.instances*) - | tok(defns.PostfixOperator.instances*)) - ~ field(lang.Expr) - ~ eof - )) - ~ eof + field( + TmpUnaryGroup.withChildren( + field( + tok(defns.PrefixOperator.instances*) + | tok(defns.PostfixOperator.instances*), + ) + ~ field(lang.Expr) + ~ eof, + ), + ) + ~ eof, ).rewrite: (op, expr) => splice( - lang.Expr(lang.Expr.OpCall( - lang.OpSym(op.unparent()), - lang.Expr.OpCall.Params( - expr.unparent(), - )))) + lang.Expr( + lang.Expr.OpCall( + lang.OpSym(op.unparent()), + lang.Expr.OpCall.Params( + expr.unparent(), + ), + ), + ), + ) end reorderOperations val removeNestedExpr = passDef: @@ -954,9 +1142,9 @@ object ExprParser extends PassSeq: .rules: on( tok(lang.Expr) *> - onlyChild(lang.Expr) + onlyChild(lang.Expr), ).rewrite: child => splice( - child.unparent() + child.unparent(), ) end removeNestedExpr diff --git a/langs/tla/ExprParser.test.scala b/langs/tla/ExprParser.test.scala index 5b98956..941f5a2 100644 --- a/langs/tla/ExprParser.test.scala +++ b/langs/tla/ExprParser.test.scala @@ -1,3 +1,17 @@ +// Copyright 2024-2025 Forja Team +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + package forja.langs.tla import forja.* @@ -14,39 +28,39 @@ class ExprParserTests extends munit.FunSuite: val wrapped_str = Source.fromString( s"""---- MODULE TestMod ---- - |EXTENDS Naturals - |VARIABLE temp - | - |Init == $str - |==== - """.stripMargin + |EXTENDS Naturals + |VARIABLE temp + | + |Init == $str + |==== + """.stripMargin, ) val top = TLAReader(SourceRange.entire(wrapped_str)) TLAParser(top) ExprParser(top) Node.Top( top(lang.Module)(lang.Module.Defns)(lang.Operator)( - lang.Expr - ).unparentedChildren + lang.Expr, + ).unparentedChildren, ) extension (str: String) def withoutParse: Node.Top = val wrapped_str = Source.fromString( s"""---- MODULE TestMod ---- - |EXTENDS Naturals - |VARIABLE temp - | - |Init == $str - |==== - """.stripMargin + |EXTENDS Naturals + |VARIABLE temp + | + |Init == $str + |==== + """.stripMargin, ) val top = TLAReader(SourceRange.entire(wrapped_str)) TLAParser(top) Node.Top( top(lang.Module)(lang.Module.Defns)(lang.Operator)( - lang.Expr - ).unparentedChildren + lang.Expr, + ).unparentedChildren, ) extension (top: Node.Top) @@ -60,13 +74,17 @@ class ExprParserTests extends munit.FunSuite: lang.Id("test"), lang.Operator.Params(), lang.Expr( - top.unparentedChildren - ))))) + top.unparentedChildren, + ), + ), + ), + ), + ) ExprParser(freshTop) Node.Top( freshTop(lang.Module)(lang.Module.Defns)(lang.Operator)( - lang.Expr - ).unparentedChildren + lang.Expr, + ).unparentedChildren, ) test("NumberLiteral"): @@ -75,11 +93,11 @@ class ExprParserTests extends munit.FunSuite: test("StringLiteral"): assertEquals( "\"string\"".parseStr, - Node.Top(lang.Expr.StringLiteral("string")) + Node.Top(lang.Expr.StringLiteral("string")), ) assertEquals( "\"string\\nnewline\"".parseStr, - Node.Top(lang.Expr.StringLiteral("string\nnewline")) + Node.Top(lang.Expr.StringLiteral("string\nnewline")), ) test("Set Literal"): @@ -89,13 +107,15 @@ class ExprParserTests extends munit.FunSuite: lang.Expr.SetLiteral( lang.Expr(lang.Expr.NumberLiteral("1")), lang.Expr(lang.Expr.NumberLiteral("2")), - lang.Expr(lang.Expr.NumberLiteral("3")) - ))) + lang.Expr(lang.Expr.NumberLiteral("3")), + ), + ), + ) assertEquals( "{}".parseStr, - Node.Top(lang.Expr.SetLiteral()) + Node.Top(lang.Expr.SetLiteral()), ) - + test("TupleLiteral"): assertEquals( "<<1, 2, 3>>".parseStr, @@ -103,13 +123,16 @@ class ExprParserTests extends munit.FunSuite: lang.Expr.TupleLiteral( lang.Expr(lang.Expr.NumberLiteral("1")), lang.Expr(lang.Expr.NumberLiteral("2")), - lang.Expr(lang.Expr.NumberLiteral("3")) - ))) + lang.Expr(lang.Expr.NumberLiteral("3")), + ), + ), + ) assertEquals( "<<>>".parseStr, Node.Top( - lang.Expr.TupleLiteral() - )) + lang.Expr.TupleLiteral(), + ), + ) test("RecordLiteral"): assertEquals( @@ -118,13 +141,16 @@ class ExprParserTests extends munit.FunSuite: lang.Expr.RecordLiteral( lang.Expr.RecordLiteral.Field( lang.Id("x"), - lang.Expr(lang.Expr.NumberLiteral("2")) + lang.Expr(lang.Expr.NumberLiteral("2")), ), lang.Expr.RecordLiteral.Field( lang.Id("y"), - lang.Expr(lang.Expr.NumberLiteral("3")) - )))) - + lang.Expr(lang.Expr.NumberLiteral("3")), + ), + ), + ), + ) + test("Projection (Record Field Acess)"): assertEquals( "x.y".parseStr, @@ -133,21 +159,32 @@ class ExprParserTests extends munit.FunSuite: lang.Expr( lang.Expr.OpCall( lang.Id("x"), - lang.Expr.OpCall.Params() - )), - lang.Id("y")))) + lang.Expr.OpCall.Params(), + ), + ), + lang.Id("y"), + ), + ), + ) assertEquals( "x.y.z".parseStr, Node.Top( lang.Expr.Project( - lang.Expr(lang.Expr.Project( - lang.Expr( - lang.Expr.OpCall( - lang.Id("x"), - lang.Expr.OpCall.Params() - )), - lang.Id("y"))), - lang.Id("z")))) + lang.Expr( + lang.Expr.Project( + lang.Expr( + lang.Expr.OpCall( + lang.Id("x"), + lang.Expr.OpCall.Params(), + ), + ), + lang.Id("y"), + ), + ), + lang.Id("z"), + ), + ), + ) assertEquals( "[y |-> 2].y".parseStr, Node.Top( @@ -156,10 +193,14 @@ class ExprParserTests extends munit.FunSuite: lang.Expr.RecordLiteral( lang.Expr.RecordLiteral.Field( lang.Id("y"), - lang.Expr(lang.Expr.NumberLiteral("2")) - ) - )), - lang.Id("y")))) + lang.Expr(lang.Expr.NumberLiteral("2")), + ), + ), + ), + lang.Id("y"), + ), + ), + ) test("RecordSetLiteral"): assertEquals( @@ -171,8 +212,13 @@ class ExprParserTests extends munit.FunSuite: lang.Expr( lang.Expr.SetLiteral( lang.Expr(lang.Expr.NumberLiteral("1")), - lang.Expr(lang.Expr.NumberLiteral("2")) - )))))) + lang.Expr(lang.Expr.NumberLiteral("2")), + ), + ), + ), + ), + ), + ) test("Name"): assertEquals( @@ -180,8 +226,10 @@ class ExprParserTests extends munit.FunSuite: Node.Top( lang.Expr.OpCall( lang.Id("x"), - lang.Expr.OpCall.Params() - ))) + lang.Expr.OpCall.Params(), + ), + ), + ) test("Single Binary Operator"): assertEquals( @@ -189,12 +237,15 @@ class ExprParserTests extends munit.FunSuite: Node.Top( lang.Expr.OpCall( lang.OpSym( - defns.+("+") + defns.+("+"), ), lang.Expr.OpCall.Params( lang.Expr(lang.Expr.NumberLiteral("5")), - lang.Expr(lang.Expr.NumberLiteral("6")) - )))) + lang.Expr(lang.Expr.NumberLiteral("6")), + ), + ), + ), + ) assertEquals( "5 $ x".parseStr, Node.Top( @@ -205,30 +256,47 @@ class ExprParserTests extends munit.FunSuite: lang.Expr( lang.Expr.OpCall( lang.Id("x"), - lang.Expr.OpCall.Params() - )))))) - + lang.Expr.OpCall.Params(), + ), + ), + ), + ), + ), + ) + test("Single Unary Operator"): assertEquals( "UNION A".parseStr, - Node.Top(lang.Expr.OpCall( - lang.OpSym(defns.UNION("UNION")), - lang.Expr.OpCall.Params( - lang.Expr( - lang.Expr.OpCall( - lang.Id("A"), - lang.Expr.OpCall.Params() - )))))) + Node.Top( + lang.Expr.OpCall( + lang.OpSym(defns.UNION("UNION")), + lang.Expr.OpCall.Params( + lang.Expr( + lang.Expr.OpCall( + lang.Id("A"), + lang.Expr.OpCall.Params(), + ), + ), + ), + ), + ), + ) assertEquals( "x'".parseStr, - Node.Top(lang.Expr.OpCall( - lang.OpSym(defns.`'`("'")), - lang.Expr.OpCall.Params( - lang.Expr( - lang.Expr.OpCall( - lang.Id("x"), - lang.Expr.OpCall.Params() - )))))) + Node.Top( + lang.Expr.OpCall( + lang.OpSym(defns.`'`("'")), + lang.Expr.OpCall.Params( + lang.Expr( + lang.Expr.OpCall( + lang.Id("x"), + lang.Expr.OpCall.Params(), + ), + ), + ), + ), + ), + ) test("Precedence: Infix - Infix"): assertEquals( @@ -236,19 +304,25 @@ class ExprParserTests extends munit.FunSuite: Node.Top( lang.Expr.OpCall( lang.OpSym( - defns.+("+") + defns.+("+"), ), lang.Expr.OpCall.Params( lang.Expr( lang.Expr.OpCall( lang.OpSym( - defns.*("*") + defns.*("*"), ), lang.Expr.OpCall.Params( lang.Expr(lang.Expr.NumberLiteral("5")), - lang.Expr(lang.Expr.NumberLiteral("6")) - ))), - lang.Expr(lang.Expr.NumberLiteral("7")))))) + lang.Expr(lang.Expr.NumberLiteral("6")), + ), + ), + ), + lang.Expr(lang.Expr.NumberLiteral("7")), + ), + ), + ), + ) assertEquals( "1 + 8 * 6 - 9 * 3".parseStr, Node.Top( @@ -256,76 +330,130 @@ class ExprParserTests extends munit.FunSuite: lang.OpSym(defns.+("+")), lang.Expr.OpCall.Params( lang.Expr(lang.Expr.NumberLiteral("1")), - lang.Expr(lang.Expr.OpCall( - lang.OpSym(defns.-("-")), - lang.Expr.OpCall.Params( - lang.Expr(lang.Expr.OpCall( - lang.OpSym(defns.*("*")), - lang.Expr.OpCall.Params( - lang.Expr(lang.Expr.NumberLiteral("8")), - lang.Expr(lang.Expr.NumberLiteral("6")) - ))), - lang.Expr(lang.Expr.OpCall( - lang.OpSym(defns.*("*")), - lang.Expr.OpCall.Params( - lang.Expr(lang.Expr.NumberLiteral("9")), - lang.Expr(lang.Expr.NumberLiteral("3")) - )))))))))) + lang.Expr( + lang.Expr.OpCall( + lang.OpSym(defns.-("-")), + lang.Expr.OpCall.Params( + lang.Expr( + lang.Expr.OpCall( + lang.OpSym(defns.*("*")), + lang.Expr.OpCall.Params( + lang.Expr(lang.Expr.NumberLiteral("8")), + lang.Expr(lang.Expr.NumberLiteral("6")), + ), + ), + ), + lang.Expr( + lang.Expr.OpCall( + lang.OpSym(defns.*("*")), + lang.Expr.OpCall.Params( + lang.Expr(lang.Expr.NumberLiteral("9")), + lang.Expr(lang.Expr.NumberLiteral("3")), + ), + ), + ), + ), + ), + ), + ), + ), + ), + ) test("Precedence: Infix - Prefix"): assertEquals( "~x /\\ y".parseStr, - Node.Top(lang.Expr.OpCall( - lang.OpSym(defns./\("/\\")), - lang.Expr.OpCall.Params( - lang.Expr(lang.Expr.OpCall( - lang.OpSym(defns.~("~")), - lang.Expr.OpCall.Params( - lang.Expr(lang.Expr.OpCall( - lang.Id("x"), - lang.Expr.OpCall.Params() - ))))), - lang.Expr(lang.Expr.OpCall( - lang.Id("y"), - lang.Expr.OpCall.Params() - )))))) + Node.Top( + lang.Expr.OpCall( + lang.OpSym(defns./\("/\\")), + lang.Expr.OpCall.Params( + lang.Expr( + lang.Expr.OpCall( + lang.OpSym(defns.~("~")), + lang.Expr.OpCall.Params( + lang.Expr( + lang.Expr.OpCall( + lang.Id("x"), + lang.Expr.OpCall.Params(), + ), + ), + ), + ), + ), + lang.Expr( + lang.Expr.OpCall( + lang.Id("y"), + lang.Expr.OpCall.Params(), + ), + ), + ), + ), + ), + ) assertEquals( "~x \\in y".parseStr, - Node.Top(lang.Expr.OpCall( - lang.OpSym(defns.~("~")), - lang.Expr.OpCall.Params( - lang.Expr(lang.Expr.OpCall( - lang.OpSym(defns.`\\in`("\\in")), - lang.Expr.OpCall.Params( - lang.Expr(lang.Expr.OpCall( - lang.Id("x"), - lang.Expr.OpCall.Params() - )), - lang.Expr(lang.Expr.OpCall( - lang.Id("y"), - lang.Expr.OpCall.Params() - ))))))))) - + Node.Top( + lang.Expr.OpCall( + lang.OpSym(defns.~("~")), + lang.Expr.OpCall.Params( + lang.Expr( + lang.Expr.OpCall( + lang.OpSym(defns.`\\in`("\\in")), + lang.Expr.OpCall.Params( + lang.Expr( + lang.Expr.OpCall( + lang.Id("x"), + lang.Expr.OpCall.Params(), + ), + ), + lang.Expr( + lang.Expr.OpCall( + lang.Id("y"), + lang.Expr.OpCall.Params(), + ), + ), + ), + ), + ), + ), + ), + ), + ) + test("Precedence: Infix - Postfix"): assertEquals( "1 + x' * 2".parseStr, - Node.Top(lang.Expr.OpCall( - lang.OpSym(defns.+("+")), - lang.Expr.OpCall.Params( - lang.Expr(lang.Expr.NumberLiteral("1")), - lang.Expr(lang.Expr.OpCall( - lang.OpSym(defns.*("*")), - lang.Expr.OpCall.Params( - lang.Expr(lang.Expr.OpCall( - lang.OpSym(defns.`'`("'")), + Node.Top( + lang.Expr.OpCall( + lang.OpSym(defns.+("+")), + lang.Expr.OpCall.Params( + lang.Expr(lang.Expr.NumberLiteral("1")), + lang.Expr( + lang.Expr.OpCall( + lang.OpSym(defns.*("*")), lang.Expr.OpCall.Params( - lang.Expr(lang.Expr.OpCall( - lang.Id("x"), - lang.Expr.OpCall.Params() - ))))), - lang.Expr(lang.Expr.NumberLiteral("2")) - ))))))) - + lang.Expr( + lang.Expr.OpCall( + lang.OpSym(defns.`'`("'")), + lang.Expr.OpCall.Params( + lang.Expr( + lang.Expr.OpCall( + lang.Id("x"), + lang.Expr.OpCall.Params(), + ), + ), + ), + ), + ), + lang.Expr(lang.Expr.NumberLiteral("2")), + ), + ), + ), + ), + ), + ), + ) + test("Precedence: Unary - Unary"): assertEquals( "[] ~x".parseStr, @@ -333,16 +461,26 @@ class ExprParserTests extends munit.FunSuite: lang.Expr.OpCall( lang.OpSym(defns.`[]`("[]")), lang.Expr.OpCall.Params( - lang.Expr(lang.Expr.OpCall( - lang.OpSym(defns.~("~")), - lang.Expr.OpCall.Params( - lang.Expr(lang.Expr.OpCall( - lang.Id("x"), - lang.Expr.OpCall.Params() - ))))))))) - - // TODO???: postfix postfix: never allowed - + lang.Expr( + lang.Expr.OpCall( + lang.OpSym(defns.~("~")), + lang.Expr.OpCall.Params( + lang.Expr( + lang.Expr.OpCall( + lang.Id("x"), + lang.Expr.OpCall.Params(), + ), + ), + ), + ), + ), + ), + ), + ), + ) + + // TODO???: postfix postfix: never allowed + test("Precedence: Associative"): assertEquals( "1 + 2 + 3".parseStr, @@ -351,37 +489,47 @@ class ExprParserTests extends munit.FunSuite: lang.OpSym(defns.+("+")), lang.Expr.OpCall.Params( lang.Expr(lang.Expr.NumberLiteral("1")), - lang.Expr(lang.Expr.OpCall( - lang.OpSym(defns.+("+")), - lang.Expr.OpCall.Params( - lang.Expr(lang.Expr.NumberLiteral("2")), - lang.Expr(lang.Expr.NumberLiteral("3")) - ))))))) + lang.Expr( + lang.Expr.OpCall( + lang.OpSym(defns.+("+")), + lang.Expr.OpCall.Params( + lang.Expr(lang.Expr.NumberLiteral("2")), + lang.Expr(lang.Expr.NumberLiteral("3")), + ), + ), + ), + ), + ), + ), + ) assertEquals( "1 * 2 / 3".parseStr, - Node.Top(lang.Expr( - Builtin.Error( - s"forja.langs.tla.defns.* and forja.langs.tla.defns./ must have different precedence, or be duplicates of an associative operator.", - TmpInfixGroup( - defns.*("*"), - lang.Expr(lang.Expr.NumberLiteral("1")), + Node.Top( + lang.Expr( + Builtin.Error( + s"forja.langs.tla.defns.* and forja.langs.tla.defns./ must have different precedence, or be duplicates of an associative operator.", TmpInfixGroup( - defns./("/"), - lang.Expr(lang.Expr.NumberLiteral("2")), - lang.Expr(lang.Expr.NumberLiteral("3")), + defns.*("*"), + lang.Expr(lang.Expr.NumberLiteral("1")), + TmpInfixGroup( + defns./("/"), + lang.Expr(lang.Expr.NumberLiteral("2")), + lang.Expr(lang.Expr.NumberLiteral("3")), + ), ), ), ), - )), + ), ) - + // test("Precedence: Error"): // assertEquals( // "x \\in A \\in B".parseStr, // Node.Top(lang.Expr( // Node(Builtin.Error)( // Builtin.Error.Message( - // s"26:distcompiler.tla.defns.\\in and 26:distcompiler.tla.defns.\\in must have different precedence, or be duplicates of an associative operator." + /* s"26:distcompiler.tla.defns.\\in and 26:distcompiler.tla.defns.\\in must + * have different precedence, or be duplicates of an associative operator." */ // ), // Builtin.Error.AST( // lang.Expr.TmpInfixGroup( @@ -397,7 +545,8 @@ class ExprParserTests extends munit.FunSuite: // Node.Top(lang.Expr( // Node(Builtin.Error)( // Builtin.Error.Message( - // s"26:distcompiler.tla.defns.\\in and distcompiler.tla.defns.= must have different precedence, or be duplicates of an associative operator." + /* s"26:distcompiler.tla.defns.\\in and distcompiler.tla.defns.= must have + * different precedence, or be duplicates of an associative operator." */ // ), // Builtin.Error.AST( // lang.Expr.TmpInfixGroup( @@ -418,8 +567,11 @@ class ExprParserTests extends munit.FunSuite: lang.Expr.OpCall.Params( lang.Expr(lang.Expr.NumberLiteral("1")), lang.Expr(lang.Expr.NumberLiteral("2")), - lang.Expr(lang.Expr.NumberLiteral("3")) - )))) + lang.Expr(lang.Expr.NumberLiteral("3")), + ), + ), + ), + ) // TODO: conjunction alignment @@ -428,121 +580,158 @@ class ExprParserTests extends munit.FunSuite: "x[\"y\"]".parseStr, Node.Top( lang.Expr.FnCall( - lang.Expr(lang.Expr.OpCall( - lang.Id("x"), - lang.Expr.OpCall.Params() - )), - lang.Expr(lang.Expr.StringLiteral("y")) - ))) + lang.Expr( + lang.Expr.OpCall( + lang.Id("x"), + lang.Expr.OpCall.Params(), + ), + ), + lang.Expr(lang.Expr.StringLiteral("y")), + ), + ), + ) assertEquals( "x[1, 2, 3]".parseStr, Node.Top( lang.Expr.FnCall( - lang.Expr(lang.Expr.OpCall( - lang.Id("x"), - lang.Expr.OpCall.Params() - )), - lang.Expr(lang.Expr.TupleLiteral( - lang.Expr(lang.Expr.NumberLiteral("1")), - lang.Expr(lang.Expr.NumberLiteral("2")), - lang.Expr(lang.Expr.NumberLiteral("3")), - )) - ))) - + lang.Expr( + lang.Expr.OpCall( + lang.Id("x"), + lang.Expr.OpCall.Params(), + ), + ), + lang.Expr( + lang.Expr.TupleLiteral( + lang.Expr(lang.Expr.NumberLiteral("1")), + lang.Expr(lang.Expr.NumberLiteral("2")), + lang.Expr(lang.Expr.NumberLiteral("3")), + ), + ), + ), + ), + ) + test("If"): assertEquals( """IF A - |THEN 1 - |ELSE 2""".stripMargin.parseStr, + |THEN 1 + |ELSE 2""".stripMargin.parseStr, Node.Top( lang.Expr.If( lang.Expr( lang.Expr.OpCall( lang.Id("A"), - lang.Expr.OpCall.Params() - )), + lang.Expr.OpCall.Params(), + ), + ), lang.Expr(lang.Expr.NumberLiteral("1")), - lang.Expr(lang.Expr.NumberLiteral("2")) - ))) - + lang.Expr(lang.Expr.NumberLiteral("2")), + ), + ), + ) + test("Case"): assertEquals( """CASE A -> 1 - | [] B -> 2""".stripMargin.parseStr, + | [] B -> 2""".stripMargin.parseStr, Node.Top( lang.Expr.Case( lang.Expr.Case.Branches( lang.Expr.Case.Branch( - lang.Expr(lang.Expr.OpCall( - lang.Id("A"), - lang.Expr.OpCall.Params() - )), - lang.Expr(lang.Expr.NumberLiteral("1")) + lang.Expr( + lang.Expr.OpCall( + lang.Id("A"), + lang.Expr.OpCall.Params(), + ), + ), + lang.Expr(lang.Expr.NumberLiteral("1")), ), lang.Expr.Case.Branch( - lang.Expr(lang.Expr.OpCall( - lang.Id("B"), - lang.Expr.OpCall.Params() - )), - lang.Expr(lang.Expr.NumberLiteral("2")) - )), - lang.Expr.Case.Other(lang.Expr.Case.Other.None()) - ))) + lang.Expr( + lang.Expr.OpCall( + lang.Id("B"), + lang.Expr.OpCall.Params(), + ), + ), + lang.Expr(lang.Expr.NumberLiteral("2")), + ), + ), + lang.Expr.Case.Other(lang.Expr.Case.Other.None()), + ), + ), + ) assertEquals( """CASE A -> 1 - | [] B -> 2 - | OTHER -> 3""".stripMargin.parseStr, + | [] B -> 2 + | OTHER -> 3""".stripMargin.parseStr, Node.Top( lang.Expr.Case( lang.Expr.Case.Branches( lang.Expr.Case.Branch( - lang.Expr(lang.Expr.OpCall( - lang.Id("A"), - lang.Expr.OpCall.Params() - )), - lang.Expr(lang.Expr.NumberLiteral("1")) + lang.Expr( + lang.Expr.OpCall( + lang.Id("A"), + lang.Expr.OpCall.Params(), + ), + ), + lang.Expr(lang.Expr.NumberLiteral("1")), ), lang.Expr.Case.Branch( - lang.Expr(lang.Expr.OpCall( - lang.Id("B"), - lang.Expr.OpCall.Params() - )), - lang.Expr(lang.Expr.NumberLiteral("2")) - )), + lang.Expr( + lang.Expr.OpCall( + lang.Id("B"), + lang.Expr.OpCall.Params(), + ), + ), + lang.Expr(lang.Expr.NumberLiteral("2")), + ), + ), lang.Expr.Case.Other( - lang.Expr(lang.Expr.NumberLiteral("3")) - )))) - + lang.Expr(lang.Expr.NumberLiteral("3")), + ), + ), + ), + ) + test("LET"): assertEquals( """LET x == 1 - |y == 2 - |IN {y, x}""".stripMargin.parseStr, + |y == 2 + |IN {y, x}""".stripMargin.parseStr, Node.Top( lang.Expr.Let( lang.Expr.Let.Defns( lang.Operator( lang.Id("x"), lang.Operator.Params(), - lang.Expr(lang.Expr.NumberLiteral("1")) + lang.Expr(lang.Expr.NumberLiteral("1")), ), lang.Operator( lang.Id("y"), lang.Operator.Params(), - lang.Expr(lang.Expr.NumberLiteral("2")) - ) + lang.Expr(lang.Expr.NumberLiteral("2")), + ), ), lang.Expr( lang.Expr.SetLiteral( - lang.Expr(lang.Expr.OpCall( - lang.Id("y"), - lang.Expr.OpCall.Params() - )), - lang.Expr(lang.Expr.OpCall( - lang.Id("x"), - lang.Expr.OpCall.Params() - ))))))) - + lang.Expr( + lang.Expr.OpCall( + lang.Id("y"), + lang.Expr.OpCall.Params(), + ), + ), + lang.Expr( + lang.Expr.OpCall( + lang.Id("x"), + lang.Expr.OpCall.Params(), + ), + ), + ), + ), + ), + ), + ) + test("Exists"): assertEquals( "\\E x \\in {1, 2, 3} : x = 2".parseStr, @@ -551,20 +740,32 @@ class ExprParserTests extends munit.FunSuite: lang.QuantifierBounds( lang.QuantifierBound( lang.Id("x"), - lang.Expr(lang.Expr.SetLiteral( - lang.Expr(lang.Expr.NumberLiteral("1")), + lang.Expr( + lang.Expr.SetLiteral( + lang.Expr(lang.Expr.NumberLiteral("1")), + lang.Expr(lang.Expr.NumberLiteral("2")), + lang.Expr(lang.Expr.NumberLiteral("3")), + ), + ), + ), + ), + lang.Expr( + lang.Expr.OpCall( + lang.OpSym(defns.`=`("=")), + lang.Expr.OpCall.Params( + lang.Expr( + lang.Expr.OpCall( + lang.Id("x"), + lang.Expr.OpCall.Params(), + ), + ), lang.Expr(lang.Expr.NumberLiteral("2")), - lang.Expr(lang.Expr.NumberLiteral("3")) - )))), - lang.Expr(lang.Expr.OpCall( - lang.OpSym(defns.`=`("=")), - lang.Expr.OpCall.Params( - lang.Expr(lang.Expr.OpCall( - lang.Id("x"), - lang.Expr.OpCall.Params() - )), - lang.Expr(lang.Expr.NumberLiteral("2")) - )))))) + ), + ), + ), + ), + ), + ) assertEquals( "\\E <> \\in {1, 2, 3} : x = 2".parseStr, Node.Top( @@ -574,22 +775,34 @@ class ExprParserTests extends munit.FunSuite: lang.Ids( lang.Id("x"), lang.Id("y"), - lang.Id("z") + lang.Id("z"), ), - lang.Expr(lang.Expr.SetLiteral( - lang.Expr(lang.Expr.NumberLiteral("1")), + lang.Expr( + lang.Expr.SetLiteral( + lang.Expr(lang.Expr.NumberLiteral("1")), + lang.Expr(lang.Expr.NumberLiteral("2")), + lang.Expr(lang.Expr.NumberLiteral("3")), + ), + ), + ), + ), + lang.Expr( + lang.Expr.OpCall( + lang.OpSym(defns.`=`("=")), + lang.Expr.OpCall.Params( + lang.Expr( + lang.Expr.OpCall( + lang.Id("x"), + lang.Expr.OpCall.Params(), + ), + ), lang.Expr(lang.Expr.NumberLiteral("2")), - lang.Expr(lang.Expr.NumberLiteral("3")) - )))), - lang.Expr(lang.Expr.OpCall( - lang.OpSym(defns.`=`("=")), - lang.Expr.OpCall.Params( - lang.Expr(lang.Expr.OpCall( - lang.Id("x"), - lang.Expr.OpCall.Params() - )), - lang.Expr(lang.Expr.NumberLiteral("2")) - )))))) + ), + ), + ), + ), + ), + ) assertEquals( "\\E x \\in {1, 2, 3}, y \\in {4, 5, 6} : x = 2".parseStr, Node.Top( @@ -597,27 +810,42 @@ class ExprParserTests extends munit.FunSuite: lang.QuantifierBounds( lang.QuantifierBound( lang.Id("x"), - lang.Expr(lang.Expr.SetLiteral( - lang.Expr(lang.Expr.NumberLiteral("1")), - lang.Expr(lang.Expr.NumberLiteral("2")), - lang.Expr(lang.Expr.NumberLiteral("3")) - ))), + lang.Expr( + lang.Expr.SetLiteral( + lang.Expr(lang.Expr.NumberLiteral("1")), + lang.Expr(lang.Expr.NumberLiteral("2")), + lang.Expr(lang.Expr.NumberLiteral("3")), + ), + ), + ), lang.QuantifierBound( lang.Id("y"), - lang.Expr(lang.Expr.SetLiteral( - lang.Expr(lang.Expr.NumberLiteral("4")), - lang.Expr(lang.Expr.NumberLiteral("5")), - lang.Expr(lang.Expr.NumberLiteral("6")) - )))), - lang.Expr(lang.Expr.OpCall( - lang.OpSym(defns.`=`("=")), - lang.Expr.OpCall.Params( - lang.Expr(lang.Expr.OpCall( - lang.Id("x"), - lang.Expr.OpCall.Params() - )), - lang.Expr(lang.Expr.NumberLiteral("2")) - )))))) + lang.Expr( + lang.Expr.SetLiteral( + lang.Expr(lang.Expr.NumberLiteral("4")), + lang.Expr(lang.Expr.NumberLiteral("5")), + lang.Expr(lang.Expr.NumberLiteral("6")), + ), + ), + ), + ), + lang.Expr( + lang.Expr.OpCall( + lang.OpSym(defns.`=`("=")), + lang.Expr.OpCall.Params( + lang.Expr( + lang.Expr.OpCall( + lang.Id("x"), + lang.Expr.OpCall.Params(), + ), + ), + lang.Expr(lang.Expr.NumberLiteral("2")), + ), + ), + ), + ), + ), + ) test("Forall"): assertEquals( @@ -627,23 +855,35 @@ class ExprParserTests extends munit.FunSuite: lang.QuantifierBounds( lang.QuantifierBound( lang.Id("x"), - lang.Expr(lang.Expr.SetLiteral( - lang.Expr(lang.Expr.NumberLiteral("1")), + lang.Expr( + lang.Expr.SetLiteral( + lang.Expr(lang.Expr.NumberLiteral("1")), + lang.Expr(lang.Expr.NumberLiteral("2")), + lang.Expr(lang.Expr.NumberLiteral("3")), + ), + ), + ), + ), + lang.Expr( + lang.Expr.OpCall( + lang.OpSym(defns.`=`("=")), + lang.Expr.OpCall.Params( + lang.Expr( + lang.Expr.OpCall( + lang.Id("x"), + lang.Expr.OpCall.Params(), + ), + ), lang.Expr(lang.Expr.NumberLiteral("2")), - lang.Expr(lang.Expr.NumberLiteral("3")) - )))), - lang.Expr(lang.Expr.OpCall( - lang.OpSym(defns.`=`("=")), - lang.Expr.OpCall.Params( - lang.Expr(lang.Expr.OpCall( - lang.Id("x"), - lang.Expr.OpCall.Params() - )), - lang.Expr(lang.Expr.NumberLiteral("2")) - )))))) - + ), + ), + ), + ), + ), + ) + // TODO: AA EE ?? - + test("Temporal Logic Combined"): assertEquals( "s /\\ \\E x \\in y : z /\\ \\E p \\in q : r".parseStr, @@ -651,43 +891,71 @@ class ExprParserTests extends munit.FunSuite: lang.Expr.OpCall( lang.OpSym(defns./\("/\\")), lang.Expr.OpCall.Params( - lang.Expr(lang.Expr.OpCall( - lang.Id("s"), - lang.Expr.OpCall.Params() - )), - lang.Expr(lang.Expr.Exists( - lang.QuantifierBounds( - lang.QuantifierBound( - lang.Id("x"), - lang.Expr(lang.Expr.OpCall( - lang.Id("y"), - lang.Expr.OpCall.Params() - )))), - lang.Expr(lang.Expr.OpCall( - lang.OpSym(defns./\("/\\")), - lang.Expr.OpCall.Params( - lang.Expr(lang.Expr.OpCall( - lang.Id("z"), - lang.Expr.OpCall.Params() - )), - lang.Expr(lang.Expr.Exists( - lang.QuantifierBounds( - lang.QuantifierBound( - lang.Id("p"), - lang.Expr(lang.Expr.OpCall( - lang.Id("q"), - lang.Expr.OpCall.Params() - )))), - lang.Expr(lang.Expr.OpCall( - lang.Id("r"), - lang.Expr.OpCall.Params() - ))))))))))))) + lang.Expr( + lang.Expr.OpCall( + lang.Id("s"), + lang.Expr.OpCall.Params(), + ), + ), + lang.Expr( + lang.Expr.Exists( + lang.QuantifierBounds( + lang.QuantifierBound( + lang.Id("x"), + lang.Expr( + lang.Expr.OpCall( + lang.Id("y"), + lang.Expr.OpCall.Params(), + ), + ), + ), + ), + lang.Expr( + lang.Expr.OpCall( + lang.OpSym(defns./\("/\\")), + lang.Expr.OpCall.Params( + lang.Expr( + lang.Expr.OpCall( + lang.Id("z"), + lang.Expr.OpCall.Params(), + ), + ), + lang.Expr( + lang.Expr.Exists( + lang.QuantifierBounds( + lang.QuantifierBound( + lang.Id("p"), + lang.Expr( + lang.Expr.OpCall( + lang.Id("q"), + lang.Expr.OpCall.Params(), + ), + ), + ), + ), + lang.Expr( + lang.Expr.OpCall( + lang.Id("r"), + lang.Expr.OpCall.Params(), + ), + ), + ), + ), + ), + ), + ), + ), + ), + ), + ), + ), + ) // todo: function // todo: set comprehension // todo: set refinement // todo: lambda - + test("Choose"): assertEquals( "CHOOSE x \\in {1, 2, 3} : x = 2".parseStr, @@ -695,66 +963,87 @@ class ExprParserTests extends munit.FunSuite: lang.Expr.Choose( lang.QuantifierBound( lang.Id("x"), - lang.Expr(lang.Expr.SetLiteral( - lang.Expr(lang.Expr.NumberLiteral("1")), - lang.Expr(lang.Expr.NumberLiteral("2")), - lang.Expr(lang.Expr.NumberLiteral("3")) - ))), - lang.Expr(lang.Expr.OpCall( - lang.OpSym(defns.`=`("=")), - lang.Expr.OpCall.Params( - lang.Expr(lang.Expr.OpCall( - lang.Id("x"), - lang.Expr.OpCall.Params() - )), - lang.Expr(lang.Expr.NumberLiteral("2")) - )))))) + lang.Expr( + lang.Expr.SetLiteral( + lang.Expr(lang.Expr.NumberLiteral("1")), + lang.Expr(lang.Expr.NumberLiteral("2")), + lang.Expr(lang.Expr.NumberLiteral("3")), + ), + ), + ), + lang.Expr( + lang.Expr.OpCall( + lang.OpSym(defns.`=`("=")), + lang.Expr.OpCall.Params( + lang.Expr( + lang.Expr.OpCall( + lang.Id("x"), + lang.Expr.OpCall.Params(), + ), + ), + lang.Expr(lang.Expr.NumberLiteral("2")), + ), + ), + ), + ), + ), + ) // todo: id nil, tuple expr, tuple nil // todo: except - + test("Parentheses"): assertEquals( "(1)".parseStr, - Node.Top(lang.Expr.NumberLiteral("1")) + Node.Top(lang.Expr.NumberLiteral("1")), ) assertEquals( "(((x)))".parseStr, Node.Top( lang.Expr.OpCall( lang.Id("x"), - lang.Expr.OpCall.Params() - ))) + lang.Expr.OpCall.Params(), + ), + ), + ) assertEquals( "(5 + 6)".parseStr, Node.Top( lang.Expr.OpCall( lang.OpSym( - defns.+("+") + defns.+("+"), ), lang.Expr.OpCall.Params( lang.Expr(lang.Expr.NumberLiteral("5")), - lang.Expr(lang.Expr.NumberLiteral("6")) - )))) + lang.Expr(lang.Expr.NumberLiteral("6")), + ), + ), + ), + ) assertEquals( "(1 + 2) * 3".parseStr, Node.Top( lang.Expr.OpCall( lang.OpSym( - defns.*("*") + defns.*("*"), ), lang.Expr.OpCall.Params( - lang.Expr(lang.Expr.OpCall( - lang.OpSym( - defns.+("+") + lang.Expr( + lang.Expr.OpCall( + lang.OpSym( + defns.+("+"), + ), + lang.Expr.OpCall.Params( + lang.Expr(lang.Expr.NumberLiteral("1")), + lang.Expr(lang.Expr.NumberLiteral("2")), + ), ), - lang.Expr.OpCall.Params( - lang.Expr(lang.Expr.NumberLiteral("1")), - lang.Expr(lang.Expr.NumberLiteral("2")) - ) - )), - lang.Expr(lang.Expr.NumberLiteral("3")) - )))) + ), + lang.Expr(lang.Expr.NumberLiteral("3")), + ), + ), + ), + ) // assertEquals( // "\\A x \\in {1, 2, 3} : x = (2)".parseStr, // Node.Top( @@ -836,67 +1125,67 @@ class ExprParserTests extends munit.FunSuite: // lang.Expr(lang.Expr.NumberLiteral("3")) // )))))))))) - // assertEquals( - // s""" - // |/\\ 1 - // | /\\ 2 - // |/\\ 3 - // |""".stripMargin.parseStr, - // Node.Top( - // lang.Expr.OpCall( - // lang.OpSym(defns./\("/\\")), - // lang.Expr.OpCall.Params( - // lang.Expr(lang.Expr.OpCall( - // lang.OpSym(defns./\("/\\")), - // lang.Expr.OpCall.Params( - // lang.Expr(lang.Expr.NumberLiteral("1")), - // lang.Expr(lang.Expr.NumberLiteral("2")) - // ) - // )), - // lang.Expr(lang.Expr.NumberLiteral("3")) - // ) - // ) - // )) - - // assertEquals( - // s""" - // |/\\ \\E x \in {1, 2, 3} : 1 - // | /\\ 2 - // |""".stripMargin.parseStr, - // Node.Top( - // lang.Expr.NumberLiteral("1") - // )) + // assertEquals( + // s""" + // |/\\ 1 + // | /\\ 2 + // |/\\ 3 + // |""".stripMargin.parseStr, + // Node.Top( + // lang.Expr.OpCall( + // lang.OpSym(defns./\("/\\")), + // lang.Expr.OpCall.Params( + // lang.Expr(lang.Expr.OpCall( + // lang.OpSym(defns./\("/\\")), + // lang.Expr.OpCall.Params( + // lang.Expr(lang.Expr.NumberLiteral("1")), + // lang.Expr(lang.Expr.NumberLiteral("2")) + // ) + // )), + // lang.Expr(lang.Expr.NumberLiteral("3")) + // ) + // ) + // )) - // assertEquals( - // s""" - // |/\\ \\E x \in {1, 2, 3} : 1 - // |/\\ 2 - // |""".stripMargin.parseStr, - // Node.Top( - // lang.Expr.NumberLiteral("1") - // )) - - // assertEquals( - // s""" - // | /\\ \\E x \in {1, 2, 3} : 1 - // |/\\ 2 - // |""".stripMargin.parseStr, - // Node.Top( - // lang.Expr.NumberLiteral("1") - // )) + // assertEquals( + // s""" + // |/\\ \\E x \in {1, 2, 3} : 1 + // | /\\ 2 + // |""".stripMargin.parseStr, + // Node.Top( + // lang.Expr.NumberLiteral("1") + // )) - // assertEquals( - // s""" - // |/\\ 1 - // | /\\ 2 - // | /\\ 3 - // | /\\ 4 - // |/\\ 5 - // | /\\ 6 - // |""".stripMargin.parseStr, - // Node.Top( - // lang.Expr.NumberLiteral("1") - // )) + // assertEquals( + // s""" + // |/\\ \\E x \in {1, 2, 3} : 1 + // |/\\ 2 + // |""".stripMargin.parseStr, + // Node.Top( + // lang.Expr.NumberLiteral("1") + // )) + + // assertEquals( + // s""" + // | /\\ \\E x \in {1, 2, 3} : 1 + // |/\\ 2 + // |""".stripMargin.parseStr, + // Node.Top( + // lang.Expr.NumberLiteral("1") + // )) + + // assertEquals( + // s""" + // |/\\ 1 + // | /\\ 2 + // | /\\ 3 + // | /\\ 4 + // |/\\ 5 + // | /\\ 6 + // |""".stripMargin.parseStr, + // Node.Top( + // lang.Expr.NumberLiteral("1") + // )) // TODO // paren diff --git a/langs/tla/TLAParser.scala b/langs/tla/TLAParser.scala index cace1d7..3f0f577 100644 --- a/langs/tla/TLAParser.scala +++ b/langs/tla/TLAParser.scala @@ -179,21 +179,22 @@ object TLAParser extends PassSeq: nodeSpanMatchedBy(impl).map(RawExpression.apply) end rawExpression - def rawConjunction(col : Integer): SeqPattern[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 + | 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) + | repeatedSepBy1(`,`)(Alpha), ) ~ skip(defns.`\\in`) ~ skip(defer(impl)) @@ -205,7 +206,7 @@ object TLAParser extends PassSeq: lazy val forallExists: SeqPattern[EmptyTuple] = skip( tok(LaTexLike).src("\\A") | tok(LaTexLike).src("\\AA") | tok(LaTexLike) - .src("\\E") | tok(LaTexLike).src("\\EE") + .src("\\E") | tok(LaTexLike).src("\\EE"), ) ~ skip(quantifierBounds | repeatedSepBy1(`,`)(Alpha)) ~ skip(`:`) @@ -237,7 +238,7 @@ object TLAParser extends PassSeq: | choose | lambda | idFrag - | simpleCases // last, otherwise it eats parts of the above + | simpleCases, // last, otherwise it eats parts of the above ).void nodeSpanMatchedBy(impl).map(RawExpression.apply) diff --git a/langs/tla/TLAParser.test.scala b/langs/tla/TLAParser.test.scala index e1af57d..1b31489 100644 --- a/langs/tla/TLAParser.test.scala +++ b/langs/tla/TLAParser.test.scala @@ -14,10 +14,9 @@ package forja.langs.tla -import forja.test.WithTLACorpus - import forja.* import forja.source.{Source, SourceRange} +import forja.test.WithTLACorpus class TLAParserTests extends munit.FunSuite, WithTLACorpus: self => diff --git a/langs/tla/defns.scala b/langs/tla/defns.scala index 9c4c32d..fb8dbd1 100644 --- a/langs/tla/defns.scala +++ b/langs/tla/defns.scala @@ -219,4 +219,4 @@ object defns: case object `^+` extends PostfixOperator(15) case object `^*` extends PostfixOperator(15) case object `^#` extends PostfixOperator(15) - case object `'` extends PostfixOperator(15) + case object `'` extends PostfixOperator(15) diff --git a/langs/tla/package.scala b/langs/tla/package.scala index bba4131..492d348 100644 --- a/langs/tla/package.scala +++ b/langs/tla/package.scala @@ -190,9 +190,10 @@ object lang extends WellformedDef: Expr, ), ) - object Other extends t( - choice(Expr, Other.None) - ): + object Other + extends t( + choice(Expr, Other.None), + ): object None extends t(Atom) end Case