import Clock;

interface Dining_Philosophers<Num_Phils : Univ_Integer := 5; Context<>> is

    func Dinner_Party (Length_Of_Party : Clock::Interval_Type; Context);

    type Philosopher_Index is new Integer<1..Num_Phils>;
    type Left_Or_Right is Enum<[#is_left_fork, #is_right_fork]>;

    concurrent interface Fork<> is  
        func Pick_Up_Fork(queued var F : Fork; Which_Fork : Left_Or_Right);
        func Put_Down_Fork(locked var F : Fork);
        func Create(Index : Philosopher_Index) -> Fork;
    end interface Fork;

    type Fork_Array is Array<Fork, Indexed_By => Philosopher_Index>;
        
end interface Dining_Philosophers;

class Dining_Philosophers<Num_Phils : Univ_Integer := 5; Context<>> is

  exports

    func Dinner_Party(Length_Of_Party : Clock::Interval_Type; Context) is
        Delay(Context.Clock.Wall_Clock, Length_Of_Party);
        Display(Context.IO.Standard_Output, "Dinner Party is over\n");
        return; 
      ||
        var Forks : Fork_Array := [for I in 1..Num_Phils => Create(I)];
        
        for Phil in Philosopher_Index concurrent loop
            const Left_Fork := Phil;
            const Right_Fork := Phil mod Num_Phils + 1;
           
            while True loop
                Display(Context.IO.Standard_Output, "Philosopher " | Phil | " is thinking\n");
                Delay(Clock, Next(Context.Random));  // Think
              then
                Pick_Up_Fork(Forks[Left_Fork], #is_left_fork);
              ||
                Pick_Up_Fork(Forks[Right_Fork], #is_right_fork);
              then
                Display(Context.IO.Standard_Output, "Philosopher " | Phil | " is eating\n");
                Delay(Clock, Next(Context.Random));  // Eat
              then
                Put_Down_Fork(Forks[Left_Fork]);
              ||
                Put_Down_Fork(Forks[Right_Fork]);
            end loop;
        end loop;
    end func Dinner_Party;
    
    concurrent class Fork<> is
        var Is_Available : Boolean;
        
      exports

        func Create(Index : Philosopher_Index) -> Fork is
            return (Is_Available => True);
        end func Create;
        
        func Pick_Up_Fork (queued var F : Fork; Which_Fork : Left_Or_Right) is 
          queued until F.Is_Available then
            F.Is_Available := False;
        end func Pick_Up_Fork;       
            
        func Put_Down_Fork(locked var F : Fork) is
            F.Is_Available := True;
        end func Put_Down_Fork;
        
    end class Fork;

end class Dining_Philosophers;