Tennis Kata, in Idris, with Dependent types.

TennisDT.idr

module TennisDT

%default total

data Player = Player1 | Player2


||| Prove that the game is not over after a point
data NotWinning : Nat -> Nat -> Type where
  ||| Game is not over because the winning player is below 40
  ThresholdNotMet : LTE x 3 -> NotWinning x y
  ||| Game is not over because we only reach deuce or advantage
  OpponentTooClose : LTE x (S y) -> NotWinning x y

||| Decision procedure to obtain a NotWinningProof
notWinning : (winnerScore : Nat)
              -> (loserScore : Nat)
              -> Dec (NotWinning winnerScore loserScore)
notWinning winnerScore loserScore =
  case isLTE winnerScore 3 of
       (Yes prfT)    => Yes (ThresholdNotMet prfT)
       (No contraT) => case isLTE winnerScore (S loserScore) of
                            Yes prfO => Yes (OpponentTooClose prfO)
                            No contraO => No (winningProof contraT contraO)
  where
    winningProof : (contraT : Not (LTE winnerScore 3))
                -> (contraO : Not (LTE winnerScore (S loserScore)))
                -> Not (NotWinning winnerScore loserScore)
    winningProof contraT contraO (ThresholdNotMet x) = contraT x
    winningProof contraT contraO (OpponentTooClose x) = contraO x

||| Score is built by stacking ball winners, along with the proof that the game is not over
data Score : Nat -> Nat -> Type where
  Start : Score 0 0
  Player1Scores : Score x y -> {auto prf: NotWinning (S x) y} -> Score (S x) y
  Player2Scores : Score x y -> {auto prf: NotWinning (S y) x} -> Score x (S y)

nextScore : (winner : Player) -> (pointsOwner : Player) -> (points : Nat) -> Nat
nextScore Player1 Player1 points = S points
nextScore Player1 Player2 points = points
nextScore Player2 Player1 points = points
nextScore Player2 Player2 points = S points

||| Add the result of a point to a score
score : (previousScore : Score p1Points p2Points)
      -> (p : Player)
      -> Maybe (Score (nextScore p Player1 p1Points) (nextScore p Player2 p2Points))
score previousScore p {p1Points} {p2Points} =
  case notWinning (winnerPoints p) (loserPoints p) of
       Yes _      => pure (builder p)
       No  contra => empty
  where
    winnerPoints : Player -> Nat
    winnerPoints Player1 = S p1Points
    winnerPoints Player2 = S p2Points
    loserPoints : Player -> Nat
    loserPoints  Player1 = p2Points
    loserPoints  Player2 = p1Points
    builder : (p : Player)
    -> {auto prf : NotWinning (winnerPoints p) (loserPoints p)}
           -> Score (nextScore p Player1 p1Points) (nextScore p Player2 p2Points)
    builder Player1 = Player1Scores previousScore
    builder Player2 = Player2Scores previousScore

|||| Replay a full list of points, if the game ends, the remaining points are discarded
replay : List Player ->  Either Player (x' ** y' ** Score x' y')
replay = foldlM f (_ ** (_ ** Start))
  where
    f : (a ** b ** Score a b) -> Player -> Either Player (x' ** y' ** Score x' y')
    f (_ ** _ ** s) p = maybe (Left p)
                                (pure . (\s' => (_ ** _ ** s')))
                                $ score s p

displayPoints : LTE x 3 -> String
displayPoints LTEZero = "0"
displayPoints (LTESucc LTEZero) = "15"
displayPoints (LTESucc (LTESucc LTEZero)) = "30"
displayPoints (LTESucc (LTESucc (LTESucc LTEZero))) = "40"

displayScore : Score x y -> String
displayScore {x = Z} {y = Z} _ = "love"
displayScore {x = S (S (S Z))} {y = S (S (S Z))} _ = "deuce"
displayScore {x} {y} _ = case (isLTE x 3, isLTE y 3) of
  (Yes prfX,   Yes prfY)   => concat [displayPoints prfX
                                     , " - "
                                     , displayPoints prfY
                                     ]
  _                        => case compare x y of
                                   LT => "advantage Player2"
                                   EQ => "deuce"
                                   GT => "advantage Player1"

