From 74a30f4ae5a0f3944b09e313aa77619419bb8c21 Mon Sep 17 00:00:00 2001
From: KuterBora <kuterbora29@gmail.com>
Date: Wed, 11 Jun 2025 13:45:14 -0700
Subject: [PATCH 1/2] minor fixes to package and defns

---
 langs/tla/defns.scala   | 10 +++++++---
 langs/tla/package.scala |  6 +++++-
 src/Node.scala          |  2 +-
 src/wf/Wellformed.scala |  9 +++++++++
 4 files changed, 22 insertions(+), 5 deletions(-)

diff --git a/langs/tla/defns.scala b/langs/tla/defns.scala
index 0372867..fb8dbd1 100644
--- a/langs/tla/defns.scala
+++ b/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)
diff --git a/langs/tla/package.scala b/langs/tla/package.scala
index be312f0..2bfee44 100644
--- a/langs/tla/package.scala
+++ b/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,7 +181,8 @@ 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(
@@ -188,6 +190,8 @@ object lang extends WellformedDef:
               Expr,
             ),
           )
+      object Other extends t(choice(Expr, None))
+      object None extends t(Atom)
     end Case
 
     object Let
diff --git a/src/Node.scala b/src/Node.scala
index 953b660..015fb44 100644
--- a/src/Node.scala
+++ b/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
 
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 4393db2d75719d0ddce7d532fe7340e3ccee4260 Mon Sep 17 00:00:00 2001
From: KuterBora <kuterbora29@gmail.com>
Date: Wed, 11 Jun 2025 14:49:18 -0700
Subject: [PATCH 2/2] fix format manually

---
 src/wf/Wellformed.scala | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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 =>