src/Pure/Concurrent/counter.scala
author wenzelm
Mon, 29 Aug 2022 19:26:27 +0200
changeset 76019 f3d8da992445
parent 75393 87ebf5a50283
child 78243 0e221a8128e4
permissions -rw-r--r--
provide cvc5-1.0.2 (inactive);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43660
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Concurrent/counter.scala
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
     3
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
     4
Synchronized counter for unique identifiers < 0.
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
     5
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
     6
NB: ML ticks forwards, JVM ticks backwards.
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
     7
*/
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
     8
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
     9
package isabelle
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
    10
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
    11
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73120
diff changeset
    12
object Counter {
43660
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
    13
  type ID = Long
52537
4b5941730bd8 more uniform Counter in ML and Scala;
wenzelm
parents: 46712
diff changeset
    14
  def make(): Counter = new Counter
43660
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
    15
}
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
    16
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73120
diff changeset
    17
final class Counter private {
43660
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
    18
  private var count: Counter.ID = 0
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
    19
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
    20
  def apply(): Counter.ID = synchronized {
73120
c3589f2dff31 more informative errors: simplify diagnosis of spurious failures reported by users;
wenzelm
parents: 64443
diff changeset
    21
    require(count > java.lang.Long.MIN_VALUE, "counter overflow")
43660
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
    22
    count -= 1
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
    23
    count
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
    24
  }
56685
535d59d4ed12 more uniform synchronized variables;
wenzelm
parents: 52537
diff changeset
    25
535d59d4ed12 more uniform synchronized variables;
wenzelm
parents: 52537
diff changeset
    26
  override def toString: String = count.toString
43660
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
    27
}