Merge branch 'main' into th/rfc-manage-apalache

CHANGELOG.md

@@ -11,6 +11,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ### Changed
 ### Deprecated
 ### Removed
+
+- The long deprecated union types have been removed, in favor of the new sum
+  types (#1245).
+
 ### Fixed
 ### Security
 

README.md

@@ -75,6 +75,7 @@ Visit the [Tutorials][] page.
 - [Cheatsheet](./doc/quint-cheatsheet.pdf)
 - [Reference API documentation for built-in operators](./doc/builtin.md)
 - [Syntax documentation](./doc/lang.md)
+- [Frequently asked questions](./doc/faq.md)
 
 ### Examples :musical_score:
 

doc/faq.md

@@ -0,0 +1,106 @@
+# Frequently Asked Questions
+
+Here you can find answers to the questions that are often asked by people who
+would like to start with Quint.
+
+### What are spells?
+
+Spells are simply Quint modules that contain often-used definitions. There is
+nothing special about these definitions. They are probably a bit more
+thought-out than a definition someone would write on the spot. Check the page
+on [Spells][].
+
+### Difference between `pure def` and `def`
+
+Definitions that are tagged as `pure def` are not allowed to read state
+variables (that is, the names declared with `var`). Definitions that are tagged
+with `def` are allowed to read state variables, though they do not have to.
+
+Pure definitions have the following important property: A **pure definition
+always returns the same result for the same parameter values**.
+
+Consider the following operator definition:
+
+```bluespec
+pure def min(x, y) = if (x < y) x else y
+```
+
+Whenever we call `min(2, 3)`, we get `2` as a result, no matter what the values of state variables are.
+
+Impure definitions have the following important property:
+**An impure definition may produce different results for the same parameter
+values**. An impure definition **may read** the values of state variables, which
+may effect in different results.
+
+Consider the following definitions:
+
+```bluespec
+var limit: int
+
+def minWithLimit(x, y) = min(min(x, y), limit)
+```
+
+In the above example, `minWithLimit(10, 20)` produces the value `10`, when
+`limit == 100`, whereas `minWithLimit(10, 20)` produces the value `5`, when
+`limit == 5`.
+
+### Difference between `val` and `def`
+
+The definitions that have at least one parameter should be tagged with `def`,
+whereas the definitions that have no parameters should be tagged with `val`. We
+could say that `val`'s are nullary `def`'s.
+
+As a result, a `pure val` is never changing its value in an execution. For example:
+
+```bluespec
+pure val avogadro = 602214076^(23 - 8)
+```
+
+Note that an impure `val` may still depend on the value of a state variable.
+For example:
+
+```bluespec
+var time: int
+var velocity: int
+
+val distance = velocity * time
+```
+
+In the above example, `distance` does not need any parameters, as it only
+depends on the state variables. However, the value of `distance` is still
+changing with the values of `time` and `velocity`.
+
+### Difference between `pure val` and `const`
+
+A value that is defined via `pure val` is constant in the sense that it never
+changes in an execution. A `const` definition also declares a constant value.
+However, the value of `const` is not fixed at the time of specification writing,
+but it has to be fixed by instantiating the module.  
+
+Here is an example that illustrates the difference between `pure val` and `const`:
+
+```bluespec
+module fixed {
+  // this module is written for N=4, e.g., for N processes
+  pure val N = 4
+
+  pure val procs = 1.to(N)
+  // etc.
+}
+
+module parameterized {
+  // this module is written for a parameter N
+  const N: int
+
+  pure val procs = 1.to(N)
+  // etc.
+}
+
+module instance4 {
+  import parameterized(N = 4) as I
+
+  pure val procs = 1.to(I::N)
+}
+```
+
+[Spells]: https://github.com/informalsystems/quint/tree/main/examples/spells

doc/lang.md

@@ -51,8 +51,8 @@ Table of Contents
       * [Other set operators](#other-set-operators)
     * [Maps (aka Functions)](#maps-aka-functions)
     * [Records](#records)
-    * [Discriminated unions](#discriminated-unions)
     * [Tuples](#tuples)
+    * [Sum Types](#sum-types)
     * [Lists (aka Sequences)](#lists-aka-sequences)
     * [Integers](#integers)
     * [Nested operator definitions](#nested-operator-definitions)
@@ -142,8 +142,7 @@ expressions).
 
 ### Type System 1.2
 
-This is the same type system as in Apalache, except we have added discriminated
-unions:
+This is the same type system as in Apalache:
 
 A type is one of the following:
 
@@ -167,13 +166,8 @@ A type is one of the following:
  - Operator: `(T_1, ..., T_n) => R` for `n >= 0` argument types `T_1, ..., T_n`
    and result type `R`.
 
- - **Work in progress:** Discriminated union:
-    ```
-       | { tag: string_1, <ident>: T_1_1, ..., <ident>: T_1_n_1}
-       ...
-       | { tag: string_k, <ident>: T_k_1, ..., <ident>: T_k_n_k}
-    ```
-    for `n >= 1` types `T_1_1`, ..., `T_k_n_k`.
+ - Sum Types: `type T = L_1(T_1) | ... | L_n(T_n) ` for `n >= 1`, argument types
+   `T_1`, ..., `T_n`, and a type alais `T`.
 
  - Type in parentheses: `(T)` for a type `T`.
 
@@ -1290,8 +1284,7 @@ with(r, "f", e)
 Note that we are using the syntax `{ name_1: value_1, ..., name_n: value_n }`
 for records, similar to Python and JavaScript. We have removed the syntax for
 sets of records: (1) It often confuses beginners, (2) It can be expressed with
-`map` and a record constructor. Moreover, sets of records do not combine well
-with discriminated unions.
+`map` and a record constructor.
 
 *Mode:* Stateless, State. Other modes are not allowed.
 
@@ -1326,6 +1319,46 @@ of items.
 
 *Mode:* Stateless, State. Other modes are not allowed.
 
+### Sum Types
+
+Exclusive disjunction of different possible data types is expressed via sum
+types, also known as tagged unions, discriminated unions, or variants. TLA+,
+being untyped, doesn't have a strict correlate, but it is common to use records
+with a discriminator field for this purpose.
+
+```scala
+// Declaration
+type T = L_1(T_1) | ... | L_n(T_n)
+// variant constructor
+// where
+//  - 1 =< k <= n for the declared sum type's variants L_1(T_1) | ... | L_n(T_n)
+//  - x : T_k
+L_k(x)
+variant("L_k", x)
+// variant eliminator: "match expression"
+// where 
+//  - x_1 : T_1, ..., x_n : T_n
+//  - e_1 : S, ..., e_n : S, and S will be the resulting type of the expression
+match L_k(x) {
+  | L_1(x_1) => e_1
+  | ...
+  | L_n(x_n) => e_n
+}
+matchVariant(L_k(x), "L_1", (x_1) => e_1, ..., (x_n) => e_n)
+```
+
+E.g., to form and operate on a heterogeneous set containing both integer and
+string values, you might find:
+
+```scala
+type Elem = S(str) | I(int)
+val mySet: Set[Elem] =  Set(S("Foo"), I(1), S("Bar"), I(2))
+val transformMySet: Set[Str] = mySet.map(e => match e { S(s) => s | I(_) => "An int"})
+```
+
+*Mode:* Stateless, State. Other modes are not allowed.
+
+
 ### Lists (aka Sequences)
 
 In contrast to TLA+, there is no special module for lists. They are built

examples/classic/distributed/Paxos/Paxos.qnt

@@ -34,15 +34,41 @@ module Paxos {
   var maxVal:   str -> int  // ballot number cast by a; it equals <<-1, None>> if
                             // a has not cast any vote.
 
-  // A union type for records representing messages.
+  // Particular message types we need to refer to later:
+  type Msg1bT = { acceptor: str, bal: int, mbal: int, mval: int }
+  type Msg2aT = { bal: int, value: int }
+
+  // A union type for records representing different types of messages.
   type MSG =
-      | { tag: "1a", bal: int }
-      | { tag: "1b", acceptor: str, bal: int, mbal: int, mval: int }
-      | { tag: "2a", bal: int, value: int }
-      | { tag: "2b", acc: str, bal: int, value: int }
+      | Msg1a({ bal: int })
+      | Msg1b(Msg1bT)
+      | Msg2a(Msg2aT)
+      | Msg2b({ acc: str, bal: int, value: int })
 
   var msgs: Set[MSG] // The set of all messages that have been sent.
 
+  // Access the balance of a message, irrespictive of the message variant
+  def balance(m: MSG): int = match m {
+    | Msg1a(mm) => mm.bal
+    | Msg1b(mm) => mm.bal
+    | Msg2a(mm) => mm.bal
+    | Msg2b(mm) => mm.bal
+  }
+
+  // Filter a set of messager into just 1b messages
+  def filterMsg1b(ms: Set[MSG]): Set[Msg1bT] =
+    ms.fold(Set(), (acc, m) => match m {
+      | Msg1b(m1b) => acc.union(Set(m1b))
+      | _          => acc
+    })
+
+  // Filter a set of messager into just 2a messages
+  def filterMsg2a(ms: Set[MSG]): Set[Msg2aT] =
+    ms.fold(Set(), (acc, m) => match m {
+      | Msg2a(m2a) => acc.union(Set(m2a))
+      | _          => acc
+    })
+
   /***************************************************************************)
   (* NOTE:                                                                   *)
   (* The algorithm is easier to understand in terms of the set msgs of all   *)
@@ -87,7 +113,7 @@ module Paxos {
   (* The actions.  We begin with the subaction (an action that will be used  *)
   (* to define the actions that make up the next-state action.               *)
   (***************************************************************************/
-  action Send(m) = {
+  action Send(m: MSG): bool = {
       msgs' = msgs.union(Set(m))
   }
 
@@ -98,7 +124,7 @@ module Paxos {
   (* m with m.type = "1a") that begins ballot b.                             *)
   (***************************************************************************/
   action Phase1a(b) = all {
-      Send({ tag: "1a", bal: b }),
+      Send(Msg1a({ bal: b })),
       maxVBal' = maxVBal,
       maxVal'  = maxVal,
   }
@@ -110,12 +136,11 @@ module Paxos {
   (* maxVBal[a] and maxVal[a].                                               *)
   (***************************************************************************/
   action Phase1b(a) = {
-      nondet m = msgs.filter(m2 => m2.tag == "1a").oneOf()
+      nondet m = msgs.filter(m2 => match m2 { Msg1a(_) => true | _ => false }).oneOf()
       all {
-          m.bal > maxBal.get(a),
-          Send({ tag: "1b", acc: a, bal: m.bal,
-                   mbal: maxVBal.get(a), mval: maxVal.get(a) }),
-          maxBal' = maxBal.set(a, m.bal),
+          m.balance() > maxBal.get(a),
+          Send(Msg1b({ acceptor: a, bal: m.balance(), mbal: maxVBal.get(a), mval: maxVal.get(a) })),
+          maxBal' = maxBal.set(a, m.balance()),
           maxVBal' = maxVBal,
           maxVal'  = maxVal,
       }
@@ -142,14 +167,13 @@ module Paxos {
   (* greater than b (thereby promising not to vote in ballot b).             *)
   (***************************************************************************/
   action Phase2a(b, v) = all {
-    not(msgs.filter(m => m.tag == "2a")
-            .exists(m => m.bal == b)),
+    not(msgs.exists(m => match m { Msg2a(m2a) => m2a.bal == b | _ => false })),
     Quorum.exists(Q =>
-      val Q1b = msgs.filter(m => m.tag == "1b")
-                    .filter(m => (m.acc.in(Q)) and (m.bal == b))
+      val Q1b = msgs.filterMsg1b()
+                    .filter(m => (m.acceptor.in(Q)) and (m.bal == b))
       val Q1bv = Q1b.filter(m => m.mbal >= 0)
       and {
-          Q.forall(a => Q1b.exists(m => m.acc == a)),
+          Q.forall(a => Q1b.exists(m => m.acceptor == a)),
           or {
               Q1bv == Set(),
               Q1bv.exists(m => or {
@@ -159,7 +183,7 @@ module Paxos {
           }
       }
     ),
-    Send({ tag: "2a", bal: b, value: v }),
+    Send(Msg2a({ bal: b, value: v })),
     maxVBal' = maxVBal,
     maxVal'  = maxVal,
   }
@@ -174,10 +198,10 @@ module Paxos {
   (* message's.  ballot number                                               *)
   (***************************************************************************/
   action Phase2b(a) = {
-    nondet m = msgs.filter(m2 => m2.tag == "2a").oneOf()
+    nondet m = msgs.filterMsg2a().oneOf()
     all {
       m.bal >= maxBal.get(a),
-      Send({ tag: "2b", acc: a, bal: m.bal, value: m.value }),
+      Send(Msg2b({ acc: a, bal: m.bal, value: m.value })),
       maxBal'  = maxBal.set(a, m.bal),
       maxVBal' = maxVBal.set(a, m.bal),
       maxVal'  = maxVal.set(a, m.value),
@@ -221,11 +245,13 @@ module Paxos {
   (* the array `votes' describing the votes cast by the acceptors is defined *)
   (* as follows.                                                             *)
   (***************************************************************************/
-  val votes = Acceptor.mapBy( a =>
-             msgs.filter(mm => mm.tag == "2b")
-                 .filter(mm => mm.acc == a)
-                 .map(m => (m.bal, m.value))
-  )
+  val votes =
+    Acceptor.mapBy(a =>
+      msgs.fold(Set(), (acc, mm) =>
+        match mm {
+        | Msg2b(m) => if (m.acc == a) acc.union(Set((m.bal, m.value))) else acc
+        | _ => acc }))
+
   /***************************************************************************)
   (* We now instantiate module Voting, substituting the constants Value,     *)
   (* Acceptor, and Quorum declared in this module for the corresponding      *)
@@ -251,11 +277,11 @@ module Paxos {
          maxVal.get(a) == None
          else (maxVBal.get(a), maxVal.get(a)).in(votes.get(a))
      ),
-     msgs.filter(m => m.tag == "1b")
+     msgs.filterMsg1b()
          .forall(m =>
-            (maxBal.get(m.acc) >= m.bal
-                and ((m.mbal >= 0) implies (m.mbal, m.mval).in(votes.get(m.acc))))),
-     val M2as = msgs.filter( m => m.tag == "2a" )
+            (maxBal.get(m.acceptor) >= m.bal
+                and ((m.mbal >= 0) implies (m.mbal, m.mval).in(votes.get(m.acceptor))))),
+     val M2as = msgs.filterMsg2a()
      M2as.forall(m => and {
         Quorum.exists(Q => V::ShowsSafeAt(Q, m.bal, m.value)),
         M2as.forall(mm =>