|
| 1 | +// Copyright 2024-2025 Forja Team |
| 2 | +// |
| 3 | +// Licensed under the Apache License, Version 2.0 (the "License"); |
| 4 | +// you may not use this file except in compliance with the License. |
| 5 | +// You may obtain a copy of the License at |
| 6 | +// |
| 7 | +// http://www.apache.org/licenses/LICENSE-2.0 |
| 8 | +// |
| 9 | +// Unless required by applicable law or agreed to in writing, software |
| 10 | +// distributed under the License is distributed on an "AS IS" BASIS, |
| 11 | +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. |
| 12 | +// See the License for the specific language governing permissions and |
| 13 | +// limitations under the License. |
| 14 | + |
| 15 | +package forja.langs.tla |
| 16 | + |
| 17 | +import cats.syntax.all.given |
| 18 | + |
| 19 | +import forja.* |
| 20 | +import forja.dsl.* |
| 21 | +import forja.wf.Wellformed |
| 22 | + |
| 23 | +import TLAReader.* |
| 24 | + |
| 25 | +object ExprMarker extends PassSeq: |
| 26 | + |
| 27 | + lazy val passes = List( |
| 28 | + buildExpressions, |
| 29 | + // removeNestedExpr |
| 30 | + ) |
| 31 | + |
| 32 | + object ExprTry extends Token |
| 33 | + def inputWellformed: Wellformed = TLAParser.outputWellformed |
| 34 | + |
| 35 | + def parsedChildrenSepBy( |
| 36 | + parent: Token, |
| 37 | + split: SeqPattern[?], |
| 38 | + ): SeqPattern[List[Node]] = |
| 39 | + leftSibling(ExprTry) *> |
| 40 | + tok(parent) *> |
| 41 | + children: |
| 42 | + field( |
| 43 | + repeatedSepBy(split)( |
| 44 | + skip(ExprTry) |
| 45 | + ~ field(lang.Expr) |
| 46 | + ~ trailing, |
| 47 | + ), |
| 48 | + ) |
| 49 | + ~ eof |
| 50 | + end parsedChildrenSepBy |
| 51 | + |
| 52 | + // TODO: I wonder if this pattern is a bad idea |
| 53 | + def firstUnmarkedChildStart( |
| 54 | + paren: Token, |
| 55 | + ): SeqPattern[Node] = |
| 56 | + parent(leftSibling(ExprTry) *> paren) *> |
| 57 | + not(leftSibling(anyNode)) *> |
| 58 | + not(ExprTry) *> not(lang.Expr) *> anyNode |
| 59 | + end firstUnmarkedChildStart |
| 60 | + |
| 61 | + def unMarkedChildSplit( |
| 62 | + paren: Token, |
| 63 | + split: Token, |
| 64 | + ): SeqPattern[Node] = |
| 65 | + parent(leftSibling(ExprTry) *> paren) *> |
| 66 | + possibleExprTryToRight(split) |
| 67 | + end unMarkedChildSplit |
| 68 | + |
| 69 | + def rightSiblingNotExprTry(): SeqPattern[Unit] = |
| 70 | + rightSibling(not(lang.Expr) *> not(ExprTry)) |
| 71 | + end rightSiblingNotExprTry |
| 72 | + |
| 73 | + def possibleExprTryToRight( |
| 74 | + node: SeqPattern[Node], |
| 75 | + ): SeqPattern[Node] = |
| 76 | + node <* rightSiblingNotExprTry() |
| 77 | + end possibleExprTryToRight |
| 78 | + |
| 79 | + object buildExpressions extends Pass: |
| 80 | + val wellformed = prevWellformed.makeDerived: |
| 81 | + val removedCases = Seq( |
| 82 | + TLAReader.StringLiteral, |
| 83 | + TLAReader.NumberLiteral, |
| 84 | + TLAReader.TupleGroup, |
| 85 | + // TODO: remove cases |
| 86 | + ) |
| 87 | + TLAReader.groupTokens.foreach: tok => |
| 88 | + tok.removeCases(removedCases*) |
| 89 | + tok.addCases(lang.Expr) |
| 90 | + |
| 91 | + lang.Expr.deleteShape() |
| 92 | + lang.Expr.importFrom(lang.wf) |
| 93 | + lang.Expr.addCases(lang.Expr) |
| 94 | + |
| 95 | + val rules = |
| 96 | + pass(once = false, strategy = pass.bottomUp) |
| 97 | + .rules: |
| 98 | + // Parse Number and String Literals |
| 99 | + on( |
| 100 | + leftSibling(ExprTry) *> |
| 101 | + field(TLAReader.NumberLiteral) |
| 102 | + ~ trailing, |
| 103 | + ).rewrite: lit => |
| 104 | + splice(lang.Expr(lang.Expr.NumberLiteral().like(lit))) |
| 105 | + | on( |
| 106 | + leftSibling(ExprTry) *> |
| 107 | + field(TLAReader.StringLiteral) |
| 108 | + ~ trailing, |
| 109 | + ).rewrite: lit => |
| 110 | + splice(lang.Expr(lang.Expr.StringLiteral().like(lit))) |
| 111 | + // Parse Id |
| 112 | + | on( |
| 113 | + leftSibling(ExprTry) *> |
| 114 | + field(TLAReader.Alpha) |
| 115 | + ~ trailing, |
| 116 | + ).rewrite: id => |
| 117 | + splice( |
| 118 | + lang.Expr( |
| 119 | + lang.Expr.OpCall( |
| 120 | + lang.Id().like(id.unparent()), |
| 121 | + lang.Expr.OpCall.Params(), |
| 122 | + ), |
| 123 | + ), |
| 124 | + ) |
| 125 | + // TupleLiteral is complete when all the elements are parsed |
| 126 | + | on( |
| 127 | + parsedChildrenSepBy(TLAReader.TupleGroup, `,`), |
| 128 | + ).rewrite: exprs => |
| 129 | + splice( |
| 130 | + lang.Expr( |
| 131 | + lang.Expr.TupleLiteral(exprs.iterator.map(_.unparent())), |
| 132 | + ), |
| 133 | + ) |
| 134 | + // If the TupleLiteral not complete, mark the elements with ExprTry |
| 135 | + // Mark the first child in the first pass, and then mark the rest in |
| 136 | + // the second |
| 137 | + | on( |
| 138 | + firstUnmarkedChildStart(TLAReader.TupleGroup), |
| 139 | + ).rewrite: first => |
| 140 | + splice(ExprTry(), first.unparent()) |
| 141 | + | on( |
| 142 | + unMarkedChildSplit(TLAReader.TupleGroup, `,`), |
| 143 | + ).rewrite: split => |
| 144 | + splice(split.unparent(), ExprTry()) |
| 145 | + // SetLiteral is complete when all the elements are parsed |
| 146 | + | on( |
| 147 | + parsedChildrenSepBy(TLAReader.BracesGroup, `,`), |
| 148 | + ).rewrite: exprs => |
| 149 | + splice( |
| 150 | + lang.Expr( |
| 151 | + lang.Expr.SetLiteral(exprs.iterator.map(_.unparent())), |
| 152 | + ), |
| 153 | + ) |
| 154 | + // If the SetLiteral is not complete, mark the elements with ExprTry |
| 155 | + // Mark the first child in the first pass, and then mark the rest in |
| 156 | + // the second |
| 157 | + | on( |
| 158 | + firstUnmarkedChildStart(TLAReader.BracesGroup), |
| 159 | + ).rewrite: first => |
| 160 | + splice(ExprTry(), first.unparent()) |
| 161 | + | on( |
| 162 | + unMarkedChildSplit(TLAReader.BracesGroup, `,`), |
| 163 | + ).rewrite: split => |
| 164 | + splice(split.unparent(), ExprTry()) |
| 165 | + // RecordLiteral is complete when all the elements are parsed |
| 166 | + | on( |
| 167 | + leftSibling(ExprTry) *> tok(TLAReader.SqBracketsGroup) *> |
| 168 | + children: |
| 169 | + field( |
| 170 | + repeatedSepBy1(`,`)( |
| 171 | + field(TLAReader.Alpha) |
| 172 | + ~ skip(TLAReader.`|->`) |
| 173 | + ~ skip(ExprTry) |
| 174 | + ~ field(lang.Expr) |
| 175 | + ~ trailing, |
| 176 | + ), |
| 177 | + ) |
| 178 | + ~ eof, |
| 179 | + ).rewrite: records => |
| 180 | + splice( |
| 181 | + lang.Expr( |
| 182 | + lang.Expr.RecordLiteral( |
| 183 | + records.iterator.map((id, expr) => |
| 184 | + lang.Expr.RecordLiteral.Field( |
| 185 | + lang.Id().like(id.unparent()), |
| 186 | + expr.unparent(), |
| 187 | + ), |
| 188 | + ), |
| 189 | + ), |
| 190 | + ), |
| 191 | + ) |
| 192 | + // If the RecordLiteral is not complete, place ExprTry after each |-> |
| 193 | + | on( |
| 194 | + unMarkedChildSplit(TLAReader.SqBracketsGroup, `|->`), |
| 195 | + ).rewrite: split => |
| 196 | + splice(split.unparent(), ExprTry()) |
| 197 | + // Parse Projection (Record field access) |
| 198 | + | on( |
| 199 | + leftSibling(ExprTry) *> |
| 200 | + field(lang.Expr) |
| 201 | + ~ skip(defns.`.`) |
| 202 | + ~ field(TLAReader.Alpha) |
| 203 | + ~ trailing, |
| 204 | + ).rewrite: (expr, id) => |
| 205 | + splice( |
| 206 | + lang.Expr( |
| 207 | + lang.Expr.Project( |
| 208 | + expr.unparent(), |
| 209 | + lang.Id().like(id.unparent()), |
| 210 | + ), |
| 211 | + ), |
| 212 | + ) |
| 213 | + // IF is complete when every branch is parsed. |
| 214 | + | on( |
| 215 | + leftSibling(ExprTry) *> |
| 216 | + skip(defns.IF) |
| 217 | + ~ skip(ExprTry) |
| 218 | + ~ field(lang.Expr) |
| 219 | + ~ skip(defns.THEN) |
| 220 | + ~ skip(ExprTry) |
| 221 | + ~ field(lang.Expr) |
| 222 | + ~ skip(defns.ELSE) |
| 223 | + ~ skip(ExprTry) |
| 224 | + ~ field(lang.Expr) |
| 225 | + ~ trailing, |
| 226 | + ).rewrite: (pred, t, f) => |
| 227 | + splice( |
| 228 | + lang.Expr( |
| 229 | + lang.Expr.If( |
| 230 | + pred.unparent(), |
| 231 | + t.unparent(), |
| 232 | + f.unparent(), |
| 233 | + ), |
| 234 | + ), |
| 235 | + ) |
| 236 | + // If IF is not complete, place ExprTry before the pred and branches |
| 237 | + | on( |
| 238 | + possibleExprTryToRight( |
| 239 | + tok(defns.IF) | tok(defns.THEN) | tok(defns.ELSE), |
| 240 | + ), |
| 241 | + ).rewrite: split => |
| 242 | + splice(split.unparent(), ExprTry()) |
| 243 | + // CASE is complete when every branch is parsed. |
| 244 | + | on( |
| 245 | + leftSibling(ExprTry) *> |
| 246 | + skip(defns.CASE) |
| 247 | + ~ field( |
| 248 | + repeatedSepBy1(defns.`[]`)( |
| 249 | + skip(ExprTry) |
| 250 | + ~ field(lang.Expr) |
| 251 | + ~ skip(TLAReader.`->`) |
| 252 | + ~ skip(ExprTry) |
| 253 | + ~ field(lang.Expr) |
| 254 | + ~ trailing, |
| 255 | + ), |
| 256 | + ) |
| 257 | + ~ field( |
| 258 | + optional( |
| 259 | + skip(defns.OTHER) |
| 260 | + ~ skip(TLAReader.`->`) |
| 261 | + ~ skip(ExprTry) |
| 262 | + ~ field(lang.Expr) |
| 263 | + ~ eof, |
| 264 | + ), |
| 265 | + ) |
| 266 | + ~ trailing, |
| 267 | + ).rewrite: (cases, other) => |
| 268 | + splice( |
| 269 | + lang.Expr( |
| 270 | + lang.Expr.Case( |
| 271 | + lang.Expr.Case.Branches( |
| 272 | + cases.iterator.map((pred, branch) => |
| 273 | + lang.Expr.Case.Branch(pred.unparent(), branch.unparent()), |
| 274 | + ), |
| 275 | + ), |
| 276 | + lang.Expr.Case.Other( |
| 277 | + other match |
| 278 | + case None => lang.Expr.Case.None() |
| 279 | + case Some(expr) => expr.unparent(), |
| 280 | + ), |
| 281 | + ), |
| 282 | + ), |
| 283 | + ) |
| 284 | + // If the CASE is not complete, insert ExprTry after [], ->, and OTHER |
| 285 | + // as well as before the first case. |
| 286 | + | on( |
| 287 | + possibleExprTryToRight(leftSibling(ExprTry) *> defns.CASE), |
| 288 | + ).rewrite: c => |
| 289 | + splice(c.unparent(), ExprTry()) |
| 290 | + | on( |
| 291 | + possibleExprTryToRight((tok(defns.`[]`) | tok(TLAReader.`->`))), |
| 292 | + ).rewrite: split => |
| 293 | + splice(split.unparent(), ExprTry()) |
| 294 | + | on( |
| 295 | + possibleExprTryToRight( |
| 296 | + leftSibling(defns.OTHER) *> tok(TLAReader.`->`), |
| 297 | + ), |
| 298 | + ).rewrite: split => |
| 299 | + splice(split.unparent(), ExprTry()) |
| 300 | + // LET is complete when the definitions and the body are parsed |
| 301 | + // I am assuming TLAParser will have inserted an ExpTry before the let |
| 302 | + // body |
| 303 | + | on( |
| 304 | + leftSibling(ExprTry) *> |
| 305 | + field( |
| 306 | + tok(TLAReader.LetGroup) *> |
| 307 | + children( |
| 308 | + repeated: |
| 309 | + tok(lang.Operator) |
| 310 | + | tok(lang.ModuleDefinition) |
| 311 | + | tok(lang.Recursive), |
| 312 | + ), |
| 313 | + ) |
| 314 | + ~ skip(ExprTry) |
| 315 | + ~ field(lang.Expr) |
| 316 | + ~ trailing, |
| 317 | + ).rewrite: (defs, body) => |
| 318 | + splice( |
| 319 | + lang.Expr( |
| 320 | + lang.Expr.Let( |
| 321 | + lang.Expr.Let.Defns( |
| 322 | + defs.iterator.map(_.unparent()), |
| 323 | + ), |
| 324 | + body.unparent(), |
| 325 | + ), |
| 326 | + ), |
| 327 | + ) |
| 328 | + // Parentheses can be removed when its children are parsed |
| 329 | + | on( |
| 330 | + leftSibling(ExprTry) *> |
| 331 | + tok(TLAReader.ParenthesesGroup) *> |
| 332 | + children( |
| 333 | + skip(ExprTry) |
| 334 | + ~ field(lang.Expr) |
| 335 | + ~ eof, |
| 336 | + ), |
| 337 | + ).rewrite: expr => |
| 338 | + splice(expr.unparent()) |
| 339 | + // Mark the children of the parentheses |
| 340 | + | on( |
| 341 | + firstUnmarkedChildStart(TLAReader.ParenthesesGroup), |
| 342 | + ).rewrite: node => |
| 343 | + splice(ExprTry(), node.unparent()) |
| 344 | + *> pass(once = false, strategy = pass.bottomUp) |
| 345 | + .rules: |
| 346 | + // Expr has been parsed sucessfully, and ExprTry can be removed |
| 347 | + // I have to do it this way, otherwise ExprTry might get removed too |
| 348 | + // early. |
| 349 | + on( |
| 350 | + skip(ExprTry) |
| 351 | + ~ field(lang.Expr) |
| 352 | + ~ eof, |
| 353 | + ).rewrite: expr => |
| 354 | + splice(expr.unparent()) |
| 355 | + end buildExpressions |
| 356 | + |
| 357 | + object removeNestedExpr extends Pass: |
| 358 | + val wellformed = prevWellformed.makeDerived: |
| 359 | + lang.Expr.removeCases(lang.Expr) |
| 360 | + |
| 361 | + val rules = |
| 362 | + pass(once = true, strategy = pass.bottomUp) |
| 363 | + .rules: |
| 364 | + on( |
| 365 | + tok(lang.Expr) *> |
| 366 | + onlyChild(lang.Expr), |
| 367 | + ).rewrite: child => |
| 368 | + splice( |
| 369 | + child.unparent(), |
| 370 | + ) |
| 371 | + end removeNestedExpr |
0 commit comments