refactor VariantUnwrap into VariantTag

src/tla/Variants.tla

@@ -41,24 +41,18 @@ VariantFilter(__tagName, __S) ==
     { __d \in { __e \in __S: __e.tag = __tagName }: __d.value }
 
 (**
- * In cases where `variant` allows for one value,
- * extract the associated value and return it.
- * The type checker must enforce that `variant` allows for one option.
+ * Get the tag name that is associated with a variant.
  *
- * @param `tagValue` the tag attached to the variant
  * @param `variant` a variant that is constructed with `Variant(...)`
- * @return the value extracted from the variant
+ * @return the tag name associated with a variant
  *
- * Its type could look like follows:
+ * Its type is as follows:
  *
- *   (Str, Tag(a)) => a
+ *   Variant(a) => Str
  *)
-VariantUnwrap(__tagName, __variant) ==
+VariantTag(__variant) ==
     \* default untyped implementation
-    IF __variant.tag = __tagName
-    THEN __variant.value
-    ELSE \* trigger an error in TLC by choosing a non-existent element
-         CHOOSE x \in { __variant }: x.tag = __tagName
+    __variant.tag
 
 (**
  * Return the value associated with the tag, when the tag equals to __tagName.

test/tla/TestVariants.tla

@@ -33,10 +33,8 @@ TestVariantFilter ==
     \E v \in VariantFilter("B", { VarA, VarB }):
         v.value = "hello"
 
-TestVariantUnwrap ==
-    \* We could just pass "world", without wrapping it in a record.
-    \* But we want to see how it works with records too.
-    VariantUnwrap("C", VarC) = [ value |-> "world" ]
+TestVariantTag ==
+    VariantTag(VarC) = "C"
 
 TestVariantGetUnsafe ==
     \* The unsafe version gives us only a type guarantee.
@@ -49,7 +47,7 @@ TestVariantGetOrElse ==
 AllTests ==
     /\ TestVariant
     /\ TestVariantFilter
-    /\ TestVariantUnwrap
+    /\ TestVariantTag
     /\ TestVariantGetUnsafe
     /\ TestVariantGetOrElse