0 | module Main
  1 |
  2 | import System
  3 | import System.Random
  4 |
  5 | import Data.Matrix
  6 | import Data.String
  7 | import Data.Fin
  8 | import Data.Nat
  9 | import Data.List
 10 | import Control.App
 11 | import Control.App.Console
 12 | import Data.Vect
 13 |
 14 | Tile : Type
 15 | Tile = Int
 16 |
 17 | record  GameField (rows: Nat) (cols: Nat) where
 18 |   constructor MkGameField
 19 |   gameField : Matrix rows cols Tile
 20 |
 21 | prettyShowRow : (Vect cols Int) -> String
 22 | prettyShowRow vect= (concat $ map (\el => "\t" ++ show el)vect) ++ "\n\n\n"
 23 |
 24 | prettyShow : GameField rows cols -> String
 25 | prettyShow (MkGameField matrix) = concat $ map prettyShowRow $ (toVects matrix) 
 26 |
 27 |
 28 | Show (GameField r c) where
 29 |   show s = prettyShow s
 30 |
 31 | Eq (GameField r c) where
 32 |   (MkGameField s1) == (MkGameField s2) = s1 == s2
 33 |
 34 | toMatrix :  GameField rows cols -> Matrix rows cols Int
 35 | toMatrix (MkGameField m) = m
 36 |
 37 | up : Vect (len) Int -> Vect (len) Int
 38 | up [] = []
 39 | up (0 :: as) = snoc (up as) 0
 40 | up (a :: as) = a :: up as
 41 |
 42 | join : Vect len Int -> Vect len Int
 43 | join (x :: y :: as) = if x == y then snoc ([x + y] ++ join as) 0  else (x :: join (y :: as))
 44 | join (x :: as) = x :: join as
 45 | join [] = []
 46 |
 47 | moveLeft :  GameField rows cols -> GameField rows cols
 48 | moveLeft (MkGameField m) = MkGameField $ fromVects $ map (join . up) $ toVects m
 49 |
 50 | moveRight : GameField rows cols-> GameField rows cols
 51 | moveRight (MkGameField m) = MkGameField $ fromVects $ (map (reverse . join . up . reverse)) $ toVects m
 52 |
 53 | moveUp : {rows : Nat} -> {cols : Nat} -> GameField rows cols-> GameField rows cols
 54 | moveUp  (MkGameField m) = MkGameField $ transpose $ toMatrix $ moveLeft $  MkGameField $ transpose  m
 55 |
 56 |
 57 | moveDown : {rows : Nat} -> {cols : Nat} -> GameField rows cols-> GameField rows cols
 58 | moveDown  (MkGameField m) = MkGameField $ transpose $ toMatrix $ moveRight $  MkGameField $ transpose  m
 59 |
 60 | -- 获取可以使用的titles
 61 | getFreeTiles : {rows: Nat} -> {cols: Nat} -> GameField rows cols -> List (Fin rows, Fin cols)
 62 | getFreeTiles (MkGameField matrix) = findIndices {rows} {cols} (== 0) matrix
 63 |
 64 | addTileToRandomPos : {rows: Nat} -> {cols: Nat} -> GameField rows cols -> IO (GameField rows cols)
 65 | addTileToRandomPos game@(MkGameField matrix) = do
 66 |   let freeTiles = getFreeTiles game 
 67 |   it <- rndFin $ length freeTiles
 68 |   case getAt (finToNat it) freeTiles of
 69 |     Nothing => pure game
 70 |     Just (r,c ) => pure $ MkGameField $ replaceAt r c 2 matrix
 71 |
 72 |
 73 | hasAvailableMoves : GameField rows cols -> Bool
 74 | hasAvailableMoves game = True
 75 |
 76 | gameLoop :  {rows: Nat} -> {cols: Nat} -> GameField rows cols ->  App Init ()
 77 | gameLoop gameField = do
 78 |     gameNext <- primIO $ addTileToRandomPos gameField
 79 |     performInput gameNext
 80 |     where
 81 |       mutual
 82 |         performInput : GameField rows cols -> App Init ()
 83 |         performInput gameField = do
 84 |           print gameField
 85 |           if hasAvailableMoves gameField
 86 |             then putStrLn "Your command ([l]eft, [r]ight, [u]p, [d]own, [s]top)?"
 87 |             else putStrLn "Game over. Press [s] to exit."
 88 |           putStrLn "============================================="
 89 |           input <- getLine
 90 |           case input of
 91 |             "l" => newMove moveLeft gameField
 92 |             "r" => newMove moveRight gameField
 93 |             "u" => newMove moveUp gameField
 94 |             "d" => newMove moveDown gameField
 95 |             "s" => putStrLn "stop!"
 96 |             _   => do 
 97 |               putStrLn "Invalid command!!!"
 98 |               performInput gameField
 99 |
100 |         newMove : (GameField rows cols -> GameField rows cols) -> GameField rows cols -> App Init ()
101 |         newMove moveFn gameField = do
102 |           let gameField' = moveFn gameField
103 |           if gameField /= gameField' then gameLoop gameField'
104 |                                     else performInput gameField
105 |         
106 |               
107 | app : App Init ()
108 | app = do
109 |   putStrLn "Enter the size to start the game。eg. 5"
110 |   rows' <- getLine
111 |   row <- pure $ stringToNatOrZ rows'
112 |   -- let row = 4
113 |   game <- pure $ MkGameField $ fill row row 0
114 |   gameLoop game
115 |
116 | main : IO ()
117 | main = do 
118 |   run app