From 0ace3604c5109061340f6a7ebc7d8936409bd68e Mon Sep 17 00:00:00 2001 From: KuterBora Date: Thu, 18 Sep 2025 11:22:51 -0700 Subject: [PATCH 1/9] temp --- langs/tla/ExprMarker.scala | 126 ++++++++++++++++++++++++++++++++ langs/tla/ExprMarker.test.scala | 119 ++++++++++++++++++++++++++++++ 2 files changed, 245 insertions(+) create mode 100644 langs/tla/ExprMarker.scala create mode 100644 langs/tla/ExprMarker.test.scala diff --git a/langs/tla/ExprMarker.scala b/langs/tla/ExprMarker.scala new file mode 100644 index 0000000..309db97 --- /dev/null +++ b/langs/tla/ExprMarker.scala @@ -0,0 +1,126 @@ +// 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 + +import forja.* +import forja.dsl.* +import forja.wf.Wellformed + +import TLAReader.* + +object ExprMarker extends PassSeq: + + lazy val passes = List( + buildExpressions, + ) + + object ExprTry extends Token + def inputWellformed: Wellformed = TLAParser.outputWellformed // .makeDerived: + // ExprTry ::= Atom + // TLAReader.groupTokens.foreach: tok => + // tok.addCases(ExprTry) + + object buildExpressions extends Pass: + val wellformed = prevWellformed.makeDerived: + val removedCases = Seq( + TLAReader.StringLiteral, + TLAReader.NumberLiteral, + TLAReader.TupleGroup, + // TODO: remove cases + ) + TLAReader.groupTokens.foreach: tok => + tok.removeCases(removedCases*) + tok.addCases(lang.Expr) + + //lang.Expr.deleteShape() + lang.Expr.importFrom(lang.wf) + lang.Expr.addCases(lang.Expr) + + + val rules = + pass(once = false, strategy = pass.bottomUp) + .rules: + // Number and String Literals can be parsed directly + on( + TLAReader.NumberLiteral, + ).rewrite: lit => + splice(lang.Expr(lang.Expr.NumberLiteral().like(lit))) + | on( + TLAReader.StringLiteral, + ).rewrite: lit => + splice(lang.Expr(lang.Expr.StringLiteral().like(lit))) + // Isolated Alpha can be parsed + | on( + skip(ExprTry) + ~ field(TLAReader.Alpha) + ~ eof + ).rewrite: id => + splice( + lang.Expr( + lang.Expr.OpCall( + lang.Id().like(id), + lang.Expr.OpCall.Params(), + ) + ) + ) + // Braces Group is complete when the elements are parsed + | on( + skip(ExprTry) + ~ field( + tok(TLAReader.BracesGroup) *> + children: + field(repeatedSepBy(`,`)(lang.Expr)) + ~ eof + ) + ~ trailing + ).rewrite: exprs => + splice( + lang.Expr( + lang.Expr.SetLiteral(exprs.iterator.map(_.unparent())), + ) + ) + // If the braces group is not complete, mark the next element as ExprTry + // | on( + // parent(tok(TLAReader.BracesGroup) *> rightSibling(ExprTry)) *> + // field(lang.Expr) + // ~ field(`,` *> rightSibling(not(ExprTry))) + // ).rewrite: (expr, comma) => + // splice(expr, comma, ExprTry()) + // Expr has been parsed and ExprTry can be removed + | on( + skip(ExprTry) + ~ field(lang.Expr) + ~ eof + ).rewrite: expr => + splice(expr.unparent()) + end buildExpressions + + object removeNestedExpr extends Pass: + val wellformed = prevWellformed.makeDerived: + lang.Expr.removeCases(lang.Expr) + + val rules = + pass(once = true, strategy = pass.bottomUp) + .rules: + on( + tok(lang.Expr) *> + onlyChild(lang.Expr), + ).rewrite: child => + splice( + child.unparent(), + ) + end removeNestedExpr diff --git a/langs/tla/ExprMarker.test.scala b/langs/tla/ExprMarker.test.scala new file mode 100644 index 0000000..36ab874 --- /dev/null +++ b/langs/tla/ExprMarker.test.scala @@ -0,0 +1,119 @@ +// 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.* +import forja.dsl.* +// import forja.source.{Source, SourceRange} +import ExprMarker.ExprTry + +// Run with: +// scala-cli test . -- '*ExprMarker*' + +class ExprMarkerTests extends munit.FunSuite: + extension (top: Node.Top) + def parseNode: Node.Top = + val freshTop = Node.Top( + lang.Module( + lang.Id("TestMod"), + lang.Module.Extends(), + lang.Module.Defns( + lang.Operator( + lang.Id("test"), + lang.Operator.Params(), + lang.Expr( + top.unparentedChildren, + ), + ), + ), + ), + ) + ExprMarker(freshTop) + Node.Top( + freshTop(lang.Module)(lang.Module.Defns)(lang.Operator)( + lang.Expr, + ).unparentedChildren, + ) + + test("NumberLiteral"): + assertEquals( + Node.Top(TLAReader.NumberLiteral("1")).parseNode, + Node.Top(lang.Expr(lang.Expr.NumberLiteral("1"))), + ) + assertEquals( + Node.Top(ExprTry(), TLAReader.NumberLiteral("1")).parseNode, + Node.Top(lang.Expr(lang.Expr.NumberLiteral("1"))), + ) + + test("StringLiteral"): + assertEquals( + Node.Top(TLAReader.StringLiteral("string")).parseNode, + Node.Top(lang.Expr(lang.Expr.StringLiteral("string"))), + ) + + assertEquals( + Node.Top(ExprTry(), TLAReader.StringLiteral("string")).parseNode, + Node.Top(lang.Expr(lang.Expr.StringLiteral("string"))), + ) + + test("Alpha"): + assertEquals( + Node.Top(ExprTry(), TLAReader.Alpha("x")).parseNode, + Node.Top( + lang.Expr(lang.Expr.OpCall(lang.Id("x"), lang.Expr.OpCall.Params())) + ) + ) + + // test("Set Literal"): + // assertEquals( + // Node.Top(ExprTry(), TLAReader.BracesGroup( + // TLAReader.NumberLiteral("1"), + // TLAReader.`,`(","), + // TLAReader.NumberLiteral("2"), + // TLAReader.`,`(","), + // TLAReader.NumberLiteral("3") + // )).parseNode, + // Node.Top( + // lang.Expr( + // lang.Expr.SetLiteral( + // lang.Expr(lang.Expr.NumberLiteral("1")), + // lang.Expr(lang.Expr.NumberLiteral("2")), + // lang.Expr(lang.Expr.NumberLiteral("3")), + // ), + // ) + // ) + // ) + // assertEquals( + // Node.Top(ExprTry(), TLAReader.BracesGroup( + // TLAReader.NumberLiteral("1"), + // TLAReader.`,`(","), + // TLAReader.BracesGroup(), + // TLAReader.`,`(","), + // TLAReader.NumberLiteral("3") + // )).parseNode, + // Node.Top( + // lang.Expr( + // lang.Expr.SetLiteral( + // lang.Expr(lang.Expr.NumberLiteral("1")), + // lang.Expr(lang.Expr.SetLiteral()), + // lang.Expr(lang.Expr.NumberLiteral("3")), + // ), + // ) + // ) + // ) + // assertEquals( + // Node.Top(ExprTry(), TLAReader.BracesGroup()).parseNode, + // Node.Top(lang.Expr(lang.Expr.SetLiteral())), + // ) \ No newline at end of file From 0c6152c3be55ced18a78d8de64874b4492ed83d3 Mon Sep 17 00:00:00 2001 From: KuterBora Date: Thu, 18 Sep 2025 11:29:35 -0700 Subject: [PATCH 2/9] tmp2 --- langs/tla/ExprMarker.scala | 7 ++----- src/wf/Wellformed.scala | 9 +++++++++ 2 files changed, 11 insertions(+), 5 deletions(-) diff --git a/langs/tla/ExprMarker.scala b/langs/tla/ExprMarker.scala index 309db97..dd8ce58 100644 --- a/langs/tla/ExprMarker.scala +++ b/langs/tla/ExprMarker.scala @@ -29,10 +29,7 @@ object ExprMarker extends PassSeq: ) object ExprTry extends Token - def inputWellformed: Wellformed = TLAParser.outputWellformed // .makeDerived: - // ExprTry ::= Atom - // TLAReader.groupTokens.foreach: tok => - // tok.addCases(ExprTry) + def inputWellformed: Wellformed = TLAParser.outputWellformed object buildExpressions extends Pass: val wellformed = prevWellformed.makeDerived: @@ -46,7 +43,7 @@ object ExprMarker extends PassSeq: tok.removeCases(removedCases*) tok.addCases(lang.Expr) - //lang.Expr.deleteShape() + lang.Expr.deleteShape() lang.Expr.importFrom(lang.wf) lang.Expr.addCases(lang.Expr) diff --git a/src/wf/Wellformed.scala b/src/wf/Wellformed.scala index 7141ab5..607f82b 100644 --- a/src/wf/Wellformed.scala +++ b/src/wf/Wellformed.scala @@ -554,6 +554,15 @@ object Wellformed: throw IllegalArgumentException( 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 = From 008b149fce5a6175c96eb1e091dca6bde808f2bb Mon Sep 17 00:00:00 2001 From: KuterBora Date: Thu, 18 Sep 2025 11:48:28 -0700 Subject: [PATCH 3/9] tmp3 --- langs/tla/ExprMarker.scala | 12 ++++++------ langs/tla/TLAReader.scala | 4 ++++ 2 files changed, 10 insertions(+), 6 deletions(-) diff --git a/langs/tla/ExprMarker.scala b/langs/tla/ExprMarker.scala index dd8ce58..55a57c3 100644 --- a/langs/tla/ExprMarker.scala +++ b/langs/tla/ExprMarker.scala @@ -91,12 +91,12 @@ object ExprMarker extends PassSeq: ) ) // If the braces group is not complete, mark the next element as ExprTry - // | on( - // parent(tok(TLAReader.BracesGroup) *> rightSibling(ExprTry)) *> - // field(lang.Expr) - // ~ field(`,` *> rightSibling(not(ExprTry))) - // ).rewrite: (expr, comma) => - // splice(expr, comma, ExprTry()) + | on( + parent(tok(TLAReader.BracesGroup) *> rightSibling(ExprTry)) *> + field(lang.Expr) + ~ field(`,` *> rightSibling(not(ExprTry))) + ).rewrite: (expr, comma) => + splice(expr, comma, ExprTry()) // Expr has been parsed and ExprTry can be removed | on( skip(ExprTry) diff --git a/langs/tla/TLAReader.scala b/langs/tla/TLAReader.scala index 91d955d..52e1998 100644 --- a/langs/tla/TLAReader.scala +++ b/langs/tla/TLAReader.scala @@ -20,6 +20,7 @@ import forja.* import forja.dsl.* import forja.source.{Reader, SourceRange} import forja.wf.Wellformed +import forja.langs.tla.ExprMarker.ExprTry object TLAReader extends Reader: lazy val groupTokens: List[Token] = List( @@ -54,6 +55,8 @@ object TLAReader extends Reader: Comment, DashSeq, EqSeq, + // + ExprTry, ) | choice(NonAlpha.instances.toSet) | choice(allOperators.toSet) @@ -70,6 +73,7 @@ object TLAReader extends Reader: NumberLiteral ::= Atom Alpha ::= Atom LaTexLike ::= Atom + ExprTry ::= Atom StepMarker ::= fields( choice(StepMarker.Num, StepMarker.Plus, StepMarker.Star), From 479baadd2cd8b42cbe100f403e92d1745756eff2 Mon Sep 17 00:00:00 2001 From: KuterBora Date: Thu, 2 Oct 2025 18:47:29 -0700 Subject: [PATCH 4/9] refactor patterns --- langs/tla/ExprMarker.scala | 104 ++++++++++++++++++-------------- langs/tla/ExprMarker.test.scala | 2 +- 2 files changed, 61 insertions(+), 45 deletions(-) diff --git a/langs/tla/ExprMarker.scala b/langs/tla/ExprMarker.scala index 081a805..4bdf640 100644 --- a/langs/tla/ExprMarker.scala +++ b/langs/tla/ExprMarker.scala @@ -50,6 +50,50 @@ object ExprMarker extends PassSeq: object ExprTry extends Token def inputWellformed: Wellformed = TLAParser.outputWellformed + def parsedChildrenSepBy( + parent: Token, split: SeqPattern[?] + ): SeqPattern[List[Node]] = + leftSibling(ExprTry) *> + field(tok(parent) *> + children: + field( + repeatedSepBy(split)( + skip(ExprTry) + ~ field(lang.Expr) + ~ trailing + ) + ) + ~ eof + ) + ~ trailing + end parsedChildrenSepBy + + def firstUnmarkedChildStart( + paren: Token + ): SeqPattern[Node] = + parent(leftSibling(ExprTry) *> paren) *> + not(leftSibling(anyNode)) *> + not(ExprTry) *> not(lang.Expr) *> anyNode + end firstUnmarkedChildStart + + def unMarkedChildComma( + paren: Token, + ): SeqPattern[Node] = + parent(leftSibling(ExprTry) *> paren) *> + possibleExprTryToRight(tok(`,`)) + end unMarkedChildComma + + def rightSiblingNotExprTry(): SeqPattern[Unit] = + rightSibling(not(lang.Expr) *> not(ExprTry)) + end rightSiblingNotExprTry + + def possibleExprTryToRight( + node: SeqPattern[Node] + ): SeqPattern[Node] = + node <* rightSiblingNotExprTry() + end possibleExprTryToRight + + object buildExpressions extends Pass: val wellformed = prevWellformed.makeDerived: val removedCases = Seq( @@ -82,21 +126,10 @@ object ExprMarker extends PassSeq: ~ trailing ).rewrite: lit => splice(lang.Expr(lang.Expr.StringLiteral().like(lit))) + // // Braces Group is complete when all the elements are parsed | on( - leftSibling(ExprTry) *> - field(tok(TLAReader.BracesGroup) *> - children: - field( - repeatedSepBy(`,`)( - skip(ExprTry) - ~ field(lang.Expr) - ~ trailing - ) - ) - ~ eof - ) - ~ trailing + parsedChildrenSepBy(TLAReader.BracesGroup, `,`) ).rewrite: exprs => splice( lang.Expr( @@ -106,15 +139,13 @@ object ExprMarker extends PassSeq: // If the braces group is not complete, mark the elements with ExprTry // Mark the first child in the first pass, and then mark the rest in the second // TODO: I wonder if this pattern is a bad idea - | on(parent(leftSibling(ExprTry) *> tok(TLAReader.BracesGroup)) *> - not(leftSibling(anyNode)) *> - not(ExprTry) *> not(lang.Expr) *> anyNode + | on( + firstUnmarkedChildStart(TLAReader.BracesGroup) ).rewrite: first => splice(ExprTry(), first.unparent()) | on( - parent(leftSibling(ExprTry) *> tok(TLAReader.BracesGroup)) *> - tok(`,`) <* rightSibling(not(ExprTry) *> not(lang.Expr)) - ).rewrite: comma => + unMarkedChildComma(TLAReader.BracesGroup) + ).rewrite: comma => splice(comma.unparent(), ExprTry()) // CASE is complete when every branch is parsed. | on( @@ -160,23 +191,18 @@ object ExprMarker extends PassSeq: // If the CASE is not complete, insert ExprTry after [], ->, and OTHER // as well as before the first case. | on( - leftSibling(leftSibling(ExprTry) *> defns.CASE) *> - field(not(lang.Expr) *> not(ExprTry) *> anyNode) - ~ trailing, - ).rewrite: first => - splice(ExprTry(), first.unparent()) + possibleExprTryToRight(leftSibling(ExprTry) *> defns.CASE) + ).rewrite: c => + splice(c.unparent(), ExprTry()) | on( - (tok(defns.`[]`) | tok(TLAReader.`->`)) - <* rightSibling(not(lang.Expr) *> not(ExprTry)) + possibleExprTryToRight((tok(defns.`[]`) | tok(TLAReader.`->`))) ).rewrite: split => splice(split.unparent(), ExprTry()) | on( - leftSibling(defns.OTHER) *> - tok(TLAReader.`->`) - <* rightSibling(not(lang.Expr) *> not(ExprTry)) + possibleExprTryToRight(leftSibling(defns.OTHER) *> tok(TLAReader.`->`)) ).rewrite: split => splice(split.unparent(), ExprTry()) - // Parenthesis can be removed when its children are parsed + // Parentheses can be removed when its children are parsed | on( leftSibling(ExprTry) *> tok(TLAReader.ParenthesesGroup) *> @@ -187,10 +213,9 @@ object ExprMarker extends PassSeq: ) ).rewrite: expr => splice(expr.unparent()) - // Mark the children of the parenthesis - | on(parent(leftSibling(ExprTry) *> tok(TLAReader.ParenthesesGroup)) *> - not(leftSibling(anyNode)) *> - not(ExprTry) *> not(lang.Expr) *> anyNode + // Mark the children of the parentheses + | on( + firstUnmarkedChildStart(TLAReader.ParenthesesGroup) ).rewrite: node => splice(ExprTry(), node.unparent()) *> pass(once = false, strategy = pass.bottomUp) @@ -219,13 +244,4 @@ object ExprMarker extends PassSeq: splice( child.unparent(), ) - end removeNestedExpr - - - -// | on( -// skip(ExprTry) -// ~ field(tok(lang.Expr) <* rightSibling(tok(`,`) | tok(`->`) | tok(defns.`[]`))) -// ~ trailing -// ).rewrite: expr => -// splice(expr.unparent()) \ No newline at end of file + end removeNestedExpr \ No newline at end of file diff --git a/langs/tla/ExprMarker.test.scala b/langs/tla/ExprMarker.test.scala index 4d703f0..23417d4 100644 --- a/langs/tla/ExprMarker.test.scala +++ b/langs/tla/ExprMarker.test.scala @@ -60,7 +60,7 @@ class ExprMarkerTests extends munit.FunSuite: Node.Top(lang.Expr(lang.Expr.StringLiteral("string"))), ) - test("ParanthesisGroup"): + test("ParenthesesGroup"): assertEquals( Node.Top(ExprTry(), TLAReader.ParenthesesGroup( TLAReader.NumberLiteral("1") From 284a38976f6431135ebaa4d163be65517a50cd4a Mon Sep 17 00:00:00 2001 From: KuterBora Date: Thu, 2 Oct 2025 18:57:08 -0700 Subject: [PATCH 5/9] tuples --- langs/tla/ExprMarker.scala | 26 ++++++++++++++++++++++---- langs/tla/ExprMarker.test.scala | 27 +++++++++++++++++++++++++++ 2 files changed, 49 insertions(+), 4 deletions(-) diff --git a/langs/tla/ExprMarker.scala b/langs/tla/ExprMarker.scala index 4bdf640..da607a7 100644 --- a/langs/tla/ExprMarker.scala +++ b/langs/tla/ExprMarker.scala @@ -68,6 +68,7 @@ object ExprMarker extends PassSeq: ~ trailing end parsedChildrenSepBy + // TODO: I wonder if this pattern is a bad idea def firstUnmarkedChildStart( paren: Token ): SeqPattern[Node] = @@ -126,8 +127,26 @@ object ExprMarker extends PassSeq: ~ trailing ).rewrite: lit => splice(lang.Expr(lang.Expr.StringLiteral().like(lit))) - // - // Braces Group is complete when all the elements are parsed + // TupleLiteral is complete when all the elements are parsed + | on( + parsedChildrenSepBy(TLAReader.TupleGroup, `,`) + ).rewrite: exprs => + splice( + lang.Expr( + lang.Expr.TupleLiteral(exprs.iterator.map(_.unparent())), + ) + ) + // If the TupleLiteral not complete, mark the elements with ExprTry + // Mark the first child in the first pass, and then mark the rest in the second + | on( + firstUnmarkedChildStart(TLAReader.TupleGroup) + ).rewrite: first => + splice(ExprTry(), first.unparent()) + | on( + unMarkedChildComma(TLAReader.TupleGroup) + ).rewrite: comma => + splice(comma.unparent(), ExprTry()) + // SetLiteral is complete when all the elements are parsed | on( parsedChildrenSepBy(TLAReader.BracesGroup, `,`) ).rewrite: exprs => @@ -136,9 +155,8 @@ object ExprMarker extends PassSeq: lang.Expr.SetLiteral(exprs.iterator.map(_.unparent())), ) ) - // If the braces group is not complete, mark the elements with ExprTry + // If the SetLiteral is not complete, mark the elements with ExprTry // Mark the first child in the first pass, and then mark the rest in the second - // TODO: I wonder if this pattern is a bad idea | on( firstUnmarkedChildStart(TLAReader.BracesGroup) ).rewrite: first => diff --git a/langs/tla/ExprMarker.test.scala b/langs/tla/ExprMarker.test.scala index 23417d4..5f6d129 100644 --- a/langs/tla/ExprMarker.test.scala +++ b/langs/tla/ExprMarker.test.scala @@ -115,6 +115,33 @@ class ExprMarkerTests extends munit.FunSuite: ) ) + test("Tuple Literal"): + // empty tuple + assertEquals( + Node.Top(ExprTry(), TLAReader.TupleGroup()).parseNode, + Node.Top(lang.Expr(lang.Expr.TupleLiteral())) + ) + // tuple with three elements + assertEquals( + Node.Top(ExprTry(), TLAReader.TupleGroup( + TLAReader.NumberLiteral("1"), + TLAReader.`,`(","), + TLAReader.StringLiteral("two"), + TLAReader.`,`(","), + TLAReader.NumberLiteral("3") + )).parseNode, + Node.Top( + lang.Expr( + lang.Expr.TupleLiteral( + lang.Expr(lang.Expr.NumberLiteral("1")), + lang.Expr(lang.Expr.StringLiteral("two")), + lang.Expr(lang.Expr.NumberLiteral("3")), + ), + ) + ) + ) + + test("Case"): assertEquals( From c25c3837c32845f632e16826520bb518c33e1652 Mon Sep 17 00:00:00 2001 From: KuterBora Date: Thu, 2 Oct 2025 19:43:26 -0700 Subject: [PATCH 6/9] records --- langs/tla/ExprMarker.scala | 66 +++++++++++++++-------- langs/tla/ExprMarker.test.scala | 96 ++++++++++++++++++++++++--------- 2 files changed, 117 insertions(+), 45 deletions(-) diff --git a/langs/tla/ExprMarker.scala b/langs/tla/ExprMarker.scala index da607a7..38cc1dc 100644 --- a/langs/tla/ExprMarker.scala +++ b/langs/tla/ExprMarker.scala @@ -28,20 +28,12 @@ object ExprMarker extends PassSeq: buildExpressions, ) -// PART 1 -// HARD: -// - identifiers -// - opcalls -// - prefix operators -// - infix operators -// - postfix operators -// EASY: +// TODO: // - records // - "." operand -// - tuples // - IF/THEN/ELSE // - LET @@ -54,7 +46,7 @@ object ExprMarker extends PassSeq: parent: Token, split: SeqPattern[?] ): SeqPattern[List[Node]] = leftSibling(ExprTry) *> - field(tok(parent) *> + tok(parent) *> children: field( repeatedSepBy(split)( @@ -64,8 +56,6 @@ object ExprMarker extends PassSeq: ) ) ~ eof - ) - ~ trailing end parsedChildrenSepBy // TODO: I wonder if this pattern is a bad idea @@ -77,12 +67,13 @@ object ExprMarker extends PassSeq: not(ExprTry) *> not(lang.Expr) *> anyNode end firstUnmarkedChildStart - def unMarkedChildComma( + def unMarkedChildSplit( paren: Token, + split: Token, ): SeqPattern[Node] = parent(leftSibling(ExprTry) *> paren) *> - possibleExprTryToRight(tok(`,`)) - end unMarkedChildComma + possibleExprTryToRight(split) + end unMarkedChildSplit def rightSiblingNotExprTry(): SeqPattern[Unit] = rightSibling(not(lang.Expr) *> not(ExprTry)) @@ -143,9 +134,9 @@ object ExprMarker extends PassSeq: ).rewrite: first => splice(ExprTry(), first.unparent()) | on( - unMarkedChildComma(TLAReader.TupleGroup) - ).rewrite: comma => - splice(comma.unparent(), ExprTry()) + unMarkedChildSplit(TLAReader.TupleGroup, `,`) + ).rewrite: split => + splice(split.unparent(), ExprTry()) // SetLiteral is complete when all the elements are parsed | on( parsedChildrenSepBy(TLAReader.BracesGroup, `,`) @@ -162,9 +153,42 @@ object ExprMarker extends PassSeq: ).rewrite: first => splice(ExprTry(), first.unparent()) | on( - unMarkedChildComma(TLAReader.BracesGroup) - ).rewrite: comma => - splice(comma.unparent(), ExprTry()) + unMarkedChildSplit(TLAReader.BracesGroup, `,`) + ).rewrite: split => + splice(split.unparent(), ExprTry()) + // RecordLiteral is complete when all the elements are parsed + | on( + leftSibling(ExprTry) *> tok(TLAReader.SqBracketsGroup) *> + children: + field( + repeatedSepBy1(`,`)( + field(TLAReader.Alpha) + ~ skip(TLAReader.`|->`) + ~ skip(ExprTry) + ~ field(lang.Expr) + ~ trailing + ) + ) + ~ eof + ).rewrite: records => + splice( + lang.Expr( + lang.Expr.RecordLiteral( + records.iterator.map( + (id, expr) => + lang.Expr.RecordLiteral.Field( + lang.Id().like(id.unparent()), + expr.unparent(), + ) + ) + ) + ) + ) + // If the RecordLiteral is not complete, place ExprTry after each |-> + | on ( + unMarkedChildSplit(TLAReader.SqBracketsGroup, `|->`) + ).rewrite: split => + splice(split.unparent(), ExprTry()) // CASE is complete when every branch is parsed. | on( leftSibling(ExprTry) *> diff --git a/langs/tla/ExprMarker.test.scala b/langs/tla/ExprMarker.test.scala index 5f6d129..4c51792 100644 --- a/langs/tla/ExprMarker.test.scala +++ b/langs/tla/ExprMarker.test.scala @@ -40,7 +40,7 @@ class ExprMarkerTests extends munit.FunSuite: ), ), ) - // instrumentWithTracer(forja.manip.RewriteDebugTracer(os.pwd / "dbg_exprmarker")): + // instrumentWithTracer(forja.manip.RewriteDebugTracer(os.pwd / "dbg_exprmarker")): ExprMarker(freshTop) Node.Top( freshTop(lang.Module)(lang.Module.Defns)(lang.Operator)( @@ -70,7 +70,7 @@ class ExprMarkerTests extends munit.FunSuite: // TODO: paranthesis with op - test("Set Literal"): + test("SetLiteral"): // empty set assertEquals( Node.Top(ExprTry(), TLAReader.BracesGroup()).parseNode, @@ -78,13 +78,16 @@ class ExprMarkerTests extends munit.FunSuite: ) // set with three elements assertEquals( - Node.Top(ExprTry(), TLAReader.BracesGroup( - TLAReader.NumberLiteral("1"), - TLAReader.`,`(","), - TLAReader.NumberLiteral("2"), - TLAReader.`,`(","), - TLAReader.NumberLiteral("3") - )).parseNode, + Node.Top( + ExprTry(), + TLAReader.BracesGroup( + TLAReader.NumberLiteral("1"), + TLAReader.`,`(","), + TLAReader.NumberLiteral("2"), + TLAReader.`,`(","), + TLAReader.NumberLiteral("3") + ) + ).parseNode, Node.Top( lang.Expr( lang.Expr.SetLiteral( @@ -97,13 +100,16 @@ class ExprMarkerTests extends munit.FunSuite: ) // nested sets assertEquals( - Node.Top(ExprTry(), TLAReader.BracesGroup( - TLAReader.NumberLiteral("1"), - TLAReader.`,`(","), - TLAReader.BracesGroup(), - TLAReader.`,`(","), - TLAReader.NumberLiteral("3") - )).parseNode, + Node.Top( + ExprTry(), + TLAReader.BracesGroup( + TLAReader.NumberLiteral("1"), + TLAReader.`,`(","), + TLAReader.BracesGroup(), + TLAReader.`,`(","), + TLAReader.NumberLiteral("3") + ) + ).parseNode, Node.Top( lang.Expr( lang.Expr.SetLiteral( @@ -115,7 +121,7 @@ class ExprMarkerTests extends munit.FunSuite: ) ) - test("Tuple Literal"): + test("TupleLiteral"): // empty tuple assertEquals( Node.Top(ExprTry(), TLAReader.TupleGroup()).parseNode, @@ -123,13 +129,16 @@ class ExprMarkerTests extends munit.FunSuite: ) // tuple with three elements assertEquals( - Node.Top(ExprTry(), TLAReader.TupleGroup( - TLAReader.NumberLiteral("1"), - TLAReader.`,`(","), - TLAReader.StringLiteral("two"), - TLAReader.`,`(","), - TLAReader.NumberLiteral("3") - )).parseNode, + Node.Top( + ExprTry(), + TLAReader.TupleGroup( + TLAReader.NumberLiteral("1"), + TLAReader.`,`(","), + TLAReader.StringLiteral("two"), + TLAReader.`,`(","), + TLAReader.NumberLiteral("3") + ) + ).parseNode, Node.Top( lang.Expr( lang.Expr.TupleLiteral( @@ -140,6 +149,45 @@ class ExprMarkerTests extends munit.FunSuite: ) ) ) + + test("RecordLiteral"): + // record with three fields + assertEquals( + Node.Top( + ExprTry(), + TLAReader.SqBracketsGroup( + TLAReader.Alpha("X"), + TLAReader.`|->`("|->"), + TLAReader.NumberLiteral("1"), + TLAReader.`,`(","), + TLAReader.Alpha("Y"), + TLAReader.`|->`("|->"), + TLAReader.NumberLiteral("2"), + TLAReader.`,`(","), + TLAReader.Alpha("Z"), + TLAReader.`|->`("|->"), + TLAReader.NumberLiteral("3"), + ) + ).parseNode, + Node.Top( + lang.Expr( + lang.Expr.RecordLiteral( + lang.Expr.RecordLiteral.Field( + lang.Id("X"), + lang.Expr(lang.Expr.NumberLiteral("1")), + ), + lang.Expr.RecordLiteral.Field( + lang.Id("Y"), + lang.Expr(lang.Expr.NumberLiteral("2")), + ), + lang.Expr.RecordLiteral.Field( + lang.Id("Z"), + lang.Expr(lang.Expr.NumberLiteral("3")), + ) + ), + ) + ) + ) From 717224098f0db7e3ca007ce12ff30ce7c83bcba9 Mon Sep 17 00:00:00 2001 From: KuterBora Date: Thu, 2 Oct 2025 20:16:13 -0700 Subject: [PATCH 7/9] ids and projection --- langs/tla/ExprMarker.scala | 38 +++++++++++++++++--- langs/tla/ExprMarker.test.scala | 63 +++++++++++++++++++++++++++++++++ 2 files changed, 96 insertions(+), 5 deletions(-) diff --git a/langs/tla/ExprMarker.scala b/langs/tla/ExprMarker.scala index 38cc1dc..84a9d2f 100644 --- a/langs/tla/ExprMarker.scala +++ b/langs/tla/ExprMarker.scala @@ -26,15 +26,13 @@ object ExprMarker extends PassSeq: lazy val passes = List( buildExpressions, + // removeNestedExpr ) // TODO: -// - records -// - "." operand - // - IF/THEN/ELSE // - LET @@ -105,7 +103,7 @@ object ExprMarker extends PassSeq: val rules = pass(once = false, strategy = pass.bottomUp) .rules: - // Parse Number and String literals + // Parse Number and String Literals on( leftSibling(ExprTry) *> field(TLAReader.NumberLiteral) @@ -118,6 +116,20 @@ object ExprMarker extends PassSeq: ~ trailing ).rewrite: lit => splice(lang.Expr(lang.Expr.StringLiteral().like(lit))) + // Parse Id + | on( + leftSibling(ExprTry) *> + field(TLAReader.Alpha) + ~ trailing + ).rewrite: id => + splice( + lang.Expr( + lang.Expr.OpCall( + lang.Id().like(id.unparent()), + lang.Expr.OpCall.Params(), + ), + ) + ) // TupleLiteral is complete when all the elements are parsed | on( parsedChildrenSepBy(TLAReader.TupleGroup, `,`) @@ -188,7 +200,23 @@ object ExprMarker extends PassSeq: | on ( unMarkedChildSplit(TLAReader.SqBracketsGroup, `|->`) ).rewrite: split => - splice(split.unparent(), ExprTry()) + splice(split.unparent(), ExprTry()) + // Parse Projection (Record field access) + | on( + leftSibling(ExprTry) *> + field(lang.Expr) + ~ skip(defns.`.`) + ~ field(TLAReader.Alpha) + ~ trailing + ).rewrite: (expr, id) => + splice( + lang.Expr( + lang.Expr.Project( + expr.unparent(), + lang.Id().like(id.unparent()) + ) + ) + ) // CASE is complete when every branch is parsed. | on( leftSibling(ExprTry) *> diff --git a/langs/tla/ExprMarker.test.scala b/langs/tla/ExprMarker.test.scala index 4c51792..b2b9ced 100644 --- a/langs/tla/ExprMarker.test.scala +++ b/langs/tla/ExprMarker.test.scala @@ -60,6 +60,19 @@ class ExprMarkerTests extends munit.FunSuite: Node.Top(lang.Expr(lang.Expr.StringLiteral("string"))), ) + test("Id"): + assertEquals( + Node.Top(ExprTry(), TLAReader.Alpha("X")).parseNode, + Node.Top( + lang.Expr( + lang.Expr.OpCall( + lang.Id("X"), + lang.Expr.OpCall.Params() + ) + ) + ) + ) + test("ParenthesesGroup"): assertEquals( Node.Top(ExprTry(), TLAReader.ParenthesesGroup( @@ -189,6 +202,56 @@ class ExprMarkerTests extends munit.FunSuite: ) ) + test("Projection (Record Field Acess)"): + assertEquals( + Node.Top( + ExprTry(), + TLAReader.Alpha("X"), + defns.`.`("."), + TLAReader.Alpha("Y") + ).parseNode, + Node.Top( + lang.Expr( + lang.Expr.Project( + lang.Expr( + lang.Expr.OpCall( + lang.Id("X"), + lang.Expr.OpCall.Params(), + ), + ), + lang.Id("Y"), + ), + ) + ) + ) + assertEquals( + Node.Top( + ExprTry(), + TLAReader.Alpha("X"), + defns.`.`("."), + TLAReader.Alpha("Y"), + defns.`.`("."), + TLAReader.Alpha("Z") + ).parseNode, + Node.Top( + lang.Expr( + 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") + ) + ) + ) + ) test("Case"): From c9bcc1aa907e38d2c0abec85b51c521a35ba0abd Mon Sep 17 00:00:00 2001 From: KuterBora Date: Thu, 2 Oct 2025 21:35:36 -0700 Subject: [PATCH 8/9] let --- langs/tla/ExprMarker.scala | 70 +++++++++++++++++---- langs/tla/ExprMarker.test.scala | 104 +++++++++++++++++++++++--------- 2 files changed, 134 insertions(+), 40 deletions(-) diff --git a/langs/tla/ExprMarker.scala b/langs/tla/ExprMarker.scala index 84a9d2f..b5eb08a 100644 --- a/langs/tla/ExprMarker.scala +++ b/langs/tla/ExprMarker.scala @@ -29,14 +29,6 @@ object ExprMarker extends PassSeq: // removeNestedExpr ) - - -// TODO: - -// - IF/THEN/ELSE -// - LET - - object ExprTry extends Token def inputWellformed: Wellformed = TLAParser.outputWellformed @@ -188,10 +180,10 @@ object ExprMarker extends PassSeq: lang.Expr.RecordLiteral( records.iterator.map( (id, expr) => - lang.Expr.RecordLiteral.Field( - lang.Id().like(id.unparent()), - expr.unparent(), - ) + lang.Expr.RecordLiteral.Field( + lang.Id().like(id.unparent()), + expr.unparent(), + ) ) ) ) @@ -217,6 +209,34 @@ object ExprMarker extends PassSeq: ) ) ) + // IF is complete when every branch is parsed. + | on( + leftSibling(ExprTry) *> + skip(defns.IF) + ~ skip(ExprTry) + ~ field(lang.Expr) + ~ skip(defns.THEN) + ~ skip(ExprTry) + ~ field(lang.Expr) + ~ skip(defns.ELSE) + ~ skip(ExprTry) + ~ field(lang.Expr) + ~ trailing, + ).rewrite: (pred, t, f) => + splice( + lang.Expr( + lang.Expr.If( + pred.unparent(), + t.unparent(), + f.unparent(), + ) + ) + ) + // If IF is not complete, place ExprTry before the pred and branches + | on( + possibleExprTryToRight(tok(defns.IF) | tok(defns.THEN) | tok(defns.ELSE)) + ).rewrite: split => + splice(split.unparent(), ExprTry()) // CASE is complete when every branch is parsed. | on( leftSibling(ExprTry) *> @@ -272,6 +292,32 @@ object ExprMarker extends PassSeq: possibleExprTryToRight(leftSibling(defns.OTHER) *> tok(TLAReader.`->`)) ).rewrite: split => splice(split.unparent(), ExprTry()) + // LET is complete when the definitions and the body are parsed + // I am assuming TLAParser will have inserted an ExpTry before the let body + | on ( + leftSibling(ExprTry) *> + field(tok(TLAReader.LetGroup) *> + children( + repeated: + tok(lang.Operator) + | tok(lang.ModuleDefinition) + | tok(lang.Recursive) + ) + ) + ~ skip(ExprTry) + ~ field(lang.Expr) + ~ trailing + ).rewrite: (defs, body) => + splice( + lang.Expr( + lang.Expr.Let( + lang.Expr.Let.Defns( + defs.iterator.map(_.unparent()) + ), + body.unparent() + ) + ) + ) // Parentheses can be removed when its children are parsed | on( leftSibling(ExprTry) *> diff --git a/langs/tla/ExprMarker.test.scala b/langs/tla/ExprMarker.test.scala index b2b9ced..d02e883 100644 --- a/langs/tla/ExprMarker.test.scala +++ b/langs/tla/ExprMarker.test.scala @@ -254,6 +254,33 @@ class ExprMarkerTests extends munit.FunSuite: ) + test("If"): + assertEquals( + Node.Top( + ExprTry(), + defns.IF(), + TLAReader.Alpha("A"), + defns.THEN(), + TLAReader.NumberLiteral("1"), + defns.ELSE(), + TLAReader.NumberLiteral("2"), + ).parseNode, + Node.Top( + lang.Expr( + lang.Expr.If( + lang.Expr( + lang.Expr.OpCall( + lang.Id("A"), + lang.Expr.OpCall.Params(), + ), + ), + lang.Expr(lang.Expr.NumberLiteral("1")), + lang.Expr(lang.Expr.NumberLiteral("2")), + ), + ), + ) + ) + test("Case"): assertEquals( Node.Top( @@ -326,43 +353,64 @@ class ExprMarkerTests extends munit.FunSuite: ) ) - + // This test assumes that TLAParser has parsed the definitions and has inserted the ExprTry before the let body. + // TODO: I am not sure what kind of node I should pass to lang.Operator. It complains if it is an Expr. // test("LET"): // assertEquals( - // """LET x == 1 - // |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.Operator( - // lang.Id("y"), - // lang.Operator.Params(), - // lang.Expr(lang.Expr.NumberLiteral("2")), - // ), + // ExprTry(), + // TLAReader.LetGroup( + // lang.Operator( + // lang.Id("X"), + // lang.Operator.Params(), + // lang.Expr(lang.Expr.NumberLiteral("1")), // ), - // lang.Expr( - // lang.Expr.SetLiteral( - // lang.Expr( - // lang.Expr.OpCall( - // lang.Id("y"), - // lang.Expr.OpCall.Params(), - // ), + // lang.Operator( + // lang.Id("Y"), + // lang.Operator.Params(), + // lang.Expr(lang.Expr.NumberLiteral("2")), + // ), + // ), + // ExprTry(), + // TLAReader.BracesGroup( + // TLAReader.Alpha("X"), + // TLAReader.`,`(","), + // TLAReader.Alpha("Y"), + // ) + // ).parseNode, + // Node.Top( + // lang.Expr( + // 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.OpCall( - // lang.Id("x"), - // lang.Expr.OpCall.Params(), + // lang.Operator( + // lang.Id("Y"), + // lang.Operator.Params(), + // 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(), + // ), // ), // ), // ), // ), // ), - // ), + // ) // ) From 6e9a14da91426d0aeb743edb7ee354b58de359e3 Mon Sep 17 00:00:00 2001 From: Finn Hackett Date: Tue, 21 Oct 2025 23:02:19 +0000 Subject: [PATCH 9/9] format --- .scalafmt.conf | 2 - langs/tla/ExprMarker.scala | 216 +++++++++++----------- langs/tla/ExprMarker.test.scala | 318 ++++++++++++++++++-------------- langs/tla/TLAReader.scala | 2 +- project.scala | 6 +- src/wf/Wellformed.scala | 2 +- 6 files changed, 296 insertions(+), 250 deletions(-) diff --git a/.scalafmt.conf b/.scalafmt.conf index 3e5cd95..1899ebf 100644 --- a/.scalafmt.conf +++ b/.scalafmt.conf @@ -4,5 +4,3 @@ runner.dialect = scala3 assumeStandardLibraryStripMargin = true align.stripMargin = true rewrite.trailingCommas.style = "always" - -comments.wrap = "standalone" diff --git a/langs/tla/ExprMarker.scala b/langs/tla/ExprMarker.scala index b5eb08a..f8e090e 100644 --- a/langs/tla/ExprMarker.scala +++ b/langs/tla/ExprMarker.scala @@ -33,36 +33,37 @@ object ExprMarker extends PassSeq: def inputWellformed: Wellformed = TLAParser.outputWellformed def parsedChildrenSepBy( - parent: Token, split: SeqPattern[?] + parent: Token, + split: SeqPattern[?], ): SeqPattern[List[Node]] = leftSibling(ExprTry) *> tok(parent) *> - children: - field( - repeatedSepBy(split)( - skip(ExprTry) + children: + field( + repeatedSepBy(split)( + skip(ExprTry) ~ field(lang.Expr) - ~ trailing - ) - ) + ~ trailing, + ), + ) ~ eof end parsedChildrenSepBy // TODO: I wonder if this pattern is a bad idea def firstUnmarkedChildStart( - paren: Token - ): SeqPattern[Node] = + paren: Token, + ): SeqPattern[Node] = parent(leftSibling(ExprTry) *> paren) *> not(leftSibling(anyNode)) *> not(ExprTry) *> not(lang.Expr) *> anyNode end firstUnmarkedChildStart - + def unMarkedChildSplit( - paren: Token, - split: Token, + paren: Token, + split: Token, ): SeqPattern[Node] = parent(leftSibling(ExprTry) *> paren) *> - possibleExprTryToRight(split) + possibleExprTryToRight(split) end unMarkedChildSplit def rightSiblingNotExprTry(): SeqPattern[Unit] = @@ -70,11 +71,10 @@ object ExprMarker extends PassSeq: end rightSiblingNotExprTry def possibleExprTryToRight( - node: SeqPattern[Node] + node: SeqPattern[Node], ): SeqPattern[Node] = - node <* rightSiblingNotExprTry() + node <* rightSiblingNotExprTry() end possibleExprTryToRight - object buildExpressions extends Pass: val wellformed = prevWellformed.makeDerived: @@ -92,27 +92,27 @@ object ExprMarker extends PassSeq: lang.Expr.importFrom(lang.wf) lang.Expr.addCases(lang.Expr) - val rules = + val rules = pass(once = false, strategy = pass.bottomUp) .rules: // Parse Number and String Literals on( leftSibling(ExprTry) *> field(TLAReader.NumberLiteral) - ~ trailing + ~ trailing, ).rewrite: lit => splice(lang.Expr(lang.Expr.NumberLiteral().like(lit))) | on( leftSibling(ExprTry) *> field(TLAReader.StringLiteral) - ~ trailing + ~ trailing, ).rewrite: lit => splice(lang.Expr(lang.Expr.StringLiteral().like(lit))) // Parse Id | on( leftSibling(ExprTry) *> field(TLAReader.Alpha) - ~ trailing + ~ trailing, ).rewrite: id => splice( lang.Expr( @@ -120,46 +120,48 @@ object ExprMarker extends PassSeq: lang.Id().like(id.unparent()), lang.Expr.OpCall.Params(), ), - ) + ), ) // TupleLiteral is complete when all the elements are parsed | on( - parsedChildrenSepBy(TLAReader.TupleGroup, `,`) + parsedChildrenSepBy(TLAReader.TupleGroup, `,`), ).rewrite: exprs => splice( lang.Expr( lang.Expr.TupleLiteral(exprs.iterator.map(_.unparent())), - ) - ) - // If the TupleLiteral not complete, mark the elements with ExprTry - // Mark the first child in the first pass, and then mark the rest in the second + ), + ) + // If the TupleLiteral not complete, mark the elements with ExprTry + // Mark the first child in the first pass, and then mark the rest in + // the second | on( - firstUnmarkedChildStart(TLAReader.TupleGroup) + firstUnmarkedChildStart(TLAReader.TupleGroup), ).rewrite: first => splice(ExprTry(), first.unparent()) | on( - unMarkedChildSplit(TLAReader.TupleGroup, `,`) + unMarkedChildSplit(TLAReader.TupleGroup, `,`), ).rewrite: split => - splice(split.unparent(), ExprTry()) + splice(split.unparent(), ExprTry()) // SetLiteral is complete when all the elements are parsed | on( - parsedChildrenSepBy(TLAReader.BracesGroup, `,`) + parsedChildrenSepBy(TLAReader.BracesGroup, `,`), ).rewrite: exprs => splice( lang.Expr( lang.Expr.SetLiteral(exprs.iterator.map(_.unparent())), - ) - ) + ), + ) // If the SetLiteral is not complete, mark the elements with ExprTry - // Mark the first child in the first pass, and then mark the rest in the second + // Mark the first child in the first pass, and then mark the rest in + // the second | on( - firstUnmarkedChildStart(TLAReader.BracesGroup) + firstUnmarkedChildStart(TLAReader.BracesGroup), ).rewrite: first => splice(ExprTry(), first.unparent()) | on( - unMarkedChildSplit(TLAReader.BracesGroup, `,`) + unMarkedChildSplit(TLAReader.BracesGroup, `,`), ).rewrite: split => - splice(split.unparent(), ExprTry()) + splice(split.unparent(), ExprTry()) // RecordLiteral is complete when all the elements are parsed | on( leftSibling(ExprTry) *> tok(TLAReader.SqBracketsGroup) *> @@ -167,30 +169,29 @@ object ExprMarker extends PassSeq: field( repeatedSepBy1(`,`)( field(TLAReader.Alpha) - ~ skip(TLAReader.`|->`) - ~ skip(ExprTry) - ~ field(lang.Expr) - ~ trailing - ) + ~ skip(TLAReader.`|->`) + ~ skip(ExprTry) + ~ field(lang.Expr) + ~ trailing, + ), ) - ~ eof + ~ eof, ).rewrite: records => splice( lang.Expr( lang.Expr.RecordLiteral( - records.iterator.map( - (id, expr) => - lang.Expr.RecordLiteral.Field( - lang.Id().like(id.unparent()), - expr.unparent(), - ) - ) - ) - ) + records.iterator.map((id, expr) => + lang.Expr.RecordLiteral.Field( + lang.Id().like(id.unparent()), + expr.unparent(), + ), + ), + ), + ), ) // If the RecordLiteral is not complete, place ExprTry after each |-> - | on ( - unMarkedChildSplit(TLAReader.SqBracketsGroup, `|->`) + | on( + unMarkedChildSplit(TLAReader.SqBracketsGroup, `|->`), ).rewrite: split => splice(split.unparent(), ExprTry()) // Parse Projection (Record field access) @@ -199,15 +200,15 @@ object ExprMarker extends PassSeq: field(lang.Expr) ~ skip(defns.`.`) ~ field(TLAReader.Alpha) - ~ trailing + ~ trailing, ).rewrite: (expr, id) => splice( lang.Expr( lang.Expr.Project( expr.unparent(), - lang.Id().like(id.unparent()) - ) - ) + lang.Id().like(id.unparent()), + ), + ), ) // IF is complete when every branch is parsed. | on( @@ -229,12 +230,14 @@ object ExprMarker extends PassSeq: pred.unparent(), t.unparent(), f.unparent(), - ) - ) + ), + ), ) // If IF is not complete, place ExprTry before the pred and branches - | on( - possibleExprTryToRight(tok(defns.IF) | tok(defns.THEN) | tok(defns.ELSE)) + | on( + possibleExprTryToRight( + tok(defns.IF) | tok(defns.THEN) | tok(defns.ELSE), + ), ).rewrite: split => splice(split.unparent(), ExprTry()) // CASE is complete when every branch is parsed. @@ -262,86 +265,91 @@ object ExprMarker extends PassSeq: ) ~ trailing, ).rewrite: (cases, other) => - splice( - lang.Expr( - lang.Expr.Case( - lang.Expr.Case.Branches( - cases.iterator.map((pred, branch) => - lang.Expr.Case.Branch(pred.unparent(), branch.unparent()), - ), - ), - lang.Expr.Case.Other( - other match - case None => lang.Expr.Case.None() - case Some(expr) => expr.unparent() + splice( + lang.Expr( + lang.Expr.Case( + lang.Expr.Case.Branches( + cases.iterator.map((pred, branch) => + lang.Expr.Case.Branch(pred.unparent(), branch.unparent()), ), ), - ) - ) + lang.Expr.Case.Other( + other match + case None => lang.Expr.Case.None() + case Some(expr) => expr.unparent(), + ), + ), + ), + ) // If the CASE is not complete, insert ExprTry after [], ->, and OTHER // as well as before the first case. | on( - possibleExprTryToRight(leftSibling(ExprTry) *> defns.CASE) + possibleExprTryToRight(leftSibling(ExprTry) *> defns.CASE), ).rewrite: c => splice(c.unparent(), ExprTry()) | on( - possibleExprTryToRight((tok(defns.`[]`) | tok(TLAReader.`->`))) + possibleExprTryToRight((tok(defns.`[]`) | tok(TLAReader.`->`))), ).rewrite: split => splice(split.unparent(), ExprTry()) | on( - possibleExprTryToRight(leftSibling(defns.OTHER) *> tok(TLAReader.`->`)) + possibleExprTryToRight( + leftSibling(defns.OTHER) *> tok(TLAReader.`->`), + ), ).rewrite: split => splice(split.unparent(), ExprTry()) // LET is complete when the definitions and the body are parsed - // I am assuming TLAParser will have inserted an ExpTry before the let body - | on ( + // I am assuming TLAParser will have inserted an ExpTry before the let + // body + | on( leftSibling(ExprTry) *> - field(tok(TLAReader.LetGroup) *> - children( - repeated: - tok(lang.Operator) - | tok(lang.ModuleDefinition) - | tok(lang.Recursive) - ) + field( + tok(TLAReader.LetGroup) *> + children( + repeated: + tok(lang.Operator) + | tok(lang.ModuleDefinition) + | tok(lang.Recursive), + ), ) ~ skip(ExprTry) ~ field(lang.Expr) - ~ trailing + ~ trailing, ).rewrite: (defs, body) => splice( lang.Expr( lang.Expr.Let( lang.Expr.Let.Defns( - defs.iterator.map(_.unparent()) + defs.iterator.map(_.unparent()), ), - body.unparent() - ) - ) + body.unparent(), + ), + ), ) // Parentheses can be removed when its children are parsed | on( - leftSibling(ExprTry) *> + leftSibling(ExprTry) *> tok(TLAReader.ParenthesesGroup) *> - children( - skip(ExprTry) + children( + skip(ExprTry) ~ field(lang.Expr) - ~ eof - ) + ~ eof, + ), ).rewrite: expr => splice(expr.unparent()) // Mark the children of the parentheses | on( - firstUnmarkedChildStart(TLAReader.ParenthesesGroup) + firstUnmarkedChildStart(TLAReader.ParenthesesGroup), ).rewrite: node => splice(ExprTry(), node.unparent()) *> pass(once = false, strategy = pass.bottomUp) .rules: // Expr has been parsed sucessfully, and ExprTry can be removed - // I have to do it this way, otherwise ExprTry might get removed too early. + // I have to do it this way, otherwise ExprTry might get removed too + // early. on( skip(ExprTry) - ~ field(lang.Expr) - ~ eof + ~ field(lang.Expr) + ~ eof, ).rewrite: expr => splice(expr.unparent()) end buildExpressions @@ -350,7 +358,7 @@ object ExprMarker extends PassSeq: val wellformed = prevWellformed.makeDerived: lang.Expr.removeCases(lang.Expr) - val rules = + val rules = pass(once = true, strategy = pass.bottomUp) .rules: on( @@ -360,4 +368,4 @@ object ExprMarker extends PassSeq: splice( child.unparent(), ) - end removeNestedExpr \ No newline at end of file + end removeNestedExpr diff --git a/langs/tla/ExprMarker.test.scala b/langs/tla/ExprMarker.test.scala index d02e883..bf4f271 100644 --- a/langs/tla/ExprMarker.test.scala +++ b/langs/tla/ExprMarker.test.scala @@ -16,7 +16,7 @@ package forja.langs.tla import forja.* import forja.dsl.* -// import forja.source.{Source, SourceRange} + import ExprMarker.ExprTry // Run with: @@ -40,8 +40,9 @@ class ExprMarkerTests extends munit.FunSuite: ), ), ) - // instrumentWithTracer(forja.manip.RewriteDebugTracer(os.pwd / "dbg_exprmarker")): - ExprMarker(freshTop) + /* instrumentWithTracer(forja.manip.RewriteDebugTracer(os.pwd / + * "dbg_exprmarker")): */ + ExprMarker(freshTop) Node.Top( freshTop(lang.Module)(lang.Module.Defns)(lang.Operator)( lang.Expr, @@ -50,57 +51,63 @@ class ExprMarkerTests extends munit.FunSuite: test("NumberLiteral"): assertEquals( - Node.Top(ExprTry(), TLAReader.NumberLiteral("1")).parseNode, - Node.Top(lang.Expr(lang.Expr.NumberLiteral("1"))), + Node.Top(ExprTry(), TLAReader.NumberLiteral("1")).parseNode, + Node.Top(lang.Expr(lang.Expr.NumberLiteral("1"))), ) test("StringLiteral"): assertEquals( - Node.Top(ExprTry(), TLAReader.StringLiteral("string")).parseNode, - Node.Top(lang.Expr(lang.Expr.StringLiteral("string"))), + Node.Top(ExprTry(), TLAReader.StringLiteral("string")).parseNode, + Node.Top(lang.Expr(lang.Expr.StringLiteral("string"))), ) test("Id"): assertEquals( - Node.Top(ExprTry(), TLAReader.Alpha("X")).parseNode, - Node.Top( - lang.Expr( - lang.Expr.OpCall( - lang.Id("X"), - lang.Expr.OpCall.Params() - ) - ) - ) + Node.Top(ExprTry(), TLAReader.Alpha("X")).parseNode, + Node.Top( + lang.Expr( + lang.Expr.OpCall( + lang.Id("X"), + lang.Expr.OpCall.Params(), + ), + ), + ), ) test("ParenthesesGroup"): assertEquals( - Node.Top(ExprTry(), TLAReader.ParenthesesGroup( - TLAReader.NumberLiteral("1") - )).parseNode, - Node.Top(lang.Expr(lang.Expr.NumberLiteral("1"))), + Node + .Top( + ExprTry(), + TLAReader.ParenthesesGroup( + TLAReader.NumberLiteral("1"), + ), + ) + .parseNode, + Node.Top(lang.Expr(lang.Expr.NumberLiteral("1"))), ) // TODO: paranthesis with op - test("SetLiteral"): - // empty set + // empty set assertEquals( Node.Top(ExprTry(), TLAReader.BracesGroup()).parseNode, - Node.Top(lang.Expr(lang.Expr.SetLiteral())) + Node.Top(lang.Expr(lang.Expr.SetLiteral())), ) // set with three elements assertEquals( - Node.Top( - ExprTry(), - TLAReader.BracesGroup( - TLAReader.NumberLiteral("1"), - TLAReader.`,`(","), - TLAReader.NumberLiteral("2"), - TLAReader.`,`(","), - TLAReader.NumberLiteral("3") + Node + .Top( + ExprTry(), + TLAReader.BracesGroup( + TLAReader.NumberLiteral("1"), + TLAReader.`,`(","), + TLAReader.NumberLiteral("2"), + TLAReader.`,`(","), + TLAReader.NumberLiteral("3"), + ), ) - ).parseNode, + .parseNode, Node.Top( lang.Expr( lang.Expr.SetLiteral( @@ -108,21 +115,23 @@ class ExprMarkerTests extends munit.FunSuite: lang.Expr(lang.Expr.NumberLiteral("2")), lang.Expr(lang.Expr.NumberLiteral("3")), ), - ) - ) + ), + ), ) // nested sets assertEquals( - Node.Top( - ExprTry(), - TLAReader.BracesGroup( - TLAReader.NumberLiteral("1"), - TLAReader.`,`(","), - TLAReader.BracesGroup(), - TLAReader.`,`(","), - TLAReader.NumberLiteral("3") + Node + .Top( + ExprTry(), + TLAReader.BracesGroup( + TLAReader.NumberLiteral("1"), + TLAReader.`,`(","), + TLAReader.BracesGroup(), + TLAReader.`,`(","), + TLAReader.NumberLiteral("3"), + ), ) - ).parseNode, + .parseNode, Node.Top( lang.Expr( lang.Expr.SetLiteral( @@ -130,28 +139,30 @@ class ExprMarkerTests extends munit.FunSuite: lang.Expr(lang.Expr.SetLiteral()), lang.Expr(lang.Expr.NumberLiteral("3")), ), - ) - ) + ), + ), ) test("TupleLiteral"): // empty tuple assertEquals( Node.Top(ExprTry(), TLAReader.TupleGroup()).parseNode, - Node.Top(lang.Expr(lang.Expr.TupleLiteral())) + Node.Top(lang.Expr(lang.Expr.TupleLiteral())), ) // tuple with three elements assertEquals( - Node.Top( - ExprTry(), - TLAReader.TupleGroup( - TLAReader.NumberLiteral("1"), - TLAReader.`,`(","), - TLAReader.StringLiteral("two"), - TLAReader.`,`(","), - TLAReader.NumberLiteral("3") + Node + .Top( + ExprTry(), + TLAReader.TupleGroup( + TLAReader.NumberLiteral("1"), + TLAReader.`,`(","), + TLAReader.StringLiteral("two"), + TLAReader.`,`(","), + TLAReader.NumberLiteral("3"), + ), ) - ).parseNode, + .parseNode, Node.Top( lang.Expr( lang.Expr.TupleLiteral( @@ -159,29 +170,31 @@ class ExprMarkerTests extends munit.FunSuite: lang.Expr(lang.Expr.StringLiteral("two")), lang.Expr(lang.Expr.NumberLiteral("3")), ), - ) - ) + ), + ), ) test("RecordLiteral"): // record with three fields assertEquals( - Node.Top( - ExprTry(), - TLAReader.SqBracketsGroup( - TLAReader.Alpha("X"), - TLAReader.`|->`("|->"), - TLAReader.NumberLiteral("1"), - TLAReader.`,`(","), - TLAReader.Alpha("Y"), - TLAReader.`|->`("|->"), - TLAReader.NumberLiteral("2"), - TLAReader.`,`(","), - TLAReader.Alpha("Z"), - TLAReader.`|->`("|->"), - TLAReader.NumberLiteral("3"), + Node + .Top( + ExprTry(), + TLAReader.SqBracketsGroup( + TLAReader.Alpha("X"), + TLAReader.`|->`("|->"), + TLAReader.NumberLiteral("1"), + TLAReader.`,`(","), + TLAReader.Alpha("Y"), + TLAReader.`|->`("|->"), + TLAReader.NumberLiteral("2"), + TLAReader.`,`(","), + TLAReader.Alpha("Z"), + TLAReader.`|->`("|->"), + TLAReader.NumberLiteral("3"), + ), ) - ).parseNode, + .parseNode, Node.Top( lang.Expr( lang.Expr.RecordLiteral( @@ -196,20 +209,22 @@ class ExprMarkerTests extends munit.FunSuite: lang.Expr.RecordLiteral.Field( lang.Id("Z"), lang.Expr(lang.Expr.NumberLiteral("3")), - ) + ), ), - ) - ) + ), + ), ) - + test("Projection (Record Field Acess)"): assertEquals( - Node.Top( - ExprTry(), - TLAReader.Alpha("X"), - defns.`.`("."), - TLAReader.Alpha("Y") - ).parseNode, + Node + .Top( + ExprTry(), + TLAReader.Alpha("X"), + defns.`.`("."), + TLAReader.Alpha("Y"), + ) + .parseNode, Node.Top( lang.Expr( lang.Expr.Project( @@ -221,18 +236,20 @@ class ExprMarkerTests extends munit.FunSuite: ), lang.Id("Y"), ), - ) - ) + ), + ), ) assertEquals( - Node.Top( - ExprTry(), - TLAReader.Alpha("X"), - defns.`.`("."), - TLAReader.Alpha("Y"), - defns.`.`("."), - TLAReader.Alpha("Z") - ).parseNode, + Node + .Top( + ExprTry(), + TLAReader.Alpha("X"), + defns.`.`("."), + TLAReader.Alpha("Y"), + defns.`.`("."), + TLAReader.Alpha("Z"), + ) + .parseNode, Node.Top( lang.Expr( lang.Expr.Project( @@ -242,29 +259,30 @@ class ExprMarkerTests extends munit.FunSuite: lang.Expr.OpCall( lang.Id("X"), lang.Expr.OpCall.Params(), - ) + ), ), lang.Id("Y"), - ) + ), ), - lang.Id("Z") - ) - ) - ) + lang.Id("Z"), + ), + ), + ), ) - test("If"): assertEquals( - Node.Top( - ExprTry(), - defns.IF(), - TLAReader.Alpha("A"), - defns.THEN(), - TLAReader.NumberLiteral("1"), - defns.ELSE(), - TLAReader.NumberLiteral("2"), - ).parseNode, + Node + .Top( + ExprTry(), + defns.IF(), + TLAReader.Alpha("A"), + defns.THEN(), + TLAReader.NumberLiteral("1"), + defns.ELSE(), + TLAReader.NumberLiteral("2"), + ) + .parseNode, Node.Top( lang.Expr( lang.Expr.If( @@ -278,17 +296,22 @@ class ExprMarkerTests extends munit.FunSuite: lang.Expr(lang.Expr.NumberLiteral("2")), ), ), - ) + ), ) - + test("Case"): assertEquals( + Node + .Top( + ExprTry(), + defns.CASE(), + TLAReader.StringLiteral("A"), + TLAReader.`->`("->"), + TLAReader.NumberLiteral("1"), + ) + .parseNode, Node.Top( - ExprTry(), - defns.CASE(), TLAReader.StringLiteral("A"), TLAReader.`->`("->"), TLAReader.NumberLiteral("1") - ).parseNode, - Node.Top( - lang.Expr( + lang.Expr( lang.Expr.Case( lang.Expr.Case.Branches( lang.Expr.Case.Branch( @@ -298,18 +321,25 @@ class ExprMarkerTests extends munit.FunSuite: ), lang.Expr.Case.Other(lang.Expr.Case.None()), ), - ) - ) + ), + ), ) assertEquals( + Node + .Top( + ExprTry(), + defns.CASE(), + TLAReader.StringLiteral("A"), + TLAReader.`->`("->"), + TLAReader.NumberLiteral("1"), + defns.`[]`("[]"), + TLAReader.StringLiteral("B"), + TLAReader.`->`("->"), + TLAReader.NumberLiteral("2"), + ) + .parseNode, Node.Top( - ExprTry(), - defns.CASE(), TLAReader.StringLiteral("A"), TLAReader.`->`("->"), TLAReader.NumberLiteral("1"), - defns.`[]`("[]"), TLAReader.StringLiteral("B"), TLAReader.`->`("->"), TLAReader.NumberLiteral("2"), - - ).parseNode, - Node.Top( - lang.Expr( + lang.Expr( lang.Expr.Case( lang.Expr.Case.Branches( lang.Expr.Case.Branch( @@ -323,19 +353,28 @@ class ExprMarkerTests extends munit.FunSuite: ), lang.Expr.Case.Other(lang.Expr.Case.None()), ), - ) - ) + ), + ), ) assertEquals( + Node + .Top( + ExprTry(), + defns.CASE(), + TLAReader.StringLiteral("A"), + TLAReader.`->`("->"), + TLAReader.NumberLiteral("1"), + defns.`[]`("[]"), + TLAReader.StringLiteral("B"), + TLAReader.`->`("->"), + TLAReader.NumberLiteral("2"), + defns.OTHER("OTHER"), + TLAReader.`->`("->"), + TLAReader.NumberLiteral("3"), + ) + .parseNode, Node.Top( - ExprTry(), - defns.CASE(), TLAReader.StringLiteral("A"), TLAReader.`->`("->"), TLAReader.NumberLiteral("1"), - defns.`[]`("[]"), TLAReader.StringLiteral("B"), TLAReader.`->`("->"), TLAReader.NumberLiteral("2"), - defns.OTHER("OTHER"), TLAReader.`->`("->"), TLAReader.NumberLiteral("3"), - - ).parseNode, - Node.Top( - lang.Expr( + lang.Expr( lang.Expr.Case( lang.Expr.Case.Branches( lang.Expr.Case.Branch( @@ -349,12 +388,14 @@ class ExprMarkerTests extends munit.FunSuite: ), lang.Expr.Case.Other(lang.Expr(lang.Expr.NumberLiteral("3"))), ), - ) - ) + ), + ), ) - // This test assumes that TLAParser has parsed the definitions and has inserted the ExprTry before the let body. - // TODO: I am not sure what kind of node I should pass to lang.Operator. It complains if it is an Expr. + /* This test assumes that TLAParser has parsed the definitions and has + * inserted the ExprTry before the let body. */ + /* TODO: I am not sure what kind of node I should pass to lang.Operator. It + * complains if it is an Expr. */ // test("LET"): // assertEquals( // Node.Top( @@ -413,4 +454,3 @@ class ExprMarkerTests extends munit.FunSuite: // ), // ) // ) - diff --git a/langs/tla/TLAReader.scala b/langs/tla/TLAReader.scala index 9a3ef1a..8affd1e 100644 --- a/langs/tla/TLAReader.scala +++ b/langs/tla/TLAReader.scala @@ -18,9 +18,9 @@ import cats.syntax.all.given import forja.* import forja.dsl.* +import forja.langs.tla.ExprMarker.ExprTry import forja.source.{Reader, SourceRange} import forja.wf.Wellformed -import forja.langs.tla.ExprMarker.ExprTry object TLAReader extends Reader: lazy val groupTokens: List[Token] = List( diff --git a/project.scala b/project.scala index 0a77987..ee80bbe 100644 --- a/project.scala +++ b/project.scala @@ -5,9 +5,9 @@ //> using dependency com.github.scopt::scopt:4.1.0 //> using dependency com.lihaoyi::os-lib:0.11.5 -//> using dependency com.lihaoyi::pprint:0.9.3 +//> using dependency com.lihaoyi::pprint:0.9.4 //> using dependency com.lihaoyi::sourcecode:0.4.4 -//> using dependency com.lihaoyi::ujson::4.3.0 +//> using dependency com.lihaoyi::ujson::4.4.0 //> using dependency dev.zio::izumi-reflect:3.0.6 //> using dependency edu.berkeley.cs.jqf:jqf-fuzz:2.1 //> using dependency edu.berkeley.cs.jqf:jqf-instrument:2.1 @@ -15,4 +15,4 @@ //> using dependency org.typelevel::cats-core:2.13.0 // Test -//> using test.dependency org.scalameta::munit:1.1.1 +//> using test.dependency org.scalameta::munit:1.2.1 diff --git a/src/wf/Wellformed.scala b/src/wf/Wellformed.scala index 607f82b..dcf0201 100644 --- a/src/wf/Wellformed.scala +++ b/src/wf/Wellformed.scala @@ -554,7 +554,7 @@ object Wellformed: throw IllegalArgumentException( s"$token's shape is not appropriate for adding cases ($shape)", ) - + def deleteShape(): Unit = token match case Node.Top =>