| author | panny | 
| Sat, 15 Mar 2014 03:37:22 +0100 | |
| changeset 56153 | 2008f1cf3030 | 
| parent 39616 | 8052101883c3 | 
| permissions | -rw-r--r-- | 
| 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 | ||
| 32736 
f126e68d003d
Dummy version of state variables -- plain refs for sequential access.
 wenzelm parents: 
29564diff
changeset | 38 | fun unavailable () = fail (); | 
| 
f126e68d003d
Dummy version of state variables -- plain refs for sequential access.
 wenzelm parents: 
29564diff
changeset | 39 | |
| 28152 | 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 | ||
| 39616 
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
 wenzelm parents: 
32776diff
changeset | 63 | val data = ref ([]: Universal.universal ref list); | 
| 28152 | 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 | |
| 39616 
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
 wenzelm parents: 
32776diff
changeset | 78 | | NONE => data := ref (Universal.tagInject tag x) :: ! data); | 
| 28152 | 79 | |
| 80 | end; | |
| 81 | end; | |
| 82 | end; |