author | wenzelm |
Wed, 23 Apr 2014 15:57:06 +0200 | |
changeset 56674 | 70cc1164fb83 |
parent 56673 | 42bf8fffdf6a |
child 56731 | 326e8a7ea287 |
permissions | -rw-r--r-- |
34217 | 1 |
/* Title: Pure/Concurrent/future.scala |
45673
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
wenzelm
parents:
45667
diff
changeset
|
2 |
Module: PIDE |
34217 | 3 |
Author: Makarius |
4 |
||
56673
42bf8fffdf6a
modernized Future/Promise implementation, bypassing old actors;
wenzelm
parents:
56663
diff
changeset
|
5 |
Value-oriented parallelism via futures and promises in Scala -- with |
42bf8fffdf6a
modernized Future/Promise implementation, bypassing old actors;
wenzelm
parents:
56663
diff
changeset
|
6 |
signatures as in Isabelle/ML. |
34217 | 7 |
*/ |
8 |
||
9 |
package isabelle |
|
10 |
||
11 |
||
56673
42bf8fffdf6a
modernized Future/Promise implementation, bypassing old actors;
wenzelm
parents:
56663
diff
changeset
|
12 |
import scala.util.{Success, Failure} |
42bf8fffdf6a
modernized Future/Promise implementation, bypassing old actors;
wenzelm
parents:
56663
diff
changeset
|
13 |
import scala.concurrent.{Future => Scala_Future, Promise => Scala_Promise, Await} |
42bf8fffdf6a
modernized Future/Promise implementation, bypassing old actors;
wenzelm
parents:
56663
diff
changeset
|
14 |
import scala.concurrent.duration.Duration |
42bf8fffdf6a
modernized Future/Promise implementation, bypassing old actors;
wenzelm
parents:
56663
diff
changeset
|
15 |
import scala.concurrent.ExecutionContext.Implicits.global |
34217 | 16 |
|
17 |
||
18 |
object Future |
|
19 |
{ |
|
20 |
def value[A](x: A): Future[A] = new Finished_Future(x) |
|
56673
42bf8fffdf6a
modernized Future/Promise implementation, bypassing old actors;
wenzelm
parents:
56663
diff
changeset
|
21 |
def fork[A](body: => A): Future[A] = new Pending_Future(Scala_Future[A](body)) |
42bf8fffdf6a
modernized Future/Promise implementation, bypassing old actors;
wenzelm
parents:
56663
diff
changeset
|
22 |
def promise[A]: Promise[A] = new Promise_Future[A](Scala_Promise[A]) |
34217 | 23 |
} |
24 |
||
56673
42bf8fffdf6a
modernized Future/Promise implementation, bypassing old actors;
wenzelm
parents:
56663
diff
changeset
|
25 |
trait Future[A] |
34217 | 26 |
{ |
27 |
def peek: Option[Exn.Result[A]] |
|
28 |
def is_finished: Boolean = peek.isDefined |
|
38848
9483bb678d96
use Future.get_finished where this is the intended meaning -- prefer immediate crash over deadlock due to promises that are never fulfilled;
wenzelm
parents:
34262
diff
changeset
|
29 |
def get_finished: A = { require(is_finished); Exn.release(peek.get) } |
34217 | 30 |
def join: A |
31 |
def map[B](f: A => B): Future[B] = Future.fork { f(join) } |
|
32 |
||
33 |
override def toString = |
|
34 |
peek match { |
|
35 |
case None => "<future>" |
|
36 |
case Some(Exn.Exn(_)) => "<failed>" |
|
37 |
case Some(Exn.Res(x)) => x.toString |
|
38 |
} |
|
39 |
} |
|
40 |
||
56673
42bf8fffdf6a
modernized Future/Promise implementation, bypassing old actors;
wenzelm
parents:
56663
diff
changeset
|
41 |
trait Promise[A] extends Future[A] |
34240
3274571e45c1
added Future.promise -- essentially a single-assignment variable with signalling, using the Future interface;
wenzelm
parents:
34217
diff
changeset
|
42 |
{ |
34262 | 43 |
def fulfill_result(res: Exn.Result[A]): Unit |
56674 | 44 |
def fulfill(x: A): Unit |
34240
3274571e45c1
added Future.promise -- essentially a single-assignment variable with signalling, using the Future interface;
wenzelm
parents:
34217
diff
changeset
|
45 |
} |
3274571e45c1
added Future.promise -- essentially a single-assignment variable with signalling, using the Future interface;
wenzelm
parents:
34217
diff
changeset
|
46 |
|
56673
42bf8fffdf6a
modernized Future/Promise implementation, bypassing old actors;
wenzelm
parents:
56663
diff
changeset
|
47 |
|
34217 | 48 |
private class Finished_Future[A](x: A) extends Future[A] |
49 |
{ |
|
50 |
val peek: Option[Exn.Result[A]] = Some(Exn.Res(x)) |
|
51 |
val join: A = x |
|
52 |
} |
|
53 |
||
56673
42bf8fffdf6a
modernized Future/Promise implementation, bypassing old actors;
wenzelm
parents:
56663
diff
changeset
|
54 |
private class Pending_Future[A](future: Scala_Future[A]) extends Future[A] |
34217 | 55 |
{ |
56673
42bf8fffdf6a
modernized Future/Promise implementation, bypassing old actors;
wenzelm
parents:
56663
diff
changeset
|
56 |
def peek: Option[Exn.Result[A]] = |
42bf8fffdf6a
modernized Future/Promise implementation, bypassing old actors;
wenzelm
parents:
56663
diff
changeset
|
57 |
future.value match { |
42bf8fffdf6a
modernized Future/Promise implementation, bypassing old actors;
wenzelm
parents:
56663
diff
changeset
|
58 |
case Some(Success(x)) => Some(Exn.Res(x)) |
42bf8fffdf6a
modernized Future/Promise implementation, bypassing old actors;
wenzelm
parents:
56663
diff
changeset
|
59 |
case Some(Failure(e)) => Some(Exn.Exn(e)) |
42bf8fffdf6a
modernized Future/Promise implementation, bypassing old actors;
wenzelm
parents:
56663
diff
changeset
|
60 |
case None => None |
42bf8fffdf6a
modernized Future/Promise implementation, bypassing old actors;
wenzelm
parents:
56663
diff
changeset
|
61 |
} |
42bf8fffdf6a
modernized Future/Promise implementation, bypassing old actors;
wenzelm
parents:
56663
diff
changeset
|
62 |
override def is_finished: Boolean = future.isCompleted |
34217 | 63 |
|
56673
42bf8fffdf6a
modernized Future/Promise implementation, bypassing old actors;
wenzelm
parents:
56663
diff
changeset
|
64 |
def join: A = Await.result(future, Duration.Inf) |
42bf8fffdf6a
modernized Future/Promise implementation, bypassing old actors;
wenzelm
parents:
56663
diff
changeset
|
65 |
override def map[B](f: A => B): Future[B] = new Pending_Future[B](future.map(f)) |
34217 | 66 |
} |
67 |
||
56673
42bf8fffdf6a
modernized Future/Promise implementation, bypassing old actors;
wenzelm
parents:
56663
diff
changeset
|
68 |
private class Promise_Future[A](promise: Scala_Promise[A]) |
42bf8fffdf6a
modernized Future/Promise implementation, bypassing old actors;
wenzelm
parents:
56663
diff
changeset
|
69 |
extends Pending_Future(promise.future) with Promise[A] |
34240
3274571e45c1
added Future.promise -- essentially a single-assignment variable with signalling, using the Future interface;
wenzelm
parents:
34217
diff
changeset
|
70 |
{ |
56673
42bf8fffdf6a
modernized Future/Promise implementation, bypassing old actors;
wenzelm
parents:
56663
diff
changeset
|
71 |
override def is_finished: Boolean = promise.isCompleted |
34240
3274571e45c1
added Future.promise -- essentially a single-assignment variable with signalling, using the Future interface;
wenzelm
parents:
34217
diff
changeset
|
72 |
|
56674 | 73 |
def fulfill_result(res: Exn.Result[A]): Unit = |
56673
42bf8fffdf6a
modernized Future/Promise implementation, bypassing old actors;
wenzelm
parents:
56663
diff
changeset
|
74 |
res match { |
42bf8fffdf6a
modernized Future/Promise implementation, bypassing old actors;
wenzelm
parents:
56663
diff
changeset
|
75 |
case Exn.Res(x) => promise.success(x) |
42bf8fffdf6a
modernized Future/Promise implementation, bypassing old actors;
wenzelm
parents:
56663
diff
changeset
|
76 |
case Exn.Exn(e) => promise.failure(e) |
34240
3274571e45c1
added Future.promise -- essentially a single-assignment variable with signalling, using the Future interface;
wenzelm
parents:
34217
diff
changeset
|
77 |
} |
56674 | 78 |
def fulfill(x: A): Unit = promise.success(x) |
34240
3274571e45c1
added Future.promise -- essentially a single-assignment variable with signalling, using the Future interface;
wenzelm
parents:
34217
diff
changeset
|
79 |
} |
3274571e45c1
added Future.promise -- essentially a single-assignment variable with signalling, using the Future interface;
wenzelm
parents:
34217
diff
changeset
|
80 |