Require Export NextPort.

Set Implicit Arguments.
Unset Strict Implicit.

Section Round_Robin_function.

  Variable i o : nat.   Let Inportno := T_Inportno i.
  Let Outportno := T_Outportno o.

  Variable k : nat.

 Fixpoint RoundRobin (n : nat) (requests_set : d_list Inportno k)
  (last : Inportno) {struct n} : Inportno :=
   match n with
   | O ⇒ last
   | S p ⇒
       match
         In_or_not eq_nat_dec (no_in (SUC_MODN last))
           (d_map (no_in (i:=i)) requests_set)
       with
       | left _ ⇒ SUC_MODN last
       | right _ ⇒ RoundRobin p requests_set (SUC_MODN last)
       end
   end.

  Definition RoundRobinArbiter (requests_set : d_list Inportno k)
    (last : Inportno) :=
    match requests_set with
    | d_nil ⇒ last
    | d_cons p _ _ ⇒ RoundRobin i requests_set last
    end.

End Round_Robin_function.