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