Merge pull request #1525 from informalsystems/gabriela/get-only-element

Add `getOnlyElement()` built in operator

CHANGELOG.md

@@ -23,6 +23,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 - `quint verify` has the option `--apalache-version` to pull a custom version (#1521)
 - Grammar updated with support for an optional leading hashbang (`#!`) line (#1522)
+- Added a new operator called `getOnlyElement()` to extract elements out of singleton sets (#1525)
 
 ### Changed
 ### Deprecated

docs/pages/docs/builtin.md

@@ -306,6 +306,19 @@ assert(Set(1, 2).allListsUpTo(1) == Set([], [1], [2]))
 assert(Set(1).allListsUpTo(2) == Set([], [1], [1, 1]))
 ```
 
+## getOnlyElement
+
+Signature: `pure def getOnlyElement: (Set[a]) => a`
+
+`s.getOnlyElement()` is, deterministically, the only element of `s`.
+If the size of `s` is not 1, this operator has undefined behavior.
+
+### Examples
+
+```quint
+assert(Set(5).getOnlyElement() == 5)
+```
+
 ## chooseSome
 
 Signature: `pure def chooseSome: (Set[a]) => a`

quint/src/builtin.qnt

@@ -236,6 +236,16 @@ module builtin {
   /// ```
   pure def allListsUpTo(s: Set[a], max_length: int): Set[List[a]]
 
+  /// `s.getOnlyElement()` is, deterministically, the only element of `s`.
+  /// If the size of `s` is not 1, this operator has undefined behavior.
+  ///
+  /// ### Examples
+  ///
+  /// ```quint
+  /// assert(Set(5).getOnlyElement() == 5)
+  /// ```
+  pure def getOnlyElement(s): (Set[a]) => a
+
   /// `s.chooseSome()` is, deterministically, one element of `s`.
   ///
   /// ### Examples

quint/src/effects/builtinSignatures.ts

@@ -144,6 +144,7 @@ export const setOperators = [
   { name: 'flatten', effect: standardPropagation(1) },
   { name: 'allLists', effect: standardPropagation(1) },
   { name: 'allListsUpTo', effect: standardPropagation(2) },
+  { name: 'getOnlyElement', effect: standardPropagation(1) },
   { name: 'chooseSome', effect: standardPropagation(1) },
   { name: 'oneOf', effect: standardPropagation(1) },
   { name: 'isFinite', effect: standardPropagation(1) },

quint/src/names/base.ts

@@ -175,6 +175,7 @@ export const builtinNames = [
   'flatten',
   'allLists',
   'allListsUpTo',
+  'getOnlyElement',
   'chooseSome',
   'oneOf',
   'isFinite',

quint/src/runtime/impl/builtins.ts

@@ -752,6 +752,19 @@ export function builtinLambda(op: string): (ctx: Context, args: RuntimeValue[])
 
         return right(rv.mkSet(lists.map(list => rv.mkList(list)).toOrderedSet()))
       }
+    case 'getOnlyElement':
+      // Get the only element of a set, or an error if the set is empty or has more than one element.
+      return (_, args) => {
+        const set = args[0].toSet()
+        if (set.size !== 1) {
+          return left({
+            code: 'QNT505',
+            message: `Called 'getOnlyElement' on a set with ${set.size} elements. Make sure the set has exactly one element.`,
+          })
+        }
+
+        return right(set.first())
+      }
 
     case 'q::debug':
       // Print a value to the console, and return it

quint/src/types/builtinSignatures.ts

@@ -60,6 +60,7 @@ const setOperators = [
   { name: 'flatten', type: '(Set[Set[a]]) => Set[a]' },
   { name: 'allLists', type: '(Set[a]) => Set[List[a]]' },
   { name: 'allListsUpTo', type: '(Set[a], int) => Set[List[a]]' },
+  { name: 'getOnlyElement', type: '(Set[a]) => a' },
   { name: 'chooseSome', type: '(Set[a]) => a' },
   { name: 'oneOf', type: '(Set[a]) => a' },
   { name: 'isFinite', type: '(Set[a]) => bool' },

quint/test/runtime/compile.test.ts

@@ -779,6 +779,12 @@ describe('compiling specs to runtime values', () => {
       assertResultAsString('Set().allListsUpTo(3)', 'Set(List())')
       assertResultAsString('Set(1).allListsUpTo(0)', 'Set(List())')
     })
+
+    it('getOnlyElement', () => {
+      assertResultAsString('Set(5).getOnlyElement()', '5')
+      assertResultAsString('Set().getOnlyElement()', undefined)
+      assertResultAsString('Set(1, 2).getOnlyElement()', undefined)
+    })
   })
 
   describe('compile over records', () => {