package TL9 (sysTL, TL) where

  -- Simple model of a traffic light

  -- Version 9: Use Bluespec layout rules to reduce lexical noise

  interface TL =   ped_button_push :: Action
                   set_car_state_N :: Bool -> Action
                   set_car_state_S :: Bool -> Action
                   set_car_state_E :: Bool -> Action
                   set_car_state_W :: Bool -> Action

                   lampRedNS       :: Bool
                   lampAmberNS     :: Bool
                   lampGreenNS     :: Bool

                   lampRedE        :: Bool
                   lampAmberE      :: Bool
                   lampGreenE      :: Bool

                   lampRedW        :: Bool
                   lampAmberW      :: Bool
                   lampGreenW      :: Bool

                   lampRedPed      :: Bool
                   lampAmberPed    :: Bool
                   lampGreenPed    :: Bool

  data TLstates = AllRed
                | GreenNS  | AmberNS
                | GreenE   | AmberE
                | GreenW   | AmberW
                | GreenPed | AmberPed
                deriving (Eq, Bits)

  type Time32 = UInt 5

  sysTL :: Module TL
  sysTL =
      module
          state :: Reg TLstates
          state <- mkReg AllRed

          next_green :: Reg TLstates
          next_green <- mkReg GreenNS

          secs :: Reg Time32
          secs <- mkReg 0

          ped_button_pushed :: Reg Bool
          ped_button_pushed <- mkReg False

          car_present_NS :: Reg Bool
          car_present_NS <- mkReg True

          car_present_E :: Reg Bool
          car_present_E <- mkReg True

          car_present_W :: Reg Bool
          car_present_W <- mkReg True

          let
              allRedDelay :: Time32
              allRedDelay = 2

              amberDelay :: Time32
              amberDelay = 4

              ns_green_delay :: Time32
              ns_green_delay = 20

              ew_green_delay :: Time32
              ew_green_delay = 10

              pedGreenDelay :: Time32
              pedGreenDelay = 10

              pedAmberDelay :: Time32
              pedAmberDelay = 6

              next_state :: TLstates -> Action
              next_state  ns = action { state := ns; secs := 0; }

              green_seq  :: TLstates -> TLstates
              green_seq  GreenNS = GreenE
              green_seq  GreenE  = GreenW
              green_seq  GreenW  = GreenNS

              car_present  :: TLstates -> Bool
              car_present  GreenNS = car_present_NS
              car_present  GreenE  = car_present_E
              car_present  GreenW  = car_present_W

              make_from_green_rule :: String -> TLstates -> Time32 -> Bool -> TLstates -> Rules
              make_from_green_rule  rule_name  green_state  delay  car_present  ns =
                  rules
                    rule_name:
                      when (state == green_state) &&
                           (((secs + 1) >= delay) || not car_present)
                      ==>  next_state (ns)

              make_from_amber_rule :: String -> TLstates -> TLstates -> Rules
              make_from_amber_rule  rule_name  amber_state  ng =
                  rules
                    rule_name:
                      when (state == amber_state) && ((secs + 1) >= amberDelay)
                      ==>  action { next_state (AllRed); next_green := ng; }

          interface
              ped_button_push   = ped_button_pushed  := True
              set_car_state_N b = car_present_NS     := b
              set_car_state_S b = car_present_NS     := b
              set_car_state_E b = car_present_E      := b
              set_car_state_W b = car_present_W      := b

              lampRedNS    = not ((state == GreenNS) || (state == AmberNS))
              lampAmberNS  = state == AmberNS
              lampGreenNS  = state == GreenNS

              lampRedE     = not ((state == GreenE) || (state == AmberE))
              lampAmberE   = state == AmberE
              lampGreenE   = state == GreenE

              lampRedW     = not ((state == GreenW) || (state == AmberW))
              lampAmberW   = state == AmberW
              lampGreenW   = state == GreenW

              lampRedPed   = not ((state == GreenPed) || (state == AmberPed))
              lampAmberPed = state == AmberPed
              lampGreenPed = state == GreenPed

          addRules $
            rules
              "wait": when True ==> secs := secs + 1

            +>

            (
            rules
              "fromAllRed":
                when (state == AllRed) && ((secs + 1) >= allRedDelay)
                  ==> if ped_button_pushed then
                          action { ped_button_pushed := False; next_state (GreenPed); }
                      else if car_present (next_green) then
                          next_state (next_green)
                      else if car_present (green_seq next_green) then
                          next_state (green_seq next_green)
                      else if car_present (green_seq (green_seq next_green)) then
                          next_state (green_seq (green_seq next_green))
                      else
                          next_state (AllRed)

              "fromGreenPed":
                when (state == GreenPed) && ((secs + 1) >= pedGreenDelay)
                ==>  next_state (AmberPed)

              "fromAmberPed":
                when (state == AmberPed) && ((secs + 1) >= pedAmberDelay)
                ==>  next_state (AllRed)

            <+>
            make_from_green_rule "fromGreenNS" GreenNS ns_green_delay car_present_NS AmberNS
            <+>
            make_from_amber_rule "fromAmberNS" AmberNS GreenE
            <+>
            make_from_green_rule "fromGreenE" GreenE ew_green_delay car_present_E AmberE
            <+>
            make_from_amber_rule "fromAmberE" AmberE GreenW
            <+>
            make_from_green_rule "fromGreenW" GreenW ew_green_delay car_present_W AmberW
            <+>
            make_from_amber_rule "fromAmberW" AmberW GreenNS
            )