
  0 | module Libraries.Utils.Octal
  1 | 
  2 | import Data.Primitives.Views
  3 | 
  4 | %default total
  5 | 
  6 | octDigit : Int -> Char
  7 | octDigit 0 = '0'
  8 | octDigit 1 = '1'
  9 | octDigit 2 = '2'
 10 | octDigit 3 = '3'
 11 | octDigit 4 = '4'
 12 | octDigit 5 = '5'
 13 | octDigit 6 = '6'
 14 | octDigit 7 = '7'
 15 | octDigit _ = 'X' -- TMP HACK: Ideally we'd have a bounds proof, generated below
 16 | 
 17 | ||| Convert a positive integer into a list of octal characters
 18 | export
 19 | asOct : Int -> String
 20 | asOct n = pack $ asOct' n []
 21 |   where
 22 |     asOct' : Int -> List Char -> List Char
 23 |     asOct' 0 oct = oct
 24 |     asOct' n oct with (n `divides` 8)
 25 |       asOct' (8 * div + rem) oct | DivBy div rem _ =
 26 |         assert_total $ asOct' div (octDigit rem :: oct)
 27 | 
 28 | export
 29 | fromOctDigit : Char -> Maybe Int
 30 | fromOctDigit '0' = Just 0
 31 | fromOctDigit '1' = Just 1
 32 | fromOctDigit '2' = Just 2
 33 | fromOctDigit '3' = Just 3
 34 | fromOctDigit '4' = Just 4
 35 | fromOctDigit '5' = Just 5
 36 | fromOctDigit '6' = Just 6
 37 | fromOctDigit '7' = Just 7
 38 | fromOctDigit _ = Nothing
 39 | 
 40 | export
 41 | fromOctChars : List Char -> Maybe Integer
 42 | fromOctChars = fromOctChars' 1
 43 |   where
 44 |     fromOctChars' : Integer -> List Char -> Maybe Integer
 45 |     fromOctChars' _ [] = Just 0
 46 |     fromOctChars' m (d :: ds)
 47 |       = do digit <- fromOctDigit (toLower d)
 48 |            digits <- fromOctChars' (m*8) ds
 49 |            pure $ cast digit * m + digits
 50 | 
 51 | export
 52 | fromOct : String -> Maybe Integer
 53 | fromOct = fromOctChars . unpack
 54 |