src/Pure/Concurrent/par_list.scala
author wenzelm
Mon, 02 Dec 2024 14:08:28 +0100
changeset 81537 d230683a35fc
parent 80885 42ab8c52067e
permissions -rw-r--r--
more direct Proof_Context.lookup_free -- bypass redundancy of Proof_Context.check_const;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
59136
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Concurrent/par_list.scala
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
     3
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
     4
Parallel list combinators.
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
     5
*/
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
     6
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
     7
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
     8
package isabelle
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
     9
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
    10
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73512
diff changeset
    11
object Par_List {
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73512
diff changeset
    12
  def managed_results[A, B](
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73512
diff changeset
    13
    f: A => B,
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73512
diff changeset
    14
    xs: List[A],
78429
103a81e60126 tuned signature: more options;
wenzelm
parents: 76538
diff changeset
    15
    sequential: Boolean = false,
103a81e60126 tuned signature: more options;
wenzelm
parents: 76538
diff changeset
    16
    thread: Boolean = false
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73512
diff changeset
    17
  ) : List[Exn.Result[B]] = {
73512
e52a9b208481 support sequential LaTeX jobs: more robust when TeX installation is self-installing packages etc.;
wenzelm
parents: 73367
diff changeset
    18
    if (sequential || xs.isEmpty || xs.tail.isEmpty) xs.map(x => Exn.capture { f(x) })
59136
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
    19
    else {
61590
wenzelm
parents: 61562
diff changeset
    20
      val state = Synchronized[(List[Future[B]], Boolean)]((Nil, false))
59136
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
    21
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
    22
      def cancel_other(self: Int = -1): Unit =
61562
264c7488d532 prefer Isabelle/Scala Future;
wenzelm
parents: 61556
diff changeset
    23
        state.change { case (futures, canceled) =>
59136
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
    24
          if (!canceled) {
61562
264c7488d532 prefer Isabelle/Scala Future;
wenzelm
parents: 61556
diff changeset
    25
            for ((future, i) <- futures.iterator.zipWithIndex if i != self)
73367
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 61590
diff changeset
    26
              future.cancel()
59136
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
    27
          }
61562
264c7488d532 prefer Isabelle/Scala Future;
wenzelm
parents: 61556
diff changeset
    28
          (futures, true)
59136
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
    29
        }
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
    30
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
    31
      try {
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
    32
        state.change(_ =>
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
    33
          (xs.iterator.zipWithIndex.map({ case (x, self) =>
78429
103a81e60126 tuned signature: more options;
wenzelm
parents: 76538
diff changeset
    34
            def run =
61562
264c7488d532 prefer Isabelle/Scala Future;
wenzelm
parents: 61556
diff changeset
    35
              Exn.capture { f(x) } match {
264c7488d532 prefer Isabelle/Scala Future;
wenzelm
parents: 61556
diff changeset
    36
                case Exn.Exn(exn) => cancel_other(self); throw exn
264c7488d532 prefer Isabelle/Scala Future;
wenzelm
parents: 61556
diff changeset
    37
                case Exn.Res(res) => res
264c7488d532 prefer Isabelle/Scala Future;
wenzelm
parents: 61556
diff changeset
    38
              }
78429
103a81e60126 tuned signature: more options;
wenzelm
parents: 76538
diff changeset
    39
            if (thread) Future.thread("Par_List.managed_results") { run }
103a81e60126 tuned signature: more options;
wenzelm
parents: 76538
diff changeset
    40
            else Future.fork { run }
59136
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
    41
          }).toList, false))
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
    42
61562
264c7488d532 prefer Isabelle/Scala Future;
wenzelm
parents: 61556
diff changeset
    43
        state.value._1.map(_.join_result)
59136
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
    44
      }
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
    45
      finally { cancel_other() }
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
    46
    }
73512
e52a9b208481 support sequential LaTeX jobs: more robust when TeX installation is self-installing packages etc.;
wenzelm
parents: 73367
diff changeset
    47
  }
59136
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
    48
80885
42ab8c52067e clarified signature;
wenzelm
parents: 78429
diff changeset
    49
  def map[A, B](f: A => B, list: List[A],
78429
103a81e60126 tuned signature: more options;
wenzelm
parents: 76538
diff changeset
    50
    sequential: Boolean = false,
103a81e60126 tuned signature: more options;
wenzelm
parents: 76538
diff changeset
    51
    thread: Boolean = false
103a81e60126 tuned signature: more options;
wenzelm
parents: 76538
diff changeset
    52
  ): List[B] = {
80885
42ab8c52067e clarified signature;
wenzelm
parents: 78429
diff changeset
    53
    Exn.release_first(managed_results(f, list, sequential = sequential, thread = thread))
78429
103a81e60126 tuned signature: more options;
wenzelm
parents: 76538
diff changeset
    54
  }
59136
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
    55
80885
42ab8c52067e clarified signature;
wenzelm
parents: 78429
diff changeset
    56
  def maps[A, B](f: A => Iterable[B], list: List[A],
42ab8c52067e clarified signature;
wenzelm
parents: 78429
diff changeset
    57
    sequential: Boolean = false,
42ab8c52067e clarified signature;
wenzelm
parents: 78429
diff changeset
    58
    thread: Boolean = false
42ab8c52067e clarified signature;
wenzelm
parents: 78429
diff changeset
    59
  ): List[B] = map(f, list, sequential = sequential, thread = thread).flatten
42ab8c52067e clarified signature;
wenzelm
parents: 78429
diff changeset
    60
76538
0bab4c751478 clarified exception: avoid odd compiler warning;
wenzelm
parents: 76537
diff changeset
    61
  private class Found(val res: Any) extends Exception
0bab4c751478 clarified exception: avoid odd compiler warning;
wenzelm
parents: 76537
diff changeset
    62
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73512
diff changeset
    63
  def get_some[A, B](f: A => Option[B], xs: List[A]): Option[B] = {
59136
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
    64
    val results =
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
    65
      managed_results(
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
    66
        (x: A) => f(x) match { case None => () case Some(y) => throw new Found(y) }, xs)
76537
cdbe20024038 update to scala-3.2.1;
wenzelm
parents: 75393
diff changeset
    67
    results.collectFirst({
76538
0bab4c751478 clarified exception: avoid odd compiler warning;
wenzelm
parents: 76537
diff changeset
    68
      case Exn.Exn(found) if found.isInstanceOf[Found] =>
0bab4c751478 clarified exception: avoid odd compiler warning;
wenzelm
parents: 76537
diff changeset
    69
        found.asInstanceOf[Found].res.asInstanceOf[B]
76537
cdbe20024038 update to scala-3.2.1;
wenzelm
parents: 75393
diff changeset
    70
    }) match {
59136
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
    71
      case None => Exn.release_first(results); None
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
    72
      case some => some
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
    73
    }
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
    74
  }
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
    75
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
    76
  def find_some[A](P: A => Boolean, xs: List[A]): Option[A] =
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
    77
    get_some((x: A) => if (P(x)) Some(x) else None, xs)
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
    78
59137
wenzelm
parents: 59136
diff changeset
    79
  def exists[A](P: A => Boolean, xs: List[A]): Boolean = find_some(P, xs).isDefined
59136
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
    80
  def forall[A](P: A => Boolean, xs: List[A]): Boolean = !exists((x: A) => !P(x), xs)
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
diff changeset
    81
}