-
Notifications
You must be signed in to change notification settings - Fork 3
/
Idris 2048.idr
172 lines (146 loc) · 6.23 KB
/
Idris 2048.idr
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
import Effects
import Effect.Exception
import Effect.StdIO
import Effect.Random
import Effect.System
import Data.Vect
%default total
--------------------------------------------------------------------------------
-- Operations on individual rows
--------------------------------------------------------------------------------
||| Fills in an array
fillIn : LTE n m -> a -> Vect n a -> Vect m a
fillIn LTEZero c [] = replicate _ c
fillIn (LTESucc w) c (x :: xs) = x :: (fillIn w c xs)
||| Filters out the Nothings from a vector of maybes.
|||
||| Takes a vector of length n with elements of type Maybe a
||| and returns the dependent pair (m ** (Vect m a, LTE m n)) where
||| m is the new length, Vect m a is the filtered list, and LTE m n
||| is a prove that m <= n, that is, that the new list has length
||| less than or equal to the original list.
filterMaybes : Vect n (Maybe a) -> (m ** (Vect m a, LTE m n))
filterMaybes [] = (Z ** ([], LTEZero))
filterMaybes (Just x :: xs) = let (_ ** (ys, w)) = filterMaybes xs in
(_ ** ((x :: ys), LTESucc w))
filterMaybes (Nothing :: xs) = let (_ ** (ys, w)) = filterMaybes xs in
(_ ** (ys, lteSuccRight w))
||| The collapsing of pairs operation of the 2048 game.
|||
||| Takes a vector of elements of type a, and performs the "collapsing"
||| operation of the 2048 game. This takes adjacent pairs, and if they
||| are equal, combines them into a single element with double the value.
||| Returns a vector of length m and proof that m <= n.
collapsePairs : (Num a, Eq a) => Vect n a -> (m ** (Vect m a, LTE m n))
collapsePairs (x::x'::xs) =
if x == x' then
let (_ ** (ys, w)) = collapsePairs xs in (_ ** ((2 * x) :: ys, lteSuccRight (LTESucc w)))
else
let (_ ** (ys, w)) = collapsePairs (x' :: xs) in (_ ** (x :: ys, LTESucc w))
collapsePairs (x::[]) = (_ ** ([x], LTESucc LTEZero))
collapsePairs [] = (_ ** ([], LTEZero))
||| The basic row operation of the 2048 game.
|||
||| Combines the operations of filterMaybes and collapsePairs,
||| and combines their proofs, and transitivity of <=, to
||| prove that the result of applying both operations is
||| a shorter vector than the original. This proof is used
||| to apply the fillIn function.
basicRowOperation : (Eq a, Num a) => Vect n (Maybe a) -> Vect n (Maybe a)
basicRowOperation xs = let (m ** (ys, w)) = filterMaybes xs in let
(l ** (zs, wPrime)) = collapsePairs ys in
(fillIn (lteTransitive wPrime w) Nothing (map Just zs))
--------------------------------------------------------------------------------
-- Operations on the game board
--------------------------------------------------------------------------------
||| Takes the transpose of a rectangular array
transposeArray : Vect n (Vect m a) -> Vect m (Vect n a)
transposeArray [] = replicate _ []
transposeArray (x::xs) = zipWith (::) x (transposeArray xs)
||| Flattens a rectangular array
flattenArray : Vect n (Vect m a) -> Vect (n * m) a
flattenArray Nil = Nil
flattenArray (x::xs) = x ++ (flattenArray xs)
||| Splits an array
split' : Vect (plus n m) a -> (Vect n a, Vect m a)
split' {n=Z} xs = ([], xs)
split' {n=(S k)}{m=l} (x::xs) = let (ys, zs) = split' {n=k}{m=l} xs in
(x::ys, zs)
||| Unflattens an array
unFlattenArray : Vect (n * m) a -> Vect n (Vect m a)
unFlattenArray {n=Z} Nil = Nil
unFlattenArray {n=(S k)}{m=l} xs = let (ys, zs) = split' {n=l}{m=k*l} xs in
(ys :: (unFlattenArray zs))
||| Find the indices of all elements of a vector that satisfy some test
findIndicesFin : (a -> Bool) -> Vect n a -> List (Fin n)
findIndicesFin f [] = []
findIndicesFin f (x::xs) = let tail = (map FS (findIndicesFin f xs)) in
if f x then (FZ :: tail) else tail
--------------------------------------------------------------------------------
-- Display functions
--------------------------------------------------------------------------------
showValue : Show a => Maybe a -> String
showValue Nothing = "...."
showValue (Just x) = pack (List.take 4 (unpack ((show x) ++ "....")))
showRow : Show a => Vect n (Maybe a) -> String
showRow [] = ""
showRow (x::xs) = (showValue x) ++ " " ++ (showRow xs)
showBoard : Show a => Vect m (Vect n (Maybe a)) -> String
showBoard [] = ""
showBoard (x::xs) = (showRow x) ++ "\n" ++ (showBoard xs)
--------------------------------------------------------------------------------
-- High level game logic
--------------------------------------------------------------------------------
Board : Type
Board = Vect 4 (Vect 4 (Maybe Int))
data Direction = Left | Right | Up | Down
partial
move : (Eq a, Num a) => Direction -> Vect m (Vect n (Maybe a)) -> Vect m (Vect n (Maybe a))
move Left xs = map basicRowOperation xs
move Right xs = map (reverse . basicRowOperation . reverse) xs
move Up xs = (transposeArray . (move Left) . transposeArray) xs
move Down xs = (transposeArray . (move Right) . transposeArray) xs
addRandomPiece : Board -> {[RND, EXCEPTION String]} Eff Board
addRandomPiece arr = case !(rndSelect indices) of
Nothing => raise "Game Over"
Just idx => pure (unFlattenArray (replaceAt idx (Just 2) flattened))
where
flattened : Vect 16 (Maybe Int)
flattened = flattenArray arr
indices : List (Fin 16)
indices = findIndicesFin isNothing flattened
data UserAction = Quit | Invalid | Move Direction
getAction : Char -> UserAction
getAction 'a' = Move Left
getAction 'd' = Move Right
getAction 'w' = Move Up
getAction 's' = Move Down
getAction 'x' = Quit
getAction _ = Invalid
partial
mainLoop : Board -> {[RND, STDIO, EXCEPTION String]} Eff (Board)
mainLoop b = do putStrLn (showBoard b)
c <- getChar
performAction (getAction c)
where
partial
performAction : UserAction -> {[RND, STDIO, EXCEPTION String]} Eff (Board)
performAction Quit = raise "You have quit"
performAction Invalid = mainLoop b
performAction (Move dir) = let b' = move dir b in
if b == b' then
mainLoop b'
else
do
b'' <- addRandomPiece b'
mainLoop b''
partial
startGame : { [RND, STDIO, SYSTEM, EXCEPTION String] } Eff ()
startGame = do
srand !time
initialBoard <- addRandomPiece (replicate _ (replicate _ Nothing))
mainLoop initialBoard
pure ()
partial
main : IO ()
main = run startGame