-- Tests

-- Helpers (to handle Ordering in proofs)

compareToSuccIsLT : (x : Nat) -> LT = compare x (S x)
compareToSuccIsLT Z = Refl
compareToSuccIsLT (S k) = compareToSuccIsLT k

compareSameIsEq : (x : Nat) -> EQ = compare x x
compareSameIsEq Z = Refl
compareSameIsEq (S k) = compareSameIsEq k

compareToPredIsGT : (x : Nat) -> GT = compare (S x) x
compareToPredIsGT Z = Refl
compareToPredIsGT (S k) = compareToPredIsGT k

LTnotEQ : (LT = EQ) -> Void
LTnotEQ Refl impossible

LTnotGT : (LT = GT) -> Void
LTnotGT Refl impossible

EQnotGT : (EQ = GT) -> Void
EQnotGT Refl impossible

DecEq Ordering where
  decEq LT LT = Yes Refl
  decEq LT EQ = No LTnotEQ
  decEq LT GT = No LTnotGT
  decEq EQ LT = No (negEqSym LTnotEQ)
  decEq EQ EQ = Yes Refl
  decEq EQ GT = No EQnotGT
  decEq GT LT = No (negEqSym LTnotGT)
  decEq GT EQ = No (negEqSym EQnotGT)
  decEq GT GT = Yes Refl


-- Scores

replayEmptyListGivesStart : Right (0 ** 0 ** Start) = replay []
replayEmptyListGivesStart = Refl

testLoveGame : (p : Player) -> Left p = replay (replicate 4 p)
testLoveGame Player1 = Refl
testLoveGame Player2 = Refl

opponent : Player -> Player
opponent Player1 = Player2
opponent Player2 = Player1

testCantWinFromDeuce : (p : Player) -> True = isRight (replay (take 11 $ cycle [p, opponent p]))
testCantWinFromDeuce Player1 = Refl
testCantWinFromDeuce Player2 = Refl

gainWith2PointsFromDeuce : (p : Player) -> Left p = replay ((take 10 $ cycle [Player1, Player2]) <+> replicate 2 p)
gainWith2PointsFromDeuce Player1 = Refl
gainWith2PointsFromDeuce Player2 = Refl


-- Display

displayStartIsLove : "love" = displayScore Start
displayStartIsLove = Refl

display1stWinnerGot15 : (s : Score 1 0) -> "15 - 0" = displayScore s
display1stWinnerGot15 _ = Refl

displayDeuce : (x : Nat) -> (s : Score (3 + x) (3 + x)) -> "deuce" = displayScore s
displayDeuce Z _ = Refl
displayDeuce (S k) s with (compare k k) proof p
  displayDeuce (S k) s | LT = void (LTnotEQ (rewrite compareSameIsEq k in p))
  displayDeuce (S k) s | EQ = Refl
  displayDeuce (S k) s | GT = void (negEqSym EQnotGT (rewrite compareSameIsEq k in p))

displayAdvantageP1 : (x : Nat) -> (s : Score (S (3 + x)) (3 + x)) -> "advantage Player1" = displayScore s
displayAdvantageP1 Z _     = Refl
displayAdvantageP1 (S k) _ with (compare (S k) k) proof p
  displayAdvantageP1 (S k) _ | LT = void (LTnotGT (rewrite compareToPredIsGT k in p))
  displayAdvantageP1 (S k) _ | EQ = void (EQnotGT (rewrite compareToPredIsGT k in p))
  displayAdvantageP1 (S k) _ | GT = Refl

displayAdvantageP2 : (x : Nat) -> (s : Score (3 + x) (S (3 + x))) -> "advantage Player2" = displayScore s
displayAdvantageP2 Z _     = Refl
displayAdvantageP2 (S k) _ with (compare k (S k)) proof p
  displayAdvantageP2 (S k) _ | LT = Refl
  displayAdvantageP2 (S k) _ | EQ = void (negEqSym LTnotEQ (rewrite compareToSuccIsLT k in p))
  displayAdvantageP2 (S k) _ | GT = void (negEqSym LTnotGT (rewrite compareToSuccIsLT k in p))