tennis-kata.idr

module TennisKata

%default total

-- Data types

data Point = Love | Fiftheen | Thirteen | Fourteen

isFourteen : Point -> Bool
isFourteen Fourteen = True
isFourteen _        = False

nextPoint : (p:Point) -> { auto prf : isFourteen p = False } -> Point
nextPoint Love     = Fiftheen
nextPoint Fiftheen = Thirteen
nextPoint Thirteen = Fourteen

data Player = Player1 | Player2

Eq Player where
   (==) Player1 Player1 = True
   (==) Player2 Player2 = True
   (==) _       _       = False

data Score : Type where
     Played    : (p1:Point) -> (p2:Point) -> { auto prf : (isFourteen p1) && (isFourteen p2) = False } -> Score
     Deuce     : Score
     Advantage : Player -> Score

-- Basic Predicates

canWin : Score -> Player -> Bool
canWin (Played Fourteen p2) Player1 = True
canWin (Played p1 Fourteen) Player2 = True
canWin (Advantage p1)       p2      = p1 == p2
canWin _                    _       = False

winPoint : (s:Score) -> (p:Player) -> { auto prf : canWin s p = False } -> Score
winPoint Deuce                      p       = Advantage p
winPoint (Played Thirteen Fourteen) Player1 = Deuce
winPoint (Played Fourteen Thirteen) Player2 = Deuce
winPoint (Played p1 p2)             Player1 = Played (nextPoint p1) p2
winPoint (Played p1 p2)             Player2 = Played p1 (nextPoint p2)

winGame : (s:Score) -> (p:Player) -> { auto prf : canWin s p = True } -> Player
winGame _ p = p

-- Tests corner

player1CanWinEasily : canWin (Played Fourteen Thirteen) Player1 = True
player1CanWinEasily = Refl

aPlayerCanWin : (p:Player) -> canWin (Advantage p) p = True
aPlayerCanWin Player1 = Refl
aPlayerCanWin Player2 = Refl

player2CanWinEasily : canWin (Played Thirteen Fourteen) Player2 = True
player2CanWinEasily = Refl