minor fixes to package and defns

langs/tla/defns.scala

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

langs/tla/package.scala

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

src/Node.scala

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

src/wf/Wellformed.scala

@@ -555,6 +555,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