
  0 | module Protocol.Hex
  1 | 
  2 | import Data.Bits
  3 | import Data.List
  4 | 
  5 | %default total
  6 | 
  7 | hexDigit : Bits64 -> Char
  8 | hexDigit 0 = '0'
  9 | hexDigit 1 = '1'
 10 | hexDigit 2 = '2'
 11 | hexDigit 3 = '3'
 12 | hexDigit 4 = '4'
 13 | hexDigit 5 = '5'
 14 | hexDigit 6 = '6'
 15 | hexDigit 7 = '7'
 16 | hexDigit 8 = '8'
 17 | hexDigit 9 = '9'
 18 | hexDigit 10 = 'a'
 19 | hexDigit 11 = 'b'
 20 | hexDigit 12 = 'c'
 21 | hexDigit 13 = 'd'
 22 | hexDigit 14 = 'e'
 23 | hexDigit 15 = 'f'
 24 | hexDigit _ = 'X' -- TMP HACK: Ideally we'd have a bounds proof, generated below
 25 | 
 26 | ||| Convert a Bits64 value into a list of (lower case) hexadecimal characters
 27 | export
 28 | asHex : Bits64 -> String
 29 | asHex 0 = "0"
 30 | asHex n = pack $ asHex' n []
 31 |   where
 32 |     asHex' : Bits64 -> List Char -> List Char
 33 |     asHex' 0 hex = hex
 34 |     asHex' n hex = asHex' (assert_smaller n (n `shiftR` 4)) (hexDigit (n .&. 0xf) :: hex)
 35 | 
 36 | export
 37 | leftPad : Char -> Nat -> String -> String
 38 | leftPad paddingChar padToLength str =
 39 |   if length str < padToLength
 40 |     then pack (List.replicate (minus padToLength (length str)) paddingChar) ++ str
 41 |     else str
 42 | 
 43 | export
 44 | fromHexDigit : Char -> Maybe Int
 45 | fromHexDigit '0' = Just 0
 46 | fromHexDigit '1' = Just 1
 47 | fromHexDigit '2' = Just 2
 48 | fromHexDigit '3' = Just 3
 49 | fromHexDigit '4' = Just 4
 50 | fromHexDigit '5' = Just 5
 51 | fromHexDigit '6' = Just 6
 52 | fromHexDigit '7' = Just 7
 53 | fromHexDigit '8' = Just 8
 54 | fromHexDigit '9' = Just 9
 55 | fromHexDigit 'a' = Just 10
 56 | fromHexDigit 'b' = Just 11
 57 | fromHexDigit 'c' = Just 12
 58 | fromHexDigit 'd' = Just 13
 59 | fromHexDigit 'e' = Just 14
 60 | fromHexDigit 'f' = Just 15
 61 | fromHexDigit _ = Nothing
 62 | 
 63 | export
 64 | fromHexChars : List Char -> Maybe Integer
 65 | fromHexChars = fromHexChars' 1
 66 |   where
 67 |     fromHexChars' : Integer -> List Char -> Maybe Integer
 68 |     fromHexChars' _ [] = Just 0
 69 |     fromHexChars' m (d :: ds)
 70 |       = do digit <- fromHexDigit (toLower d)
 71 |            digits <- fromHexChars' (m*16) ds
 72 |            pure $ cast digit * m + digits
 73 | 
 74 | export
 75 | fromHex : String -> Maybe Integer
 76 | fromHex = fromHexChars . unpack
 77 |