src/Pure/ML-Systems/thread_dummy.ML
author wenzelm
Mon, 19 Jan 2009 19:38:03 +0100
changeset 29564 f8b933a62151
parent 28154 3c3663e24ba7
child 32736 f126e68d003d
permissions -rw-r--r--
removed Ids;
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
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    38
  fun fork _ = fail ();
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    39
  fun exit _ = fail ();
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    40
  fun isActive _ = fail ();
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    41
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    42
  fun equal _ = fail ();
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    43
  fun self _ = fail ();
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    44
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    45
  fun interrupt _ = fail ();
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    46
  fun broadcastInterrupt _ = fail ();
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    47
  fun testInterrupt _ = fail ();
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    48
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    49
  fun kill _ = fail ();
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    50
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    51
  fun setAttributes _ = fail ();
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    52
  fun getAttributes _ = fail ();
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    53
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    54
  fun numProcessors _ = fail ();
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    55
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    56
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    57
(* thread data *)
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    58
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    59
local
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    60
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    61
val data = ref ([]: Universal.universal ref list);
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    62
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    63
fun find_data tag =
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    64
  let
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    65
    fun find (r :: rs) = if Universal.tagIs tag (! r) then SOME r else find rs
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    66
      | find [] = NONE;
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    67
  in find (! data) end;
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    68
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    69
in
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    70
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    71
fun getLocal tag = Option.map (Universal.tagProject tag o !) (find_data tag);
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    72
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    73
fun setLocal (tag, x) =
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    74
  (case find_data tag of
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    75
    SOME r => r := Universal.tagInject tag x
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    76
  | NONE => data := ref (Universal.tagInject tag x) :: ! data);
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    77
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    78
end;
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    79
end;
c1277547d59f *** empty log message ***
wenzelm
parents:
diff changeset
    80
end;