0 | module Util
  1 |
  2 | import public Util.Eff as Util
  3 |
  4 | import Data.String
  5 | import public Data.Vect
  6 | import public Data.List.Lazy
  7 |
  8 | public export
  9 | Coord : (rows, cols : Nat) -> Type
 10 | Coord rows cols = (Fin (S rows),  Fin (S cols))
 11 |
 12 | export
 13 | allCords : {rows, cols : Nat} -> LazyList (Coord rows cols)
 14 | allCords = concat . map row $ all
 15 |   where
 16 |     all : {n : Nat} -> LazyList (Fin (S n))
 17 |     all = FZ :: all' FZ
 18 |       where
 19 |         all' : {n : Nat} -> (acc : Fin (S n)) -> LazyList (Fin (S n))
 20 |         all' acc =
 21 |           if acc < last
 22 |             then finS acc :: all' (finS acc)
 23 |             else []
 24 |     row : Fin (S rows) -> LazyList (Coord rows cols)
 25 |     row r = map (\c => (r, c)) all
 26 |
 27 | ||| Attempt to step a coordinate in a given direction
 28 | export
 29 | step : {rows, cols : Nat} -> (input : Coord rows cols) -> (direction : (Integer, Integer))
 30 |      -> Maybe (Coord rows cols)
 31 | step (row, col) (d_row, d_col) = do
 32 |   let (row, col) = (finToInteger row, finToInteger col)
 33 |   row <- integerToFin (row + d_row) (S rows)
 34 |   col <- integerToFin (col + d_col) (S cols)
 35 |   pure (row, col)
 36 |
 37 | public export
 38 | Grid : (rows, cols : Nat) -> (a : Type) -> Type
 39 | Grid rows cols a = Vect (S rows) (Vect (S cols) a)
 40 |
 41 | namespace Grid
 42 |   export
 43 |   index : Coord rows cols -> Grid rows cols a -> a
 44 |   index (row, col) xs =
 45 |     let row' = row `index` xs
 46 |     in col `index` row'
 47 |
 48 |   export
 49 |   replaceAt : Coord rows cols -> a -> Grid rows cols a -> Grid rows cols a
 50 |   replaceAt (row, col) value xs =
 51 |     let row' = row `index` xs
 52 |         row'' = replaceAt col value row'
 53 |     in replaceAt row row'' xs
 54 |
 55 |   export
 56 |   flat : {rows, cols : Nat} -> Grid rows cols a -> LazyList (Coord rows cols, a)
 57 |   flat xs =
 58 |     -- TODO: Lazy allFins?
 59 |     let rs : LazyList _ = fromList (allFins (S rows))
 60 |         cs : LazyList _ = fromList (allFins (S cols))
 61 |     in concat . map fixRow . zip rs . map (zip cs) . vectToLazy . map vectToLazy $ xs
 62 |     where
 63 |       vectToLazy : Vect n e -> LazyList e
 64 |       vectToLazy [] = []
 65 |       vectToLazy (x :: xs) = x :: vectToLazy xs
 66 |       fixRow : (e1, LazyList (e2, e3)) -> LazyList ((e1, e2), e3)
 67 |       fixRow (x, xs) = map (\(y, z) => ((x, y), z)) xs
 68 |
 69 |   export
 70 |   const : {rows, cols : Nat} -> a -> Grid rows cols a
 71 |   const x =
 72 |     let row = replicate (S cols) x
 73 |     in replicate (S rows) row
 74 |
 75 |   export
 76 |   mapGrid : {rows, cols : Nat} -> (f : a -> b) -> Grid rows cols a -> Grid rows cols b
 77 |   mapGrid f xs = map (map f) xs
 78 |
 79 | export
 80 | stringTo2D : String -> Maybe (rows : Nat ** cols : Nat ** Grid rows cols Char)
 81 | stringTo2D str = do
 82 |   let xs = map (unpack . trim) . lines . trim $ str
 83 |   S cols <- map length . head' $ xs
 84 |     | _ => Nothing
 85 |   xs <- traverse (toVect (S cols)) xs
 86 |   S rows <- pure $ length xs
 87 |     | _ => Nothing
 88 |   xs <- toVect (S rows) xs
 89 |   Just (rows ** cols ** xs)
 90 |
 91 | export
 92 | gridToString : Grid rows cols Char -> String
 93 | gridToString xs =
 94 |   joinBy "\n" . toList . map (pack . toList) $ xs
 95 |
 96 | export
 97 | lazyTimes : (times : Nat) -> (f : seed -> seed) -> seed -> LazyList seed
 98 | lazyTimes 0 f x = []
 99 | lazyTimes (S k) f x = x :: lazyTimes k f (f x)
100 |
101 | export
102 | lazyRange : Num n => (limit : Nat) -> LazyList n
103 | lazyRange limit = lazyTimes limit (+1) 0
104 |
105 | export
106 | lazyRange' : Ord n => Num n => (lower, upper : n) -> LazyList n
107 | lazyRange' lower upper =
108 |   if lower <= upper
109 |     then lower :: lazyRange' (lower + 1) upper
110 |     else []
111 |
112 | export
113 | allPairs : LazyList a -> LazyList (a, a)
114 | allPairs [] = []
115 | allPairs (x :: xs) =
116 |   let here = map (x,) xs
117 |   in concat (the (LazyList _) [here, allPairs xs])
118 |
119 | export
120 | cartProd : LazyList a -> LazyList (a, a)
121 | cartProd x = cartProd' x x
122 |   where
123 |   cartProd' : (orig, acc : LazyList a) -> (LazyList (a, a))
124 |   cartProd' orig [] = []
125 |   cartProd' orig (y :: xs) = map (\x => (x, y)) orig ++ cartProd' orig xs
126 |
127 |
128 | export
129 | listToVect : List a -> (len : Nat ** Vect len a)
130 | listToVect xs = (length xs ** fromList xs)
131 |
132 | export
133 | swap : (i, j : Fin (S len)) -> Vect (S len) a -> Vect (S len) a
134 | swap i j xs =
135 |   let elem_i = i `index` xs
136 |       elem_j = j `index` xs
137 |       xs = replaceAt i elem_j xs
138 |   in replaceAt j elem_i xs
139 |
140 | export
141 | doTimes : (f : a -> a) -> (times : Nat) -> a -> a
142 | doTimes f 0 x = x
143 | doTimes f (S k) x = doTimes f k (f x)
144 |
145 | public export
146 | data Direction = Up | Right | Down | Left
147 |
148 | export
149 | Eq Direction where
150 |   (==) Up Up = True
151 |   (==) Right Right = True
152 |   (==) Down Down = True
153 |   (==) Left Left = True
154 |   (==) _ _ = False
155 |
156 | export
157 | Show Direction where
158 |   show Up = "Up"
159 |   show Right = "Right"
160 |   show Down = "Down"
161 |   show Left = "Left"
162 |
163 | public export
164 | turns : Direction -> List Direction
165 | turns Up = [Left, Right]
166 | turns Right = [Up, Down]
167 | turns Down = [Right, Left]
168 | turns Left = [Down, Up]
169 |
170 | public export
171 | directionToStep : Direction -> (Integer, Integer)
172 | directionToStep Up = (-1, 0)
173 | directionToStep Right = (0, -1)
174 | directionToStep Down = (1, 0)
175 | directionToStep Left = (0, 1)
176 |
177 | public export
178 | directions : List (Maybe Direction)
179 | directions = Nothing :: map Just [Up, Down, Left, Right]
180 |
181 | public export
182 | data ShowString = Show String
183 |
184 | export
185 | Show ShowString where show (Show x) = x
186 |