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