author | wenzelm |
Mon, 02 Dec 2024 14:08:28 +0100 | |
changeset 81537 | d230683a35fc |
parent 80885 | 42ab8c52067e |
permissions | -rw-r--r-- |
59136 | 1 |
/* Title: Pure/Concurrent/par_list.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Parallel list combinators. |
|
5 |
*/ |
|
6 |
||
7 |
||
8 |
package isabelle |
|
9 |
||
10 |
||
75393 | 11 |
object Par_List { |
12 |
def managed_results[A, B]( |
|
13 |
f: A => B, |
|
14 |
xs: List[A], |
|
78429 | 15 |
sequential: Boolean = false, |
16 |
thread: Boolean = false |
|
75393 | 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 | 19 |
else { |
61590 | 20 |
val state = Synchronized[(List[Future[B]], Boolean)]((Nil, false)) |
59136 | 21 |
|
22 |
def cancel_other(self: Int = -1): Unit = |
|
61562 | 23 |
state.change { case (futures, canceled) => |
59136 | 24 |
if (!canceled) { |
61562 | 25 |
for ((future, i) <- futures.iterator.zipWithIndex if i != self) |
73367 | 26 |
future.cancel() |
59136 | 27 |
} |
61562 | 28 |
(futures, true) |
59136 | 29 |
} |
30 |
||
31 |
try { |
|
32 |
state.change(_ => |
|
33 |
(xs.iterator.zipWithIndex.map({ case (x, self) => |
|
78429 | 34 |
def run = |
61562 | 35 |
Exn.capture { f(x) } match { |
36 |
case Exn.Exn(exn) => cancel_other(self); throw exn |
|
37 |
case Exn.Res(res) => res |
|
38 |
} |
|
78429 | 39 |
if (thread) Future.thread("Par_List.managed_results") { run } |
40 |
else Future.fork { run } |
|
59136 | 41 |
}).toList, false)) |
42 |
||
61562 | 43 |
state.value._1.map(_.join_result) |
59136 | 44 |
} |
45 |
finally { cancel_other() } |
|
46 |
} |
|
73512
e52a9b208481
support sequential LaTeX jobs: more robust when TeX installation is self-installing packages etc.;
wenzelm
parents:
73367
diff
changeset
|
47 |
} |
59136 | 48 |
|
80885 | 49 |
def map[A, B](f: A => B, list: List[A], |
78429 | 50 |
sequential: Boolean = false, |
51 |
thread: Boolean = false |
|
52 |
): List[B] = { |
|
80885 | 53 |
Exn.release_first(managed_results(f, list, sequential = sequential, thread = thread)) |
78429 | 54 |
} |
59136 | 55 |
|
80885 | 56 |
def maps[A, B](f: A => Iterable[B], list: List[A], |
57 |
sequential: Boolean = false, |
|
58 |
thread: Boolean = false |
|
59 |
): List[B] = map(f, list, sequential = sequential, thread = thread).flatten |
|
60 |
||
76538 | 61 |
private class Found(val res: Any) extends Exception |
62 |
||
75393 | 63 |
def get_some[A, B](f: A => Option[B], xs: List[A]): Option[B] = { |
59136 | 64 |
val results = |
65 |
managed_results( |
|
66 |
(x: A) => f(x) match { case None => () case Some(y) => throw new Found(y) }, xs) |
|
76537 | 67 |
results.collectFirst({ |
76538 | 68 |
case Exn.Exn(found) if found.isInstanceOf[Found] => |
69 |
found.asInstanceOf[Found].res.asInstanceOf[B] |
|
76537 | 70 |
}) match { |
59136 | 71 |
case None => Exn.release_first(results); None |
72 |
case some => some |
|
73 |
} |
|
74 |
} |
|
75 |
||
76 |
def find_some[A](P: A => Boolean, xs: List[A]): Option[A] = |
|
77 |
get_some((x: A) => if (P(x)) Some(x) else None, xs) |
|
78 |
||
59137 | 79 |
def exists[A](P: A => Boolean, xs: List[A]): Boolean = find_some(P, xs).isDefined |
59136 | 80 |
def forall[A](P: A => Boolean, xs: List[A]): Boolean = !exists((x: A) => !P(x), xs) |
81 |
} |