-- monomorphic version, since no polymorphic templates yet!  KH

type BIT = word 1;

type Channel = (Bit,Bit,Bit);

-- data Channel   = RDY| SND TrainID | NAK
-- RDY == (0,0,0)
-- SND Train1 == (0,0,1)
-- SND Train2 == (0,1,0)
-- NAK == (1,1,1)

type Ctl = BIT;

-- data Ctl =       0 | 1;
-- RCV == 0
-- ACK == 1

type State = (Bit,Bit,Bit);

-- data State =     Just TrainID | Nothing | Nothing2 | WaitI | WaitI2 | WaitO ;
-- Just Train1 == (1,0,1)
-- Just Train2 == (1,1,0)
-- Nothing == (0,0,0)
-- Nothing2 = (0,0,1)
-- WaitI == (0,1,0)
-- WaitI2 == (0,1,1)
-- WaitO == (1,0,0)

--type TrainID =   String;
--type String = 	 [char];

template SyncMerge
in  ( value  :: State, in1,    in2    :: Channel, outctl :: Ctl       )
out ( value' :: State, in1ctl, in2ctl :: Ctl,     outp   :: Channel   )
match
   ( (0,0,0),  (0,0,0),     *,       *   ) -> ( (0,1,0),    0, *,   *       )  
|  ( (0,0,0),  *,       (0,0,0),     *   ) -> ( (0,1,0),    *,   0, *       )
|  ( (0,1,0),    (0,0,1), *,       *   ) -> ( (1,0,1), 1, *,   (0,0,0)     )
|  ( (0,1,0),    (0,0,1), *,       *   ) -> ( (1,1,0), 1, *,   (0,0,0)     )
|  ( (0,1,0),    (0,1,0), *,       *   ) -> ( (1,0,1), 1, *,   (0,0,0)     )
|  ( (0,1,0),    (0,1,0), *,       *   ) -> ( (1,1,0), 1, *,   (0,0,0)     )
|  ( (0,1,0),    (1,1,1),     *,       *   ) -> ( (0,0,0),  *,   *,   *       )
|  ( (0,1,0),    *,       (0,0,1), *   ) -> ( (1,0,1), *,   1, (0,0,0)     )
|  ( (0,1,0),    *,       (0,0,1), *   ) -> ( (1,1,0), *,   1, (0,0,0)     )
|  ( (0,1,0),    *,       (0,1,0), *   ) -> ( (1,0,1), *,   1, (0,0,0)     )
|  ( (0,1,0),    *,       (0,1,0), *   ) -> ( (1,1,0), *,   1, (0,0,0)     )
|  ( (0,1,0),    *,       (1,1,1),     *   ) -> ( (0,0,0),  *,   *,   *       )
|  ( (1,0,1), *,       *,       0 ) -> ( (1,0,0),    *,   *,   (0,0,1) )
|  ( (1,1,0), *,       *,       0 ) -> ( (1,0,0),    *,   *,   (0,0,1) )
|  ( (1,0,1), *,       *,       0 ) -> ( (1,0,0),    *,   *,   (0,1,0) )
|  ( (1,1,0), *,       *,       0 ) -> ( (1,0,0),    *,   *,   (0,1,0) )
|  ( (1,0,1),   *,       *,       0 ) -> ( (1,0,1),   *,   *,   (1,1,1)     )
|  ( (1,1,0),   *,       *,       0 ) -> ( (1,1,0),   *,   *,   (1,1,1)     )
|  ( state,    *,       *,       0 ) -> ( state,   *,    *,   (1,1,1)     )
-- Are the (1,1,1) cases required?
|  ( state,    (1,1,1),     *,       *   ) -> ( state,   *,    *,   *       )
|  ( state,    *,       (1,1,1),     *   ) -> ( state,   *,    *,   *       )
|  ( (1,0,0),    *,       *,       1 ) -> ( (0,0,0),  *,   *,   *       ) 
;
-- |  ( (1,0,0),    *,       *,       0 ) -> ( (1,0,0),   *,   *,    (1,1,1)     ) ;

template SyncSplit
in  ( value  :: State, inp    :: Channel,  out1ctl, out2ctl :: Ctl      )
out ( value' :: State, inctl :: Ctl ,      out1,    out2    :: Channel  )
match
   ( (0,0,0),  (0,0,0),     *,   *   ) -> ( (0,1,0),    0, *,   *       )
|  ( (0,0,1), (0,0,0),     *,   *   ) -> ( (0,1,1),   0, *,   *       )
|  ( (0,1,0),    (0,0,1), *,   *   ) -> ( (1,0,1), 1, (0,0,0), *       )
|  ( (0,1,0),    (0,0,1), *,   *   ) -> ( (1,1,0), 1, (0,0,0), *       )
|  ( (0,1,0),    (0,1,0), *,   *   ) -> ( (1,0,1), 1, (0,0,0), *       )
|  ( (0,1,0),    (0,1,0), *,   *   ) -> ( (1,1,0), 1, (0,0,0), *       )
|  ( (0,1,0),    (1,1,1),     *,   *   ) -> ( (0,0,0),  *,   *,   *       )
|  ( (0,1,1),   (0,0,1), *,   *   ) -> ( (1,0,1), 1, *,   (0,0,0)     )
|  ( (0,1,1),   (0,0,1), *,   *   ) -> ( (1,1,0), 1, *,   (0,0,0)     )
|  ( (0,1,1),   (0,1,0), *,   *   ) -> ( (1,0,1), 1, *,   (0,0,0)     )
|  ( (0,1,1),   (0,1,0), *,   *   ) -> ( (1,1,0), 1, *,   (0,0,0)     )
|  ( (0,1,1),   (1,1,1),     *,   *   ) -> ( (0,0,1), *,   *,   *       )
-- Gives priority to the left without match matching
|  ( (1,0,1), *,       0, *   ) -> ( (1,0,0),    *,   (0,0,1), *   )
|  ( (1,1,0), *,       0, *   ) -> ( (1,0,0),    *,   (0,0,1), *   )
|  ( (1,0,1), *,       0, *   ) -> ( (1,0,0),    *,   (0,1,0), *   )
|  ( (1,1,0), *,       0, *   ) -> ( (1,0,0),    *,   (0,1,0), *   )
|  ( (1,0,1), *,       *,   0 ) -> ( (1,0,0),    *,   *,   (0,0,1) )
|  ( (1,1,0), *,       *,   0 ) -> ( (1,0,0),    *,   *,   (0,0,1) )
|  ( (1,0,1), *,       *,   0 ) -> ( (1,0,0),    *,   *,   (0,1,0) )
|  ( (1,1,0), *,       *,   0 ) -> ( (1,0,0),    *,   *,   (0,1,0) )
|  ( (1,0,1),   *,       (0,0,0), *   ) -> ( (1,0,1),   *,   (1,1,1), *       )
|  ( (1,1,0),   *,       (0,0,0), *   ) -> ( (1,1,0),   *,   (1,1,1), *       )
-- |  ( (1,0,0),    *,       *,   0 ) -> ( (1,0,0),    *,   *,   (1,1,1)     )
-- |  ( (1,0,0),    *,       0, *   ) -> ( (1,0,0),    *,   (1,1,1), *       )
|  ( (1,0,1),   *,       *,   0 ) -> ( (1,0,1),   *,   *,   (1,1,1)     )
|  ( (1,1,0),   *,       *,   0 ) -> ( (1,1,0),   *,   *,   (1,1,1)     )
|  ( (1,0,0),    *,       1, *   ) -> ( (0,0,1), *,   *,   *       )
|  ( (1,0,0),    *,       *,   1 ) -> ( (0,0,0),  *,   *,   *       )
-- Beware of overlap with Just val case
|  ( state,    *,       0, *   ) -> ( state,    *,   (1,1,1), *       )
-- Are the (1,1,1) cases required?
|  ( state,    (1,1,1),     *,   *   ) -> ( state,    *,   *,   *       )
|  ( state,    *,       *,   0 ) -> ( state,    *,   *,   (1,1,1)     )
;

template Track
in  ( value  :: State, inp     :: Channel, outctl :: Ctl       )
out ( value' :: State, inctl  :: Ctl ,      outp    :: Channel )
match
   ( (0,0,0), (0,0,0),   *   ) -> ( (0,1,0),   0, *     )
|  ( (0,1,0),   (0,0,1), *   ) -> ( (1,0,1),  1, (0,0,0)   )
|  ( (0,1,0),   (0,0,1), *   ) -> ( (1,1,0),  1, (0,0,0)   )
|  ( (0,1,0),   (0,1,0), *   ) -> ( (1,0,1),  1, (0,0,0)   )
|  ( (0,1,0),   (0,1,0), *   ) -> ( (1,1,0),  1, (0,0,0)   )
|  ( (0,1,0),   (1,1,1),   *   ) -> ( (0,0,0), *,   *     )
|  ( (1,0,1),  *,     0 ) -> ( (1,0,0),   *,   (0,0,1) )
|  ( (1,1,0),  *,     0 ) -> ( (1,0,0),   *,   (0,0,1) )
|  ( (1,0,1),  *,     0 ) -> ( (1,0,0),   *,   (0,1,0) )
|  ( (1,1,0),  *,     0 ) -> ( (1,0,0),   *,   (0,1,0) )
|  ( (1,0,1),  *,     0 ) -> ( (1,0,1),  *,   (1,1,1)   )
|  ( (1,1,0),  *,     0 ) -> ( (1,1,0),  *,   (1,1,1)   )
|  ( state,   *,     0 ) -> ( state,   *,   (1,1,1)   )
-- Are the (1,1,1) cases required?
|  ( state,   (1,1,1),   *   ) -> ( state,   *,   *     )
|  ( (1,0,0),   *,     1 ) -> ( (0,0,0), *,   *     ) ;
-- |  ( (1,0,0),   *,     0 ) -> ( (1,0,0),   *,   0   ) ;

constant RingSize =   16;
constant BypassSize = 4;
constant ForkPos  =   11;
constant JoinPos  =   4;

instantiate SyncSplit as Fork ; -- NYI initial ( value = (0,0,0) );
instantiate SyncMerge as Join ; -- NYI initial ( value = (0,0,0) );

for i =  0 to RingSize-1 except (ForkPos, JoinPos)
   instantiate Track as Ring{i};

for i = 0 to BypassSize-1
   instantiate Track as Bypass{i};

constant Train1Pos = 0;
constant Train2Pos = 2;
--constant Train3Pos = 1;

initial Ring   {Train1Pos} ( value = (1,0,1) );
initial Ring   {(Train1Pos+1) mod RingSize} ( inp = (0,0,0) ) ;

initial Bypass {Train2Pos} ( value = (1,1,0) );
initial Bypass {Train2Pos+1} ( inp = (0,0,0) ) ;

--initial Ring   {Train3Pos} ( value = Just "Train3" );
--initial Ring   {(Train3Pos+1) mod RingSize} ( inp = (0,0,0) ) ;

--initial Ring  {Train1Pos} ( value = (0,0,0) );
--initial Bypass{Train2Pos} ( value = (0,0,0) );
--initial Ring{Train3Pos} ( value = (0,0,0) );

for i = 0 to RingSize-1 except ( ForkPos, JoinPos, Train1Pos)
--, Train3Pos )
    initial Ring{i} ( value = (0,0,0) );

for i =  0 to BypassSize-1 except Train2Pos
    initial Bypass{i} ( value = (0,0,0) );
    
initial Fork ( value = (0,0,0) );
initial Join ( value = (0,0,0) );

wire Track ( this, prev, next ) =
    wire {this} ( {this}.value', {prev}.outp,    {next}.inctl )
                ( {this}.value trace,  {prev}.outctl, {next}.inp    );

macro predR pos = (pos - 1)  mod  RingSize;
macro succR pos = (pos + 1)  mod  RingSize;

--predRF pos = (pos - 1)  mod  RingSize;
--succRF pos = (pos + 1)  mod  RingSize;

constant BeforeFork  = (ForkPos - 1)  mod  RingSize; -- predR(ForkPos);
constant AfterFork   = (ForkPos + 1)  mod  RingSize; -- succR(ForkPos);
constant BeforeFork1  = (BeforeFork - 1)  mod  RingSize; -- predR(ForkPos);
constant AfterFork1   = (AfterFork + 1)  mod  RingSize; -- succR(ForkPos);

constant BeforeJoin  = (JoinPos - 1)  mod  RingSize; -- {predR(JoinPos);
constant AfterJoin   = (JoinPos + 1)  mod  RingSize; -- {succR(JoinPos)};
constant BeforeJoin1  = (BeforeJoin - 1)  mod  RingSize; -- predR(JoinPos);
constant AfterJoin1   = (AfterJoin + 1)  mod  RingSize; -- succR(JoinPos);

for i = 1 to RingSize-2
  except ( ForkPos, JoinPos, BeforeFork, AfterFork, BeforeJoin, AfterJoin )
  wire Track ( Ring{i}, Ring{i-1}, Ring{i+1} );

wire Track ( Ring{0},Ring{RingSize-1},Ring{1} );

wire Track ( Ring{RingSize-1},Ring{RingSize-2},Ring{0} );

for i = 1 to BypassSize-2
    wire Bypass{i} ( Bypass{i}.value', Bypass{i-1}.outp,    Bypass{i+1}.inctl )
                   ( Bypass{i}.value trace,  Bypass{i-1}.outctl, Bypass{i+1}.inp    );

wire Bypass{BypassSize-1}
    ( Bypass{BypassSize-1}.value', Bypass{BypassSize-2}.outp,    Join.in1ctl )
    ( Bypass{BypassSize-1}.value trace,  Bypass{BypassSize-2}.outctl, Join.in1    );

wire Track ( Ring{BeforeFork}, Ring{BeforeFork1}, Fork );
                   
wire Ring{AfterFork}
    ( Ring{AfterFork}.value', Fork.out1,    Ring{AfterFork1}.inctl )
    ( Ring{AfterFork}.value trace,  Fork.out1ctl, Ring{AfterFork1}.inp    );

wire Bypass{0} ( Bypass{0}.value', Fork.out2,    Bypass{1}.inctl )
               ( Bypass{0}.value trace,  Fork.out2ctl, Bypass{1}.inp    );
                   
wire Fork
    ( Fork.value', Ring{BeforeFork}.outp,   Ring{AfterFork}.inctl trace,  Bypass{0}.inctl trace )
    ( Fork.value trace,  Ring{BeforeFork}.outctl, Ring{AfterFork}.inp trace,    Bypass{0}.inp  trace  );

wire Ring{BeforeJoin}
    ( Ring{BeforeJoin}.value', Ring{BeforeJoin1}.outp,   Join.in2ctl )
    ( Ring{BeforeJoin}.value trace,  Ring{BeforeJoin1}.outctl, Join.in2    );
                   
wire Track ( Ring{AfterJoin}, Join, Ring{AfterJoin1} );
                   
wire Join
    ( Join.value', Bypass{BypassSize-1}.outp,    Ring{BeforeJoin}.outp,    Ring{AfterJoin}.inctl )
    ( Join.value trace,  Bypass{BypassSize-1}.outctl, Ring{BeforeJoin}.outctl, Ring{AfterJoin}.inp    );