Add octal literals

idris2.ipkg

@@ -128,6 +128,7 @@ modules =
 
     Utils.Binary,
     Utils.Hex,
+    Utils.Octal,
     Utils.Shunting,
     Utils.String,
 

idris2api.ipkg

@@ -121,6 +121,7 @@ modules =
 
     Utils.Binary,
     Utils.Hex,
+    Utils.Octal,
     Utils.Shunting,
     Utils.String,
 

src/Parser/Lexer.idr

@@ -2,6 +2,7 @@ module Parser.Lexer
 
 import public Text.Lexer
 import Utils.Hex
+import Utils.Octal
 import Utils.String
 
 %default total
@@ -233,6 +234,15 @@ fromHexLit str
                   Nothing => 0 -- can't happen if the literal lexed correctly
                   Just n => cast n
 
+fromOctLit : String -> Integer
+fromOctLit str
+  = if length str <= 2
+       then 0
+       else let num = assert_total (strTail (strTail str)) in
+             case fromOct (reverse num) of
+                  Nothing => 0 -- can't happen if the literal lexed correctly
+                  Just n => cast n
+
 rawTokens : TokenMap Token
 rawTokens =
     [(comment, Comment),
@@ -243,6 +253,7 @@ rawTokens =
     map (\x => (exact x, Symbol)) symbols ++
     [(doubleLit, \x => DoubleLit (cast x)),
      (hexLit, \x => Literal (fromHexLit x)),
+     (octLit, \x => Literal (fromOctLit x)),
      (digits, \x => Literal (cast x)),
      (stringLit, \x => StrLit (stripQuotes x)),
      (charLit, \x => CharLit (stripQuotes x)),

src/Text/Lexer.idr

@@ -163,12 +163,12 @@ hexDigits = some hexDigit
 ||| Recognise a single octal digit
 ||| /[0-8]/
 octDigit : Lexer
-octDigit = pred isHexDigit
+octDigit = pred isOctDigit
 
 ||| Recognise one or more octal digits
 ||| /[0-8]+/
 octDigits : Lexer
-octDigits = some hexDigit
+octDigits = some octDigit
 
 ||| Recognise a single alpha character
 ||| /[A-Za-z]/
@@ -305,6 +305,11 @@ intLit = opt (is '-') <+> digits
 hexLit : Lexer
 hexLit = approx "0x" <+> hexDigits
 
+||| Recognise an octal literal, prefixed by "0o"
+||| /0[Xx][0-9A-Fa-f]+/
+octLit : Lexer
+octLit = exact "0o" <+> octDigits
+
 ||| Recognise `start`, then recognise all input until a newline is encountered,
 ||| and consume the newline. Will succeed if end-of-input is encountered before
 ||| a newline.

src/Utils/Hex.idr

@@ -2,7 +2,6 @@ module Utils.Hex
 
 import Data.Primitives.Views
 
-export
 hexDigit : Int -> Char
 hexDigit 0 = '0'
 hexDigit 1 = '1'
@@ -61,4 +60,4 @@ fromHexChars = fromHexChars' 1
 
 export
 fromHex : String -> Maybe Int
-fromHex = fromHexChars . unpack
+fromHex = fromHexChars . unpack

src/Utils/Octal.idr

@@ -0,0 +1,48 @@
+module Utils.Octal
+
+import Data.Primitives.Views
+
+octDigit : Int -> Char
+octDigit 0 = '0'
+octDigit 1 = '1'
+octDigit 2 = '2'
+octDigit 3 = '3'
+octDigit 4 = '4'
+octDigit 5 = '5'
+octDigit 6 = '6'
+octDigit 7 = '7'
+
+||| Convert a positive integer into a list of octal characters
+export
+asOct : Int -> String
+asOct n = pack $ asOct' n []
+  where
+    asOct' : Int -> List Char -> List Char
+    asOct' 0 oct = oct
+    asOct' n oct with (n `divides` 8)
+      asOct' (8 * div + rem) oct | DivBy {div} {rem} _ = asOct' div (octDigit rem :: oct)
+
+export
+fromOctDigit : Char -> Maybe Int
+fromOctDigit '0' = Just 0
+fromOctDigit '1' = Just 1
+fromOctDigit '2' = Just 2
+fromOctDigit '3' = Just 3
+fromOctDigit '4' = Just 4
+fromOctDigit '5' = Just 5
+fromOctDigit '6' = Just 6
+fromOctDigit '7' = Just 7
+fromOctDigit _ = Nothing
+
+export
+fromOctChars : List Char -> Maybe Int
+fromOctChars = fromOctChars' 1
+  where
+    fromOctChars' : Int -> List Char -> Maybe Int
+    fromOctChars' _ [] = Just 0
+    fromOctChars' m (d :: ds) = pure $ !(fromOctDigit (toLower d)) * m + !(fromOctChars' (m*8) ds)
+
+export
+fromOct : String -> Maybe Int
+fromOct = fromOctChars . unpack
+