BrokenTennis.idr

%default total

data Player = P1 | P2

-- How can we prove that it's not the same player?
otherPlayer : Player -> Player
otherPlayer P1 = P2
otherPlayer P2 = P1

data PointValue = Love | Fifteen | Thirty | Forty

-- Maybe this should also take a proof that the input is not Forty?
nextPointValue : (input : PointValue) -> PointValue

nextPointValue Love = Fifteen
nextPointValue Fifteen = Thirty
nextPointValue Thirty = Forty
nextPointValue Forty = Forty -- Ouch!

mutual
  data Point : (player : Player) -> (value : PointValue) -> (otherPlayer : PointValue) -> Type where
    NewGame : Point P1 Love Love
    MkPoint : (player : Player)
            -> (prev : Point _ _ _)
            -> Point player (nextPointValue (playerPointValue player prev)) (playerPointValue (otherPlayer player) prev)

  playerPointValue : (player : Player) -> (Point pointPlayer pointValue otherPlayerValue) -> PointValue
  -- Can this be done with just 2 lines?
  playerPointValue P1 _ {pointPlayer = P1} {pointValue} = pointValue
  playerPointValue P2 _ {pointPlayer = P2} {pointValue} = pointValue
  playerPointValue P1 _ {pointPlayer = P2} {otherPlayerValue}= otherPlayerValue
  playerPointValue P2 _ {pointPlayer = P1} {otherPlayerValue} = otherPlayerValue

mutual
  data Deuce : Type where
    -- Can this be encoded with one constructor?
    MkDeuceSamePlayer : (player : Player) -> (prev : Point player Thirty Forty) -> Deuce
    -- How to ensure player and otherPlayer are not the same - add a proof maybe?
    MkDeuceOtherPlayer : (player : Player) -> (prev : Point notSamePlayer Forty Thirty) -> Deuce
    MkDeuceFromAdvantage : (player : Player) -> (prev : Advantage notSamePlayer) -> Deuce

  data Advantage : (player : Player) -> Type where
    MkAdvantage : (player : Player) -> (prev : Deuce) -> Advantage player

data Game : (player : Player) -> Type where
  MkGameFromForty : (player : Player) -> (prev : Point player Forty _) -> Game player
  MkGameFromAdvantage : (player : Player) -> (prev : Advantage player) -> Game player

-- Implementation time

interface Score s where
  NextType : (player : Player) -> (prev : s) -> Type
  score : (player : Player) -> (prev : s) -> NextType player prev

ScorePlayerPointType : (player : Player) -> (currentScore : PointValue) -> (otherScore : PointValue) -> Type
ScorePlayerPointType player prev@Love otherScore = Point player (nextPointValue prev) otherScore
ScorePlayerPointType player prev@Fifteen otherScore = Point player (nextPointValue prev) otherScore
ScorePlayerPointType player prev@Thirty otherScore = Point player (nextPointValue prev) otherScore
ScorePlayerPointType player prev@Forty otherScore = Game player

scoreSamePlayerPoint : (player : Player)
                     -> (currentScore : PointValue)
                     -> (otherScore : PointValue)
                     -> (prev : Point player currentScore otherScore)
                     -> ScorePlayerPointType player currentScore otherScore
scoreSamePlayerPoint player Forty _ prev = MkGameFromForty player prev
scoreSamePlayerPoint player Thirty otherScore prev = MkPoint player prev -- <<< WHY DON'T YOU WORK!?!?
scoreSamePlayerPoint player Fifteen otherScore prev = ?hepfdf3
scoreSamePlayerPoint player Love otherScore prev = ?hepfdf2

Score (Point pointPlayer pointValue pointOtherValue) where
  NextType P1 prev {pointPlayer = P1} {pointValue = Forty} = Game P1
  NextType P2 prev {pointPlayer = P2} {pointValue = Forty} = Game P2
  -- NextType P1 prev {pointPlayer = P1} {pointOtherValue = Forty} = Game P1
  -- NextType P2 prev {pointPlayer = P2} {pointOtherValue = Forty} = Game P2
  NextType player prev = Point player (nextPointValue (playerPointValue player prev)) (playerPointValue (otherPlayer player) prev)

  score P1 prev {pointPlayer = P1} {pointValue = Forty} {pointOtherValue} = scoreSamePlayerPoint P1 Forty pointOtherValue prev  -- MkGameFromForty P1 prev
  score P2 prev {pointPlayer = P2} {pointValue = Forty} {pointOtherValue} = scoreSamePlayerPoint P2 Forty pointOtherValue prev
  score P1 prev {pointPlayer = P1} {pointValue = Thirty} = MkPoint P1 prev
  score P2 prev {pointPlayer = P2} {pointValue = Thirty} = MkPoint P2 prev
  score P1 prev {pointPlayer = P1} {pointValue = Fifteen} = MkPoint P1 prev
  score P2 prev {pointPlayer = P2} {pointValue = Fifteen} = MkPoint P2 prev
  score P1 prev {pointPlayer = P1} {pointValue = Love} = MkPoint P1 prev
  score P2 prev {pointPlayer = P2} {pointValue = Love} = MkPoint P2 prev

  score P1 prev {pointPlayer = P2} {pointValue = Forty} = MkPoint P1 prev
  score P2 prev {pointPlayer = P1} {pointValue = Forty} = MkPoint P2 prev
  score P2 prev {pointPlayer = P1} {pointValue = Thirty} = MkPoint P2 prev
  score P1 prev {pointPlayer = P2} {pointValue = Thirty} = MkPoint P1 prev
  score P2 prev {pointPlayer = P1} {pointValue = Fifteen} = MkPoint P2 prev
  score P1 prev {pointPlayer = P2} {pointValue = Fifteen} = MkPoint P1 prev
  score P2 prev {pointPlayer = P1} {pointValue = Love} = MkPoint P2 prev
  score P1 prev {pointPlayer = P2} {pointValue = Love} = MkPoint P1 prev

-- The big challenge

scoreGame : List Player -> Game player
scoreGame xs = ?score_rhs