module DiningPhilo where

import Array

struct Table =
   pickup  :: Int -> Action -> Action
   putdown :: Int -> Action

data PhiloState = Thinking | Hungry Action | Eating

instance Eq PhiloState where
   Thinking == Thinking  =  True
   Eating   == Eating    =  True
   _        == _         =  False

dining_table n = 
   template
      state := array (0,n-1) Thinking
   in let
      left  k = (k+n-1) `mod` n

      right k = (k+1) `mod` n

      test k = do
         case state!k of
            Hungry grant 
               | state!(left k)  /= Eating &&
                 state!(right k) /= Eating -> do
                    state!k := Eating
                    grant
            _ -> done

   in struct
      pickup i grant = action
         state!i := Hungry grant
         test i

      putdown i = action
         state!i := Thinking
         test (left i)
         test (right i)

struct Philo =
   become_hungry   :: Action
   become_inspired :: Action
   
dining_philosopher i table =
   template
      state_of_mind := undefined
   in let
      eat = undefined
      think = undefined
   in struct
      become_hungry = action
         table.pickup i (action 
            eat
            table.putdown i)
      become_inspired = action
         think