
   0 | module Utils.Misc
   1 | 
   2 | import Data.Bits
   3 | import Data.DPair
   4 | import Data.Fin
   5 | import Data.List
   6 | import Data.Nat
   7 | import Data.Nat.Division
   8 | import Data.Stream
   9 | import Data.Vect
  10 | import Data.List1
  11 | import Data.Fin.Extra
  12 | import Syntax.WithProof
  13 | 
  14 | ||| primarily used for `hack_*` functions for hacking open ADTs into sums ^/v products
  15 | public export
  16 | Eithers : List Type -> Type
  17 | Eithers [] = Void
  18 | Eithers (x :: []) = x
  19 | Eithers (x :: xs) = Either x (Eithers xs)
  20 | 
  21 | public export
  22 | kill_linear : Void -> (1 _ : a) -> s
  23 | kill_linear x = void x
  24 | 
  25 | public export
  26 | pair_to_list : (a, a) -> List a
  27 | pair_to_list (x1, x2) = [x1, x2]
  28 | 
  29 | public export
  30 | vect_to_pair : Vect 2 a -> (a, a)
  31 | vect_to_pair [x1, x2] = (x1, x2)
  32 | 
  33 | public export
  34 | pair_to_vect : (a, a) -> Vect 2 a
  35 | pair_to_vect (x1, x2) = [x1, x2]
  36 | 
  37 | public export
  38 | from_vect : Vect 1 a -> a
  39 | from_vect [x] = x
  40 | 
  41 | public export
  42 | to_vect : a -> Vect 1 a
  43 | to_vect x = [x]
  44 | 
  45 | ||| strict version of `(&&)`
  46 | public export
  47 | s_and : Bool -> Bool -> Bool
  48 | s_and True False = False
  49 | s_and True True = True
  50 | s_and False False = False
  51 | s_and False True = False
  52 | 
  53 | public export
  54 | mmod : Integer -> (m : Nat) -> {auto 0 ok : NonZero m} -> Nat
  55 | mmod n m =
  56 |   let m' = natToInteger m
  57 |   in integerToNat ((m' + n `mod` m') `mod` m')
  58 | 
  59 | public export
  60 | mod': Integer -> Integer -> Integer
  61 | mod' _ 0 = 0
  62 | mod' n m = (m + n `mod` m) `mod` m
  63 | 
  64 | public export
  65 | s_eq : (Bits b, Eq b) => Vect n b -> Vect n b -> Bool
  66 | s_eq a b = (zeroBits ==) $ foldr (.|.) zeroBits $ zipWith xor a b
  67 | 
  68 | public export
  69 | s_eq' : (Bits b, Eq b) => List b -> List b -> Bool
  70 | s_eq' a b = (length a == length b) `s_and` ((zeroBits ==) $ foldr (.|.) zeroBits $ zipWith xor a b)
  71 | 
  72 | public export
  73 | vect_zip_with : {n : Nat} -> {m : Nat} -> (a -> b -> c) -> Vect n a -> Vect m b -> Vect (minimum n m) c
  74 | vect_zip_with {n=0} {m} f [] _ = []
  75 | vect_zip_with {n} {m=0} f _ [] = rewrite minimumZeroZeroLeft n in []
  76 | vect_zip_with f (x::xs) (y::ys) = f x y :: vect_zip_with f xs ys
  77 | 
  78 | public export
  79 | group : (n : Nat) -> (m : Nat) -> Vect (n * m) a -> Vect n (Vect m a)
  80 | group Z     _ _  = []
  81 | group (S n) m xs = let (l, r) = splitAt m xs in l :: group n m r
  82 | 
  83 | public export
  84 | chunk : Nat -> List a -> List (List a)
  85 | chunk _ [] = []
  86 | chunk n xs = (take n xs) :: (chunk n (drop n xs))
  87 | 
  88 | -- https://gist.github.com/buzden/afc798fd2b01388f1626ae58c6ab8548
  89 | public export
  90 | group' : (n : Nat) -> (m : Nat) -> Vect (n * m) a -> Vect m (Vect n a)
  91 | group' n m xs = group m n $ rewrite multCommutative m n in xs
  92 | 
  93 | -- https://gist.github.com/buzden/afc798fd2b01388f1626ae58c6ab8548
  94 | -- to prove that, say given `xs : Vect (n + m) a`, can be splitted at index `n` into `l` and `r` (the (0 _ : splitAt n xs = (l, r)) part), and then be concatenated back into xs
  95 | export
  96 | split_at_concat_rev : (n : Nat) -> (xs : Vect (n + m) a) -> {0 l : Vect n a} -> {0 r : Vect m a} -> (0 _ : splitAt n xs = (l, r)) -> l ++ r = xs
  97 | split_at_concat_rev Z _ Refl = Refl
  98 | split_at_concat_rev (S n) (x :: xs) {l} prf with (splitAt n xs) proof sprf
  99 |   split_at_concat_rev (S n) (x :: xs) {l = x :: l} Refl | (l, _) = cong (x ::) $ split_at_concat_rev n xs sprf
 100 | 
 101 | -- https://gist.github.com/buzden/afc798fd2b01388f1626ae58c6ab8548
 102 | public export
 103 | concat_group_id : (n : Nat) -> (m : Nat) -> (v : Vect (n * m) a) -> concat (group n m v) = v
 104 | concat_group_id Z     _ [] = Refl
 105 | concat_group_id (S n) m xs with (splitAt m xs) proof prf
 106 |   _ | (l, r) = rewrite concat_group_id n m r in split_at_concat_rev m xs prf
 107 | 
 108 | pow_mod' : Integer -> Integer -> Integer -> Integer -> Integer
 109 | pow_mod' n x y m =
 110 |   if y == 0
 111 |      then n
 112 |      else let n' = (n * x) `mod` m
 113 |               y' = shiftR y 1
 114 |               x' = (x * x) `mod` m
 115 |           in pow_mod' (if testBit y 0 then n' else n) x' y' m
 116 | 
 117 | public export
 118 | pow_mod : Integer -> Integer -> Integer -> Integer
 119 | pow_mod x y m = pow_mod' 1 (x `mod'` m) (y `mod'` m) m
 120 | 
 121 | mul_mod' : Integer -> Integer -> Integer -> Integer -> Integer
 122 | mul_mod' n x y m =
 123 |   if y == 0
 124 |      then n
 125 |      else let n' = (n + x) `mod` m
 126 |               y' = shiftR y 1
 127 |               x' = (x * 2) `mod` m
 128 |           in mul_mod' (if testBit y 0 then n' else n) x' y' m
 129 | 
 130 | public export
 131 | mul_mod : Integer -> Integer -> Integer -> Integer
 132 | mul_mod x y m = mul_mod' 0 (x `mod'` m) (y `mod'` m) m
 133 | 
 134 | public export
 135 | quot_rem : Integer -> Integer -> (Integer, Integer)
 136 | quot_rem val d =
 137 |   let dividend = if d < 0 then -(val `div` abs d) else val `div` d
 138 |       remainder = abs (val - dividend * d)
 139 |   in (dividend, remainder)
 140 | 
 141 | public export
 142 | gcd' : Integer -> Integer -> Integer
 143 | gcd' a 0 = a
 144 | gcd' a b = gcd' b (a `mod` b)
 145 | 
 146 | public export
 147 | are_coprimes : Integer -> Integer -> Bool
 148 | are_coprimes x y = (gcd' x y) == 1
 149 | 
 150 | -- Extended Euclidean Algorithm
 151 | -- Only valid when gcd(a, b) = 1
 152 | public export
 153 | extended_gcd : Integer -> Integer -> (Integer, Integer)
 154 | extended_gcd a 0 = (1, 0)
 155 | extended_gcd a b =
 156 |   let (q, r) = quot_rem a b
 157 |       (s, t) = extended_gcd b r
 158 |   in (t, s - q * t)
 159 | 
 160 | -- Only valid when gcd(a, b) = 1
 161 | public export
 162 | inv_mul_mod : Integer -> Integer -> Integer
 163 | inv_mul_mod a m =
 164 |   let (x, y) = extended_gcd a m
 165 |   in mod' x m
 166 | 
 167 | public export
 168 | forM : Applicative f => (n : Nat) -> (f b) -> f (Vect n b)
 169 | forM n f = for (the (Vect n (Fin n)) range) (const f)
 170 | 
 171 | utf8_bytelen : Bits8 -> Maybe (Bits8, Nat)
 172 | utf8_bytelen x =
 173 |   if (x .&. 0b01111111) == x then Just (x, 0) -- ascii
 174 |     else if (shiftR x 5) == 0b110   then Just (x .&. 0b0011111, 1)
 175 |     else if (shiftR x 4) == 0b1110  then Just (x .&. 0b0001111, 2)
 176 |     else if (shiftR x 3) == 0b11110 then Just (x .&. 0b0000111, 3)
 177 |     else Nothing
 178 | 
 179 | utf8_unmask : Bits8 -> Maybe Bits8
 180 | utf8_unmask x = const (x .&. 0b00111111) <$> guard (shiftR x 6 == 0b10)
 181 | 
 182 | utf8_pushbits : Integer -> List Bits8 -> Integer
 183 | utf8_pushbits acc [] = acc
 184 | utf8_pushbits acc (x::xs) = utf8_pushbits ((shiftL acc 6) .|. (cast x)) xs
 185 | 
 186 | public export
 187 | utf8_decode : List Bits8 -> Maybe String
 188 | utf8_decode = go []
 189 |   where
 190 |     go : List Char -> List Bits8 -> Maybe String
 191 |     go acc [] = Just $ pack $ reverse acc
 192 |     go acc (x :: xs) = do
 193 |       (x, l) <- utf8_bytelen x
 194 |       let (y,ys) = splitAt l xs
 195 |       guard (length y == l)
 196 |       y <- traverse utf8_unmask y
 197 |       let c = utf8_pushbits (cast x) y
 198 |       go ((cast c) :: acc) ys
 199 | 
 200 | public export
 201 | stream_concat : Foldable t => Stream (t a) -> Stream a
 202 | stream_concat = go . map toList
 203 |   where
 204 |     go : Stream (List a) -> Stream a
 205 |     go ([] :: ys) = stream_concat ys
 206 |     go ((x :: xs) :: ys) = x :: stream_concat (xs :: ys)
 207 | 
 208 | public export
 209 | ok_minus : (n : Nat) -> (m : Nat) -> LTE m n -> Nat
 210 | ok_minus n Z LTEZero = n
 211 | ok_minus (S n) (S m) (LTESucc wit) = ok_minus n m wit
 212 | 
 213 | namespace List
 214 |   public export
 215 |   enumerate : Nat -> List a -> List (Nat, a)
 216 |   enumerate n [] = []
 217 |   enumerate n (x :: xs) = (n, x) :: enumerate (S n) xs
 218 | 
 219 | namespace Vect
 220 |   public export
 221 |   replace_vect : (0 _ : n = m) -> Vect n a -> Vect m a
 222 |   replace_vect prf input = rewrite sym prf in input
 223 | 
 224 |   public export
 225 |   cycle : Vect (S n) a -> Stream a
 226 |   cycle xs = go xs
 227 |     where
 228 |     go : Vect i a -> Stream a
 229 |     go [] = go xs
 230 |     go (z :: zs) = z :: go zs
 231 | 
 232 | namespace Stream
 233 |   public export
 234 |   prepend : List a -> Stream a -> Stream a
 235 |   prepend [] ys = ys
 236 |   prepend (x :: xs) ys = x :: prepend xs ys
 237 | 
 238 |   public export
 239 |   duplicate : Stream a -> Stream (Stream a)
 240 |   duplicate (x :: xs) = (x :: xs) :: duplicate xs
 241 | 
 242 |   public export
 243 |   split : (n : Nat) -> Stream a -> (Vect n a, Stream a)
 244 |   split Z xs = ([], xs)
 245 |   split (S n) (v :: xs) = let (vs, xs') = split n xs in (v :: vs, xs')
 246 | 
 247 |   public export
 248 |   chunk : (n : Nat) -> Stream a -> Stream (Vect n a)
 249 |   chunk n xs = let (y, ys) = split n xs in y :: chunk n ys
 250 | 
 251 | public export
 252 | lte_plus_left : (a : _) -> LTE (a + b) c -> LTE b c
 253 | lte_plus_left Z x = x
 254 | lte_plus_left (S k) x = lte_plus_left k (lteSuccLeft x)
 255 | 
 256 | public export
 257 | maybe_to_either : Maybe a -> Lazy b -> Either b a
 258 | maybe_to_either Nothing b = Left $ force b
 259 | maybe_to_either (Just a) _ = Right a
 260 | 
 261 | public export
 262 | init' : List a -> List a
 263 | init' [] = []
 264 | init' (x :: xs) = init (x :: xs)
 265 | 
 266 | public export
 267 | uncons1 : List1 a -> (List a, a)
 268 | uncons1 lst = (init lst, last lst)
 269 | 
 270 | public export
 271 | splitAt : (n : Nat) -> Stream a -> (Vect n a, Stream a)
 272 | splitAt n s = (take n s, drop n s)
 273 | 
 274 | public export
 275 | zeros : {n : Nat} -> Vect n Bits8
 276 | zeros = map (const 0) Fin.range
 277 | 
 278 | public export
 279 | splitLastAt1 : (n : Nat) -> List a -> Maybe (List1 a, Vect n a)
 280 | splitLastAt1 n v = do
 281 |   let m = minus (length v) n
 282 |   let (a, b) = splitAt m v
 283 |   a' <- fromList a
 284 |   b' <- exactLength n $ fromList b
 285 |   pure (a', b')
 286 | 
 287 | public export
 288 | modFinNZ : Nat -> (b : Nat) -> NonZero b -> Fin b
 289 | modFinNZ a b prf = let x = boundModNatNZ a b prf in natToFinLTE (modNatNZ a b prf) x
 290 | 
 291 | public export
 292 | collapse_ordering : List Ordering -> Ordering
 293 | collapse_ordering (LT :: xs) = LT
 294 | collapse_ordering (GT :: xs) = GT
 295 | collapse_ordering (EQ :: xs) = collapse_ordering xs
 296 | collapse_ordering [] = EQ
 297 | 
 298 | public export
 299 | pad_zero : Nat -> List Bits8 -> List Bits8
 300 | pad_zero Z a = a
 301 | pad_zero (S n) a =
 302 |   let l = length a
 303 |       l = minus ((S n) * (divCeilNZ l (S n) SIsNonZero)) l
 304 |   in a <+> replicate l 0
 305 | 
 306 | public export
 307 | splitAtExact : (n : Nat) -> List a -> Maybe (Vect n a, List a)
 308 | splitAtExact n list =
 309 |   let (a, b) = splitAt n list
 310 |   in (, b) <$> exactLength n (fromList a)
 311 |