28152
|
1 |
(* Title: Pure/ML-Systems/thread_dummy.ML
|
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Default (mostly dummy) implementation of thread structures
|
|
5 |
(cf. polyml/basis/Thread.sml).
|
|
6 |
*)
|
|
7 |
|
|
8 |
exception Thread of string;
|
|
9 |
|
|
10 |
local fun fail _ = raise Thread "No multithreading support on this ML platform" in
|
|
11 |
|
|
12 |
structure Mutex =
|
|
13 |
struct
|
|
14 |
type mutex = unit;
|
|
15 |
fun mutex _ = ();
|
|
16 |
fun lock _ = fail ();
|
|
17 |
fun unlock _ = fail ();
|
|
18 |
fun trylock _ = fail ();
|
|
19 |
end;
|
|
20 |
|
|
21 |
structure ConditionVar =
|
|
22 |
struct
|
|
23 |
type conditionVar = unit;
|
|
24 |
fun conditionVar _ = ();
|
|
25 |
fun wait _ = fail ();
|
|
26 |
fun waitUntil _ = fail ();
|
|
27 |
fun signal _ = fail ();
|
|
28 |
fun broadcast _ = fail ();
|
|
29 |
end;
|
|
30 |
|
|
31 |
structure Thread =
|
|
32 |
struct
|
|
33 |
type thread = unit;
|
|
34 |
|
|
35 |
datatype threadAttribute = EnableBroadcastInterrupt of bool | InterruptState of interruptState
|
|
36 |
and interruptState = InterruptDefer | InterruptSynch | InterruptAsynch | InterruptAsynchOnce;
|
|
37 |
|
|
38 |
fun fork _ = fail ();
|
|
39 |
fun exit _ = fail ();
|
|
40 |
fun isActive _ = fail ();
|
|
41 |
|
|
42 |
fun equal _ = fail ();
|
|
43 |
fun self _ = fail ();
|
|
44 |
|
|
45 |
fun interrupt _ = fail ();
|
|
46 |
fun broadcastInterrupt _ = fail ();
|
|
47 |
fun testInterrupt _ = fail ();
|
|
48 |
|
|
49 |
fun kill _ = fail ();
|
|
50 |
|
|
51 |
fun setAttributes _ = fail ();
|
|
52 |
fun getAttributes _ = fail ();
|
|
53 |
|
|
54 |
fun numProcessors _ = fail ();
|
|
55 |
|
|
56 |
|
|
57 |
(* thread data *)
|
|
58 |
|
|
59 |
local
|
|
60 |
|
|
61 |
val data = ref ([]: Universal.universal ref list);
|
|
62 |
|
|
63 |
fun find_data tag =
|
|
64 |
let
|
|
65 |
fun find (r :: rs) = if Universal.tagIs tag (! r) then SOME r else find rs
|
|
66 |
| find [] = NONE;
|
|
67 |
in find (! data) end;
|
|
68 |
|
|
69 |
in
|
|
70 |
|
|
71 |
fun getLocal tag = Option.map (Universal.tagProject tag o !) (find_data tag);
|
|
72 |
|
|
73 |
fun setLocal (tag, x) =
|
|
74 |
(case find_data tag of
|
|
75 |
SOME r => r := Universal.tagInject tag x
|
|
76 |
| NONE => data := ref (Universal.tagInject tag x) :: ! data);
|
|
77 |
|
|
78 |
end;
|
|
79 |
end;
|
|
80 |
end;
|