Tennis Scoring Kata in Idris [WIP]

Tennis.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

Score (Point pointPlayer pointValue pointOtherValue) where
  NextType player prev = Point player (nextPointValue (playerPointValue player prev)) (playerPointValue (otherPlayer player) prev)

  score = MkPoint

-- The big challenge

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