| author | wenzelm |
| Sun, 26 Jul 2015 20:57:35 +0200 | |
| changeset 60788 | 5e2df6bd906c |
| parent 59004 | 6573e6d64ec8 |
| permissions | -rw-r--r-- |
|
32816
5db89f8d44f3
more official status of sequential implementations;
wenzelm
parents:
29368
diff
changeset
|
1 |
(* Title: Pure/Concurrent/par_list_sequential.ML |
|
28546
d57bfb44c9e5
Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
|
d57bfb44c9e5
Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff
changeset
|
3 |
|
|
d57bfb44c9e5
Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff
changeset
|
4 |
Dummy version of parallel list combinators -- plain sequential evaluation. |
|
d57bfb44c9e5
Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff
changeset
|
5 |
*) |
|
d57bfb44c9e5
Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff
changeset
|
6 |
|
| 29368 | 7 |
structure Par_List: PAR_LIST = |
|
28546
d57bfb44c9e5
Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff
changeset
|
8 |
struct |
|
d57bfb44c9e5
Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff
changeset
|
9 |
|
| 44269 | 10 |
fun managed_results _ f = map (Exn.capture f); |
| 41711 | 11 |
fun map_name _ = map; |
|
28546
d57bfb44c9e5
Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff
changeset
|
12 |
val map = map; |
| 59004 | 13 |
val map_independent = map; |
|
28546
d57bfb44c9e5
Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff
changeset
|
14 |
val get_some = get_first; |
| 28556 | 15 |
val find_some = find_first; |
|
28546
d57bfb44c9e5
Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff
changeset
|
16 |
val exists = exists; |
|
d57bfb44c9e5
Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff
changeset
|
17 |
val forall = forall; |
|
d57bfb44c9e5
Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff
changeset
|
18 |
|
|
d57bfb44c9e5
Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff
changeset
|
19 |
end; |