Cleaned up NGrammar and its test. Tweaked ParseTree string rep.

robby-phd · robby-phd · commit ee617dad298e · 2026-02-13T18:00:00.000-06:00
diff --git a/library/shared/src/main/scala/org/sireum/parser/NGrammar.scala b/library/shared/src/main/scala/org/sireum/parser/NGrammar.scala
@@ -41,18 +41,6 @@ object NElement {
     @strictpure override def toST: ST =
       st"""NElement.Ref($isTerminal, "$ruleName", u32"${conversions.U32.toZ(num)}")"""
   }
-  @datatype class Opt(val ruleName: String, val num: U32) extends NElement {
-    @strictpure override def toST: ST =
-      st"""NElement.Opt("$ruleName", u32"${conversions.U32.toZ(num)}")"""
-  }
-  @datatype class Star(val ruleName: String, val num: U32) extends NElement {
-    @strictpure override def toST: ST =
-      st"""NElement.Star("$ruleName", u32"${conversions.U32.toZ(num)}")"""
-  }
-  @datatype class Plus(val ruleName: String, val num: U32) extends NElement {
-    @strictpure override def toST: ST =
-      st"""NElement.Plus("$ruleName", u32"${conversions.U32.toZ(num)}")"""
-  }
 }
 @datatype trait NRule {
   @pure def name: String
@@ -106,18 +94,6 @@ object NGrammar {
         w.writeB(e.isTerminal)
         w.writeString(e.ruleName)
         w.writeU32(e.num)
-      case e: NElement.Opt =>
-        w.writeZ(2)
-        w.writeString(e.ruleName)
-        w.writeU32(e.num)
-      case e: NElement.Star =>
-        w.writeZ(3)
-        w.writeString(e.ruleName)
-        w.writeU32(e.num)
-      case e: NElement.Plus =>
-        w.writeZ(4)
-        w.writeString(e.ruleName)
-        w.writeU32(e.num)
     }
   }
 
@@ -133,18 +109,6 @@ object NGrammar {
         val ruleName = r.readString()
         val num = r.readU32()
         return NElement.Ref(isTerminal = isTerminal, ruleName = ruleName, num = num)
-      case 2 =>
-        val ruleName = r.readString()
-        val num = r.readU32()
-        return NElement.Opt(ruleName = ruleName, num = num)
-      case 3 =>
-        val ruleName = r.readString()
-        val num = r.readU32()
-        return NElement.Star(ruleName = ruleName, num = num)
-      case 4 =>
-        val ruleName = r.readString()
-        val num = r.readU32()
-        return NElement.Plus(ruleName = ruleName, num = num)
       case _ => halt(s"Invalid NElement tag: $tag")
     }
   }
@@ -253,22 +217,6 @@ object NGrammar {
       }
       return r
     }
