Files
linguist/samples/ATS/DiningPhil2_fork.dats

90 lines
1.3 KiB
Plaintext

(* ****** ****** *)
//
// HX-2013-11
//
// Implementing a variant of
// the problem of Dining Philosophers
//
(* ****** ****** *)
//
#include
"share/atspre_define.hats"
#include
"share/atspre_staload.hats"
//
(* ****** ****** *)
staload
UN = "prelude/SATS/unsafe.sats"
(* ****** ****** *)
staload "{$LIBATSHWXI}/teaching/mythread/SATS/channel.sats"
(* ****** ****** *)
staload _ = "libats/DATS/deqarray.dats"
staload _ = "{$LIBATSHWXI}/teaching/mythread/DATS/channel.dats"
(* ****** ****** *)
staload "./DiningPhil2.sats"
(* ****** ****** *)
datavtype fork = FORK of (nphil)
(* ****** ****** *)
assume fork_vtype = fork
(* ****** ****** *)
implement
fork_get_num (f) = let val FORK(n) = f in n end
(* ****** ****** *)
local
val
the_forkarray = let
//
typedef t = channel(fork)
//
implement
array_tabulate$fopr<t>
(n) = ch where
{
val n = $UN.cast{nphil}(n)
val ch = channel_create_exn<fork> (i2sz(2))
val () = channel_insert (ch, FORK (n))
}
//
in
arrayref_tabulate<t> (i2sz(NPHIL))
end // end of [val]
in (* in of [local] *)
implement fork_changet (n) = the_forkarray[n]
end // end of [local]
(* ****** ****** *)
local
val the_forktray =
channel_create_exn<fork> (i2sz(NPHIL+1))
in (* in of [local] *)
implement forktray_changet () = the_forktray
end // end of [local]
(* ****** ****** *)
(* end of [DiningPhil2_fork.dats] *)