
   0 | module Data.Byte
   1 | 
   2 | %default total
   3 | 
   4 | ||| ASCII code of '0'
   5 | public export %inline
   6 | byte_0 : Bits8
   7 | byte_0 = 48
   8 | 
   9 | ||| ASCII code of '1'
  10 | public export %inline
  11 | byte_1 : Bits8
  12 | byte_1 = 49
  13 | 
  14 | ||| ASCII code of '2'
  15 | public export %inline
  16 | byte_2 : Bits8
  17 | byte_2 = 50
  18 | 
  19 | ||| ASCII code of '3'
  20 | public export %inline
  21 | byte_3 : Bits8
  22 | byte_3 = 51
  23 | 
  24 | ||| ASCII code of '4'
  25 | public export %inline
  26 | byte_4 : Bits8
  27 | byte_4 = 52
  28 | 
  29 | ||| ASCII code of '5'
  30 | public export %inline
  31 | byte_5 : Bits8
  32 | byte_5 = 53
  33 | 
  34 | ||| ASCII code of '6'
  35 | public export %inline
  36 | byte_6 : Bits8
  37 | byte_6 = 54
  38 | 
  39 | ||| ASCII code of '7'
  40 | public export %inline
  41 | byte_7 : Bits8
  42 | byte_7 = 55
  43 | 
  44 | ||| ASCII code of '8'
  45 | public export %inline
  46 | byte_8 : Bits8
  47 | byte_8 = 56
  48 | 
  49 | ||| ASCII code of '9'
  50 | public export %inline
  51 | byte_9 : Bits8
  52 | byte_9 = 57
  53 | 
  54 | ||| ASCII code of 'a'
  55 | public export %inline
  56 | byte_a : Bits8
  57 | byte_a = 97
  58 | 
  59 | ||| ASCII code of 'b'
  60 | public export %inline
  61 | byte_b : Bits8
  62 | byte_b = 98
  63 | 
  64 | ||| ASCII code of 'c'
  65 | public export %inline
  66 | byte_c : Bits8
  67 | byte_c = 99
  68 | 
  69 | ||| ASCII code of 'd'
  70 | public export %inline
  71 | byte_d : Bits8
  72 | byte_d = 100
  73 | 
  74 | ||| ASCII code of 'e'
  75 | public export %inline
  76 | byte_e : Bits8
  77 | byte_e = 101
  78 | 
  79 | ||| ASCII code of 'f'
  80 | public export %inline
  81 | byte_f : Bits8
  82 | byte_f = 102
  83 | 
  84 | ||| ASCII code of 'g'
  85 | public export %inline
  86 | byte_g : Bits8
  87 | byte_g = 103
  88 | 
  89 | ||| ASCII code of 'h'
  90 | public export %inline
  91 | byte_h : Bits8
  92 | byte_h = 104
  93 | 
  94 | ||| ASCII code of 'i'
  95 | public export %inline
  96 | byte_i : Bits8
  97 | byte_i = 105
  98 | 
  99 | ||| ASCII code of 'j'
 100 | public export %inline
 101 | byte_j : Bits8
 102 | byte_j = 106
 103 | 
 104 | ||| ASCII code of 'k'
 105 | public export %inline
 106 | byte_k : Bits8
 107 | byte_k = 107
 108 | 
 109 | ||| ASCII code of 'l'
 110 | public export %inline
 111 | byte_l : Bits8
 112 | byte_l = 108
 113 | 
 114 | ||| ASCII code of 'm'
 115 | public export %inline
 116 | byte_m : Bits8
 117 | byte_m = 109
 118 | 
 119 | ||| ASCII code of 'n'
 120 | public export %inline
 121 | byte_n : Bits8
 122 | byte_n = 110
 123 | 
 124 | ||| ASCII code of 'o'
 125 | public export %inline
 126 | byte_o : Bits8
 127 | byte_o = 111
 128 | 
 129 | ||| ASCII code of 'p'
 130 | public export %inline
 131 | byte_p : Bits8
 132 | byte_p = 112
 133 | 
 134 | ||| ASCII code of 'q'
 135 | public export %inline
 136 | byte_q : Bits8
 137 | byte_q = 113
 138 | 
 139 | ||| ASCII code of 'r'
 140 | public export %inline
 141 | byte_r : Bits8
 142 | byte_r = 114
 143 | 
 144 | ||| ASCII code of 's'
 145 | public export %inline
 146 | byte_s : Bits8
 147 | byte_s = 115
 148 | 
 149 | ||| ASCII code of 't'
 150 | public export %inline
 151 | byte_t : Bits8
 152 | byte_t = 116
 153 | 
 154 | ||| ASCII code of 'u'
 155 | public export %inline
 156 | byte_u : Bits8
 157 | byte_u = 117
 158 | 
 159 | ||| ASCII code of 'v'
 160 | public export %inline
 161 | byte_v : Bits8
 162 | byte_v = 118
 163 | 
 164 | ||| ASCII code of 'w'
 165 | public export %inline
 166 | byte_w : Bits8
 167 | byte_w = 119
 168 | 
 169 | ||| ASCII code of 'x'
 170 | public export %inline
 171 | byte_x : Bits8
 172 | byte_x = 120
 173 | 
 174 | ||| ASCII code of 'y'
 175 | public export %inline
 176 | byte_y : Bits8
 177 | byte_y = 121
 178 | 
 179 | ||| ASCII code of 'z'
 180 | public export %inline
 181 | byte_z : Bits8
 182 | byte_z = 122
 183 | 
 184 | ||| ASCII code of 'A'
 185 | public export %inline
 186 | byte_A : Bits8
 187 | byte_A = 65
 188 | 
 189 | ||| ASCII code of 'B'
 190 | public export %inline
 191 | byte_B : Bits8
 192 | byte_B = 66
 193 | 
 194 | ||| ASCII code of 'C'
 195 | public export %inline
 196 | byte_C : Bits8
 197 | byte_C = 67
 198 | 
 199 | ||| ASCII code of 'D'
 200 | public export %inline
 201 | byte_D : Bits8
 202 | byte_D = 68
 203 | 
 204 | ||| ASCII code of 'E'
 205 | public export %inline
 206 | byte_E : Bits8
 207 | byte_E = 69
 208 | 
 209 | ||| ASCII code of 'F'
 210 | public export %inline
 211 | byte_F : Bits8
 212 | byte_F = 70
 213 | 
 214 | ||| ASCII code of 'G'
 215 | public export %inline
 216 | byte_G : Bits8
 217 | byte_G = 71
 218 | 
 219 | ||| ASCII code of 'H'
 220 | public export %inline
 221 | byte_H : Bits8
 222 | byte_H = 72
 223 | 
 224 | ||| ASCII code of 'I'
 225 | public export %inline
 226 | byte_I : Bits8
 227 | byte_I = 73
 228 | 
 229 | ||| ASCII code of 'J'
 230 | public export %inline
 231 | byte_J : Bits8
 232 | byte_J = 74
 233 | 
 234 | ||| ASCII code of 'K'
 235 | public export %inline
 236 | byte_K : Bits8
 237 | byte_K = 75
 238 | 
 239 | ||| ASCII code of 'L'
 240 | public export %inline
 241 | byte_L : Bits8
 242 | byte_L = 76
 243 | 
 244 | ||| ASCII code of 'M'
 245 | public export %inline
 246 | byte_M : Bits8
 247 | byte_M = 77
 248 | 
 249 | ||| ASCII code of 'N'
 250 | public export %inline
 251 | byte_N : Bits8
 252 | byte_N = 78
 253 | 
 254 | ||| ASCII code of 'O'
 255 | public export %inline
 256 | byte_O : Bits8
 257 | byte_O = 79
 258 | 
 259 | ||| ASCII code of 'P'
 260 | public export %inline
 261 | byte_P : Bits8
 262 | byte_P = 80
 263 | 
 264 | ||| ASCII code of 'Q'
 265 | public export %inline
 266 | byte_Q : Bits8
 267 | byte_Q = 81
 268 | 
 269 | ||| ASCII code of 'R'
 270 | public export %inline
 271 | byte_R : Bits8
 272 | byte_R = 82
 273 | 
 274 | ||| ASCII code of 'S'
 275 | public export %inline
 276 | byte_S : Bits8
 277 | byte_S = 83
 278 | 
 279 | ||| ASCII code of 'T'
 280 | public export %inline
 281 | byte_T : Bits8
 282 | byte_T = 84
 283 | 
 284 | ||| ASCII code of 'U'
 285 | public export %inline
 286 | byte_U : Bits8
 287 | byte_U = 85
 288 | 
 289 | ||| ASCII code of 'V'
 290 | public export %inline
 291 | byte_V : Bits8
 292 | byte_V = 86
 293 | 
 294 | ||| ASCII code of 'W'
 295 | public export %inline
 296 | byte_W : Bits8
 297 | byte_W = 87
 298 | 
 299 | ||| ASCII code of 'X'
 300 | public export %inline
 301 | byte_X : Bits8
 302 | byte_X = 88
 303 | 
 304 | ||| ASCII code of 'Y'
 305 | public export %inline
 306 | byte_Y : Bits8
 307 | byte_Y = 89
 308 | 
 309 | ||| ASCII code of 'Z'
 310 | public export %inline
 311 | byte_Z : Bits8
 312 | byte_Z = 90
 313 | 
 314 | public export
 315 | inRange : (lo,hi,scr : Bits8) -> (0 _ : (lo <= hi) === True) => Bool
 316 | inRange lo hi scr = case prim__gte_Bits8 scr lo of
 317 |   0 => False
 318 |   _ => case prim__lte_Bits8 scr hi of
 319 |     0 => False
 320 |     _ => True
 321 | 
 322 | public export %inline
 323 | isDigit : Bits8 -> Bool
 324 | isDigit x = inRange byte_0 byte_9 x
 325 | 
 326 | public export %inline
 327 | isLower : Bits8 -> Bool
 328 | isLower x = inRange byte_a byte_z x
 329 | 
 330 | public export %inline
 331 | isUpper : Bits8 -> Bool
 332 | isUpper x = inRange byte_A byte_Z x
 333 | 
 334 | public export
 335 | isAlpha : Bits8 -> Bool
 336 | isAlpha x = isLower x || isUpper x
 337 | 
 338 | public export
 339 | isAlphaNum : Bits8 -> Bool
 340 | isAlphaNum x = isDigit x || isAlpha x
 341 | 
 342 | ||| Returns true if the byte represents an ASCII whitespace character.
 343 | public export
 344 | isSpace : Bits8 -> Bool
 345 | isSpace 32 = True -- ' '
 346 | isSpace 10 = True -- '\n'
 347 | isSpace  9 = True -- '\t'
 348 | isSpace 11 = True -- '\v'
 349 | isSpace 12 = True -- '\f'
 350 | isSpace 13 = True -- '\r'
 351 | isSpace _  = False
 352 | 
 353 | ||| Returns true if the character represents a new line.
 354 | public export
 355 | isNL : Bits8 -> Bool
 356 | isNL 10 = True
 357 | isNL 13 = True
 358 | isNL _  = False
 359 | 
 360 | ||| Convert a letter to the corresponding upper-case letter, if any.
 361 | ||| Non-letters are ignored.
 362 | public export
 363 | toUpper : Bits8 -> Bits8
 364 | toUpper x = if (isLower x) then x - 32 else x
 365 | 
 366 | ||| Convert a letter to the corresponding lower-case letter, if any.
 367 | ||| Non-letters are ignored.
 368 | public export
 369 | toLower : Bits8 -> Bits8
 370 | toLower x = if (isUpper x) then x + 32 else x
 371 | 
 372 | ||| Returns true if the character is a hexadecimal digit i.e. in the range
 373 | ||| [0-9][a-f][A-F].
 374 | public export
 375 | isHexDigit : Bits8 -> Bool
 376 | isHexDigit x = isDigit x || inRange byte_a byte_f (toLower x)
 377 | 
 378 | ||| Returns true if the character is an octal digit.
 379 | public export
 380 | isOctDigit : Bits8 -> Bool
 381 | isOctDigit x = inRange byte_0 byte_7 x
 382 | 
 383 | ||| Returns true if the character is a control ASCII character.
 384 | public export
 385 | isControl : Bits8 -> Bool
 386 | isControl x = inRange 0 0x1f x
 387 | 
 388 | ||| Returns true if the character equal the '.' ASCII character
 389 | public export
 390 | isDot : Bits8 -> Bool
 391 | isDot 46 = True
 392 | isDot _  = False
 393 | 
 394 | ||| Returns true if the character equal the ',' ASCII character
 395 | public export
 396 | isComma : Bits8 -> Bool
 397 | isComma 44 = True
 398 | isComma _  = False
 399 | 
 400 | ||| Try to convert a bit digit ('0' or '1') to
 401 | ||| the natural number `0` or `1`.
 402 | public export
 403 | fromBitDigit : Bits8 -> Maybe Nat
 404 | fromBitDigit 48 = Just 0
 405 | fromBitDigit 49 = Just 1
 406 | fromBitDigit _  = Nothing
 407 | 
 408 | ||| Try to convert an ocatal digit to
 409 | ||| the corresponding natural number.
 410 | public export
 411 | fromOctDigit : Bits8 -> Maybe Nat
 412 | fromOctDigit 48 = Just 0
 413 | fromOctDigit 49 = Just 1
 414 | fromOctDigit 50 = Just 2
 415 | fromOctDigit 51 = Just 3
 416 | fromOctDigit 52 = Just 4
 417 | fromOctDigit 53 = Just 5
 418 | fromOctDigit 54 = Just 6
 419 | fromOctDigit 55 = Just 7
 420 | fromOctDigit _  = Nothing
 421 | 
 422 | ||| Try to convert a decimal digit to
 423 | ||| the corresponding natural number.
 424 | |||
 425 | ||| Implementation note: Profiling showed that a direct
 426 | ||| pattern match on the input is considerable faster
 427 | ||| than using subtraction together with `isDigit`.
 428 | public export
 429 | fromDigit : Bits8 -> Maybe Nat
 430 | fromDigit 48 = Just 0
 431 | fromDigit 49 = Just 1
 432 | fromDigit 50 = Just 2
 433 | fromDigit 51 = Just 3
 434 | fromDigit 52 = Just 4
 435 | fromDigit 53 = Just 5
 436 | fromDigit 54 = Just 6
 437 | fromDigit 55 = Just 7
 438 | fromDigit 56 = Just 8
 439 | fromDigit 57 = Just 9
 440 | fromDigit _  = Nothing
 441 | 
 442 | ||| Try to convert a hexadecimal digit to
 443 | ||| the corresponding natural number.
 444 | public export
 445 | fromHexDigit : Bits8 -> Maybe Nat
 446 | fromHexDigit 48  = Just 0
 447 | fromHexDigit 49  = Just 1
 448 | fromHexDigit 50  = Just 2
 449 | fromHexDigit 51  = Just 3
 450 | fromHexDigit 52  = Just 4
 451 | fromHexDigit 53  = Just 5
 452 | fromHexDigit 54  = Just 6
 453 | fromHexDigit 55  = Just 7
 454 | fromHexDigit 56  = Just 8
 455 | fromHexDigit 57  = Just 9
 456 | fromHexDigit 97  = Just 10
 457 | fromHexDigit 98  = Just 11
 458 | fromHexDigit 99  = Just 12
 459 | fromHexDigit 100 = Just 13
 460 | fromHexDigit 101 = Just 14
 461 | fromHexDigit 102 = Just 15
 462 | fromHexDigit 65  = Just 10
 463 | fromHexDigit 66  = Just 11
 464 | fromHexDigit 67  = Just 12
 465 | fromHexDigit 68  = Just 13
 466 | fromHexDigit 69  = Just 14
 467 | fromHexDigit 70  = Just 15
 468 | fromHexDigit _   = Nothing
 469 |