-    def parseStar(ruleNum: U32, i: Z): Option[(Z, ISZ[ParseTree])] = {
-      var trees = ISZ[ParseTree]()
-      var j = i
-      while (pt.predict(ruleNum, lookahead(j)).nonEmpty) {
-        parseRule(ruleNum, j) match {
-          case Some((next, ts)) =>
-            if (next == j) {
-              halt(s"Infeasible: rule did not consume any input")
-            }
-            j = next
-            trees = trees ++ ts
-          case _ => halt(s"Infeasible")
-        }
-      }
-      return Some((j, trees))
-    }
     def parseElement(e: NElement, i: Z): Option[(Z, ISZ[ParseTree])] = {
       e match {
         case e: NElement.Str =>
@@ -299,23 +247,6 @@ object NGrammar {
           } else {
             return parseRule(e.num, i)
           }
-        case e: NElement.Opt =>
-          if (pt.predict(e.num, lookahead(i)).nonEmpty) {
-            return parseRule(e.num, i)
-          } else {
-            return Some((i, ISZ()))
-          }
-        case e: NElement.Plus =>
-          parseRule(e.num, i) match {
-            case Some((j, ts)) =>
-              parseStar(e.num, j) match {
-                case Some((k, ts2)) => return Some((k, ts ++ ts2))
-                case _ => return Some((j, ts))
-              }
-            case _ => return None()
-          }
-        case e: NElement.Star => return parseStar(e.num, i)
-        case e => halt(s"Unsupported: $e")
       }
     }
     def parseElements(elements: NRule.Elements, i: Z): Option[(Z, ISZ[ParseTree])] = {
diff --git a/library/shared/src/main/scala/org/sireum/parser/ParseTree.scala b/library/shared/src/main/scala/org/sireum/parser/ParseTree.scala
@@ -49,20 +49,21 @@ object ParseTree {
                        @hidden val tipe: U32,
                        @hidden val isHidden: B,
                        @hidden val posOpt: Option[Position]) extends ParseTree with Token {
-    @pure override def toST: ST = {
-      return if (ops.StringOps(ruleName).startsWith("'")) st""""${ops.StringOps(text).escapeST}""""
+    @strictpure override def toST: ST =
+      if (ops.StringOps(ruleName).startsWith("'")) st""""${ops.StringOps(text).escapeST}""""
       else st"""$ruleName["${ops.StringOps(text).escapeST}"]"""
-    }
     @strictpure def toLeaf: ParseTree.Leaf = this
     @strictpure def num: U32 = tipe
   }
 
   @datatype class Node(val children: ISZ[ParseTree],
                        @hidden val ruleName: String,
                        @hidden val tipe: U32) extends ParseTree {
-    @pure override def toST: ST = {
-      return st"""$ruleName(${(for (child <- children) yield child.toST, ", ")})"""
-    }
+    @strictpure override def toST: ST =
+      st"""$ruleName(
+          |  ${(for (child <- children) yield child.toST, ",\n")}
+          |)"""
+
   }
 
   @record class DotGenerator {
diff --git a/library/shared/src/test/scala/org/sireum/NGrammarCompactTest.scala b/library/shared/src/test/scala/org/sireum/NGrammarCompactTest.scala
@@ -199,54 +199,6 @@ class NGrammarCompactTest extends TestSuite {
       assert(decoded == ng)
     }
 
-    // NGrammar: NRule.Elements with NElement.Opt
-    * - {
-      val ng = NGrammar(
-        ruleMap = HashSMap.empty[U32, NRule] +
-          u32"0" ~> NRule.Elements(
-            name = "optRule",
-            num = u32"0",
-            isSynthetic = F,
-            elements = ISZ(NElement.Opt(ruleName = "maybeExpr", num = u32"7"))
-          ),
-        pt = emptyPT
-      )
-      val decoded = NGrammar.fromCompact(ng.toCompact)
-      assert(decoded == ng)
-    }
-
-    // NGrammar: NRule.Elements with NElement.Star
-    * - {
-      val ng = NGrammar(
-        ruleMap = HashSMap.empty[U32, NRule] +
-          u32"0" ~> NRule.Elements(
-            name = "starRule",
-            num = u32"0",
-            isSynthetic = F,
-            elements = ISZ(NElement.Star(ruleName = "stmts", num = u32"8"))
-          ),
-        pt = emptyPT
-      )
-      val decoded = NGrammar.fromCompact(ng.toCompact)
-      assert(decoded == ng)
-    }
-
-    // NGrammar: NRule.Elements with NElement.Plus
-    * - {
-      val ng = NGrammar(
-        ruleMap = HashSMap.empty[U32, NRule] +
-          u32"0" ~> NRule.Elements(
-            name = "plusRule",
-            num = u32"0",
-            isSynthetic = F,
-            elements = ISZ(NElement.Plus(ruleName = "args", num = u32"9"))
-          ),
-        pt = emptyPT
-      )
-      val decoded = NGrammar.fromCompact(ng.toCompact)
-      assert(decoded == ng)
-    }
-
     // NGrammar: NRule.Alts
     * - {
       val ng = NGrammar(
@@ -274,9 +226,6 @@ class NGrammarCompactTest extends TestSuite {
             elements = ISZ(
               NElement.Str(value = "(", num = u32"10"),
               NElement.Ref(isTerminal = T, ruleName = "ID", num = u32"11"),
-              NElement.Opt(ruleName = "typeAnnot", num = u32"12"),
-              NElement.Star(ruleName = "args", num = u32"13"),
-              NElement.Plus(ruleName = "stmts", num = u32"14"),
               NElement.Ref(isTerminal = F, ruleName = "body", num = u32"15"),
               NElement.Str(value = ")", num = u32"16")
             )
