Merge pull request #1202 from informalsystems/th/tuple-unbox

Syntax sugar for tuple unpacking

CHANGELOG.md

@@ -22,6 +22,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   through Apalache (#1188)
 
 ### Changed
+
+- Changed syntax for unpacking tuples in lambda parameters (#1202)
+
 ### Deprecated
 ### Removed
 ### Fixed

README.md

@@ -165,7 +165,7 @@ completely implementing every pass.
 | [Lists][]                         | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:                |
 | [Records][]                       | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:                |
 | [Discriminated unions][]          | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: [244][]        | :x: [539][]        | :x:                | :x:                |
-| [Tuples][]                        | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :green_circle:     | :white_check_mark: |
+| [Tuples][]                        | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [Imports][]                       | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [Module definitions][]            | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [Module instances][]              | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:                |

examples/.scripts/run-example.sh

@@ -54,8 +54,6 @@ result () {
       printf "<sup>https://github.com/informalsystems/quint/issues/244</sup>"
     elif [[ "$file" == "language-features/option.qnt" && "$cmd" == "verify"  ]] ; then
       printf "<sup>https://github.com/informalsystems/quint/issues/244</sup>"
-    elif [[ "$file" == "language-features/tuples.qnt" && "$cmd" == "verify" ]] ; then
-      printf "<sup>https://github.com/informalsystems/quint/issues/1113</sup>"
     elif [[ "$file" == "solidity/icse23-fig7/lottery.qnt" && "$cmd" == "verify" ]] ; then
       printf "<sup>https://github.com/informalsystems/quint/issues/1019</sup>"
     fi

examples/README.md

@@ -83,7 +83,7 @@ listed without any additional command line arguments.
 | [language-features/option.qnt](./language-features/option.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/244</sup> |
 | [language-features/records.qnt](./language-features/records.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/sets.qnt](./language-features/sets.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [language-features/tuples.qnt](./language-features/tuples.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/1113</sup> |
+| [language-features/tuples.qnt](./language-features/tuples.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [puzzles/prisoners/prisoners.qnt](./puzzles/prisoners/prisoners.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [puzzles/river/river.qnt](./puzzles/river/river.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [puzzles/tictactoe/tictactoe.qnt](./puzzles/tictactoe/tictactoe.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |

examples/classic/distributed/Paxos/Paxos.qnt

@@ -17,7 +17,7 @@ module Paxos {
 
   assume _ = and {
       Quorum.forall(Q => Q.subseteq(Acceptor)),
-      tuples(Quorum, Quorum).forall((Q1, Q2) => (Q1.intersect(Q2)) != Set())
+      tuples(Quorum, Quorum).forall( ((Q1, Q2)) => (Q1.intersect(Q2)) != Set())
   }
 
   val Ballot = Nat

examples/classic/distributed/Paxos/Voting.qnt

@@ -15,7 +15,7 @@ const Quorum: Set[Set[str]] // The set of "quorums", where a quorum" is a
 (***************************************************************************/
 assume QuorumAssumption = and {
     Quorum.forall(Q => Q.subseteq(Acceptor)),
-    tuples(Quorum, Quorum).forall((Q1, Q2) => (Q1.intersect(Q2)) != Set())
+    tuples(Quorum, Quorum).forall( ((Q1, Q2)) => (Q1.intersect(Q2)) != Set())
 }
 
 // theorems are not supported by Quint, use TLA+ syntax
@@ -111,18 +111,18 @@ THEOREM ChoosableThm ==
  */
 //-----------------------------------------------------------------------------
 val VotesSafe =
-    tuples(Acceptor, Ballot, Value).forall((a, b, v) =>
+    tuples(Acceptor, Ballot, Value).forall( ((a, b, v)) =>
                  VotedFor(a, b, v) implies SafeAt(b, v)
     )
 
 val OneVote =
-    tuples(Acceptor, Ballot, Value, Value).forall((a, b, v, w) =>
+    tuples(Acceptor, Ballot, Value, Value).forall( ((a, b, v, w)) =>
               VotedFor(a, b, v) and VotedFor(a, b, w) implies (v == w)
     )
 
 val OneValuePerBallot =
     tuples(Acceptor, Acceptor, Ballot, Value, Value)
-       .forall((a1, a2, b, v1, v2) =>
+       .forall( ((a1, a2, b, v1, v2)) =>
          VotedFor(a1, b, v1) and VotedFor(a2, b, v2) implies (v1 == v2)
        )
 //-----------------------------------------------------------------------------
@@ -148,7 +148,7 @@ def ShowsSafeAt(Q, b, v) = and {
 
 val ShowsSafety =
     all { TypeOK, VotesSafe, OneValuePerBallot } implies
-    tuples(Quorum, Ballot, Value).forall((Q, b, v) =>
+    tuples(Quorum, Ballot, Value).forall( ((Q, b, v)) =>
         ShowsSafeAt(Q, b, v) implies SafeAt(b, v)
     )
 

examples/cosmos/ics20/denomTrace.qnt

@@ -55,7 +55,7 @@ module denomTrace {
     and {
       // Check the domain for the second level of chains
       chainNames.forall(chain => topology.get(chain).keys() == chainNames),
-      tuples(chainNames, chainNames).forall((fromChain, toChain) =>
+      tuples(chainNames, chainNames).forall( ((fromChain, toChain)) =>
         fromChain != toChain implies // we dont care about channels from chain to itself
           chainNames.forall((thirdChain) =>
             thirdChain != toChain implies

examples/cosmos/lightclient/Blockchain.qnt

@@ -28,7 +28,7 @@ module Blockchain {
     // This is a simplified version of the Block data structure in the
     // actual implementation.
     pure def BlockHeaders = 
-        tuples(Heights, Int, Commits, powerset(AllNodes), powerset(AllNodes)).map((
+        tuples(Heights, Int, Commits, powerset(AllNodes), powerset(AllNodes)).map( ((
             // the block height
             height,
             // the block timestamp in some integer units
@@ -42,7 +42,7 @@ module Blockchain {
             VS,
             // the validators of the next block.
             // We store the next validators instead of the hash.
-            NextVS) => { 
+            NextVS)) => {
                 height: height, 
                 time: time,
                 lastCommit: lastCommit,
@@ -52,7 +52,7 @@ module Blockchain {
         )
 
     // A signed header is just a header together with a set of commits 
-    pure def LightBlocks = tuples(BlockHeaders, Commits).map((header, commits) => {header: header, Commits: commits})
+    pure def LightBlocks = tuples(BlockHeaders, Commits).map( ((header, commits)) => {header: header, Commits: commits})
 
     // Current global time in integer units as perceived by the reference chain
     var refClock: int

examples/cosmos/lightclient/LCVerificationApi.qnt

@@ -116,7 +116,7 @@ module LCVerificationApi {
     // Plugin bug: see issue #808. action -> pure def once resloved
     pure def LightStoreInv(fetchedLightBlocks: LightBlockMap, lightBlockStatus: LightBlockStatus): bool = {
         val domain = fetchedLightBlocks.keys()
-        tuples(domain, domain).forall((lh, rh) => or {
+        tuples(domain, domain).forall( ((lh, rh)) => or {
             // for every pair of stored headers that have been verified
             lh >= rh,
             lightBlockStatus.get(lh) != "StateVerified",

examples/cosmos/lightclient/Lightclient.qnt

@@ -358,7 +358,7 @@ module Lightclient {
     def StoredHeadersAreVerifiedInv: bool =
         state == "finishedSuccess" implies {
             val dom = fetchedLightBlocks.keys()
-            tuples(dom,dom).forall( (lh, rh) =>  or { // for every pair of different stored headers
+            tuples(dom,dom).forall( ((lh, rh)) =>  or { // for every pair of different stored headers
                 lh >= rh,
                 // either there is a header between them
                 dom.exists(mh => lh < mh and mh < rh),
@@ -381,7 +381,7 @@ module Lightclient {
     def StoredHeadersAreVerifiedOrNotTrustedInv: bool =
         state == "finishedSuccess" implies {
             val dom = fetchedLightBlocks.keys()
-            tuples(dom,dom).forall( (lh, rh) =>  or { // for every pair of different stored headers
+            tuples(dom,dom).forall( ((lh, rh)) =>  or { // for every pair of different stored headers
                 lh >= rh,
                 // either there is a header between them
                 dom.exists(mh => lh < mh and mh < rh),
@@ -404,7 +404,7 @@ module Lightclient {
     def ProofOfChainOfTrustInv: bool =
         state == "finishedSuccess" implies {
             val dom = fetchedLightBlocks.keys()
-            tuples(dom,dom).forall( (lh, rh) => or { // for every pair of stored headers that have been verified
+            tuples(dom,dom).forall( ((lh, rh)) => or { // for every pair of stored headers that have been verified
                 lh >= rh,
                 lightBlockStatus.get(lh) == "StateUnverified",
                 lightBlockStatus.get(rh) == "StateUnverified",

examples/cosmos/tendermint/Tendermint.qnt

@@ -160,7 +160,7 @@ module Tendermint {
   //********************* PROTOCOL INITIALIZATION ******************************
   def FaultyProposals(r) =
       tuples(Faulty, Values, RoundsOrNil)
-        .map((p, v, vr) =>
+        .map( ((p, v, vr)) =>
           { src: p, round: r, proposal: v, validRound: vr })
 
   val AllFaultyProposals =
@@ -169,15 +169,15 @@ module Tendermint {
 
   def FaultyPrevotes(r) =
       tuples(Faulty, Values)
-        .map((p, v) => { src: p, round: r, id: v })
+        .map( ((p, v)) => { src: p, round: r, id: v })
 
   val AllFaultyPrevotes =
       Rounds.map(r => FaultyPrevotes(r))
             .flatten()
 
   def FaultyPrecommits(r) =
       tuples(Faulty, Values)
-        .map((p, v) => { src: p, round: r, id: v })
+        .map( ((p, v)) => { src: p, round: r, id: v })
 
   val AllFaultyPrecommits =
       Rounds.map(r => FaultyPrecommits(r))
@@ -535,7 +535,7 @@ module Tendermint {
 
   //**************************** FORK SCENARIOS  ***************************
   def EquivocationIn(p, S) =
-    tuples(S, S).exists((m1, m2) =>
+    tuples(S, S).exists( ((m1, m2)) =>
       and {
         m1 != m2,
         m1.src == p,
@@ -554,7 +554,7 @@ module Tendermint {
 
   // amnesic behavior by a process p
   def AmnesiaBy(p) =
-      tuples(Rounds, Rounds).exists((r1, r2) =>
+      tuples(Rounds, Rounds).exists( ((r1, r2)) =>
           and {
             r1 < r2,
             tuples(ValidValues, ValidValues).exists(vs =>
@@ -585,7 +585,7 @@ module Tendermint {
 
   // the safety property -- agreement
   val Agreement =
-    tuples(Corr, Corr).forall((p, q) =>
+    tuples(Corr, Corr).forall( ((p, q)) =>
       or {
         decision.get(p) == NilValue,
         decision.get(q) == NilValue,
@@ -626,7 +626,7 @@ module Tendermint {
   // It is not exactly ~Agreement, as we do not want to see the states where
   // decision.get(p) = NilValue
   val NoAgreement =
-    tuples(Corr, Corr).forall((p, q) =>
+    tuples(Corr, Corr).forall( ((p, q)) =>
       and {
         p != q,
         decision.get(p) != NilValue,

examples/language-features/tuples.qnt

@@ -9,11 +9,8 @@ module tuples {
   action step = myTup' = combineTuples(myTup, (1, "world"))
 
   // Unpacking
-  var x: int
-
-  def a(tup) = Set(tup, (x, 4)).map((p, g) => p + g)
-  def b(tup, f) = Set(tup, (x, 4)).map(f)
-  pure def c(tup, f) = Set(tup).map(f)
-  pure def func(p, g) = p
-  pure val test = c((1, 2), func)
+  pure val a = Set((1, 4), (2, 3)).map( ((p, g)) => p + g)
+  pure val s = Set(1, 2, 3)
+  pure val m = tuples(s, s).mapBy( ((j, k)) => j+k )
+  pure val n = tuples(s, s, s).mapBy( ((j, k, i)) => j+k+i )
 }

quint/src/effects/base.ts

@@ -227,7 +227,7 @@ function unifyArrows(location: string, e1: ArrowEffect, e2: ArrowEffect): Either
       if (p1.length === p2.length) {
         return right([p1, p2, [] as Substitutions])
       } else {
-        return tryToUnpack(location, p1, p2)
+        return left(buildErrorLeaf(location, `Expected ${p1.length} arguments, got ${p2.length}`))
       }
     })
     .chain(([p1, p2, unpackingSubs]) => {
@@ -374,78 +374,6 @@ function applySubstitutionsAndUnify(subs: Substitutions, e1: Effect, e2: Effect)
     .chain(newSubstitutions => compose(newSubstitutions, subs))
 }
 
-function tryToUnpack(
-  location: string,
-  effects1: Effect[],
-  effects2: Effect[]
-): Either<ErrorTree, [Effect[], Effect[], Substitutions]> {
-  // Ensure that effects1 is always the smallest
-  if (effects2.length < effects1.length) {
-    return tryToUnpack(location, effects2, effects1)
-  }
-
-  // We only handle unpacking 1 tuple into N args
-  if (effects1.length !== 1) {
-    return left(buildErrorLeaf(location, `Expected ${effects2.length} arguments, got ${effects1.length}`))
-  }
-
-  const entitiesByComponentKind: Map<ComponentKind, Entity[]> = new Map()
-
-  // Combine the other effects into a single effect, to be unified with the unpacked effect
-
-  // If all the effects are concrete, we combine them into a single concrete
-  // effect by combining the entities of each component of the same kind
-  if (effects2.every(e => e.kind === 'concrete')) {
-    effects2.forEach(e => {
-      if (e.kind === 'concrete') {
-        e.components.forEach(c => {
-          const entities = entitiesByComponentKind.get(c.kind) ?? []
-          entities.push(c.entity)
-          entitiesByComponentKind.set(c.kind, entities)
-        })
-      }
-    })
-
-    const unpacked: ConcreteEffect = {
-      kind: 'concrete',
-      components: [...entitiesByComponentKind.entries()].map(([kind, entities]) => {
-        return { kind, entity: { kind: 'union', entities: entities } }
-      }),
-    }
-
-    const result = simplify(unpacked)
-    return right([effects1, [result], []])
-  }
-
-  // If all the effects are variable like e0, ..., en, we combine them into a
-  // single variable effect called e0#...#en. See simplifyArrowEffect for a
-  // similar process description
-  if (effects2.every(e => e.kind === 'variable')) {
-    const names = effects2.map(e => (e.kind === 'variable' ? e.name : ''))
-
-    const unpacked: Effect = {
-      kind: 'variable',
-      name: names.join('#'),
-    }
-
-    const subs: Substitutions = names.map(name => ({
-      kind: 'effect',
-      name,
-      value: unpacked,
-    }))
-    const result = simplify(unpacked)
-
-    return right([effects1, [result], subs])
-  }
-
-  return left(
-    buildErrorLeaf(
-      `Trying to unpack effects: ${effects1.map(effectToString)} and ${effects2.map(effectToString)}`,
-      'Can only unpack effects if they are all concrete or all variable'
-    )
-  )
-}
-
 /**
  * Simplifies effects of the form (Read[v0, ..., vn]) => Read[v0, ..., vn] into
  * (Read[v0#...#vn]) => Read[v0#...#vn] so the entities can be unified with other