|
1 (* Title: Pure/RAW/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 unavailable () = fail (); |
|
39 |
|
40 fun fork _ = fail (); |
|
41 fun exit _ = fail (); |
|
42 fun isActive _ = fail (); |
|
43 |
|
44 fun equal _ = fail (); |
|
45 fun self _ = fail (); |
|
46 |
|
47 fun interrupt _ = fail (); |
|
48 fun broadcastInterrupt _ = fail (); |
|
49 fun testInterrupt _ = fail (); |
|
50 |
|
51 fun kill _ = fail (); |
|
52 |
|
53 fun setAttributes _ = fail (); |
|
54 fun getAttributes _ = fail (); |
|
55 |
|
56 fun numProcessors _ = fail (); |
|
57 |
|
58 |
|
59 (* thread data *) |
|
60 |
|
61 local |
|
62 |
|
63 val data = ref ([]: Universal.universal ref list); |
|
64 |
|
65 fun find_data tag = |
|
66 let |
|
67 fun find (r :: rs) = if Universal.tagIs tag (! r) then SOME r else find rs |
|
68 | find [] = NONE; |
|
69 in find (! data) end; |
|
70 |
|
71 in |
|
72 |
|
73 fun getLocal tag = Option.map (Universal.tagProject tag o !) (find_data tag); |
|
74 |
|
75 fun setLocal (tag, x) = |
|
76 (case find_data tag of |
|
77 SOME r => r := Universal.tagInject tag x |
|
78 | NONE => data := ref (Universal.tagInject tag x) :: ! data); |
|
79 |
|
80 end; |
|
81 end; |
|
82 end; |