Train Signal snippet

module test

data LineSegment = StringLineSegment String
data LineStatus = AllClear LineSegment | LimitedClearance LineSegment | Obstruction LineSegment

total
isClear : LineStatus -> Bool
isClear (AllClear _) = True
isClear (LimitedClearance _) = False
isClear (Obstruction _) = False

total
isLimitedClearance : LineStatus -> Bool
isLimitedClearance (AllClear _) = False
isLimitedClearance (LimitedClearance _) = True
isLimitedClearance (Obstruction _) = False

using (LineStatus ls)
data LightStatus : Bool -> Bool -> Bool -> Type where
  GreenOn : (isClear ls = True) -> LightStatus False False True
  OrangeOn : (isLimitedClearance ls = True) -> LightStatus False True False
  RedOn : LightStatus True False False

--prove that the green light cannot come on with an obstruction


-- prove that no light can come on with any other light