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