Create a gist now

Instantly share code, notes, and snippets.

@berewt /TennisDT.idr
Last active May 26, 2018

Embed
Tennis Kata, in Idris, with Dependent types.
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))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment